theory Ipc_R

lemma transferCapsToSlots_pres1[crunch_rules]:
  assumes x: "\<And>cap src dest. \<lbrace>P\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. P\<rbrace>"
  assumes eb: "\<And>b n. \<lbrace>P\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. P\<rbrace>"
  shows      "\<lbrace>P\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>" apply (induct caps arbitrary: slots n mi) apply simp apply (simp add: Let_def split_def whenE_def
             cong: if_cong list.case_cong
             split del: if_split) apply (rule hoare_pre) apply (wp x eb | assumption | simp split del: if_split | wpc
             | wp (once) hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slots n mi. \<lbrace>P\<rbrace> transferCapsToSlots ep buffer n [] slots mi \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>P\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> transferCapsToSlots ep buffer n (a # caps) slots mi \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>P\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> transferCapsToSlots ep buffer n (a # caps) slots mi \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>P\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> constOnFailure (msgExtraCaps_update (\<lambda>_. word_of_nat n) mi) (if isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep then doE y <- liftE (setExtraBadge buffer (capEPBadge (fst a)) n);
liftE (transferCapsToSlots ep buffer (Suc n) caps slots (msgCapsUnwrapped_update (\<lambda>_. msgCapsUnwrapped mi || 2 ^ n) mi))
odE else case slots of [] \<Rightarrow> returnOk (msgExtraCaps_update (\<lambda>_. word_of_nat n) mi) | destSlot # slots' \<Rightarrow> doE cap' <- unifyFailure (global.deriveCap (snd a) (fst a));
y <- if cap' = capability.NullCap then throwError () else returnOk ();
y <- liftE (cteInsert cap' (snd a) destSlot);
liftE (transferCapsToSlots ep buffer (Suc n) caps slots' mi)
odE) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>P\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>?Q9 a caps slots n mi\<rbrace> constOnFailure (msgExtraCaps_update (\<lambda>_. word_of_nat n) mi) (if isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep then doE y <- liftE (setExtraBadge buffer (capEPBadge (fst a)) n);
liftE (transferCapsToSlots ep buffer (Suc n) caps slots (msgCapsUnwrapped_update (\<lambda>_. msgCapsUnwrapped mi || 2 ^ n) mi))
odE else case slots of [] \<Rightarrow> returnOk (msgExtraCaps_update (\<lambda>_. word_of_nat n) mi) | destSlot # slots' \<Rightarrow> doE cap' <- unifyFailure (global.deriveCap (snd a) (fst a));
y <- if cap' = capability.NullCap then throwError () else returnOk ();
y <- liftE (cteInsert cap' (snd a) destSlot);
liftE (transferCapsToSlots ep buffer (Suc n) caps slots' mi)
odE) \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>a caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>P\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s\<rbrakk> \<Longrightarrow> ?Q9 a caps slots n mi s proof (prove)
goal:
No subgoals!