theory Ipc_AI

lemma transfer_caps_loop_presM:
  fixes P vo em ex buffer slots caps n mi
  assumes x: "\<And>cap src dest.
              \<lbrace>\<lambda>s::'state_ext state.
                               P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb 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> cap.NullCap)
                       \<and> (em \<longrightarrow> cte_wp_at ((=) cap.NullCap) dest s)
                       \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s)\<rbrace>
                 cap_insert cap src dest \<lbrace>\<lambda>rv. P\<rbrace>"
  assumes eb: "\<And>b n. \<lbrace>P\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_. P\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and>
                                 (\<forall>x \<in> set slots.  cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s \<and> real_cte_at x s) \<and>
                                 (\<forall>x \<in> set caps. valid_cap (fst x) s \<and>
                                  cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s
                                           \<and> real_cte_at (snd x) s))
                       \<and> (ex \<longrightarrow> (\<forall>x \<in> set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace>
                  transfer_caps_loop ep buffer n caps slots mi
              \<lbrace>\<lambda>rv. P\<rbrace>" apply (induct caps arbitrary: slots n mi) apply (simp, wp, simp) 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 hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift hoare_weak_lift_imp
           | 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 hoare_weak_lift_imp)+ apply (rule hoare_vcg_conj_liftE_R) apply (rule derive_cap_is_derived_foo) apply (rule_tac Q' ="\<lambda>cap' s. (vo \<longrightarrow> cap'\<noteq> cap.NullCap \<longrightarrow>
          cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s)
          \<and> (cap'\<noteq> cap.NullCap \<longrightarrow> QM s cap')" for QM
          in hoare_post_imp_R) prefer 2 apply clarsimp apply assumption apply (rule hoare_vcg_conj_liftE_R) apply (rule hoare_vcg_const_imp_lift_R) apply (rule derive_cap_is_derived) apply (wp derive_cap_is_derived_foo)+ 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] conj_comms
                 split del: if_split) apply (intro conjI) apply clarsimp apply (case_tac "cap = a",clarsimp) apply (clarsimp simp:masked_as_full_def is_cap_simps) apply (clarsimp simp: cap_master_cap_simps split:if_splits) apply (clarsimp split del: if_split) apply (intro conjI) apply (clarsimp split: if_split) apply (clarsimp) apply (rule ballI) apply (drule(1) bspec) apply clarsimp apply (intro conjI) apply (case_tac "capa = ac",clarsimp+) apply (case_tac "capa = ac") apply (clarsimp simp:masked_as_full_def is_cap_simps split:if_splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set []. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n [] slots mi \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set (a # caps). s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set (a # caps). s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a aa b caps slots n mi. (\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap 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) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE else if slots \<noteq> [] then doE cap' <- derive_cap (aa, b) a;
y <- if cap' = NullCap then throwError undefined else returnOk ();
y <- liftE (cap_insert cap' (aa, b) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) caps (tl slots) mi)
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a aa b caps slots n mi. (\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>?Q12 a aa b caps slots n mi\<rbrace> const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (if is_ep_cap a \<and> ep = Some (obj_ref_of a) then doE y <- liftE (set_extra_badge buffer (cap_ep_badge a) n);
liftE (transfer_caps_loop (Some (obj_ref_of a)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE else if slots \<noteq> [] then doE cap' <- derive_cap (aa, b) a;
y <- if cap' = NullCap then throwError undefined else returnOk ();
y <- liftE (cap_insert cap' (aa, b) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) caps (tl slots) mi)
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))) \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> ?Q12 a aa b caps slots n mi s proof (prove)
goal (5 subgoals):
 1. \<And>a aa b caps slots n mi cap'. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B78 a aa b caps slots n mi cap' ()\<rbrace> cap_insert cap' (aa, b) (hd slots) \<lbrace>\<lambda>ya s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace>
 2. \<And>a aa b caps slots n mi cap'. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B77 a aa b caps slots n mi cap'\<rbrace> if cap' = NullCap then throwError undefined else returnOk () \<lbrace>?B78 a aa b caps slots n mi cap'\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q76 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>?B77 a aa b caps slots n mi\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q76 a aa b caps slots n mi s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (5 subgoals):
 1. \<And>a aa b caps slots n mi cap'. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P174 a aa b caps slots n mi cap' ()\<rbrace> cap_insert cap' (aa, b) (hd slots) \<lbrace>\<lambda>ya s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace>
 2. \<And>a aa b caps slots n mi cap'. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B77 a aa b caps slots n mi cap'\<rbrace> if cap' = NullCap then throwError undefined else returnOk () \<lbrace>\<lambda>c d. cte_wp_at ((=) NullCap) (hd slots) d \<longrightarrow> ?P174 a aa b caps slots n mi cap' c d\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q76 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>?B77 a aa b caps slots n mi\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q76 a aa b caps slots n mi s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'243 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) 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> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> cap' \<and> tcb_cap_valid cap' (hd slots) s \<and> real_cte_at (aa, b) s \<and> cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s \<and> cap' \<noteq> NullCap) \<and> (em \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s) \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap') (hd slots) s)) \<and> (vo \<longrightarrow> (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) (aa, b) cap') (aa, b) s) and K ((aa, b) \<noteq> hd slots)) s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). (cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then cap' = NullCap else cte_wp_at (\<lambda>c. masked_as_full c cap' = NullCap) x s)) \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> (cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> 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> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). (K_bind (\<forall>xa. is_cnode_cap xa = is_cnode_cap (free_index_update (\<lambda>_. ?y232 a aa b caps slots n mi cap' () x) xa)) and ex_cte_cap_wp_to is_cnode_cap x) s)))\<rbrace>, -
 2. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ?P'243 a aa b caps slots n mi s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (4 subgoals):
 1. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P246 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>rv s. rv = NullCap \<longrightarrow> P s \<and> True\<rbrace>, -
 2. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q246 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> (P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> real_cte_at (aa, b) s \<and> cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> rv \<noteq> NullCap) \<and> (em \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s) \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap rv) (hd slots) s)) \<and> (vo \<longrightarrow> (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) (aa, b) rv) (aa, b) s) and K ((aa, b) \<noteq> hd slots)) s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). (cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then rv = NullCap else cte_wp_at (\<lambda>c. masked_as_full c rv = NullCap) x s)) \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> (cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<longrightarrow> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). (K_bind (\<forall>xa. is_cnode_cap xa = is_cnode_cap (free_index_update (\<lambda>_. ?y232 a aa b caps slots n mi rv () x) xa)) and ex_cte_cap_wp_to is_cnode_cap x) s))\<rbrace>, -
 3. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> (?P246 a aa b caps slots n mi and ?Q246 a aa b caps slots n mi) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q246 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> (P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> real_cte_at (aa, b) s \<and> cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> rv \<noteq> NullCap) \<and> (em \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s) \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap rv) (hd slots) s)) \<and> (vo \<longrightarrow> (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) (aa, b) rv) (aa, b) s) and K ((aa, b) \<noteq> hd slots)) s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). (cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then rv = NullCap else cte_wp_at (\<lambda>c. masked_as_full c rv = NullCap) x s)) \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> (cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<longrightarrow> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). (K_bind (\<forall>xa. is_cnode_cap xa = is_cnode_cap (free_index_update (\<lambda>_. ?y232 a aa b caps slots n mi rv () x) xa)) and ex_cte_cap_wp_to is_cnode_cap x) s))\<rbrace>, -
 2. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ((\<lambda>s. \<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) (aa, b) s \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) 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> True) and ?Q246 a aa b caps slots n mi) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (4 subgoals):
 1. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q246 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>cap' s. (vo \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s) \<and> (cap' \<noteq> NullCap \<longrightarrow> ?QM254 a aa b caps slots n mi s cap')\<rbrace>, -
 2. \<And>a aa b caps slots n mi rv s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; (vo \<longrightarrow> rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?QM254 a aa b caps slots n mi s rv)\<rbrakk> \<Longrightarrow> rv \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> (P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> real_cte_at (aa, b) s \<and> cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> rv \<noteq> NullCap) \<and> (em \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s) \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap rv) (hd slots) s)) \<and> (vo \<longrightarrow> (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) (aa, b) rv) (aa, b) s) and K ((aa, b) \<noteq> hd slots)) s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). (cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then rv = NullCap else cte_wp_at (\<lambda>c. masked_as_full c rv = NullCap) x s)) \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> (cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<longrightarrow> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). (K_bind (\<forall>xa. is_cnode_cap xa = is_cnode_cap (free_index_update (\<lambda>_. ?y232 a aa b caps slots n mi rv () x) xa)) and ex_cte_cap_wp_to is_cnode_cap x) s))
 3. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ((\<lambda>s. \<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) (aa, b) s \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) 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> True) and ?Q246 a aa b caps slots n mi) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (4 subgoals):
 1. \<And>a aa b caps slots n mi rv s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; (vo \<longrightarrow> rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?QM254 a aa b caps slots n mi s rv)\<rbrakk> \<Longrightarrow> rv \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s \<longrightarrow> (P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> real_cte_at (hd slots) s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> real_cte_at (aa, b) s \<and> cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> rv \<noteq> NullCap) \<and> (em \<longrightarrow> cte_wp_at ((=) NullCap) (hd slots) s) \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap rv) (hd slots) s)) \<and> (vo \<longrightarrow> (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) (aa, b) rv) (aa, b) s) and K ((aa, b) \<noteq> hd slots)) s \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). (cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then rv = NullCap else cte_wp_at (\<lambda>c. masked_as_full c rv = NullCap) x s)) \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> (cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<longrightarrow> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). (K_bind (\<forall>xa. is_cnode_cap xa = is_cnode_cap (free_index_update (\<lambda>_. ?y232 a aa b caps slots n mi rv () x) xa)) and ex_cte_cap_wp_to is_cnode_cap x) s))
 2. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q246 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>cap' s. (vo \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s) \<and> (cap' \<noteq> NullCap \<longrightarrow> ?QM254 a aa b caps slots n mi s cap')\<rbrace>, -
 3. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ((\<lambda>s. \<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) (aa, b) s \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) 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> True) and ?Q246 a aa b caps slots n mi) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (4 subgoals):
 1. \<And>a aa b caps slots n mi rv s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []; vo \<longrightarrow> cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s; rv \<noteq> NullCap; cte_wp_at ((=) NullCap) (hd slots) s; ?QM254 a aa b caps slots n mi s rv\<rbrakk> \<Longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb 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 b) aa s) \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap rv) (hd slots) s) \<and> (vo \<longrightarrow> 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> (aa, b) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). x \<noteq> hd slots \<and> (x \<noteq> hd slots \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. masked_as_full c rv = NullCap) x s \<and> real_cte_at x s)) \<and> (\<forall>x\<in>set caps. (snd x = hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> (fst x \<noteq> NullCap \<longrightarrow> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x)) \<and> real_cte_at (hd slots) s) \<and> (snd x \<noteq> hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s))) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). ex_cte_cap_wp_to is_cnode_cap x s))
 2. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q246 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>cap' s. (vo \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s) \<and> (cap' \<noteq> NullCap \<longrightarrow> ?QM254 a aa b caps slots n mi s cap')\<rbrace>, -
 3. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ((\<lambda>s. \<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) (aa, b) s \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) 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> True) and ?Q246 a aa b caps slots n mi) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q246 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>cap' s. (vo \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s) \<and> (cap' \<noteq> NullCap \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb 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 b) aa s) \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap') (hd slots) s) \<and> (vo \<longrightarrow> 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> (aa, b) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). x \<noteq> hd slots \<and> (x \<noteq> hd slots \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. masked_as_full c cap' = NullCap) x s \<and> real_cte_at x s)) \<and> (\<forall>x\<in>set caps. (snd x = hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> (fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> real_cte_at (hd slots) s) \<and> (snd x \<noteq> hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> 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> real_cte_at (snd x) s))) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). ex_cte_cap_wp_to is_cnode_cap x s)))\<rbrace>, -
 2. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ((\<lambda>s. \<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) (aa, b) s \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) 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> True) and ?Q246 a aa b caps slots n mi) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (4 subgoals):
 1. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P288 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>rv s. vo \<longrightarrow> rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s\<rbrace>, -
 2. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q288 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb 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 b) aa s) \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap rv) (hd slots) s) \<and> (vo \<longrightarrow> 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> (aa, b) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). x \<noteq> hd slots \<and> (x \<noteq> hd slots \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. masked_as_full c rv = NullCap) x s \<and> real_cte_at x s)) \<and> (\<forall>x\<in>set caps. (snd x = hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> (fst x \<noteq> NullCap \<longrightarrow> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x)) \<and> real_cte_at (hd slots) s) \<and> (snd x \<noteq> hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s))) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace>, -
 3. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ((\<lambda>s. \<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) (aa, b) s \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) 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> True) and (?P288 a aa b caps slots n mi and ?Q288 a aa b caps slots n mi)) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (4 subgoals):
 1. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []; vo\<rbrakk> \<Longrightarrow> \<lbrace>?Q291 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (aa, b) rv) (aa, b) s\<rbrace>, -
 2. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q288 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb 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 b) aa s) \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap rv) (hd slots) s) \<and> (vo \<longrightarrow> 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> (aa, b) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). x \<noteq> hd slots \<and> (x \<noteq> hd slots \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. masked_as_full c rv = NullCap) x s \<and> real_cte_at x s)) \<and> (\<forall>x\<in>set caps. (snd x = hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> (fst x \<noteq> NullCap \<longrightarrow> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x)) \<and> real_cte_at (hd slots) s) \<and> (snd x \<noteq> hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s))) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace>, -
 3. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ((\<lambda>s. \<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) (aa, b) s \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) 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> True) and ((\<lambda>s. vo \<longrightarrow> ?Q291 a aa b caps slots n mi s) and ?Q288 a aa b caps slots n mi)) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q288 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb 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 b) aa s) \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap rv) (hd slots) s) \<and> (vo \<longrightarrow> 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> (aa, b) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). x \<noteq> hd slots \<and> (x \<noteq> hd slots \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. masked_as_full c rv = NullCap) x s \<and> real_cte_at x s)) \<and> (\<forall>x\<in>set caps. (snd x = hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> (fst x \<noteq> NullCap \<longrightarrow> rv \<noteq> fst x \<longrightarrow> rv = masked_as_full (fst x) (fst x)) \<and> real_cte_at (hd slots) s) \<and> (snd x \<noteq> hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> masked_as_full c rv \<noteq> fst x \<longrightarrow> masked_as_full c rv = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s))) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace>, -
 2. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R76 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ((\<lambda>s. \<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) (aa, b) s \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) 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> True) and ((\<lambda>s. vo \<longrightarrow> 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) (aa, b) s \<and> valid_objs s) and ?Q288 a aa b caps slots n mi)) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R76 a aa b caps slots n mi s)) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<longrightarrow> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> P s \<and> ((\<lambda>s. \<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) (aa, b) s \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) 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> True) and ((\<lambda>s. vo \<longrightarrow> 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) (aa, b) s \<and> valid_objs s) and (\<lambda>s. \<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) (aa, b) s \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) 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' \<noteq> NullCap \<longrightarrow> P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb 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 b) aa s) \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap') (hd slots) s) \<and> (vo \<longrightarrow> 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> (aa, b) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). x \<noteq> hd slots \<and> (x \<noteq> hd slots \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. masked_as_full c cap' = NullCap) x s \<and> real_cte_at x s)) \<and> (\<forall>x\<in>set caps. (snd x = hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> (fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> real_cte_at (hd slots) s) \<and> (snd x \<noteq> hd slots \<longrightarrow> s \<turnstile> fst x \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> 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> real_cte_at (snd x) s))) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). ex_cte_cap_wp_to is_cnode_cap x s))))) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> P s)) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b caps slots s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))) \<and> real_cte_at (snd x) s)) \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> s \<turnstile> a \<and> (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a)) \<and> cap_table_at (length b) aa s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))) \<and> real_cte_at (snd x) s); ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> (vo \<longrightarrow> a \<noteq> NullCap \<longrightarrow> (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> 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'. ((\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> 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> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> (\<exists>cap. caps_of_state s (aa, b) = Some cap)) \<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' \<noteq> NullCap \<longrightarrow> (vo \<longrightarrow> (aa, b) \<noteq> hd slots \<and> distinct (tl slots) \<and> (\<forall>x\<in>set (tl slots). x \<noteq> hd slots \<and> (x \<noteq> hd slots \<longrightarrow> (\<exists>cap. caps_of_state s x = Some cap \<and> masked_as_full cap cap' = NullCap) \<and> real_cte_at x s)) \<and> (\<forall>x\<in>set caps. (snd x = hd slots \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> 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 \<longrightarrow> masked_as_full cap cap' \<noteq> fst x \<longrightarrow> masked_as_full cap cap' = masked_as_full (fst x) (fst x)))))) \<and> (ex \<longrightarrow> (\<forall>x\<in>set (tl slots). ex_cte_cap_wp_to is_cnode_cap x s))) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b caps s ab ba ys. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> (vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct ys \<and> s \<turnstile> a \<and> cap_table_at (length b) aa s \<and> cap_table_at (length ba) ab s \<and> (ab, ba) \<notin> set ys \<and> caps_of_state s (ab, ba) = Some NullCap \<and> (\<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a)) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))); ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a)\<rbrakk> \<Longrightarrow> (vo \<longrightarrow> a \<noteq> NullCap \<longrightarrow> (\<exists>cap. vs_cap_ref cap = vs_cap_ref a \<and> cap_asid cap = cap_asid a \<and> cap_master_cap cap = cap_master_cap a \<and> caps_of_state s (aa, b) = Some cap \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False)) \<and> (\<forall>cap'. (s \<turnstile> a \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> \<not> is_zombie a \<and> a \<noteq> IRQControlCap \<and> a \<noteq> NullCap) \<and> (valid_objs s \<and> cap' \<noteq> NullCap \<and> (\<exists>cap. vs_cap_ref cap = vs_cap_ref a \<and> cap_asid cap = cap_asid a \<and> cap_master_cap cap = cap_master_cap a \<and> caps_of_state s (aa, b) = Some cap \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, b) = Some cap)) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> vo \<longrightarrow> (b = ba \<longrightarrow> aa \<noteq> ab) \<and> (\<forall>x\<in>set ys. x \<noteq> (ab, ba)) \<and> (\<forall>x\<in>set caps. (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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 aa b caps s ab ba ys. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> (vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct ys \<and> s \<turnstile> a \<and> cap_table_at (length b) aa s \<and> cap_table_at (length ba) ab s \<and> (ab, ba) \<notin> set ys \<and> caps_of_state s (ab, ba) = Some NullCap \<and> (\<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a)) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))); ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a)\<rbrakk> \<Longrightarrow> vo \<longrightarrow> a \<noteq> NullCap \<longrightarrow> (\<exists>cap. vs_cap_ref cap = vs_cap_ref a \<and> cap_asid cap = cap_asid a \<and> cap_master_cap cap = cap_master_cap a \<and> caps_of_state s (aa, b) = Some cap \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False)
 2. \<And>a aa b caps s ab ba ys. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> (vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct ys \<and> s \<turnstile> a \<and> cap_table_at (length b) aa s \<and> cap_table_at (length ba) ab s \<and> (ab, ba) \<notin> set ys \<and> caps_of_state s (ab, ba) = Some NullCap \<and> (\<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a)) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))); ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a)\<rbrakk> \<Longrightarrow> \<forall>cap'. (s \<turnstile> a \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> \<not> is_zombie a \<and> a \<noteq> IRQControlCap \<and> a \<noteq> NullCap) \<and> (valid_objs s \<and> cap' \<noteq> NullCap \<and> (\<exists>cap. vs_cap_ref cap = vs_cap_ref a \<and> cap_asid cap = cap_asid a \<and> cap_master_cap cap = cap_master_cap a \<and> caps_of_state s (aa, b) = Some cap \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, b) = Some cap)) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> vo \<longrightarrow> (b = ba \<longrightarrow> aa \<noteq> ab) \<and> (\<forall>x\<in>set ys. x \<noteq> (ab, ba)) \<and> (\<forall>x\<in>set caps. (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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 aa b caps s ab ba ys cap. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); vo; a \<noteq> NullCap; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; \<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (aa, b) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a\<rbrakk> \<Longrightarrow> vs_cap_ref cap = vs_cap_ref a \<and> cap_asid cap = cap_asid a \<and> cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False
 2. \<And>a aa b caps s ab ba ys. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> (vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct ys \<and> s \<turnstile> a \<and> cap_table_at (length b) aa s \<and> cap_table_at (length ba) ab s \<and> (ab, ba) \<notin> set ys \<and> caps_of_state s (ab, ba) = Some NullCap \<and> (\<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a)) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))); ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a)\<rbrakk> \<Longrightarrow> \<forall>cap'. (s \<turnstile> a \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> \<not> is_zombie a \<and> a \<noteq> IRQControlCap \<and> a \<noteq> NullCap) \<and> (valid_objs s \<and> cap' \<noteq> NullCap \<and> (\<exists>cap. vs_cap_ref cap = vs_cap_ref a \<and> cap_asid cap = cap_asid a \<and> cap_master_cap cap = cap_master_cap a \<and> caps_of_state s (aa, b) = Some cap \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, b) = Some cap)) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> vo \<longrightarrow> (b = ba \<longrightarrow> aa \<noteq> ab) \<and> (\<forall>x\<in>set ys. x \<noteq> (ab, ba)) \<and> (\<forall>x\<in>set caps. (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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 aa b caps s ab ba ys cap. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); vo; a \<noteq> NullCap; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; \<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (aa, b) = Some cap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; cap \<noteq> a\<rbrakk> \<Longrightarrow> vs_cap_ref cap = vs_cap_ref a \<and> cap_asid cap = cap_asid a \<and> cap_master_cap cap = cap_master_cap a \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False
 2. \<And>a aa b caps s ab ba ys. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> (vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct ys \<and> s \<turnstile> a \<and> cap_table_at (length b) aa s \<and> cap_table_at (length ba) ab s \<and> (ab, ba) \<notin> set ys \<and> caps_of_state s (ab, ba) = Some NullCap \<and> (\<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a)) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))); ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a)\<rbrakk> \<Longrightarrow> \<forall>cap'. (s \<turnstile> a \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> \<not> is_zombie a \<and> a \<noteq> IRQControlCap \<and> a \<noteq> NullCap) \<and> (valid_objs s \<and> cap' \<noteq> NullCap \<and> (\<exists>cap. vs_cap_ref cap = vs_cap_ref a \<and> cap_asid cap = cap_asid a \<and> cap_master_cap cap = cap_master_cap a \<and> caps_of_state s (aa, b) = Some cap \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, b) = Some cap)) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> vo \<longrightarrow> (b = ba \<longrightarrow> aa \<noteq> ab) \<and> (\<forall>x\<in>set ys. x \<noteq> (ab, ba)) \<and> (\<forall>x\<in>set caps. (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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>aa b caps s ab ba ys dev r bits f. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> 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 n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> UntypedCap dev r bits f; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; \<forall>x\<in>set caps. 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 \<longrightarrow> 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 (aa, b) = Some (UntypedCap dev r bits (max_free_index bits)); 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 aa b caps s ab ba ys. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> (vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct ys \<and> s \<turnstile> a \<and> cap_table_at (length b) aa s \<and> cap_table_at (length ba) ab s \<and> (ab, ba) \<notin> set ys \<and> caps_of_state s (ab, ba) = Some NullCap \<and> (\<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a)) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))); ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a)\<rbrakk> \<Longrightarrow> \<forall>cap'. (s \<turnstile> a \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> \<not> is_zombie a \<and> a \<noteq> IRQControlCap \<and> a \<noteq> NullCap) \<and> (valid_objs s \<and> cap' \<noteq> NullCap \<and> (\<exists>cap. vs_cap_ref cap = vs_cap_ref a \<and> cap_asid cap = cap_asid a \<and> cap_master_cap cap = cap_master_cap a \<and> caps_of_state s (aa, b) = Some cap \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, b) = Some cap)) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> vo \<longrightarrow> (b = ba \<longrightarrow> aa \<noteq> ab) \<and> (\<forall>x\<in>set ys. x \<noteq> (ab, ba)) \<and> (\<forall>x\<in>set caps. (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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 aa b caps s ab ba ys. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> (vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; vo \<longrightarrow> valid_mdb s \<and> valid_objs s \<and> distinct ys \<and> s \<turnstile> a \<and> cap_table_at (length b) aa s \<and> cap_table_at (length ba) ab s \<and> (ab, ba) \<notin> set ys \<and> caps_of_state s (ab, ba) = Some NullCap \<and> (\<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a)) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))); ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a)\<rbrakk> \<Longrightarrow> \<forall>cap'. (s \<turnstile> a \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> \<not> is_zombie a \<and> a \<noteq> IRQControlCap \<and> a \<noteq> NullCap) \<and> (valid_objs s \<and> cap' \<noteq> NullCap \<and> (\<exists>cap. vs_cap_ref cap = vs_cap_ref a \<and> cap_asid cap = cap_asid a \<and> cap_master_cap cap = cap_master_cap a \<and> caps_of_state s (aa, b) = Some cap \<and> (cap_badge cap, cap_badge a) \<in> capBadge_ordering False) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, b) = Some cap)) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> vo \<longrightarrow> (b = ba \<longrightarrow> aa \<noteq> ab) \<and> (\<forall>x\<in>set ys. x \<noteq> (ab, ba)) \<and> (\<forall>x\<in>set caps. (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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 aa b caps s ab ba ys cap' cap. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; \<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a\<rbrakk> \<Longrightarrow> (b = ba \<longrightarrow> aa \<noteq> ab) \<and> (\<forall>x\<in>set ys. x \<noteq> (ab, ba)) \<and> (\<forall>x\<in>set caps. (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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 aa b caps s ab ba ys cap' cap. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; \<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a\<rbrakk> \<Longrightarrow> b = ba \<longrightarrow> aa \<noteq> ab
 2. \<And>a aa b caps s ab ba ys cap' cap. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; \<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ys. x \<noteq> (ab, ba)
 3. \<And>a aa b caps s ab ba ys cap' cap. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; \<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a\<rbrakk> \<Longrightarrow> \<forall>x\<in>set caps. (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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 aa b caps s ab ba ys cap' cap. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; \<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ys. x \<noteq> (ab, ba)
 2. \<And>a aa b caps s ab ba ys cap' cap. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; \<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a\<rbrakk> \<Longrightarrow> \<forall>x\<in>set caps. (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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 aa b caps s ab ba ys cap' cap. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; \<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a\<rbrakk> \<Longrightarrow> \<forall>x\<in>set caps. (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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 aa b caps s ab ba ys cap' cap x. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; \<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))); caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; x \<in> set caps\<rbrakk> \<Longrightarrow> (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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 aa b caps s ab ba ys cap' cap x. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; x \<in> set caps; 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x)))\<rbrakk> \<Longrightarrow> (snd x = (ab, ba) \<longrightarrow> fst x \<noteq> NullCap \<longrightarrow> cap' \<noteq> fst x \<longrightarrow> cap' = masked_as_full (fst x) (fst x)) \<and> (snd x \<noteq> (ab, ba) \<longrightarrow> (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> 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 aa b caps s ab ba ys cap' cap ac ad bb capa. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; (ac, ad, bb) \<in> set caps; s \<turnstile> ac; cap_table_at (length bb) ad s; caps_of_state s (ad, bb) = Some capa; ac \<noteq> NullCap \<longrightarrow> capa \<noteq> ac \<longrightarrow> capa = masked_as_full ac ac\<rbrakk> \<Longrightarrow> (ad = ab \<and> bb = ba \<longrightarrow> ac \<noteq> NullCap \<longrightarrow> cap' \<noteq> ac \<longrightarrow> cap' = masked_as_full ac ac) \<and> ((ad = ab \<longrightarrow> bb \<noteq> ba) \<longrightarrow> ac \<noteq> NullCap \<longrightarrow> masked_as_full capa cap' \<noteq> ac \<longrightarrow> masked_as_full capa cap' = masked_as_full ac ac) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b caps s ab ba ys cap' cap ac ad bb capa. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; (ac, ad, bb) \<in> set caps; s \<turnstile> ac; cap_table_at (length bb) ad s; caps_of_state s (ad, bb) = Some capa; ac \<noteq> NullCap \<longrightarrow> capa \<noteq> ac \<longrightarrow> capa = masked_as_full ac ac\<rbrakk> \<Longrightarrow> ad = ab \<and> bb = ba \<longrightarrow> ac \<noteq> NullCap \<longrightarrow> cap' \<noteq> ac \<longrightarrow> cap' = masked_as_full ac ac
 2. \<And>a aa b caps s ab ba ys cap' cap ac ad bb capa. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; (ac, ad, bb) \<in> set caps; s \<turnstile> ac; cap_table_at (length bb) ad s; caps_of_state s (ad, bb) = Some capa; ac \<noteq> NullCap \<longrightarrow> capa \<noteq> ac \<longrightarrow> capa = masked_as_full ac ac\<rbrakk> \<Longrightarrow> (ad = ab \<longrightarrow> bb \<noteq> ba) \<longrightarrow> ac \<noteq> NullCap \<longrightarrow> masked_as_full capa cap' \<noteq> ac \<longrightarrow> masked_as_full capa cap' = masked_as_full ac ac proof (prove)
goal (1 subgoal):
 1. \<And>a aa b caps s ab ba ys cap' cap ac ad bb capa. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; (ac, ad, bb) \<in> set caps; s \<turnstile> ac; cap_table_at (length bb) ad s; caps_of_state s (ad, bb) = Some capa; ad = ab \<longrightarrow> bb \<noteq> ba; ac \<noteq> NullCap; masked_as_full capa cap' \<noteq> ac; capa \<noteq> ac \<longrightarrow> capa = masked_as_full ac ac\<rbrakk> \<Longrightarrow> masked_as_full capa cap' = masked_as_full ac ac proof (prove)
goal (2 subgoals):
 1. \<And>a aa b caps s ab ba ys cap' cap ac ad bb capa. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; (ac, ad, bb) \<in> set caps; s \<turnstile> ac; cap_table_at (length bb) ad s; caps_of_state s (ad, bb) = Some capa; ad = ab \<longrightarrow> bb \<noteq> ba; ac \<noteq> NullCap; masked_as_full capa cap' \<noteq> ac; capa \<noteq> ac \<longrightarrow> capa = masked_as_full ac ac; capa = ac\<rbrakk> \<Longrightarrow> masked_as_full capa cap' = masked_as_full ac ac
 2. \<And>a aa b caps s ab ba ys cap' cap ac ad bb capa. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (ex \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) \<and> valid_mdb s \<and> valid_objs s \<and> distinct slots \<and> (\<forall>x\<in>set slots. caps_of_state s x = Some NullCap \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. 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 \<longrightarrow> cap \<noteq> fst x \<longrightarrow> cap = masked_as_full (fst x) (fst x))))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s; ex \<longrightarrow> ex_cte_cap_wp_to is_cnode_cap (ab, ba) s \<and> (\<forall>x\<in>set ys. ex_cte_cap_wp_to is_cnode_cap x s); is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); cap' \<noteq> NullCap; vo; valid_mdb s; valid_objs s; distinct ys; s \<turnstile> a; cap_table_at (length b) aa s; cap_table_at (length ba) ab s; (ab, ba) \<notin> set ys; caps_of_state s (ab, ba) = Some NullCap; \<forall>x\<in>set ys. caps_of_state s x = Some NullCap \<and> real_cte_at x s; caps_of_state s (aa, b) = Some cap; s \<turnstile> cap'; \<not> is_zombie a; a \<noteq> IRQControlCap; a \<noteq> NullCap; cap \<noteq> a \<longrightarrow> cap = masked_as_full a a; (ac, ad, bb) \<in> set caps; s \<turnstile> ac; cap_table_at (length bb) ad s; caps_of_state s (ad, bb) = Some capa; ad = ab \<longrightarrow> bb \<noteq> ba; ac \<noteq> NullCap; masked_as_full capa cap' \<noteq> ac; capa \<noteq> ac \<longrightarrow> capa = masked_as_full ac ac; capa \<noteq> ac\<rbrakk> \<Longrightarrow> masked_as_full capa cap' = masked_as_full ac ac proof (prove)
goal:
No subgoals!