theory ArchBCorres2_AI

lemma transfer_caps_loop_bcorres[wp]:
 "bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi)" apply (induct caps arbitrary: slots n mi ep) apply simp apply wp apply (case_tac a) apply simp apply (intro impI conjI) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi) proof (prove)
goal (2 subgoals):
 1. \<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n [] slots mi) (transfer_caps_loop ep buffer n [] slots mi)
 2. \<And>a caps slots n mi ep. (\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi)) \<Longrightarrow> bcorres (transfer_caps_loop ep buffer n (a # caps) slots mi) (transfer_caps_loop ep buffer n (a # caps) slots mi) proof (prove)
goal (2 subgoals):
 1. \<And>n mi. bcorres (return (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))) (return (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 2. \<And>a caps slots n mi ep. (\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi)) \<Longrightarrow> bcorres (transfer_caps_loop ep buffer n (a # caps) slots mi) (transfer_caps_loop ep buffer n (a # caps) slots mi) proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi ep. (\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi)) \<Longrightarrow> bcorres (transfer_caps_loop ep buffer n (a # caps) slots mi) (transfer_caps_loop ep buffer n (a # caps) slots mi) proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi ep aa b c. \<lbrakk>\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi); a = (aa, b, c)\<rbrakk> \<Longrightarrow> bcorres (transfer_caps_loop ep buffer n (a # caps) slots mi) (transfer_caps_loop ep buffer n (a # caps) slots mi) proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi ep aa b c. \<lbrakk>\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi); a = (aa, b, c)\<rbrakk> \<Longrightarrow> (is_ep_cap aa \<and> ep = Some (obj_ref_of aa) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE))) \<and> (slots = [] \<longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)))) \<and> ((is_ep_cap aa \<longrightarrow> ep \<noteq> Some (obj_ref_of aa)) \<longrightarrow> (is_ep_cap aa \<and> ep = Some (obj_ref_of aa) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE))) \<and> (slots = [] \<longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)))) \<and> (slots \<noteq> [] \<longrightarrow> (is_ep_cap aa \<and> ep = Some (obj_ref_of aa) \<longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE))) \<and> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE cap' <- derive_cap (b, c) aa;
y <- whenE (cap' = NullCap) (throwError undefined);
y <- liftE (cap_insert cap' (b, c) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) caps (tl slots) mi)
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE cap' <- derive_cap (b, c) aa;
y <- whenE (cap' = NullCap) (throwError undefined);
y <- liftE (cap_insert cap' (b, c) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) caps (tl slots) mi)
odE))) \<and> (slots = [] \<longrightarrow> (is_ep_cap aa \<and> ep = Some (obj_ref_of aa) \<longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE))) \<and> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))))) proof (prove)
goal (8 subgoals):
 1. \<And>a caps slots n mi ep aa b c. \<lbrakk>\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi); a = (aa, b, c); is_ep_cap aa \<and> ep = Some (obj_ref_of aa); slots \<noteq> []\<rbrakk> \<Longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE))
 2. \<And>a caps slots n mi ep aa b c. \<lbrakk>\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi); a = (aa, b, c); is_ep_cap aa \<and> ep = Some (obj_ref_of aa); slots = []\<rbrakk> \<Longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE))
 3. \<And>a caps slots n mi ep aa b c. \<lbrakk>\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi); a = (aa, b, c); is_ep_cap aa \<longrightarrow> ep \<noteq> Some (obj_ref_of aa); is_ep_cap aa \<and> ep = Some (obj_ref_of aa); slots \<noteq> []\<rbrakk> \<Longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE))
 4. \<And>a caps slots n mi ep aa b c. \<lbrakk>\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi); a = (aa, b, c); is_ep_cap aa \<longrightarrow> ep \<noteq> Some (obj_ref_of aa); is_ep_cap aa \<and> ep = Some (obj_ref_of aa); slots = []\<rbrakk> \<Longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE))
 5. \<And>a caps slots n mi ep aa b c. \<lbrakk>\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi); a = (aa, b, c); is_ep_cap aa \<longrightarrow> ep \<noteq> Some (obj_ref_of aa); slots \<noteq> []; is_ep_cap aa \<and> ep = Some (obj_ref_of aa)\<rbrakk> \<Longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE))
 6. \<And>a caps slots n mi ep aa b c. \<lbrakk>\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi); a = (aa, b, c); is_ep_cap aa \<longrightarrow> ep \<noteq> Some (obj_ref_of aa); slots \<noteq> []\<rbrakk> \<Longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE cap' <- derive_cap (b, c) aa;
y <- whenE (cap' = NullCap) (throwError undefined);
y <- liftE (cap_insert cap' (b, c) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) caps (tl slots) mi)
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE cap' <- derive_cap (b, c) aa;
y <- whenE (cap' = NullCap) (throwError undefined);
y <- liftE (cap_insert cap' (b, c) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) caps (tl slots) mi)
odE))
 7. \<And>a caps slots n mi ep aa b c. \<lbrakk>\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi); a = (aa, b, c); is_ep_cap aa \<longrightarrow> ep \<noteq> Some (obj_ref_of aa); slots = []; is_ep_cap aa \<and> ep = Some (obj_ref_of aa)\<rbrakk> \<Longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (doE y <- liftE (set_extra_badge buffer (cap_ep_badge aa) n);
liftE (transfer_caps_loop (Some (obj_ref_of aa)) buffer (Suc n) caps [] (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE))
 8. \<And>a caps slots n mi ep aa b c. \<lbrakk>\<And>slots n mi ep. bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi); a = (aa, b, c); is_ep_cap aa \<longrightarrow> ep \<noteq> Some (obj_ref_of aa); slots = []\<rbrakk> \<Longrightarrow> bcorres (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))) proof (prove)
goal:
No subgoals!