theory ArchIpc_AI

lemma transfer_caps_loop_valid_vspace_objs[wp, Ipc_AI_assms]:
  "\<lbrace>valid_vspace_objs\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>" apply (induct caps arbitrary: slots n mi, simp) apply (clarsimp simp: Let_def split_def whenE_def
                  cong: if_cong list.case_cong
             split del: if_split) apply (rule hoare_pre) apply (wp hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift
              derive_cap_is_derived_foo
             hoare_drop_imps
        | assumption | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>valid_vspace_objs\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>) \<Longrightarrow> \<lbrace>valid_vspace_objs\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a aa b caps slots n mi. (\<And>slots n mi. \<lbrace>valid_vspace_objs\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>) \<Longrightarrow> \<lbrace>valid_vspace_objs\<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 (Some (obj_ref_of a)) 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 <- if cap' = NullCap then throwError undefined else returnOk ();
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>rv. valid_vspace_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a aa b caps slots n mi. (\<And>slots n mi. \<lbrace>valid_vspace_objs\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>) \<Longrightarrow> \<lbrace>?Q9 a aa b caps slots n 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 (Some (obj_ref_of a)) 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 <- if cap' = NullCap then throwError undefined else returnOk ();
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>rv. valid_vspace_objs\<rbrace>
 2. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>valid_vspace_objs\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>; valid_vspace_objs s\<rbrakk> \<Longrightarrow> ?Q9 a aa b caps slots n mi s proof (prove)
goal:
No subgoals!