theory CSpace_R

lemma lookup_cap_corres:
  "\<lbrakk> epcptr = to_bl epcptr' \<rbrakk> \<Longrightarrow>
   corres (lfr \<oplus> cap_relation)
     (valid_objs and pspace_aligned and tcb_at thread)
     (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread)
     (lookup_cap thread epcptr)
     (lookupCap thread epcptr')" apply (simp add: lookup_cap_def lookupCap_def lookupCapAndSlot_def) apply (rule corres_guard_imp) apply (rule corres_splitEE[OF lookupSlotForThread_corres]) apply (simp add: split_def) apply (subst bindE_returnOk[symmetric]) apply (rule corres_splitEE) apply simp apply (rule getSlotCap_corres, rule refl) apply (rule corres_returnOk [of _ \<top> \<top>]) apply simp apply wp+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. epcptr = to_bl epcptr' \<Longrightarrow> corres (lfr \<oplus> cap_relation) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) (lookup_cap thread epcptr) (lookupCap thread epcptr') proof (prove)
goal (1 subgoal):
 1. epcptr = to_bl epcptr' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>x. cap_relation x \<circ> fst)) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) (doE (ref', uu_) <- lookup_slot_for_thread thread (to_bl epcptr');
liftE (get_cap ref')
odE) (doE slot <- lookupSlotForThread thread epcptr';
cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE) proof (prove)
goal (3 subgoals):
 1. epcptr = to_bl epcptr' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>x. cap_relation x \<circ> fst)) ?Q1 ?Q'1 (doE (ref', uu_) <- lookup_slot_for_thread thread (to_bl epcptr');
liftE (get_cap ref')
odE) (doE slot <- lookupSlotForThread thread epcptr';
cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE)
 2. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> ?Q'1 s proof (prove)
goal (5 subgoals):
 1. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; (case rv of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref) slot\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>x. cap_relation x \<circ> fst)) (?R5 rv) (?R'5 slot) (case rv of (ref', uu_) \<Rightarrow> liftE (get_cap ref')) (doE cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE)
 2. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q5\<rbrace> lookup_slot_for_thread thread (to_bl epcptr') \<lbrace>?R5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> lookupSlotForThread thread epcptr' \<lbrace>?R'5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 5. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>x. cap_relation x \<circ> fst)) (?R5 rv) (?R'5 (cte_map (fst rv))) (liftE (get_cap (fst rv))) (doE cap <- liftE (getSlotCap (cte_map (fst rv)));
returnOk (cap, cte_map (fst rv))
odE)
 2. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q5\<rbrace> lookup_slot_for_thread thread (to_bl epcptr') \<lbrace>?R5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> lookupSlotForThread thread epcptr' \<lbrace>?R'5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 5. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>x. cap_relation x \<circ> fst)) (?R12 rv rv) (?R'13 rv (cte_map (fst rv))) (liftE (get_cap (fst rv)) >>=E returnOk) (doE cap <- liftE (getSlotCap (cte_map (fst rv)));
returnOk (cap, cte_map (fst rv))
odE)
 2. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q5\<rbrace> lookup_slot_for_thread thread (to_bl epcptr') \<lbrace>\<lambda>rv. ?R12 rv rv\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> lookupSlotForThread thread epcptr' \<lbrace>?R'5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 5. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and ?Q'5) s
flex-flex pairs:
\<lambda>rv. ?R'13 rv (cte_map (fst rv)) \<equiv>\<^sup>? \<lambda>rv. ?R'5 (cte_map (fst rv)) proof (prove)
goal (8 subgoals):
 1. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> ?r'15 rv slot) (?P30 rv rv) (?P'24 rv (cte_map (fst rv))) (liftE (get_cap (fst rv))) (liftE (getSlotCap (cte_map (fst rv))))
 2. \<And>rv slot rva cap. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv); ?r'15 rv slot rva cap\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. cap_relation a \<circ> fst)) (?R15 rv slot rva) (?R'15 rv slot cap) (returnOk rva) (returnOk (cap, cte_map (fst rv)))
 3. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 rv rv\<rbrace> liftE (get_cap (fst rv)) \<lbrace>?R15 rv slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 rv (cte_map (fst rv))\<rbrace> liftE (getSlotCap (cte_map (fst rv))) \<lbrace>?R'15 rv slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q5\<rbrace> lookup_slot_for_thread thread (to_bl epcptr') \<lbrace>\<lambda>rv. ?P30 rv rv and ?Q28 rv rv\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> lookupSlotForThread thread epcptr' \<lbrace>\<lambda>a. ?P'27 a and ?Q'26 a\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 8. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and ?Q'5) s
flex-flex pairs:
\<lambda>rv. ?P'27 (cte_map (fst rv)) \<equiv>\<^sup>? \<lambda>rv. ?P'24 rv (cte_map (fst rv))
\<lambda>rv. ?Q'26 (cte_map (fst rv)) \<equiv>\<^sup>? \<lambda>rv. ?Q'22 rv (cte_map (fst rv)) proof (prove)
goal (8 subgoals):
 1. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> corres (?r'15 rv (cte_map (fst rv))) (?P30 rv rv) (?P'24 rv (cte_map (fst rv))) (get_cap (fst rv)) (getSlotCap (cte_map (fst rv)))
 2. \<And>rv slot rva cap. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv); ?r'15 rv slot rva cap\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. cap_relation a \<circ> fst)) (?R15 rv slot rva) (?R'15 rv slot cap) (returnOk rva) (returnOk (cap, cte_map (fst rv)))
 3. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 rv rv\<rbrace> liftE (get_cap (fst rv)) \<lbrace>?R15 rv slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 rv (cte_map (fst rv))\<rbrace> liftE (getSlotCap (cte_map (fst rv))) \<lbrace>?R'15 rv slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q5\<rbrace> lookup_slot_for_thread thread (to_bl epcptr') \<lbrace>\<lambda>rv. ?P30 rv rv and ?Q28 rv rv\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> lookupSlotForThread thread epcptr' \<lbrace>\<lambda>a. ?P'27 a and ?Q'26 a\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 8. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and ?Q'5) s
flex-flex pairs:
\<lambda>rv. ?P'27 (cte_map (fst rv)) \<equiv>\<^sup>? \<lambda>rv. ?P'24 rv (cte_map (fst rv))
\<lambda>rv. ?Q'26 (cte_map (fst rv)) \<equiv>\<^sup>? \<lambda>rv. ?Q'22 rv (cte_map (fst rv)) proof (prove)
goal (7 subgoals):
 1. \<And>rv slot rva cap. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv); cap_relation rva cap\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. cap_relation a \<circ> fst)) (?R15 rv slot rva) (?R'15 rv slot cap) (returnOk rva) (returnOk (cap, cte_map (fst rv)))
 2. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 rv rv\<rbrace> liftE (get_cap (fst rv)) \<lbrace>?R15 rv slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 rv (cte_map (fst rv))\<rbrace> liftE (getSlotCap (cte_map (fst rv))) \<lbrace>?R'15 rv slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q5\<rbrace> lookup_slot_for_thread thread (to_bl epcptr') \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) (fst rv) and ?Q28 rv rv\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> lookupSlotForThread thread epcptr' \<lbrace>\<lambda>a. pspace_distinct' and pspace_aligned' and ?Q'26 a\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 7. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and ?Q'5) s
flex-flex pairs:
\<lambda>rv. ?Q'26 (cte_map (fst rv)) \<equiv>\<^sup>? \<lambda>rv. ?Q'22 rv (cte_map (fst rv)) proof (prove)
goal (7 subgoals):
 1. \<And>rv slot rva cap s s'. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv); cap_relation rva cap; (s, s') \<in> state_relation; True; True\<rbrakk> \<Longrightarrow> (cap_relation rva \<circ> fst) (cap, cte_map (fst rv))
 2. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 rv rv\<rbrace> liftE (get_cap (fst rv)) \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 rv (cte_map (fst rv))\<rbrace> liftE (getSlotCap (cte_map (fst rv))) \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q5\<rbrace> lookup_slot_for_thread thread (to_bl epcptr') \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) (fst rv) and ?Q28 rv rv\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> lookupSlotForThread thread epcptr' \<lbrace>\<lambda>a. pspace_distinct' and pspace_aligned' and ?Q'26 a\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 7. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and ?Q'5) s
flex-flex pairs:
\<lambda>rv. ?Q'26 (cte_map (fst rv)) \<equiv>\<^sup>? \<lambda>rv. ?Q'22 rv (cte_map (fst rv)) proof (prove)
goal (6 subgoals):
 1. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 rv rv\<rbrace> liftE (get_cap (fst rv)) \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv slot. \<lbrakk>epcptr = to_bl epcptr'; slot = cte_map (fst rv)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 rv (cte_map (fst rv))\<rbrace> liftE (getSlotCap (cte_map (fst rv))) \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q5\<rbrace> lookup_slot_for_thread thread (to_bl epcptr') \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) (fst rv) and ?Q28 rv rv\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. epcptr = to_bl epcptr' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> lookupSlotForThread thread epcptr' \<lbrace>\<lambda>a. pspace_distinct' and pspace_aligned' and ?Q'26 a\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 6. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and ?Q'5) s
flex-flex pairs:
\<lambda>rv. ?Q'26 (cte_map (fst rv)) \<equiv>\<^sup>? \<lambda>rv. ?Q'22 rv (cte_map (fst rv)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and (\<lambda>s. True \<and> valid_objs s \<and> True \<and> True)) s
 2. \<And>s. \<lbrakk>epcptr = to_bl epcptr'; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (\<lambda>s. True \<and> (pspace_distinct' and pspace_aligned' and (\<lambda>a. True \<and> True)) s)) s proof (prove)
goal:
No subgoals!