theory Ipc_R

lemma lookupExtraCaps_srcs[wp]:
  "\<lbrace>\<top>\<rbrace> lookupExtraCaps thread buf info \<lbrace>transferCaps_srcs\<rbrace>,-" apply (simp add: lookupExtraCaps_def lookupCapAndSlot_def
                   split_def lookupSlotForThread_def
                   getSlotCap_def) apply (wp mapME_set[where R=\<top>] getCTE_wp') apply (rule_tac P=\<top> in hoare_trivE_R) apply (simp add: cte_wp_at_ctes_of) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> lookupExtraCaps thread buf info \<lbrace>\<lambda>caps s. \<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> liftE (getExtraCPtrs buf info) >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False (doE slot <- doE threadRootSlot <- liftE (getThreadCSpaceRoot thread);
threadRoot <- liftE (do cte <- getCTE threadRootSlot;
return (cteCap cte)
od);
p <- CSpace_H.resolveAddressBits threadRoot cptr (size cptr);
returnOk (fst p)
odE;
cap <- liftE (do cte <- getCTE slot;
return (cteCap cte)
od);
returnOk (cap, slot)
odE)) \<lbrace>\<lambda>caps s. \<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s\<rbrace>, - proof (prove)
goal (7 subgoals):
 1. \<And>cptrs x threadRootSlot threadRoot. \<lbrace>?P'23 cptrs x threadRootSlot threadRoot\<rbrace> CSpace_H.resolveAddressBits threadRoot x (size x) \<lbrace>\<lambda>p a. \<forall>cte. cte_wp_at' ((=) cte) (fst p) a \<longrightarrow> cte_wp_at' (\<lambda>ctea. fst (cteCap cte, fst p) \<noteq> capability.NullCap \<longrightarrow> cteCap ctea = fst (cteCap cte, fst p)) (snd (cteCap cte, fst p)) a\<rbrace>, -
 2. \<And>cptrs x threadRootSlot. \<lbrace>?P'18 cptrs x threadRootSlot\<rbrace> liftE (do cte <- getCTE threadRootSlot;
return (cteCap cte)
od) \<lbrace>\<lambda>threadRoot s. True \<and> ?P'23 cptrs x threadRootSlot threadRoot s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cptrs x. \<lbrace>\<lambda>_. True\<rbrace> liftE (getThreadCSpaceRoot thread) \<lbrace>\<lambda>threadRootSlot s. True \<and> True \<and> ?P'18 cptrs x threadRootSlot s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cptrs x y. \<lbrace>(\<lambda>_. True) and cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x)\<rbrace> capFaultOnFailure y False (doE slot <- doE threadRootSlot <- liftE (getThreadCSpaceRoot thread);
threadRoot <- liftE (do cte <- getCTE threadRootSlot;
return (cteCap cte)
od);
p <- CSpace_H.resolveAddressBits threadRoot y (size y);
returnOk (fst p)
odE;
cap <- liftE (do cte <- getCTE slot;
return (cteCap cte)
od);
returnOk (cap, slot)
odE) \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x)\<rbrace>, -
 5. \<And>cptrs x. \<lbrace>\<lambda>_. True\<rbrace> capFaultOnFailure x False (doE slot <- doE threadRootSlot <- liftE (getThreadCSpaceRoot thread);
threadRoot <- liftE (do cte <- getCTE threadRootSlot;
return (cteCap cte)
od);
p <- CSpace_H.resolveAddressBits threadRoot x (size x);
returnOk (fst p)
odE;
cap <- liftE (do cte <- getCTE slot;
return (cteCap cte)
od);
returnOk (cap, slot)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 6. \<lbrace>?P'1\<rbrace> liftE (getExtraCPtrs buf info) \<lbrace>\<lambda>cptrs _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. True \<Longrightarrow> ?P'1 s proof (prove)
goal (7 subgoals):
 1. \<And>cptrs x threadRootSlot threadRoot. \<lbrace>\<lambda>_. True\<rbrace> CSpace_H.resolveAddressBits threadRoot x (size x) \<lbrace>\<lambda>p a. \<forall>cte. cte_wp_at' ((=) cte) (fst p) a \<longrightarrow> cte_wp_at' (\<lambda>ctea. fst (cteCap cte, fst p) \<noteq> capability.NullCap \<longrightarrow> cteCap ctea = fst (cteCap cte, fst p)) (snd (cteCap cte, fst p)) a\<rbrace>, -
 2. \<And>cptrs x threadRootSlot. \<lbrace>?P'18 cptrs x threadRootSlot\<rbrace> liftE (do cte <- getCTE threadRootSlot;
return (cteCap cte)
od) \<lbrace>\<lambda>threadRoot s. True \<and> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cptrs x. \<lbrace>\<lambda>_. True\<rbrace> liftE (getThreadCSpaceRoot thread) \<lbrace>\<lambda>threadRootSlot s. True \<and> True \<and> ?P'18 cptrs x threadRootSlot s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cptrs x y. \<lbrace>(\<lambda>_. True) and cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x)\<rbrace> capFaultOnFailure y False (doE slot <- doE threadRootSlot <- liftE (getThreadCSpaceRoot thread);
threadRoot <- liftE (do cte <- getCTE threadRootSlot;
return (cteCap cte)
od);
p <- CSpace_H.resolveAddressBits threadRoot y (size y);
returnOk (fst p)
odE;
cap <- liftE (do cte <- getCTE slot;
return (cteCap cte)
od);
returnOk (cap, slot)
odE) \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x)\<rbrace>, -
 5. \<And>cptrs x. \<lbrace>\<lambda>_. True\<rbrace> capFaultOnFailure x False (doE slot <- doE threadRootSlot <- liftE (getThreadCSpaceRoot thread);
threadRoot <- liftE (do cte <- getCTE threadRootSlot;
return (cteCap cte)
od);
p <- CSpace_H.resolveAddressBits threadRoot x (size x);
returnOk (fst p)
odE;
cap <- liftE (do cte <- getCTE slot;
return (cteCap cte)
od);
returnOk (cap, slot)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 6. \<lbrace>?P'1\<rbrace> liftE (getExtraCPtrs buf info) \<lbrace>\<lambda>cptrs _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. True \<Longrightarrow> ?P'1 s proof (prove)
goal (6 subgoals):
 1. \<And>cptrs x threadRootSlot. \<lbrace>?P'18 cptrs x threadRootSlot\<rbrace> liftE (do cte <- getCTE threadRootSlot;
return (cteCap cte)
od) \<lbrace>\<lambda>threadRoot s. True \<and> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>cptrs x. \<lbrace>\<lambda>_. True\<rbrace> liftE (getThreadCSpaceRoot thread) \<lbrace>\<lambda>threadRootSlot s. True \<and> True \<and> ?P'18 cptrs x threadRootSlot s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cptrs x y. \<lbrace>(\<lambda>_. True) and cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x)\<rbrace> capFaultOnFailure y False (doE slot <- doE threadRootSlot <- liftE (getThreadCSpaceRoot thread);
threadRoot <- liftE (do cte <- getCTE threadRootSlot;
return (cteCap cte)
od);
p <- CSpace_H.resolveAddressBits threadRoot y (size y);
returnOk (fst p)
odE;
cap <- liftE (do cte <- getCTE slot;
return (cteCap cte)
od);
returnOk (cap, slot)
odE) \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x)\<rbrace>, -
 4. \<And>cptrs x. \<lbrace>\<lambda>_. True\<rbrace> capFaultOnFailure x False (doE slot <- doE threadRootSlot <- liftE (getThreadCSpaceRoot thread);
threadRoot <- liftE (do cte <- getCTE threadRootSlot;
return (cteCap cte)
od);
p <- CSpace_H.resolveAddressBits threadRoot x (size x);
returnOk (fst p)
odE;
cap <- liftE (do cte <- getCTE slot;
return (cteCap cte)
od);
returnOk (cap, slot)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 5. \<lbrace>?P'1\<rbrace> liftE (getExtraCPtrs buf info) \<lbrace>\<lambda>cptrs _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. True \<Longrightarrow> ?P'1 s proof (prove)
goal:
No subgoals!