theory VSpace_C

lemma checkMappingPPtr_pte_ccorres:
  assumes pre:
    "\<And>pte \<sigma>. \<Gamma> \<turnstile> {s. True \<and> (\<exists>pte'. cslift s (pte_Ptr pte_ptr) = Some pte' \<and> cpte_relation pte pte')
                            \<and> (\<sigma>, s) \<in> rf_sr}
           call1 ;; Cond S return_void_C Skip;; call2;; Cond T return_void_C Skip
       {s. (\<sigma>, s) \<in> rf_sr \<and> (isSmallPagePTE pte \<and> pgsz = ARMSmallPage
                                \<or> isLargePagePTE pte \<and> pgsz = ARMLargePage)
                 \<and> pteFrame pte = addrFromPPtr pptr},
       {s. (\<sigma>, s) \<in> rf_sr \<and> \<not> ((isSmallPagePTE pte \<and> pgsz = ARMSmallPage
                                \<or> isLargePagePTE pte \<and> pgsz = ARMLargePage)
                 \<and> pteFrame pte = addrFromPPtr pptr)}"
  shows
  "ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc
       \<top> UNIV [SKIP]
     (checkMappingPPtr pptr pgsz (Inl pte_ptr))
     (call1;; Cond S return_void_C Skip;; call2;; Cond T 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 pte1=rv in pre) apply clarsimp apply (erule CollectE, assumption) apply (fold_subgoals (prefix))[2] subgoal by (auto simp: in_monad Bex_def isSmallPagePTE_def isLargePagePTE_def
                         split: pte.split vmpage_size.split) apply (wp empty_fail_getObject | simp)+ apply (erule cmap_relationE1[OF rf_sr_cpte_relation]) apply (erule ko_at_projectKO_opt) apply simp apply (wp empty_fail_getObject | simp add: objBits_simps archObjSize_def pteBits_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 (Inl pte_ptr)) (call1;;
Cond S return_void_C SKIP;;
call2;;
Cond T 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 pte_ptr >>= ARM_H.case_pte (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc. case pgsz of local.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 pgsz of local.ARMSmallPage \<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) proof (prove)
goal (5 subgoals):
 1. \<And>rv. ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc (ko_at' rv pte_ptr) UNIV [SKIP] (case rv of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<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)
 2. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 4. \<And>v. 1 < 2 ^ objBits v
 5. empty_fail (getObject pte_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.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<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)
 2. \<And>rv s s'. \<lbrakk>ko_at' rv pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> ?Q21 rv s
 3. \<And>rv s s'. \<lbrakk>ko_at' rv pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> ?Q'21 rv
 4. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 6. \<And>v. 1 < 2 ^ objBits v
 7. empty_fail (getObject pte_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 {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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 pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 3. \<And>rv s s'. \<lbrakk>ko_at' rv pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> ?Q'21 rv
 4. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 6. \<And>v. 1 < 2 ^ objBits v
 7. empty_fail (getObject pte_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 {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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 pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 3. \<And>rv s s'. \<lbrakk>ko_at' rv pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> ?Q'21 rv
 4. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 6. \<And>v. 1 < 2 ^ objBits v
 7. empty_fail (getObject pte_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>pte'. cslift s (pte_Ptr pte_ptr) = Some pte' \<and> cpte_relation rv pte') \<and> (\<sigma>, s) \<in> rf_sr}
 2. \<And>rv \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> (isSmallPagePTE rv \<and> pgsz = Wellformed_C.ARMSmallPage \<or> isLargePagePTE rv \<and> pgsz = Wellformed_C.ARMLargePage) \<and> pteFrame rv = addrFromPPtr pptr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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> ((isSmallPagePTE rv \<and> pgsz = Wellformed_C.ARMSmallPage \<or> isLargePagePTE rv \<and> pgsz = Wellformed_C.ARMLargePage) \<and> pteFrame rv = addrFromPPtr pptr)} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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 pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 5. \<And>rv s s'. \<lbrakk>ko_at' rv pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> ?Q'21 rv
 6. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 8. \<And>v. 1 < 2 ^ objBits v
 9. empty_fail (getObject pte_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>pte'. cslift x (pte_Ptr pte_ptr) = Some pte' \<and> cpte_relation rv pte'
 2. \<And>rv \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> (isSmallPagePTE rv \<and> pgsz = Wellformed_C.ARMSmallPage \<or> isLargePagePTE rv \<and> pgsz = Wellformed_C.ARMLargePage) \<and> pteFrame rv = addrFromPPtr pptr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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> ((isSmallPagePTE rv \<and> pgsz = Wellformed_C.ARMSmallPage \<or> isLargePagePTE rv \<and> pgsz = Wellformed_C.ARMLargePage) \<and> pteFrame rv = addrFromPPtr pptr)} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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 pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 5. \<And>rv s s'. \<lbrakk>ko_at' rv pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> ?Q'21 rv
 6. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 8. \<And>v. 1 < 2 ^ objBits v
 9. empty_fail (getObject pte_ptr) proof (prove)
goal (8 subgoals):
 1. \<And>rv \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> (isSmallPagePTE rv \<and> pgsz = Wellformed_C.ARMSmallPage \<or> isLargePagePTE rv \<and> pgsz = Wellformed_C.ARMLargePage) \<and> pteFrame rv = addrFromPPtr pptr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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> ((isSmallPagePTE rv \<and> pgsz = Wellformed_C.ARMSmallPage \<or> isLargePagePTE rv \<and> pgsz = Wellformed_C.ARMLargePage) \<and> pteFrame rv = addrFromPPtr pptr)} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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 pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 4. \<And>rv s s'. \<lbrakk>ko_at' rv pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> {x. \<exists>pte'. cslift x (pte_Ptr pte_ptr) = Some pte' \<and> cpte_relation rv pte'}
 5. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 7. \<And>v. 1 < 2 ^ objBits v
 8. empty_fail (getObject pte_ptr) proof (prove)
goal (7 subgoals):
 1. \<And>rv \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> (isSmallPagePTE rv \<and> pgsz = Wellformed_C.ARMSmallPage \<or> isLargePagePTE rv \<and> pgsz = Wellformed_C.ARMLargePage) \<and> pteFrame rv = addrFromPPtr pptr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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> ((isSmallPagePTE rv \<and> pgsz = Wellformed_C.ARMSmallPage \<or> isLargePagePTE rv \<and> pgsz = Wellformed_C.ARMLargePage) \<and> pteFrame rv = addrFromPPtr pptr)} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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 pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 3. \<And>rv s s'. \<lbrakk>ko_at' rv pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> {x. \<exists>pte'. cslift x (pte_Ptr pte_ptr) = Some pte' \<and> cpte_relation rv pte'}
 4. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 6. \<And>v. 1 < 2 ^ objBits v
 7. empty_fail (getObject pte_ptr) proof (prove)
goal (1 subgoal):
 1. {s. (\<sigma>_, s) \<in> rf_sr \<and> (isSmallPagePTE rv_ \<and> pgsz = Wellformed_C.ARMSmallPage \<or> isLargePagePTE rv_ \<and> pgsz = Wellformed_C.ARMLargePage) \<and> pteFrame rv_ = addrFromPPtr pptr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv_ of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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> ((isSmallPagePTE rv_ \<and> pgsz = Wellformed_C.ARMSmallPage \<or> isLargePagePTE rv_ \<and> pgsz = Wellformed_C.ARMLargePage) \<and> pteFrame rv_ = addrFromPPtr pptr)} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv_ of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case pgsz of local.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 pgsz of local.ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ 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 pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 2. \<And>rv s s'. \<lbrakk>ko_at' rv pte_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> {x. \<exists>pte'. cslift x (pte_Ptr pte_ptr) = Some pte' \<and> cpte_relation rv pte'}
 3. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 5. \<And>v. 1 < 2 ^ objBits v
 6. empty_fail (getObject pte_ptr) proof (prove)
goal (5 subgoals):
 1. \<And>rv s s'. \<lbrakk>ko_at' rv pte_ptr s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>pte'. cslift s' (pte_Ptr pte_ptr) = Some pte' \<and> cpte_relation rv pte'
 2. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 4. \<And>v. 1 < 2 ^ objBits v
 5. empty_fail (getObject pte_ptr) proof (prove)
goal (6 subgoals):
 1. \<And>rv s s'. ko_at' rv pte_ptr s \<Longrightarrow> map_to_ptes (ksPSpace s) (?x3 rv s s') = Some (?y3 rv s s')
 2. \<And>rv s s' y'. \<lbrakk>ko_at' rv pte_ptr s; map_to_ptes (ksPSpace s) (?x3 rv s s') = Some (?y3 rv s s'); cpte_relation (?y3 rv s s') y'; cslift s' (pte_Ptr (?x3 rv s s')) = Some y'\<rbrakk> \<Longrightarrow> \<exists>pte'. cslift s' (pte_Ptr pte_ptr) = Some pte' \<and> cpte_relation rv pte'
 3. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 5. \<And>v. 1 < 2 ^ objBits v
 6. empty_fail (getObject pte_ptr) proof (prove)
goal (5 subgoals):
 1. \<And>rv s s' y'. \<lbrakk>ko_at' rv pte_ptr s; map_to_ptes (ksPSpace s) pte_ptr = Some rv; cpte_relation rv y'; cslift s' (pte_Ptr pte_ptr) = Some y'\<rbrakk> \<Longrightarrow> \<exists>pte'. cslift s' (pte_Ptr pte_ptr) = Some pte' \<and> cpte_relation rv pte'
 2. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 4. \<And>v. 1 < 2 ^ objBits v
 5. empty_fail (getObject pte_ptr) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> getObject pte_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>q n ko. loadObject pte_ptr q n ko = loadObject_default pte_ptr q n ko
 3. \<And>v. 1 < 2 ^ objBits v
 4. empty_fail (getObject pte_ptr) proof (prove)
goal:
No subgoals!