theory Ipc_AI

lemma transfer_caps_loop_mi_label[wp]:
  "\<lbrace>\<lambda>s. P (mi_label mi)\<rbrace>
     transfer_caps_loop ep buffer n caps slots mi
   \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>" apply (induct caps arbitrary: n slots mi) apply simp apply wp apply simp apply (clarsimp split del: if_split) apply (rule hoare_pre) apply (wp const_on_failure_wp hoare_drop_imps | assumption)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>n slots mi. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n [] slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>
 2. \<And>a caps n slots mi. (\<And>n slots mi. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>n mi. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> return (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>
 2. \<And>a caps n slots mi. (\<And>n slots mi. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>n mi s. P (mi_label mi) \<Longrightarrow> P (mi_label (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 2. \<And>a caps n slots mi. (\<And>n slots mi. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a caps n slots mi. (\<And>n slots mi. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a aa b caps n slots mi. (\<And>n slots mi. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (if is_ep_cap a \<and> ep = Some (obj_ref_of a) then doE y <- liftE (set_extra_badge buffer (cap_ep_badge a) n);
liftE (transfer_caps_loop ep buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE else if slots \<noteq> [] then doE cap' <- derive_cap (aa, b) a;
y <- whenE (cap' = NullCap) (throwError undefined);
y <- liftE (cap_insert cap' (aa, b) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) caps (tl slots) mi)
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))) \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a aa b caps n slots mi. (\<And>n slots mi. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>) \<Longrightarrow> \<lbrace>?Q6 a aa b caps n slots mi\<rbrace> const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (if is_ep_cap a \<and> ep = Some (obj_ref_of a) then doE y <- liftE (set_extra_badge buffer (cap_ep_badge a) n);
liftE (transfer_caps_loop ep buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE else if slots \<noteq> [] then doE cap' <- derive_cap (aa, b) a;
y <- whenE (cap' = NullCap) (throwError undefined);
y <- liftE (cap_insert cap' (aa, b) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) caps (tl slots) mi)
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))) \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>
 2. \<And>a aa b caps n slots mi s. \<lbrakk>\<And>n slots mi. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>; P (mi_label mi)\<rbrakk> \<Longrightarrow> ?Q6 a aa b caps n slots mi s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b caps n slots mi s. \<lbrakk>\<And>n slots mi. \<lbrace>\<lambda>s. P (mi_label mi)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>; P (mi_label mi)\<rbrakk> \<Longrightarrow> P (mi_label (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))) \<and> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> True \<and> P (mi_label (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> True \<and> True \<and> True \<and> P (mi_label mi)) \<and> (\<not> slots \<noteq> [] \<longrightarrow> P (mi_label (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))))) proof (prove)
goal:
No subgoals!