theory Ipc_IF

lemma transfer_caps_loop_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
   transfer_caps_loop ep rcv_buffer n caps slots mi
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" proof (induct caps arbitrary: slots n mi) case Nil thus ?case by (simp, wp, simp) next case (Cons c caps') show ?case apply (cases c) apply (simp split del: if_split cong: if_cong) apply (rule hoare_pre) apply (wp) apply (erule conjE, erule subst, rule Cons.hyps) apply (clarsimp) apply (wp set_extra_badge_globals_equiv)+ apply (rule Cons.hyps) apply (simp) apply (wp cap_insert_globals_equiv'') apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs"
                   and E="\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs"
                    in hoare_post_impErr) apply (simp add: whenE_def, rule conjI) apply (rule impI, wp)+ apply (simp)+ apply wp+ apply (fastforce) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n caps slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (state)
goal (2 subgoals):
 1. \<And>slots n mi. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n [] slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n caps slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<Longrightarrow> \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n (a # caps) slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (state)
this:


goal (2 subgoals):
 1. \<And>slots n mi. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n [] slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n caps slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<Longrightarrow> \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n (a # caps) slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n [] slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (state)
this:
\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n [] slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace>

goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n caps slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<Longrightarrow> \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n (a # caps) slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n caps slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<Longrightarrow> \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n (a # caps) slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (state)
this:
\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer ?n caps' ?slots ?mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace>

goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n caps slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<Longrightarrow> \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n (a # caps) slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n (c # caps') slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b ca. c = (a, b, ca) \<Longrightarrow> \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n (c # caps') slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b ca. c = (a, b, ca) \<Longrightarrow> \<lbrace>\<lambda>a. globals_equiv st a \<and> valid_arch_state a \<and> valid_global_objs a\<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 rcv_buffer (cap_ep_badge a) n);
liftE (transfer_caps_loop (Some (obj_ref_of a)) rcv_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 (b, ca) a;
y <- whenE (cap' = NullCap) (throwError undefined);
y <- liftE (cap_insert cap' (b, ca) (hd slots));
liftE (transfer_caps_loop ep rcv_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>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b ca. c = (a, b, ca) \<Longrightarrow> \<lbrace>?Q9 a b ca\<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 rcv_buffer (cap_ep_badge a) n);
liftE (transfer_caps_loop (Some (obj_ref_of a)) rcv_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 (b, ca) a;
y <- whenE (cap' = NullCap) (throwError undefined);
y <- liftE (cap_insert cap' (b, ca) (hd slots));
liftE (transfer_caps_loop ep rcv_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>_. globals_equiv st\<rbrace>
 2. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> ?Q9 a b ca s proof (prove)
goal (4 subgoals):
 1. \<And>a b ca y. \<lbrakk>c = (a, b, ca); is_ep_cap a \<and> ep = Some (obj_ref_of a)\<rbrakk> \<Longrightarrow> \<lbrace>?B15 a b ca y\<rbrace> transfer_caps_loop (Some (obj_ref_of a)) rcv_buffer (Suc n) caps' slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>a b ca. \<lbrakk>c = (a, b, ca); is_ep_cap a \<and> ep = Some (obj_ref_of a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 a b ca\<rbrace> liftE (set_extra_badge rcv_buffer (cap_ep_badge a) n) \<lbrace>?B15 a b ca\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 3. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a))\<rbrakk> \<Longrightarrow> \<lbrace>?R14 a b ca\<rbrace> if slots \<noteq> [] then doE cap' <- derive_cap (b, ca) a;
y <- whenE (cap' = NullCap) (throwError undefined);
y <- liftE (cap_insert cap' (b, ca) (hd slots));
liftE (transfer_caps_loop ep rcv_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>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 4. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> ?Q14 a b ca s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> ?R14 a b ca s) proof (prove)
goal (3 subgoals):
 1. \<And>a b ca. \<lbrakk>c = (a, b, ca); is_ep_cap a \<and> ep = Some (obj_ref_of a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 a b ca\<rbrace> liftE (set_extra_badge rcv_buffer (cap_ep_badge a) n) \<lbrace>\<lambda>y. globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 2. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a))\<rbrakk> \<Longrightarrow> \<lbrace>?R14 a b ca\<rbrace> if slots \<noteq> [] then doE cap' <- derive_cap (b, ca) a;
y <- whenE (cap' = NullCap) (throwError undefined);
y <- liftE (cap_insert cap' (b, ca) (hd slots));
liftE (transfer_caps_loop ep rcv_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>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 3. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> ?Q14 a b ca s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> ?R14 a b ca s) proof (prove)
goal (3 subgoals):
 1. \<And>a b ca. \<lbrakk>c = (a, b, ca); is_ep_cap a; ep = Some (obj_ref_of a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 a b ca\<rbrace> set_extra_badge rcv_buffer (cap_ep_badge a) n \<lbrace>\<lambda>y a. globals_equiv st a \<and> valid_arch_state a \<and> valid_global_objs a\<rbrace>
 2. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a))\<rbrakk> \<Longrightarrow> \<lbrace>?R14 a b ca\<rbrace> if slots \<noteq> [] then doE cap' <- derive_cap (b, ca) a;
y <- whenE (cap' = NullCap) (throwError undefined);
y <- liftE (cap_insert cap' (b, ca) (hd slots));
liftE (transfer_caps_loop ep rcv_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>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 3. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> ?Q14 a b ca s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> ?R14 a b ca s) proof (prove)
goal (6 subgoals):
 1. \<And>a b ca cap' y ya. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B38 a b ca cap' y ya\<rbrace> transfer_caps_loop ep rcv_buffer (Suc n) caps' (tl slots) mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>a b ca cap' y. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B37 a b ca cap' y\<rbrace> liftE (cap_insert cap' (b, ca) (hd slots)) \<lbrace>?B38 a b ca cap' y\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 3. \<And>a b ca cap'. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B36 a b ca cap'\<rbrace> whenE (cap' = NullCap) (throwError undefined) \<lbrace>?B37 a b ca cap'\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 4. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a b ca\<rbrace> derive_cap (b, ca) a \<lbrace>?B36 a b ca\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 5. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R35 a b ca\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 6. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q35 a b ca s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R35 a b ca s)) proof (prove)
goal (5 subgoals):
 1. \<And>a b ca cap' y. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B37 a b ca cap' y\<rbrace> liftE (cap_insert cap' (b, ca) (hd slots)) \<lbrace>\<lambda>ya. globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 2. \<And>a b ca cap'. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B36 a b ca cap'\<rbrace> whenE (cap' = NullCap) (throwError undefined) \<lbrace>?B37 a b ca cap'\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 3. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a b ca\<rbrace> derive_cap (b, ca) a \<lbrace>?B36 a b ca\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 4. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R35 a b ca\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 5. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q35 a b ca s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R35 a b ca s)) proof (prove)
goal (5 subgoals):
 1. \<And>a b ca cap'. \<lbrakk>c = (a, b, ca); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B37 a b ca cap' ()\<rbrace> cap_insert cap' (b, ca) (hd slots) \<lbrace>\<lambda>ya a. globals_equiv st a \<and> valid_arch_state a \<and> valid_global_objs a\<rbrace>
 2. \<And>a b ca cap'. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B36 a b ca cap'\<rbrace> whenE (cap' = NullCap) (throwError undefined) \<lbrace>?B37 a b ca cap'\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 3. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a b ca\<rbrace> derive_cap (b, ca) a \<lbrace>?B36 a b ca\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 4. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R35 a b ca\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 5. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q35 a b ca s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R35 a b ca s)) proof (prove)
goal (4 subgoals):
 1. \<And>a b ca cap'. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B36 a b ca cap'\<rbrace> whenE (cap' = NullCap) (throwError undefined) \<lbrace>\<lambda>a b. (globals_equiv st and valid_global_objs and valid_arch_state) b \<and> valid_arch_state b \<and> valid_global_objs b\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 2. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a b ca\<rbrace> derive_cap (b, ca) a \<lbrace>?B36 a b ca\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 3. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R35 a b ca\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 4. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q35 a b ca s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R35 a b ca s)) proof (prove)
goal (6 subgoals):
 1. \<And>a b ca cap'. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B36 a b ca cap'\<rbrace> whenE (cap' = NullCap) (throwError undefined) \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
 2. \<And>a b ca cap' rv s. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; (globals_equiv st and valid_arch_state and valid_global_objs) s\<rbrakk> \<Longrightarrow> (globals_equiv st and valid_global_objs and valid_arch_state) s \<and> valid_arch_state s \<and> valid_global_objs s
 3. \<And>a b ca cap' e s. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; (globals_equiv st and valid_arch_state and valid_global_objs) s\<rbrakk> \<Longrightarrow> globals_equiv st s
 4. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a b ca\<rbrace> derive_cap (b, ca) a \<lbrace>?B36 a b ca\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 5. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R35 a b ca\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 6. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q35 a b ca s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R35 a b ca s)) proof (prove)
goal (7 subgoals):
 1. \<And>a b ca cap'. \<lbrakk>c = (a, b, ca); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> cap' = NullCap \<longrightarrow> \<lbrace>?B36 a b ca NullCap\<rbrace> throwError undefined \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
 2. \<And>a b ca cap'. \<lbrakk>c = (a, b, ca); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> cap' \<noteq> NullCap \<longrightarrow> \<lbrace>?B36 a b ca cap'\<rbrace> returnOk () \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
 3. \<And>a b ca cap' rv s. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; (globals_equiv st and valid_arch_state and valid_global_objs) s\<rbrakk> \<Longrightarrow> (globals_equiv st and valid_global_objs and valid_arch_state) s \<and> valid_arch_state s \<and> valid_global_objs s
 4. \<And>a b ca cap' e s. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; (globals_equiv st and valid_arch_state and valid_global_objs) s\<rbrakk> \<Longrightarrow> globals_equiv st s
 5. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a b ca\<rbrace> derive_cap (b, ca) a \<lbrace>?B36 a b ca\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 6. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R35 a b ca\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 7. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q35 a b ca s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R35 a b ca s)) proof (prove)
goal (6 subgoals):
 1. \<And>a b ca cap' s. \<lbrakk>c = (a, b, ca); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []; cap' \<noteq> NullCap; (globals_equiv st and valid_arch_state and valid_global_objs) s \<and> True\<rbrakk> \<Longrightarrow> (globals_equiv st and valid_arch_state and valid_global_objs) s
 2. \<And>a b ca cap' rv s. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; (globals_equiv st and valid_arch_state and valid_global_objs) s\<rbrakk> \<Longrightarrow> (globals_equiv st and valid_global_objs and valid_arch_state) s \<and> valid_arch_state s \<and> valid_global_objs s
 3. \<And>a b ca cap' e s. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; (globals_equiv st and valid_arch_state and valid_global_objs) s\<rbrakk> \<Longrightarrow> globals_equiv st s
 4. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a b ca\<rbrace> derive_cap (b, ca) a \<lbrace>\<lambda>a b. (globals_equiv st and valid_arch_state and valid_global_objs) b \<and> True\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 5. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R35 a b ca\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 6. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q35 a b ca s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R35 a b ca s)) proof (prove)
goal (3 subgoals):
 1. \<And>a b ca. \<lbrakk>c = (a, b, ca); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a b ca\<rbrace> derive_cap (b, ca) a \<lbrace>\<lambda>a b. globals_equiv st b \<and> valid_arch_state b \<and> valid_global_objs b\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 2. \<And>a b ca. \<lbrakk>c = (a, b, ca); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R35 a b ca\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 3. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q35 a b ca s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R35 a b ca s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b ca s. \<lbrakk>c = (a, b, ca); globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> globals_equiv st s \<and> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> globals_equiv st s)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps_loop ep rcv_buffer n (c # caps') slots mi \<lbrace>\<lambda>_. globals_equiv st\<rbrace>

goal:
No subgoals!