theory Ipc_AC

lemma transfer_caps_loop_pres_dest_aux:
  assumes x: "\<And>cap src dest.
              \<lbrace>\<lambda>s. P s \<and> dest \<in> slots' \<and> src \<in> snd ` caps' \<and> valid_objs s \<and> real_cte_at dest s \<and>
                   s \<turnstile> cap \<and> tcb_cap_valid cap dest s \<and> real_cte_at src s \<and>
                   cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> NullCap\<rbrace>
              cap_insert cap src dest
              \<lbrace>\<lambda>_. P\<rbrace>"
  assumes eb: "\<And>b n'. n' \<le> N \<Longrightarrow> set_extra_badge buffer b n' \<lbrace>P\<rbrace>"
  shows "n + length caps \<le> N \<Longrightarrow>
         \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and> valid_objs s \<and>
              valid_mdb s \<and> distinct slots \<and> (\<forall>x \<in> set slots. real_cte_at x s) \<and>
              (\<forall>x \<in> set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and>
                              cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x
                                              \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace>
         transfer_caps_loop ep buffer n caps slots mi
         \<lbrace>\<lambda>_. P\<rbrace>" (is "?L \<Longrightarrow> ?P n caps slots mi") proof (induct caps arbitrary: slots n mi) case Nil thus ?case by (simp, wp, simp) next case (Cons m ms) hence nN: "n \<le> N" by simp from Cons have "\<And>slots mi. ?P (n + 1) ms slots mi" by clarsimp thus ?case apply (cases m) apply (clarsimp simp add: Let_def split_def whenE_def
                    cong: if_cong list.case_cong split del: if_split) apply (rule hoare_pre) apply (wp eb [OF nN] hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift
           | assumption | simp split del: if_split)+ apply (rule cap_insert_assume_null) apply (wp x hoare_vcg_const_Ball_lift cap_insert_cte_wp_at)+ 
      (* cannot blindly use derive_cap_is_derived_foo here , need to first hoist
         out of the postcondition the conjunct that the return value is derived,
         and solve this using derived_cap_is_derived, and then solve the rest
         using derive_cap_is_derived_foo *)
     apply (rule_tac Q'="\<lambda>r s. S r s \<and> Q r s" for S Q in hoare_post_imp_R) apply (rule hoare_vcg_conj_lift_R) apply (rule derive_cap_is_derived) prefer 2 apply clarsimp apply assumption apply (wp derive_cap_is_derived_foo)+ apply (simp only: tl_drop_1[symmetric]) apply (clarsimp simp: cte_wp_at_caps_of_state
                        ex_cte_cap_to_cnode_always_appropriate_strg
                        real_cte_tcb_valid caps_of_state_valid
             split del: if_split) apply (clarsimp simp: remove_rights_def caps_of_state_valid
                        neq_Nil_conv cte_wp_at_caps_of_state
                        imp_conjR[symmetric] cap_master_cap_masked_as_full
                        cap_badge_masked_as_full
                 split del: if_split) apply (intro conjI) apply clarsimp apply (case_tac "cap = a",clarsimp simp: remove_rights_def) apply (clarsimp simp:masked_as_full_def is_cap_simps) apply (clarsimp simp: cap_master_cap_simps remove_rights_def split:if_splits) apply clarsimp apply (intro conjI) apply (clarsimp split:if_splits elim!: image_eqI[rotated]) apply (clarsimp split:if_splits simp: remove_rights_def) apply (rule ballI) apply (drule(1) bspec) apply clarsimp apply (intro conjI) apply clarsimp apply clarsimp apply (case_tac "capa = ab",clarsimp simp: masked_as_full_def is_cap_simps split: if_splits) apply (clarsimp simp: masked_as_full_double) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n + length caps \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (state)
goal (2 subgoals):
 1. \<And>slots n mi. n + length [] \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set [] \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set []. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n [] slots mi \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>a caps slots n mi. \<lbrakk>\<And>slots n mi. n + length caps \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. P\<rbrace>; n + length (a # caps) \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set (a # caps) \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set (a # caps). s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (state)
this:
n + length [] \<le> N

goal (2 subgoals):
 1. \<And>slots n mi. n + length [] \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set [] \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set []. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n [] slots mi \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>a caps slots n mi. \<lbrakk>\<And>slots n mi. n + length caps \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. P\<rbrace>; n + length (a # caps) \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set (a # caps) \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set (a # caps). s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
using this:
n + length [] \<le> N

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set [] \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set []. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n [] slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set [] \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set []. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n [] slots mi \<lbrace>\<lambda>_. P\<rbrace>

goal (1 subgoal):
 1. \<And>a caps slots n mi. \<lbrakk>\<And>slots n mi. n + length caps \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. P\<rbrace>; n + length (a # caps) \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set (a # caps) \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set (a # caps). s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>a caps slots n mi. \<lbrakk>\<And>slots n mi. n + length caps \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. P\<rbrace>; n + length (a # caps) \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set (a # caps) \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set (a # caps). s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (state)
this:
?n + length ms \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set ?slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct ?slots \<and> (\<forall>x\<in>set ?slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer ?n ms ?slots ?mi \<lbrace>\<lambda>_. P\<rbrace>
n + length (m # ms) \<le> N

goal (1 subgoal):
 1. \<And>a caps slots n mi. \<lbrakk>\<And>slots n mi. n + length caps \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. P\<rbrace>; n + length (a # caps) \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set (a # caps) \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set (a # caps). s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
using this:
?n + length ms \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set ?slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct ?slots \<and> (\<forall>x\<in>set ?slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer ?n ms ?slots ?mi \<lbrace>\<lambda>_. P\<rbrace>
n + length (m # ms) \<le> N

goal (1 subgoal):
 1. n \<le> N proof (state)
this:
n \<le> N

goal (1 subgoal):
 1. \<And>a caps slots n mi. \<lbrakk>\<And>slots n mi. n + length caps \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. P\<rbrace>; n + length (a # caps) \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set (a # caps) \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set (a # caps). s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (chain)
picking this:
?n + length ms \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set ?slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct ?slots \<and> (\<forall>x\<in>set ?slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer ?n ms ?slots ?mi \<lbrace>\<lambda>_. P\<rbrace>
n + length (m # ms) \<le> N proof (prove)
using this:
?n + length ms \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set ?slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct ?slots \<and> (\<forall>x\<in>set ?slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer ?n ms ?slots ?mi \<lbrace>\<lambda>_. P\<rbrace>
n + length (m # ms) \<le> N

goal (1 subgoal):
 1. \<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (n + 1) ms slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. P s \<and> set ?slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct ?slots \<and> (\<forall>x\<in>set ?slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (n + 1) ms ?slots ?mi \<lbrace>\<lambda>_. P\<rbrace>

goal (1 subgoal):
 1. \<And>a caps slots n mi. \<lbrakk>\<And>slots n mi. n + length caps \<le> N \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. P\<rbrace>; n + length (a # caps) \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set (a # caps) \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set (a # caps). s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
using this:
\<lbrace>\<lambda>s. P s \<and> set ?slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct ?slots \<and> (\<forall>x\<in>set ?slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (n + 1) ms ?slots ?mi \<lbrace>\<lambda>_. P\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set (m # ms) \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set (m # ms). s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n (m # ms) slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (n + 1) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set (m # ms) \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set (m # ms). s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n (m # ms) slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<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) ms 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, c) a;
y <- if cap' = NullCap then throwError undefined else returnOk ();
y <- liftE (cap_insert cap' (b, c) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) ms (tl slots) mi)
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c)\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 a b c\<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) ms 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, c) a;
y <- if cap' = NullCap then throwError undefined else returnOk ();
y <- liftE (cap_insert cap' (b, c) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) ms (tl slots) mi)
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))) \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> ?Q9 a b c s proof (prove)
goal (5 subgoals):
 1. \<And>a b c cap'. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B69 a b c cap' ()\<rbrace> cap_insert cap' (b, c) (hd slots) \<lbrace>\<lambda>ya s. P s \<and> set (tl slots) \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace>
 2. \<And>a b c cap'. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B68 a b c cap'\<rbrace> if cap' = NullCap then throwError undefined else returnOk () \<lbrace>?B69 a b c cap'\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q67 a b c\<rbrace> derive_cap (b, c) a \<lbrace>?B68 a b c\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R67 a b c\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q67 a b c s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R67 a b c s)) proof (prove)
goal (5 subgoals):
 1. \<And>a b c cap'. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P79 a b c cap' ()\<rbrace> cap_insert cap' (b, c) (hd slots) \<lbrace>\<lambda>ya s. P s \<and> set (tl slots) \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace>
 2. \<And>a b c cap'. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B68 a b c cap'\<rbrace> if cap' = NullCap then throwError undefined else returnOk () \<lbrace>\<lambda>d e. cte_wp_at ((=) NullCap) (hd slots) e \<longrightarrow> ?P79 a b c cap' d e\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q67 a b c\<rbrace> derive_cap (b, c) a \<lbrace>?B68 a b c\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R67 a b c\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q67 a b c s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R67 a b c s)) proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'137 a b c\<rbrace> derive_cap (b, c) a \<lbrace>\<lambda>cap' s. (cap' = NullCap \<longrightarrow> P s \<and> True) \<and> (cap' \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> (P s \<and> hd slots \<in> slots' \<and> (b, c) \<in> snd ` caps' \<and> valid_objs s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> cap' \<and> tcb_cap_valid cap' (hd slots) s \<and> real_cte_at (b, c) s \<and> cte_wp_at (is_derived (cdt s) (b, c) cap') (b, c) s \<and> cap' \<noteq> NullCap) \<and> set (tl slots) \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> (valid_objs and (\<lambda>a. a \<turnstile> cap') and tcb_cap_valid cap' (hd slots)) s \<and> (valid_mdb and (\<lambda>a. a \<turnstile> cap') and valid_objs and (\<lambda>s. cte_wp_at (is_derived (cdt s) (b, c) cap') (b, c) s) and K ((b, c) \<noteq> hd slots)) s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (is_derived (cdt s) (b, c) cap') (b, c) s \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<and> masked_as_full c cap' \<noteq> fst x \<longrightarrow> masked_as_full c cap' = masked_as_full (fst x) (fst x)) (snd x) s)))\<rbrace>, -
 2. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R67 a b c\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ?P'137 a b c s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R67 a b c s)) proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'137 a b c\<rbrace> derive_cap (b, c) a \<lbrace>\<lambda>cap' s. (cap' = NullCap \<longrightarrow> P s \<and> True) \<and> (cap' \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> (P s \<and> hd slots \<in> slots' \<and> (b, c) \<in> snd ` caps' \<and> valid_objs s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> cap' \<and> tcb_cap_valid cap' (hd slots) s \<and> real_cte_at (b, c) s \<and> cte_wp_at (is_derived (cdt s) (b, c) cap') (b, c) s \<and> cap' \<noteq> NullCap) \<and> set (tl slots) \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> (valid_objs and (\<lambda>a. a \<turnstile> cap') and tcb_cap_valid cap' (hd slots)) s \<and> (valid_mdb and (\<lambda>a. a \<turnstile> cap') and valid_objs and (\<lambda>s. cte_wp_at (is_derived (cdt s) (b, c) cap') (b, c) s) and K ((b, c) \<noteq> hd slots)) s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (is_derived (cdt s) (b, c) cap') (b, c) s \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<and> masked_as_full c cap' \<noteq> fst x \<longrightarrow> masked_as_full c cap' = masked_as_full (fst x) (fst x)) (snd x) s)))\<rbrace>, -
 2. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R67 a b c\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ?P'137 a b c s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R67 a b c s)) proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'137 a b c\<rbrace> derive_cap (b, c) a \<lbrace>\<lambda>r s. ?S144 a b c r s \<and> ?Q144 a b c r s\<rbrace>, -
 2. \<And>a b c rv s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; ?S144 a b c rv s \<and> ?Q144 a b c rv s\<rbrakk> \<Longrightarrow> (rv = NullCap \<longrightarrow> P s \<and> True) \<and> (rv \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> (P s \<and> hd slots \<in> slots' \<and> (b, c) \<in> snd ` caps' \<and> valid_objs s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> real_cte_at (b, c) s \<and> cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s \<and> rv \<noteq> NullCap) \<and> set (tl slots) \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> (valid_objs and (\<lambda>a. a \<turnstile> rv) and tcb_cap_valid rv (hd slots)) s \<and> (valid_mdb and (\<lambda>a. a \<turnstile> rv) and valid_objs and (\<lambda>s. cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s) and K ((b, c) \<noteq> hd slots)) s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<and> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<and> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s)))
 3. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R67 a b c\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ?P'137 a b c s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R67 a b c s)) proof (prove)
goal (5 subgoals):
 1. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P145 a b c\<rbrace> derive_cap (b, c) a \<lbrace>?S144 a b c\<rbrace>, -
 2. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R145 a b c\<rbrace> derive_cap (b, c) a \<lbrace>?Q144 a b c\<rbrace>, -
 3. \<And>a b c rv s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; ?S144 a b c rv s \<and> ?Q144 a b c rv s\<rbrakk> \<Longrightarrow> (rv = NullCap \<longrightarrow> P s \<and> True) \<and> (rv \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> (P s \<and> hd slots \<in> slots' \<and> (b, c) \<in> snd ` caps' \<and> valid_objs s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> real_cte_at (b, c) s \<and> cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s \<and> rv \<noteq> NullCap) \<and> set (tl slots) \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> (valid_objs and (\<lambda>a. a \<turnstile> rv) and tcb_cap_valid rv (hd slots)) s \<and> (valid_mdb and (\<lambda>a. a \<turnstile> rv) and valid_objs and (\<lambda>s. cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s) and K ((b, c) \<noteq> hd slots)) s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<and> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<and> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s)))
 4. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R67 a b c\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ?P145 a b c s \<and> ?R145 a b c s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R67 a b c s)) proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R145 a b c\<rbrace> derive_cap (b, c) a \<lbrace>?Q144 a b c\<rbrace>, -
 2. \<And>a b c rv s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; (rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s) \<and> ?Q144 a b c rv s\<rbrakk> \<Longrightarrow> (rv = NullCap \<longrightarrow> P s \<and> True) \<and> (rv \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> (P s \<and> hd slots \<in> slots' \<and> (b, c) \<in> snd ` caps' \<and> valid_objs s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> real_cte_at (b, c) s \<and> cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s \<and> rv \<noteq> NullCap) \<and> set (tl slots) \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> (valid_objs and (\<lambda>a. a \<turnstile> rv) and tcb_cap_valid rv (hd slots)) s \<and> (valid_mdb and (\<lambda>a. a \<turnstile> rv) and valid_objs and (\<lambda>s. cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s) and K ((b, c) \<noteq> hd slots)) s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<and> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<and> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s)))
 3. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R67 a b c\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> (a \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid a \<and> vs_cap_ref cap = vs_cap_ref a) (b, c) s \<and> valid_objs s) \<and> ?R145 a b c s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R67 a b c s)) proof (prove)
goal (4 subgoals):
 1. \<And>a b c rv s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; (rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s) \<and> ?Q144 a b c rv s\<rbrakk> \<Longrightarrow> (rv = NullCap \<longrightarrow> P s \<and> True) \<and> (rv \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> (P s \<and> hd slots \<in> slots' \<and> (b, c) \<in> snd ` caps' \<and> valid_objs s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> real_cte_at (b, c) s \<and> cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s \<and> rv \<noteq> NullCap) \<and> set (tl slots) \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> (valid_objs and (\<lambda>a. a \<turnstile> rv) and tcb_cap_valid rv (hd slots)) s \<and> (valid_mdb and (\<lambda>a. a \<turnstile> rv) and valid_objs and (\<lambda>s. cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s) and K ((b, c) \<noteq> hd slots)) s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<and> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<and> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s)))
 2. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R145 a b c\<rbrace> derive_cap (b, c) a \<lbrace>?Q144 a b c\<rbrace>, -
 3. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R67 a b c\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> (a \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid a \<and> vs_cap_ref cap = vs_cap_ref a) (b, c) s \<and> valid_objs s) \<and> ?R145 a b c s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R67 a b c s)) proof (prove)
goal (4 subgoals):
 1. \<And>a b c rv s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []; rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (b, c) rv) (b, c) s; ?Q144 a b c rv s\<rbrakk> \<Longrightarrow> (rv = NullCap \<longrightarrow> P s) \<and> (rv \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> P s \<and> hd slots \<in> slots' \<and> (b, c) \<in> snd ` caps' \<and> valid_objs s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> cap_table_at (length c) b s \<and> set (tl slots) \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> valid_mdb s \<and> s \<turnstile> rv \<and> valid_objs s \<and> (b, c) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. (snd x = hd slots \<longrightarrow> s \<turnstile> fst x \<and> real_cte_at (hd slots) s \<and> valid_mdb s \<and> valid_objs s \<and> (fst x \<noteq> NullCap \<and> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x))) \<and> (snd x \<noteq> hd slots \<longrightarrow> s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<and> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s)))
 2. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R145 a b c\<rbrace> derive_cap (b, c) a \<lbrace>?Q144 a b c\<rbrace>, -
 3. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R67 a b c\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> (a \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid a \<and> vs_cap_ref cap = vs_cap_ref a) (b, c) s \<and> valid_objs s) \<and> ?R145 a b c s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R67 a b c s)) proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R145 a b c\<rbrace> derive_cap (b, c) a \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s) \<and> (rv \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> P s \<and> hd slots \<in> slots' \<and> (b, c) \<in> snd ` caps' \<and> valid_objs s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> cap_table_at (length c) b s \<and> set (tl slots) \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> valid_mdb s \<and> s \<turnstile> rv \<and> valid_objs s \<and> (b, c) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. (snd x = hd slots \<longrightarrow> s \<turnstile> fst x \<and> real_cte_at (hd slots) s \<and> valid_mdb s \<and> valid_objs s \<and> (fst x \<noteq> NullCap \<and> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x))) \<and> (snd x \<noteq> hd slots \<longrightarrow> s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<and> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s)))\<rbrace>, -
 2. \<And>a b c. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R67 a b c\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> (a \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid a \<and> vs_cap_ref cap = vs_cap_ref a) (b, c) s \<and> valid_objs s) \<and> ?R145 a b c s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R67 a b c s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> set slots \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> (a \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid a \<and> vs_cap_ref cap = vs_cap_ref a) (b, c) s \<and> valid_objs s) \<and> (\<forall>cap'. (cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap a \<and> (cap_badge capa, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid a \<and> vs_cap_ref capa = vs_cap_ref a) (b, c) s \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (b, c) s) \<and> (s \<turnstile> a \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> a \<noteq> NullCap \<and> \<not> is_zombie a \<and> a \<noteq> IRQControlCap) \<longrightarrow> (cap' = NullCap \<longrightarrow> P s) \<and> (cap' \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> P s \<and> hd slots \<in> slots' \<and> (b, c) \<in> snd ` caps' \<and> valid_objs s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> cap' \<and> tcb_cap_valid cap' (hd slots) s \<and> cap_table_at (length c) b s \<and> set (tl slots) \<subseteq> slots' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> s \<turnstile> cap' \<and> tcb_cap_valid cap' (hd slots) s \<and> valid_mdb s \<and> s \<turnstile> cap' \<and> valid_objs s \<and> (b, c) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. (snd x = hd slots \<longrightarrow> s \<turnstile> fst x \<and> real_cte_at (hd slots) s \<and> valid_mdb s \<and> valid_objs s \<and> (fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x))) \<and> (snd x \<noteq> hd slots \<longrightarrow> s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<and> masked_as_full c cap' \<noteq> fst x \<longrightarrow> masked_as_full c cap' = masked_as_full (fst x) (fst x)) (snd x) s))))) \<and> (\<not> slots \<noteq> [] \<longrightarrow> P s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> True \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s \<and> set slots \<subseteq> slots' \<and> (a, b, c) \<in> caps' \<and> set ms \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> s \<turnstile> a \<and> cap_table_at (length c) b s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (b, c) s \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> True \<and> (a \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid a \<and> vs_cap_ref cap = vs_cap_ref a) (b, c) s \<and> True) \<and> (\<forall>cap'. (cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap a \<and> (cap_badge capa, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid a \<and> vs_cap_ref capa = vs_cap_ref a) (b, c) s \<and> True \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (b, c) s) \<and> (True \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> a \<noteq> NullCap \<and> \<not> is_zombie a \<and> a \<noteq> IRQControlCap) \<longrightarrow> (cap' = NullCap \<longrightarrow> True) \<and> (cap' \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> True \<and> hd slots \<in> slots' \<and> (b, c) \<in> snd ` caps' \<and> True \<and> real_cte_at (hd slots) s \<and> s \<turnstile> cap' \<and> tcb_cap_valid cap' (hd slots) s \<and> True \<and> set (tl slots) \<subseteq> slots' \<and> True \<and> True \<and> s \<turnstile> cap' \<and> tcb_cap_valid cap' (hd slots) s \<and> True \<and> s \<turnstile> cap' \<and> True \<and> (b, c) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. (snd x = hd slots \<longrightarrow> s \<turnstile> fst x \<and> real_cte_at (hd slots) s \<and> True \<and> True \<and> (fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x))) \<and> (snd x \<noteq> hd slots \<longrightarrow> s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> True \<and> True \<and> cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<and> masked_as_full c cap' \<noteq> fst x \<longrightarrow> masked_as_full c cap' = masked_as_full (fst x) (fst x)) (snd x) s))))) \<and> (\<not> slots \<noteq> [] \<longrightarrow> True)) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s cap. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; set slots \<subseteq> slots'; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; distinct slots; \<forall>x\<in>set slots. real_cte_at x s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; a \<noteq> NullCap \<and> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> (a \<noteq> NullCap \<longrightarrow> cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid a \<and> vs_cap_ref cap = vs_cap_ref a) \<and> (\<forall>cap'. s \<turnstile> cap' \<and> (cap' \<noteq> NullCap \<longrightarrow> a \<noteq> NullCap \<and> \<not> is_zombie a \<and> a \<noteq> IRQControlCap) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> caps_of_state s (hd slots) = Some NullCap \<longrightarrow> hd slots \<in> slots' \<and> (b, c) \<in> snd ` caps' \<and> set (tl slots) \<subseteq> slots' \<and> (b, c) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). real_cte_at x s) \<and> (\<forall>x\<in>set ms. (snd x = hd slots \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> hd slots \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x)))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s cap aa ba ys. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; a \<noteq> NullCap \<and> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s\<rbrakk> \<Longrightarrow> (a \<noteq> NullCap \<longrightarrow> cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid a \<and> vs_cap_ref cap = vs_cap_ref a) \<and> (\<forall>cap'. s \<turnstile> cap' \<and> (cap' \<noteq> NullCap \<longrightarrow> a \<noteq> NullCap \<and> \<not> is_zombie a \<and> a \<noteq> IRQControlCap) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> caps_of_state s (aa, ba) = Some NullCap \<longrightarrow> (b, c) \<in> snd ` caps' \<and> (b = aa \<longrightarrow> c \<noteq> ba) \<and> (\<forall>x\<in>set ms. (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x)))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c s cap aa ba ys. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; a \<noteq> NullCap \<and> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s\<rbrakk> \<Longrightarrow> a \<noteq> NullCap \<longrightarrow> cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid a \<and> vs_cap_ref cap = vs_cap_ref a
 2. \<And>a b c s cap aa ba ys. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; a \<noteq> NullCap \<and> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s\<rbrakk> \<Longrightarrow> \<forall>cap'. s \<turnstile> cap' \<and> (cap' \<noteq> NullCap \<longrightarrow> a \<noteq> NullCap \<and> \<not> is_zombie a \<and> a \<noteq> IRQControlCap) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> caps_of_state s (aa, ba) = Some NullCap \<longrightarrow> (b, c) \<in> snd ` caps' \<and> (b = aa \<longrightarrow> c \<noteq> ba) \<and> (\<forall>x\<in>set ms. (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c s cap aa ba ys. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; a \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid a \<and> vs_cap_ref cap = vs_cap_ref a
 2. \<And>a b c s cap aa ba ys. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; a \<noteq> NullCap \<and> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s\<rbrakk> \<Longrightarrow> \<forall>cap'. s \<turnstile> cap' \<and> (cap' \<noteq> NullCap \<longrightarrow> a \<noteq> NullCap \<and> \<not> is_zombie a \<and> a \<noteq> IRQControlCap) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> caps_of_state s (aa, ba) = Some NullCap \<longrightarrow> (b, c) \<in> snd ` caps' \<and> (b = aa \<longrightarrow> c \<noteq> ba) \<and> (\<forall>x\<in>set ms. (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c s cap aa ba ys. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; a \<noteq> NullCap; cap \<noteq> a\<rbrakk> \<Longrightarrow> cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid a \<and> vs_cap_ref cap = vs_cap_ref a
 2. \<And>a b c s cap aa ba ys. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; a \<noteq> NullCap \<and> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s\<rbrakk> \<Longrightarrow> \<forall>cap'. s \<turnstile> cap' \<and> (cap' \<noteq> NullCap \<longrightarrow> a \<noteq> NullCap \<and> \<not> is_zombie a \<and> a \<noteq> IRQControlCap) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> caps_of_state s (aa, ba) = Some NullCap \<longrightarrow> (b, c) \<in> snd ` caps' \<and> (b = aa \<longrightarrow> c \<noteq> ba) \<and> (\<forall>x\<in>set ms. (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x))))) proof (prove)
goal (2 subgoals):
 1. \<And>b c s aa ba ys dev r bits f. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = (if \<exists>dev r bits f. fst x = UntypedCap dev r bits f then max_free_index_update (fst x) else fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (UntypedCap dev r bits f, b, c); P s; (UntypedCap dev r bits f, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> UntypedCap dev r bits f; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = (if \<exists>dev r bits f. fst x = UntypedCap dev r bits f then max_free_index_update (fst x) else fst x))); caps_of_state s (b, c) = Some (UntypedCap dev r bits (max_free_index bits)); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; max_free_index bits \<noteq> f\<rbrakk> \<Longrightarrow> cap_master_cap (UntypedCap dev r bits (max_free_index bits)) = cap_master_cap (UntypedCap dev r bits f)
 2. \<And>a b c s cap aa ba ys. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; a \<noteq> NullCap \<and> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s\<rbrakk> \<Longrightarrow> \<forall>cap'. s \<turnstile> cap' \<and> (cap' \<noteq> NullCap \<longrightarrow> a \<noteq> NullCap \<and> \<not> is_zombie a \<and> a \<noteq> IRQControlCap) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> caps_of_state s (aa, ba) = Some NullCap \<longrightarrow> (b, c) \<in> snd ` caps' \<and> (b = aa \<longrightarrow> c \<noteq> ba) \<and> (\<forall>x\<in>set ms. (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s cap aa ba ys. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; a \<noteq> NullCap \<and> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s\<rbrakk> \<Longrightarrow> \<forall>cap'. s \<turnstile> cap' \<and> (cap' \<noteq> NullCap \<longrightarrow> a \<noteq> NullCap \<and> \<not> is_zombie a \<and> a \<noteq> IRQControlCap) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> caps_of_state s (aa, ba) = Some NullCap \<longrightarrow> (b, c) \<in> snd ` caps' \<and> (b = aa \<longrightarrow> c \<noteq> ba) \<and> (\<forall>x\<in>set ms. (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s cap aa ba ys cap'. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> (b, c) \<in> snd ` caps' \<and> (b = aa \<longrightarrow> c \<noteq> ba) \<and> (\<forall>x\<in>set ms. (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x))))) proof (prove)
goal (3 subgoals):
 1. \<And>a b c s cap aa ba ys cap'. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> (b, c) \<in> snd ` caps'
 2. \<And>a b c s cap aa ba ys cap'. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> b = aa \<longrightarrow> c \<noteq> ba
 3. \<And>a b c s cap aa ba ys cap'. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ms. (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x)))) proof (prove)
goal (2 subgoals):
 1. \<And>a b c s cap aa ba ys cap'. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> b = aa \<longrightarrow> c \<noteq> ba
 2. \<And>a b c s cap aa ba ys cap'. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ms. (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x)))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s cap aa ba ys cap'. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ms. (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x)))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s cap aa ba ys cap' x. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; \<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap; x \<in> set ms\<rbrakk> \<Longrightarrow> (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x)))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s cap aa ba ys cap' x. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap; x \<in> set ms; s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))\<rbrakk> \<Longrightarrow> (snd x = (aa, ba) \<longrightarrow> fst x \<noteq> NullCap \<and> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (aa, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x)))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s cap aa ba ys cap' ab ac bb capa. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap; (ab, ac, bb) \<in> set ms; s \<turnstile> ab; cap_table_at (length bb) ac s; caps_of_state s (ac, bb) = Some capa; ab \<noteq> NullCap \<and> capa \<noteq> ab \<longrightarrow> capa = masked_as_full ab ab\<rbrakk> \<Longrightarrow> (ac = aa \<and> bb = ba \<longrightarrow> ab \<noteq> NullCap \<and> cap' \<noteq> ab \<longrightarrow> cap' = masked_as_full ab ab) \<and> ((ac = aa \<longrightarrow> bb \<noteq> ba) \<longrightarrow> ab \<noteq> NullCap \<and> masked_as_full capa cap' \<noteq> ab \<longrightarrow> masked_as_full capa cap' = masked_as_full ab ab) proof (prove)
goal (2 subgoals):
 1. \<And>a b c s cap aa ba ys cap' ab ac bb capa. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap; (ab, ac, bb) \<in> set ms; s \<turnstile> ab; cap_table_at (length bb) ac s; caps_of_state s (ac, bb) = Some capa; ab \<noteq> NullCap \<and> capa \<noteq> ab \<longrightarrow> capa = masked_as_full ab ab\<rbrakk> \<Longrightarrow> ac = aa \<and> bb = ba \<longrightarrow> ab \<noteq> NullCap \<and> cap' \<noteq> ab \<longrightarrow> cap' = masked_as_full ab ab
 2. \<And>a b c s cap aa ba ys cap' ab ac bb capa. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap; (ab, ac, bb) \<in> set ms; s \<turnstile> ab; cap_table_at (length bb) ac s; caps_of_state s (ac, bb) = Some capa; ab \<noteq> NullCap \<and> capa \<noteq> ab \<longrightarrow> capa = masked_as_full ab ab\<rbrakk> \<Longrightarrow> (ac = aa \<longrightarrow> bb \<noteq> ba) \<longrightarrow> ab \<noteq> NullCap \<and> masked_as_full capa cap' \<noteq> ab \<longrightarrow> masked_as_full capa cap' = masked_as_full ab ab proof (prove)
goal (1 subgoal):
 1. \<And>a b c s cap aa ba ys cap' ab ac bb capa. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap; (ab, ac, bb) \<in> set ms; s \<turnstile> ab; cap_table_at (length bb) ac s; caps_of_state s (ac, bb) = Some capa; ab \<noteq> NullCap \<and> capa \<noteq> ab \<longrightarrow> capa = masked_as_full ab ab\<rbrakk> \<Longrightarrow> (ac = aa \<longrightarrow> bb \<noteq> ba) \<longrightarrow> ab \<noteq> NullCap \<and> masked_as_full capa cap' \<noteq> ab \<longrightarrow> masked_as_full capa cap' = masked_as_full ab ab proof (prove)
goal (1 subgoal):
 1. \<And>a b c s cap aa ba ys cap' ab ac bb capa. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap; (ab, ac, bb) \<in> set ms; s \<turnstile> ab; cap_table_at (length bb) ac s; caps_of_state s (ac, bb) = Some capa; capa \<noteq> ab \<longrightarrow> capa = masked_as_full ab ab; ac = aa \<longrightarrow> bb \<noteq> ba; ab \<noteq> NullCap; masked_as_full capa cap' \<noteq> ab\<rbrakk> \<Longrightarrow> masked_as_full capa cap' = masked_as_full ab ab proof (prove)
goal (1 subgoal):
 1. \<And>a b c s cap aa ba ys cap' ab ac bb capa. \<lbrakk>\<And>slots mi. \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set ms. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<and> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer (Suc n) ms slots mi \<lbrace>\<lambda>_. P\<rbrace>; m = (a, b, c); P s; (a, b, c) \<in> caps'; set ms \<subseteq> caps'; valid_objs s; valid_mdb s; s \<turnstile> a; cap_table_at (length c) b s; caps_of_state s (b, c) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots = (aa, ba) # ys; (aa, ba) \<in> slots'; set ys \<subseteq> slots'; (aa, ba) \<notin> set ys; distinct ys; cap_table_at (length ba) aa s; \<forall>x\<in>set ys. real_cte_at x s; s \<turnstile> cap'; cap' \<noteq> NullCap; caps_of_state s (aa, ba) = Some NullCap; a \<noteq> NullCap; \<not> is_zombie a; a \<noteq> IRQControlCap; (ab, ac, bb) \<in> set ms; s \<turnstile> ab; cap_table_at (length bb) ac s; caps_of_state s (ac, bb) = Some capa; capa \<noteq> ab \<longrightarrow> capa = masked_as_full ab ab; ac = aa \<longrightarrow> bb \<noteq> ba; ab \<noteq> NullCap; masked_as_full capa cap' \<noteq> ab; capa \<noteq> ab\<rbrakk> \<Longrightarrow> masked_as_full capa cap' = masked_as_full ab ab proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set (m # ms) \<subseteq> caps' \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set (m # ms). s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n (m # ms) slots mi \<lbrace>\<lambda>_. P\<rbrace>

goal:
No subgoals!