theory Ipc_IF

lemma transfer_caps_loop_reads_respects':
  "reads_respects aag l
     (pas_refined aag and pspace_aligned and valid_vspace_objs and
      valid_arch_state and valid_mdb and valid_objs and
      (\<lambda>s. (\<forall>cap\<in>set caps. valid_cap (fst cap) s
                         \<and> is_subject aag (fst (snd cap))
                         \<and> pas_cap_cur_auth aag (fst cap)
                         \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap
                                           \<longrightarrow> cp \<noteq> fst cap
                                           \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s)
         \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)
                           \<and> cte_wp_at ((=) NullCap) slot s
                           \<and> real_cte_at slot s)
         \<and> distinct slots))
     (transfer_caps_loop ep rcv_buffer n caps slots mi)" apply (induct caps arbitrary: slots n mi) apply simp apply (rule return_ev_pre) apply (case_tac a, rename_tac cap obj ind) apply (simp split del: if_split) apply (rule equiv_valid_guard_imp) apply (wp const_on_failure_ev | simp | intro conjI impI)+ apply fast apply (wp set_extra_badge_reads_respects hoare_vcg_ball_lift | simp)+ apply fast apply (wp cap_insert_reads_respects cap_insert_pas_refined whenE_throwError_wp
                   derive_cap_rev derive_cap_cap_cur_auth derive_cap_is_derived
                   hoare_vcg_ball_lift cap_insert_cte_wp_at
                | simp split del: if_split)+ apply (rule_tac Q'="\<lambda>capd s. (capd \<noteq> NullCap
                                  \<longrightarrow> cte_wp_at (is_derived (cdt s) (obj,ind) capd) (obj, ind) s)
                               \<and> (capd \<noteq> NullCap \<longrightarrow> QM s capd)" for QM
                 in hoare_post_imp_R) prefer 2 apply (clarsimp simp: cte_wp_at_caps_of_state split del: if_split) apply (strengthen is_derived_is_transferable[mk_strg I' O], assumption, solves\<open>simp\<close>) apply (rule hoare_vcg_conj_liftE_R) apply (rule derive_cap_is_derived) apply (wp derive_cap_is_derived_foo') apply wp apply (clarsimp simp: remove_rights_cur_auth cte_wp_at_caps_of_state split del: if_split) apply (rename_tac actual_cap) apply (strengthen real_cte_tcb_valid) apply (clarsimp) apply (intro conjI) subgoal by (fastforce simp: masked_as_full_def is_cap_simps cap_master_cap_simps split: if_splits) apply clarsimp apply (intro conjI) apply (fastforce dest: auth_derived_pas_cur_auth) apply fastforce subgoal apply (erule ball_subsetE, fastforce) by (fastforce simp: cte_wp_at_caps_of_state masked_as_full_def is_cap_simps split: if_splits) subgoal by (fastforce simp: neq_Nil_conv cte_wp_at_caps_of_state) by (rule distinct_tl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi) proof (prove)
goal (2 subgoals):
 1. \<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set []. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n [] slots mi)
 2. \<And>a caps slots n mi. (\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi)) \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set (a # caps). s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n (a # caps) slots mi) proof (prove)
goal (2 subgoals):
 1. \<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (return (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 2. \<And>a caps slots n mi. (\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi)) \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set (a # caps). s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n (a # caps) slots mi) proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi)) \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set (a # caps). s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n (a # caps) slots mi) proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind)\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set (a # caps). s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n (a # caps) slots mi) proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind)\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (if is_ep_cap cap \<and> ep = Some (obj_ref_of cap) then doE liftE $ set_extra_badge rcv_buffer (cap_ep_badge cap) n;
liftE $ transfer_caps_loop ep rcv_buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || (1 << n)) (mi_label mi))
odE else if slots \<noteq> [] then doE cap' <- derive_cap (obj, ind) cap;
whenE (cap' = NullCap) $ throwError undefined;
liftE $ cap_insert cap' (obj, ind) (hd slots);
liftE $ transfer_caps_loop ep rcv_buffer (Suc n) caps (tl slots) mi
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))) proof (prove)
goal (2 subgoals):
 1. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind)\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q9 a caps slots n mi cap obj ind) (const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (if is_ep_cap cap \<and> ep = Some (obj_ref_of cap) then doE liftE $ set_extra_badge rcv_buffer (cap_ep_badge cap) n;
liftE $ transfer_caps_loop ep rcv_buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || (1 << n)) (mi_label mi))
odE else if slots \<noteq> [] then doE cap' <- derive_cap (obj, ind) cap;
whenE (cap' = NullCap) $ throwError undefined;
liftE $ cap_insert cap' (obj, ind) (hd slots);
liftE $ transfer_caps_loop ep rcv_buffer (Suc n) caps (tl slots) mi
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))))
 2. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> ?Q9 a caps slots n mi cap obj ind s proof (prove)
goal (5 subgoals):
 1. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop (Some (obj_ref_of cap)) rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<and> ep = Some (obj_ref_of cap)\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q15 (cap, obj, ind) caps slots n mi cap obj ind ()) (transfer_caps_loop (Some (obj_ref_of cap)) rcv_buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
 2. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<and> ep = Some (obj_ref_of cap)\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'15 a caps slots n mi cap obj ind) (liftE $ set_extra_badge rcv_buffer (cap_ep_badge cap) n)
 3. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<and> ep = Some (obj_ref_of cap)\<rbrakk> \<Longrightarrow> \<lbrace>?P''15 a caps slots n mi cap obj ind\<rbrace> liftE $ set_extra_badge rcv_buffer (cap_ep_badge cap) n \<lbrace>?Q15 a caps slots n mi cap obj ind\<rbrace>, -
 4. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap))\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q14 a caps slots n mi cap obj ind) (if slots \<noteq> [] then doE cap' <- derive_cap (obj, ind) cap;
whenE (cap' = NullCap) $ throwError undefined;
liftE $ cap_insert cap' (obj, ind) (hd slots);
liftE $ transfer_caps_loop ep rcv_buffer (Suc n) caps (tl slots) mi
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 5. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> ?P'15 a caps slots n mi cap obj ind s \<and> ?P''15 a caps slots n mi cap obj ind s) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> ?Q14 a caps slots n mi cap obj ind s) proof (prove)
goal (4 subgoals):
 1. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<and> ep = Some (obj_ref_of cap)\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'15 a caps slots n mi cap obj ind) (liftE $ set_extra_badge rcv_buffer (cap_ep_badge cap) n)
 2. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<and> ep = Some (obj_ref_of cap)\<rbrakk> \<Longrightarrow> \<lbrace>?P''15 a caps slots n mi cap obj ind\<rbrace> liftE $ set_extra_badge rcv_buffer (cap_ep_badge cap) n \<lbrace>\<lambda>a. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)\<rbrace>, -
 3. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap))\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q14 a caps slots n mi cap obj ind) (if slots \<noteq> [] then doE cap' <- derive_cap (obj, ind) cap;
whenE (cap' = NullCap) $ throwError undefined;
liftE $ cap_insert cap' (obj, ind) (hd slots);
liftE $ transfer_caps_loop ep rcv_buffer (Suc n) caps (tl slots) mi
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 4. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> ?P'15 a caps slots n mi cap obj ind s \<and> ?P''15 a caps slots n mi cap obj ind s) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> ?Q14 a caps slots n mi cap obj ind s) proof (prove)
goal (9 subgoals):
 1. \<And>a caps slots n mi cap obj ind rv. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q85 (cap, obj, ind) caps slots n mi cap obj ind rv () ()) (transfer_caps_loop ep rcv_buffer (Suc n) caps (tl slots) mi)
 2. \<And>a caps slots n mi cap obj ind rv rva. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'85 a caps slots n mi cap obj ind rv rva) (liftE $ cap_insert rv (obj, ind) (hd slots))
 3. \<And>a caps slots n mi cap obj ind rv rva. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P''85 a caps slots n mi cap obj ind rv rva\<rbrace> liftE $ cap_insert rv (obj, ind) (hd slots) \<lbrace>?Q85 a caps slots n mi cap obj ind rv rva\<rbrace>, -
 4. \<And>a caps slots n mi cap obj ind rv. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'83 a caps slots n mi cap obj ind rv) (whenE (rv = NullCap) $ throwError undefined)
 5. \<And>a caps slots n mi cap obj ind rv. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P''83 a caps slots n mi cap obj ind rv\<rbrace> whenE (rv = NullCap) $ throwError undefined \<lbrace>\<lambda>rva s. ?P'85 a caps slots n mi cap obj ind rv rva s \<and> ?P''85 a caps slots n mi cap obj ind rv rva s\<rbrace>, -
 6. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'82 a caps slots n mi cap obj ind) (derive_cap (obj, ind) cap)
 7. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P''82 a caps slots n mi cap obj ind\<rbrace> derive_cap (obj, ind) cap \<lbrace>\<lambda>rv s. ?P'83 a caps slots n mi cap obj ind rv s \<and> ?P''83 a caps slots n mi cap obj ind rv s\<rbrace>, -
 8. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q81 a caps slots n mi cap obj ind) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 9. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> True \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (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> (\<forall>x\<in>set slots. is_subject aag (fst x) \<and> cte_wp_at ((=) NullCap) x s \<and> real_cte_at x s) \<and> distinct slots) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?P'82 a caps slots n mi cap obj ind s \<and> ?P''82 a caps slots n mi cap obj ind s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?Q81 a caps slots n mi cap obj ind s)) proof (prove)
goal (8 subgoals):
 1. \<And>a caps slots n mi cap obj ind rv rva. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'85 a caps slots n mi cap obj ind rv rva) (liftE $ cap_insert rv (obj, ind) (hd slots))
 2. \<And>a caps slots n mi cap obj ind rv rva. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P''85 a caps slots n mi cap obj ind rv rva\<rbrace> liftE $ cap_insert rv (obj, ind) (hd slots) \<lbrace>\<lambda>a. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set (tl slots). is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct (tl slots))\<rbrace>, -
 3. \<And>a caps slots n mi cap obj ind rv. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'83 a caps slots n mi cap obj ind rv) (whenE (rv = NullCap) $ throwError undefined)
 4. \<And>a caps slots n mi cap obj ind rv. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P''83 a caps slots n mi cap obj ind rv\<rbrace> whenE (rv = NullCap) $ throwError undefined \<lbrace>\<lambda>rva s. ?P'85 a caps slots n mi cap obj ind rv rva s \<and> ?P''85 a caps slots n mi cap obj ind rv rva s\<rbrace>, -
 5. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'82 a caps slots n mi cap obj ind) (derive_cap (obj, ind) cap)
 6. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P''82 a caps slots n mi cap obj ind\<rbrace> derive_cap (obj, ind) cap \<lbrace>\<lambda>rv s. ?P'83 a caps slots n mi cap obj ind rv s \<and> ?P''83 a caps slots n mi cap obj ind rv s\<rbrace>, -
 7. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q81 a caps slots n mi cap obj ind) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 8. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> True \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (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> (\<forall>x\<in>set slots. is_subject aag (fst x) \<and> cte_wp_at ((=) NullCap) x s \<and> real_cte_at x s) \<and> distinct slots) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?P'82 a caps slots n mi cap obj ind s \<and> ?P''82 a caps slots n mi cap obj ind s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?Q81 a caps slots n mi cap obj ind s)) proof (prove)
goal (3 subgoals):
 1. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'183 (cap, obj, ind) caps slots n mi cap obj ind\<rbrace> derive_cap (obj, ind) cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (is_transferable_in (obj, ind) s \<and> \<not> Option.is_none (cdt s (obj, ind)) \<longrightarrow> is_transferable_cap rv) \<and> is_subject aag (fst (hd slots)) \<and> is_subject aag obj \<and> pas_cap_cur_auth aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> s \<turnstile> rv \<and> valid_objs s \<and> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) s \<and> (obj, ind) \<noteq> hd slots \<and> valid_objs s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<and> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) 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> (\<forall>x\<in>set (tl slots). is_subject aag (fst x) \<and> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) s \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then NullCap = rv else cte_wp_at (\<lambda>c. NullCap = masked_as_full c rv) x s) \<and> real_cte_at x s) \<and> distinct (tl slots)\<rbrace>, -
 2. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q81 a caps slots n mi cap obj ind) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 3. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> True \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (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> (\<forall>x\<in>set slots. is_subject aag (fst x) \<and> cte_wp_at ((=) NullCap) x s \<and> real_cte_at x s) \<and> distinct slots) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> (pas_refined aag s \<and> is_subject aag (fst (obj, ind))) \<and> aag_can_read aag obj \<and> aag_can_read aag (fst (hd slots)) \<and> ?P'183 a caps slots n mi cap obj ind s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?Q81 a caps slots n mi cap obj ind s)) proof (prove)
goal (4 subgoals):
 1. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'183 (cap, obj, ind) caps slots n mi cap obj ind\<rbrace> derive_cap (obj, ind) cap \<lbrace>\<lambda>capd s. (capd \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (obj, ind) capd) (obj, ind) s) \<and> (capd \<noteq> NullCap \<longrightarrow> ?QM193 a caps slots n mi cap obj ind s capd)\<rbrace>, -
 2. \<And>a caps slots n mi cap obj ind rv s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; (rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?QM193 a caps slots n mi cap obj ind s rv)\<rbrakk> \<Longrightarrow> rv \<noteq> NullCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (is_transferable_in (obj, ind) s \<and> \<not> Option.is_none (cdt s (obj, ind)) \<longrightarrow> is_transferable_cap rv) \<and> is_subject aag (fst (hd slots)) \<and> is_subject aag obj \<and> pas_cap_cur_auth aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> s \<turnstile> rv \<and> valid_objs s \<and> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) s \<and> (obj, ind) \<noteq> hd slots \<and> valid_objs s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<and> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) 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> (\<forall>x\<in>set (tl slots). is_subject aag (fst x) \<and> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) s \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then NullCap = rv else cte_wp_at (\<lambda>c. NullCap = masked_as_full c rv) x s) \<and> real_cte_at x s) \<and> distinct (tl slots)
 3. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q81 a caps slots n mi cap obj ind) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 4. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> True \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (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> (\<forall>x\<in>set slots. is_subject aag (fst x) \<and> cte_wp_at ((=) NullCap) x s \<and> real_cte_at x s) \<and> distinct slots) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> (pas_refined aag s \<and> is_subject aag (fst (obj, ind))) \<and> aag_can_read aag obj \<and> aag_can_read aag (fst (hd slots)) \<and> ?P'183 a caps slots n mi cap obj ind s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?Q81 a caps slots n mi cap obj ind s)) proof (prove)
goal (4 subgoals):
 1. \<And>a caps slots n mi cap obj ind rv s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; (rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?QM193 a caps slots n mi cap obj ind s rv)\<rbrakk> \<Longrightarrow> rv \<noteq> NullCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (is_transferable_in (obj, ind) s \<and> \<not> Option.is_none (cdt s (obj, ind)) \<longrightarrow> is_transferable_cap rv) \<and> is_subject aag (fst (hd slots)) \<and> is_subject aag obj \<and> pas_cap_cur_auth aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> s \<turnstile> rv \<and> valid_objs s \<and> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) s \<and> (obj, ind) \<noteq> hd slots \<and> valid_objs s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<and> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) 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> (\<forall>x\<in>set (tl slots). is_subject aag (fst x) \<and> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) s \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then NullCap = rv else cte_wp_at (\<lambda>c. NullCap = masked_as_full c rv) x s) \<and> real_cte_at x s) \<and> distinct (tl slots)
 2. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'183 (cap, obj, ind) caps slots n mi cap obj ind\<rbrace> derive_cap (obj, ind) cap \<lbrace>\<lambda>capd s. (capd \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (obj, ind) capd) (obj, ind) s) \<and> (capd \<noteq> NullCap \<longrightarrow> ?QM193 a caps slots n mi cap obj ind s capd)\<rbrace>, -
 3. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q81 a caps slots n mi cap obj ind) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 4. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> True \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (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> (\<forall>x\<in>set slots. is_subject aag (fst x) \<and> cte_wp_at ((=) NullCap) x s \<and> real_cte_at x s) \<and> distinct slots) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> (pas_refined aag s \<and> is_subject aag (fst (obj, ind))) \<and> aag_can_read aag obj \<and> aag_can_read aag (fst (hd slots)) \<and> ?P'183 a caps slots n mi cap obj ind s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?Q81 a caps slots n mi cap obj ind s)) proof (prove)
goal (4 subgoals):
 1. \<And>caps slots n mi cap obj ind rv s capa. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; ?QM193 (cap, obj, ind) caps slots n mi cap obj ind s rv; rv \<noteq> NullCap; caps_of_state s (obj, ind) = Some capa; is_derived (cdt s) (obj, ind) rv capa\<rbrakk> \<Longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (is_transferable_cap capa \<and> \<not> Option.is_none (cdt s (obj, ind)) \<longrightarrow> is_transferable_cap rv) \<and> is_subject aag (fst (hd slots)) \<and> is_subject aag obj \<and> pas_cap_cur_auth aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> s \<turnstile> rv \<and> valid_objs s \<and> (obj, ind) \<noteq> hd slots \<and> valid_objs s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<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> (\<forall>x\<in>set (tl slots). is_subject aag (fst x) \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then NullCap = rv else cte_wp_at (\<lambda>c. NullCap = masked_as_full c rv) x s) \<and> real_cte_at x s) \<and> distinct (tl slots)
 2. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'183 (cap, obj, ind) caps slots n mi cap obj ind\<rbrace> derive_cap (obj, ind) cap \<lbrace>\<lambda>capd s. (capd \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (obj, ind) capd) (obj, ind) s) \<and> (capd \<noteq> NullCap \<longrightarrow> ?QM193 a caps slots n mi cap obj ind s capd)\<rbrace>, -
 3. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q81 a caps slots n mi cap obj ind) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 4. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> True \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (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> (\<forall>x\<in>set slots. is_subject aag (fst x) \<and> cte_wp_at ((=) NullCap) x s \<and> real_cte_at x s) \<and> distinct slots) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> (pas_refined aag s \<and> is_subject aag (fst (obj, ind))) \<and> aag_can_read aag obj \<and> aag_can_read aag (fst (hd slots)) \<and> ?P'183 a caps slots n mi cap obj ind s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?Q81 a caps slots n mi cap obj ind s)) proof (prove)
goal (3 subgoals):
 1. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'183 (cap, obj, ind) caps slots n mi cap obj ind\<rbrace> derive_cap (obj, ind) cap \<lbrace>\<lambda>capd s. (capd \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (obj, ind) capd) (obj, ind) s) \<and> (capd \<noteq> NullCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag (fst (hd slots)) \<and> is_subject aag obj \<and> pas_cap_cur_auth aag capd \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> s \<turnstile> capd \<and> valid_objs s \<and> (obj, ind) \<noteq> hd slots \<and> valid_objs s \<and> s \<turnstile> capd \<and> tcb_cap_valid capd (hd slots) s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<and> valid_mdb s \<and> valid_objs s \<and> (if snd x = hd slots then fst x \<noteq> NullCap \<longrightarrow> capd \<noteq> fst x \<longrightarrow> capd = masked_as_full (fst x) (fst x) else cte_wp_at (\<lambda>c. fst x \<noteq> NullCap \<longrightarrow> masked_as_full c capd \<noteq> fst x \<longrightarrow> masked_as_full c capd = masked_as_full (fst x) (fst x)) (snd x) s)) \<and> (\<forall>x\<in>set (tl slots). is_subject aag (fst x) \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then NullCap = capd else cte_wp_at (\<lambda>c. NullCap = masked_as_full c capd) x s) \<and> real_cte_at x s) \<and> distinct (tl slots))\<rbrace>, -
 2. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q81 a caps slots n mi cap obj ind) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 3. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> True \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (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> (\<forall>x\<in>set slots. is_subject aag (fst x) \<and> cte_wp_at ((=) NullCap) x s \<and> real_cte_at x s) \<and> distinct slots) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> (pas_refined aag s \<and> is_subject aag (fst (obj, ind))) \<and> aag_can_read aag obj \<and> aag_can_read aag (fst (hd slots)) \<and> ?P'183 a caps slots n mi cap obj ind s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?Q81 a caps slots n mi cap obj ind s)) proof (prove)
goal (4 subgoals):
 1. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P242 (cap, obj, ind) caps slots n mi cap obj ind\<rbrace> derive_cap (obj, ind) cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) (obj, ind) rv) (obj, ind) s\<rbrace>, -
 2. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q240 (cap, obj, ind) caps slots n mi cap obj ind\<rbrace> derive_cap (obj, ind) cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag (fst (hd slots)) \<and> is_subject aag obj \<and> pas_cap_cur_auth aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> s \<turnstile> rv \<and> valid_objs s \<and> (obj, ind) \<noteq> hd slots \<and> valid_objs s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<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> (\<forall>x\<in>set (tl slots). is_subject aag (fst x) \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then NullCap = rv else cte_wp_at (\<lambda>c. NullCap = masked_as_full c rv) x s) \<and> real_cte_at x s) \<and> distinct (tl slots)\<rbrace>, -
 3. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q81 a caps slots n mi cap obj ind) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 4. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> True \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (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> (\<forall>x\<in>set slots. is_subject aag (fst x) \<and> cte_wp_at ((=) NullCap) x s \<and> real_cte_at x s) \<and> distinct slots) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> (pas_refined aag s \<and> is_subject aag (fst (obj, ind))) \<and> aag_can_read aag obj \<and> aag_can_read aag (fst (hd slots)) \<and> (?P242 a caps slots n mi cap obj ind and ?Q240 a caps slots n mi cap obj ind) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?Q81 a caps slots n mi cap obj ind s)) proof (prove)
goal (3 subgoals):
 1. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q240 (cap, obj, ind) caps slots n mi cap obj ind\<rbrace> derive_cap (obj, ind) cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag (fst (hd slots)) \<and> is_subject aag obj \<and> pas_cap_cur_auth aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> s \<turnstile> rv \<and> valid_objs s \<and> (obj, ind) \<noteq> hd slots \<and> valid_objs s \<and> s \<turnstile> rv \<and> tcb_cap_valid rv (hd slots) s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<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> (\<forall>x\<in>set (tl slots). is_subject aag (fst x) \<and> valid_mdb s \<and> valid_objs s \<and> (if x = hd slots then NullCap = rv else cte_wp_at (\<lambda>c. NullCap = masked_as_full c rv) x s) \<and> real_cte_at x s) \<and> distinct (tl slots)\<rbrace>, -
 2. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q81 a caps slots n mi cap obj ind) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 3. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> True \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (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> (\<forall>x\<in>set slots. is_subject aag (fst x) \<and> cte_wp_at ((=) NullCap) x s \<and> real_cte_at x s) \<and> distinct slots) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> (pas_refined aag s \<and> is_subject aag (fst (obj, ind))) \<and> aag_can_read aag obj \<and> aag_can_read aag (fst (hd slots)) \<and> ((\<lambda>a. cap \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) (obj, ind) a \<and> valid_objs a) and ?Q240 a caps slots n mi cap obj ind) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?Q81 a caps slots n mi cap obj ind s)) proof (prove)
goal (2 subgoals):
 1. \<And>a caps slots n mi cap obj ind. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); \<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q81 a caps slots n mi cap obj ind) (returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)))
 2. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> True \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (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> (\<forall>x\<in>set slots. is_subject aag (fst x) \<and> cte_wp_at ((=) NullCap) x s \<and> real_cte_at x s) \<and> distinct slots) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> (pas_refined aag s \<and> is_subject aag (fst (obj, ind))) \<and> aag_can_read aag obj \<and> aag_can_read aag (fst (hd slots)) \<and> ((\<lambda>a. cap \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) (obj, ind) a \<and> valid_objs a) and (\<lambda>a. \<forall>cap'. (valid_objs a \<and> cap' \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) (obj, ind) a \<longrightarrow> cte_wp_at (\<lambda>_. True) (obj, ind) a) \<and> (a \<turnstile> cap \<longrightarrow> a \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> auth_derived cap' cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> pas_refined aag a \<and> pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a \<and> valid_mdb a \<and> is_subject aag (fst (hd slots)) \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap' \<and> pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a \<and> valid_mdb a \<and> a \<turnstile> cap' \<and> valid_objs a \<and> (obj, ind) \<noteq> hd slots \<and> valid_objs a \<and> a \<turnstile> cap' \<and> tcb_cap_valid cap' (hd slots) a \<and> (\<forall>x\<in>set caps. a \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<and> valid_mdb a \<and> valid_objs a \<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) a)) \<and> (\<forall>x\<in>set (tl slots). is_subject aag (fst x) \<and> valid_mdb a \<and> valid_objs a \<and> (if x = hd slots then NullCap = cap' else cte_wp_at (\<lambda>c. NullCap = masked_as_full c cap') x a) \<and> real_cte_at x a) \<and> distinct (tl slots))) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?Q81 a caps slots n mi cap obj ind s)) proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi cap obj ind s. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); a = (cap, obj, ind); (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. s \<turnstile> cap \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap \<and> cte_wp_at (\<lambda>cp. cap \<noteq> NullCap \<longrightarrow> cp \<noteq> cap \<longrightarrow> cp = masked_as_full cap cap) (obj, ind) s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s\<rbrakk> \<Longrightarrow> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap) \<longrightarrow> True \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (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> (\<forall>x\<in>set slots. is_subject aag (fst x) \<and> cte_wp_at ((=) NullCap) x s \<and> real_cte_at x s) \<and> distinct slots) \<and> (\<not> (is_ep_cap cap \<and> ep = Some (obj_ref_of cap)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> (pas_refined aag s \<and> is_subject aag (fst (obj, ind))) \<and> aag_can_read aag obj \<and> aag_can_read aag (fst (hd slots)) \<and> ((\<lambda>a. cap \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) (obj, ind) a \<and> valid_objs a) and (\<lambda>a. \<forall>cap'. (valid_objs a \<and> cap' \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) (obj, ind) a \<longrightarrow> cte_wp_at (\<lambda>_. True) (obj, ind) a) \<and> (a \<turnstile> cap \<longrightarrow> a \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> auth_derived cap' cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> pas_refined aag a \<and> pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a \<and> valid_mdb a \<and> is_subject aag (fst (hd slots)) \<and> is_subject aag obj \<and> pas_cap_cur_auth aag cap' \<and> pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a \<and> valid_mdb a \<and> a \<turnstile> cap' \<and> valid_objs a \<and> (obj, ind) \<noteq> hd slots \<and> valid_objs a \<and> a \<turnstile> cap' \<and> tcb_cap_valid cap' (hd slots) a \<and> (\<forall>x\<in>set caps. a \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<and> valid_mdb a \<and> valid_objs a \<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) a)) \<and> (\<forall>x\<in>set (tl slots). is_subject aag (fst x) \<and> valid_mdb a \<and> valid_objs a \<and> (if x = hd slots then NullCap = cap' else cte_wp_at (\<lambda>c. NullCap = masked_as_full c cap') x a) \<and> real_cte_at x a) \<and> distinct (tl slots))) s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> True)) proof (prove)
goal (1 subgoal):
 1. \<And>caps slots cap obj ind s capa. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some capa; cap \<noteq> NullCap \<longrightarrow> capa \<noteq> cap \<longrightarrow> capa = masked_as_full cap cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> (cap \<noteq> NullCap \<longrightarrow> cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) \<and> (\<forall>cap'. s \<turnstile> cap' \<and> (cap' \<noteq> NullCap \<longrightarrow> auth_derived cap' cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> pas_cap_cur_auth aag cap' \<and> (obj, ind) \<noteq> hd slots \<and> tcb_cap_valid cap' (hd slots) s \<and> (\<forall>x\<in>set caps. 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> (\<forall>x\<in>set (tl slots). is_subject aag (fst x) \<and> (if x = hd slots then NullCap = cap' else cte_wp_at (\<lambda>c. NullCap = masked_as_full c cap') x s) \<and> real_cte_at x s) \<and> distinct (tl slots)) proof (prove)
goal (1 subgoal):
 1. \<And>caps slots cap obj ind s actual_cap. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; cap \<noteq> NullCap \<longrightarrow> actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> (cap \<noteq> NullCap \<longrightarrow> cap_master_cap actual_cap = cap_master_cap cap \<and> (cap_badge actual_cap, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid actual_cap = cap_asid cap \<and> vs_cap_ref actual_cap = vs_cap_ref cap) \<and> (\<forall>cap'. s \<turnstile> cap' \<and> (cap' \<noteq> NullCap \<longrightarrow> auth_derived cap' cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> cap' \<noteq> NullCap \<longrightarrow> pas_cap_cur_auth aag cap' \<and> (obj, ind) \<noteq> hd slots \<and> tcb_cap_valid cap' (hd slots) s \<and> (\<forall>x\<in>set caps. 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> (\<forall>x\<in>set (tl slots). is_subject aag (fst x) \<and> (if x = hd slots then NullCap = cap' else cte_wp_at (\<lambda>c. NullCap = masked_as_full c cap') x s) \<and> real_cte_at x s) \<and> distinct (tl slots)) proof (prove)
goal (1 subgoal):
 1. \<And>caps slots cap obj ind s actual_cap. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; cap \<noteq> NullCap \<longrightarrow> actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> (cap \<noteq> NullCap \<longrightarrow> cap_master_cap actual_cap = cap_master_cap cap \<and> (cap_badge actual_cap, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid actual_cap = cap_asid cap \<and> vs_cap_ref actual_cap = vs_cap_ref cap) \<and> (\<forall>x. s \<turnstile> x \<and> (x \<noteq> NullCap \<longrightarrow> auth_derived x cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> x \<noteq> NullCap \<longrightarrow> pas_cap_cur_auth aag x \<and> (obj, ind) \<noteq> hd slots \<and> real_cte_at (hd slots) s \<and> (\<forall>xa\<in>set caps. if snd xa = hd slots then fst xa \<noteq> NullCap \<longrightarrow> x \<noteq> fst xa \<longrightarrow> x = masked_as_full (fst xa) (fst xa) else cte_wp_at (\<lambda>c. fst xa \<noteq> NullCap \<longrightarrow> masked_as_full c x \<noteq> fst xa \<longrightarrow> masked_as_full c x = masked_as_full (fst xa) (fst xa)) (snd xa) s) \<and> (\<forall>xa\<in>set (tl slots). is_subject aag (fst xa) \<and> (if xa = hd slots then NullCap = x else cte_wp_at (\<lambda>c. NullCap = masked_as_full c x) xa s) \<and> real_cte_at xa s) \<and> distinct (tl slots)) proof (prove)
goal (1 subgoal):
 1. \<And>caps slots cap obj ind s actual_cap. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; cap \<noteq> NullCap \<longrightarrow> actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> (cap \<noteq> NullCap \<longrightarrow> cap_master_cap actual_cap = cap_master_cap cap \<and> (cap_badge actual_cap, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid actual_cap = cap_asid cap \<and> vs_cap_ref actual_cap = vs_cap_ref cap) \<and> (\<forall>x. s \<turnstile> x \<and> (x \<noteq> NullCap \<longrightarrow> auth_derived x cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> x \<noteq> NullCap \<longrightarrow> pas_cap_cur_auth aag x \<and> (obj, ind) \<noteq> hd slots \<and> (\<forall>xa\<in>set caps. (snd xa = hd slots \<longrightarrow> fst xa \<noteq> NullCap \<longrightarrow> x \<noteq> fst xa \<longrightarrow> x = masked_as_full (fst xa) (fst xa)) \<and> (snd xa \<noteq> hd slots \<longrightarrow> cte_wp_at (\<lambda>c. fst xa \<noteq> NullCap \<longrightarrow> masked_as_full c x \<noteq> fst xa \<longrightarrow> masked_as_full c x = masked_as_full (fst xa) (fst xa)) (snd xa) s)) \<and> (\<forall>xa\<in>set (tl slots). xa \<noteq> hd slots \<and> (xa \<noteq> hd slots \<longrightarrow> is_subject aag (fst xa) \<and> cte_wp_at (\<lambda>c. NullCap = masked_as_full c x) xa s \<and> real_cte_at xa s)) \<and> distinct (tl slots)) proof (prove)
goal (2 subgoals):
 1. \<And>caps slots cap obj ind s actual_cap. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; cap \<noteq> NullCap \<longrightarrow> actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> cap \<noteq> NullCap \<longrightarrow> cap_master_cap actual_cap = cap_master_cap cap \<and> (cap_badge actual_cap, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid actual_cap = cap_asid cap \<and> vs_cap_ref actual_cap = vs_cap_ref cap
 2. \<And>caps slots cap obj ind s actual_cap. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; cap \<noteq> NullCap \<longrightarrow> actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>x. s \<turnstile> x \<and> (x \<noteq> NullCap \<longrightarrow> auth_derived x cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> x \<noteq> NullCap \<longrightarrow> pas_cap_cur_auth aag x \<and> (obj, ind) \<noteq> hd slots \<and> (\<forall>xa\<in>set caps. (snd xa = hd slots \<longrightarrow> fst xa \<noteq> NullCap \<longrightarrow> x \<noteq> fst xa \<longrightarrow> x = masked_as_full (fst xa) (fst xa)) \<and> (snd xa \<noteq> hd slots \<longrightarrow> cte_wp_at (\<lambda>c. fst xa \<noteq> NullCap \<longrightarrow> masked_as_full c x \<noteq> fst xa \<longrightarrow> masked_as_full c x = masked_as_full (fst xa) (fst xa)) (snd xa) s)) \<and> (\<forall>xa\<in>set (tl slots). xa \<noteq> hd slots \<and> (xa \<noteq> hd slots \<longrightarrow> is_subject aag (fst xa) \<and> cte_wp_at (\<lambda>c. NullCap = masked_as_full c x) xa s \<and> real_cte_at xa s)) \<and> distinct (tl slots) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps_. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps_ slots mi); pas_refined aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; valid_mdb s_; valid_objs s_; s_ \<turnstile> cap_; is_subject aag obj_; pas_cap_cur_auth aag cap_; \<forall>cap\<in>set caps_. s_ \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s_ (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s_ (obj_, ind_) = Some actual_cap_; cap_ \<noteq> NullCap \<longrightarrow> actual_cap_ \<noteq> cap_ \<longrightarrow> actual_cap_ = masked_as_full cap_ cap_; \<forall>slot\<in>set slots_. is_subject aag (fst slot) \<and> caps_of_state s_ slot = Some NullCap \<and> real_cte_at slot s_; distinct slots_; is_ep_cap cap_ \<longrightarrow> ep \<noteq> Some (obj_ref_of cap_); slots_ \<noteq> []\<rbrakk> \<Longrightarrow> cap_ \<noteq> NullCap \<longrightarrow> cap_master_cap actual_cap_ = cap_master_cap cap_ \<and> (cap_badge actual_cap_, cap_badge cap_) \<in> capBadge_ordering False \<and> cap_asid actual_cap_ = cap_asid cap_ \<and> vs_cap_ref actual_cap_ = vs_cap_ref cap_ proof (prove)
goal (1 subgoal):
 1. \<And>caps slots cap obj ind s actual_cap. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; cap \<noteq> NullCap \<longrightarrow> actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>x. s \<turnstile> x \<and> (x \<noteq> NullCap \<longrightarrow> auth_derived x cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> x \<noteq> NullCap \<longrightarrow> pas_cap_cur_auth aag x \<and> (obj, ind) \<noteq> hd slots \<and> (\<forall>xa\<in>set caps. (snd xa = hd slots \<longrightarrow> fst xa \<noteq> NullCap \<longrightarrow> x \<noteq> fst xa \<longrightarrow> x = masked_as_full (fst xa) (fst xa)) \<and> (snd xa \<noteq> hd slots \<longrightarrow> cte_wp_at (\<lambda>c. fst xa \<noteq> NullCap \<longrightarrow> masked_as_full c x \<noteq> fst xa \<longrightarrow> masked_as_full c x = masked_as_full (fst xa) (fst xa)) (snd xa) s)) \<and> (\<forall>xa\<in>set (tl slots). xa \<noteq> hd slots \<and> (xa \<noteq> hd slots \<longrightarrow> is_subject aag (fst xa) \<and> cte_wp_at (\<lambda>c. NullCap = masked_as_full c x) xa s \<and> real_cte_at xa s)) \<and> distinct (tl slots) proof (prove)
goal (1 subgoal):
 1. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag x \<and> (obj, ind) \<noteq> hd slots \<and> (\<forall>xa\<in>set caps. (snd xa = hd slots \<longrightarrow> fst xa \<noteq> NullCap \<longrightarrow> x \<noteq> fst xa \<longrightarrow> x = masked_as_full (fst xa) (fst xa)) \<and> (snd xa \<noteq> hd slots \<longrightarrow> cte_wp_at (\<lambda>c. fst xa \<noteq> NullCap \<longrightarrow> masked_as_full c x \<noteq> fst xa \<longrightarrow> masked_as_full c x = masked_as_full (fst xa) (fst xa)) (snd xa) s)) \<and> (\<forall>xa\<in>set (tl slots). xa \<noteq> hd slots \<and> (xa \<noteq> hd slots \<longrightarrow> is_subject aag (fst xa) \<and> cte_wp_at (\<lambda>c. NullCap = masked_as_full c x) xa s \<and> real_cte_at xa s)) \<and> distinct (tl slots) proof (prove)
goal (5 subgoals):
 1. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag x
 2. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> (obj, ind) \<noteq> hd slots
 3. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set caps. (snd xa = hd slots \<longrightarrow> fst xa \<noteq> NullCap \<longrightarrow> x \<noteq> fst xa \<longrightarrow> x = masked_as_full (fst xa) (fst xa)) \<and> (snd xa \<noteq> hd slots \<longrightarrow> cte_wp_at (\<lambda>c. fst xa \<noteq> NullCap \<longrightarrow> masked_as_full c x \<noteq> fst xa \<longrightarrow> masked_as_full c x = masked_as_full (fst xa) (fst xa)) (snd xa) s)
 4. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set (tl slots). xa \<noteq> hd slots \<and> (xa \<noteq> hd slots \<longrightarrow> is_subject aag (fst xa) \<and> cte_wp_at (\<lambda>c. NullCap = masked_as_full c x) xa s \<and> real_cte_at xa s)
 5. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> distinct (tl slots) proof (prove)
goal (4 subgoals):
 1. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> (obj, ind) \<noteq> hd slots
 2. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set caps. (snd xa = hd slots \<longrightarrow> fst xa \<noteq> NullCap \<longrightarrow> x \<noteq> fst xa \<longrightarrow> x = masked_as_full (fst xa) (fst xa)) \<and> (snd xa \<noteq> hd slots \<longrightarrow> cte_wp_at (\<lambda>c. fst xa \<noteq> NullCap \<longrightarrow> masked_as_full c x \<noteq> fst xa \<longrightarrow> masked_as_full c x = masked_as_full (fst xa) (fst xa)) (snd xa) s)
 3. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set (tl slots). xa \<noteq> hd slots \<and> (xa \<noteq> hd slots \<longrightarrow> is_subject aag (fst xa) \<and> cte_wp_at (\<lambda>c. NullCap = masked_as_full c x) xa s \<and> real_cte_at xa s)
 4. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> distinct (tl slots) proof (prove)
goal (3 subgoals):
 1. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set caps. (snd xa = hd slots \<longrightarrow> fst xa \<noteq> NullCap \<longrightarrow> x \<noteq> fst xa \<longrightarrow> x = masked_as_full (fst xa) (fst xa)) \<and> (snd xa \<noteq> hd slots \<longrightarrow> cte_wp_at (\<lambda>c. fst xa \<noteq> NullCap \<longrightarrow> masked_as_full c x \<noteq> fst xa \<longrightarrow> masked_as_full c x = masked_as_full (fst xa) (fst xa)) (snd xa) s)
 2. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set (tl slots). xa \<noteq> hd slots \<and> (xa \<noteq> hd slots \<longrightarrow> is_subject aag (fst xa) \<and> cte_wp_at (\<lambda>c. NullCap = masked_as_full c x) xa s \<and> real_cte_at xa s)
 3. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> distinct (tl slots) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps_. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps_ slots mi); pas_refined aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; valid_mdb s_; valid_objs s_; s_ \<turnstile> cap_; is_subject aag obj_; pas_cap_cur_auth aag cap_; \<forall>cap\<in>set caps_. s_ \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s_ (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s_ (obj_, ind_) = Some actual_cap_; \<forall>slot\<in>set slots_. is_subject aag (fst slot) \<and> caps_of_state s_ slot = Some NullCap \<and> real_cte_at slot s_; distinct slots_; is_ep_cap cap_ \<longrightarrow> ep \<noteq> Some (obj_ref_of cap_); slots_ \<noteq> []; s_ \<turnstile> x_; x_ \<noteq> NullCap; auth_derived x_ cap_; cap_ \<noteq> NullCap; \<not> is_zombie cap_; cap_ \<noteq> IRQControlCap; actual_cap_ \<noteq> cap_ \<longrightarrow> actual_cap_ = masked_as_full cap_ cap_\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set caps_. (snd xa = hd slots_ \<longrightarrow> fst xa \<noteq> NullCap \<longrightarrow> x_ \<noteq> fst xa \<longrightarrow> x_ = masked_as_full (fst xa) (fst xa)) \<and> (snd xa \<noteq> hd slots_ \<longrightarrow> cte_wp_at (\<lambda>c. fst xa \<noteq> NullCap \<longrightarrow> masked_as_full c x_ \<noteq> fst xa \<longrightarrow> masked_as_full c x_ = masked_as_full (fst xa) (fst xa)) (snd xa) s_) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps_. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps_ slots mi); pas_refined aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; valid_mdb s_; valid_objs s_; s_ \<turnstile> cap_; is_subject aag obj_; pas_cap_cur_auth aag cap_; caps_of_state s_ (obj_, ind_) = Some actual_cap_; \<forall>slot\<in>set slots_. is_subject aag (fst slot) \<and> caps_of_state s_ slot = Some NullCap \<and> real_cte_at slot s_; distinct slots_; is_ep_cap cap_ \<longrightarrow> ep \<noteq> Some (obj_ref_of cap_); slots_ \<noteq> []; s_ \<turnstile> x_; x_ \<noteq> NullCap; auth_derived x_ cap_; cap_ \<noteq> NullCap; \<not> is_zombie cap_; cap_ \<noteq> IRQControlCap; actual_cap_ \<noteq> cap_ \<longrightarrow> actual_cap_ = masked_as_full cap_ cap_; s_ \<turnstile> fst xa \<and> is_subject aag (fst (snd xa)) \<and> pas_cap_cur_auth aag (fst xa) \<and> (\<exists>cap. caps_of_state s_ (snd xa) = Some cap \<and> (fst xa \<noteq> NullCap \<longrightarrow> cap \<noteq> fst xa \<longrightarrow> cap = masked_as_full (fst xa) (fst xa)))\<rbrakk> \<Longrightarrow> (snd xa = hd slots_ \<longrightarrow> fst xa \<noteq> NullCap \<longrightarrow> x_ \<noteq> fst xa \<longrightarrow> x_ = masked_as_full (fst xa) (fst xa)) \<and> (snd xa \<noteq> hd slots_ \<longrightarrow> cte_wp_at (\<lambda>c. fst xa \<noteq> NullCap \<longrightarrow> masked_as_full c x_ \<noteq> fst xa \<longrightarrow> masked_as_full c x_ = masked_as_full (fst xa) (fst xa)) (snd xa) s_) proof (prove)
goal (2 subgoals):
 1. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set (tl slots). xa \<noteq> hd slots \<and> (xa \<noteq> hd slots \<longrightarrow> is_subject aag (fst xa) \<and> cte_wp_at (\<lambda>c. NullCap = masked_as_full c x) xa s \<and> real_cte_at xa s)
 2. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> distinct (tl slots) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps_. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps_ slots mi); pas_refined aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; valid_mdb s_; valid_objs s_; s_ \<turnstile> cap_; is_subject aag obj_; pas_cap_cur_auth aag cap_; \<forall>cap\<in>set caps_. s_ \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s_ (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s_ (obj_, ind_) = Some actual_cap_; \<forall>slot\<in>set slots_. is_subject aag (fst slot) \<and> caps_of_state s_ slot = Some NullCap \<and> real_cte_at slot s_; distinct slots_; is_ep_cap cap_ \<longrightarrow> ep \<noteq> Some (obj_ref_of cap_); slots_ \<noteq> []; s_ \<turnstile> x_; x_ \<noteq> NullCap; auth_derived x_ cap_; cap_ \<noteq> NullCap; \<not> is_zombie cap_; cap_ \<noteq> IRQControlCap; actual_cap_ \<noteq> cap_ \<longrightarrow> actual_cap_ = masked_as_full cap_ cap_\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set (tl slots_). xa \<noteq> hd slots_ \<and> (xa \<noteq> hd slots_ \<longrightarrow> is_subject aag (fst xa) \<and> cte_wp_at (\<lambda>c. NullCap = masked_as_full c x_) xa s_ \<and> real_cte_at xa s_) proof (prove)
goal (1 subgoal):
 1. \<And>caps slots cap obj ind s actual_cap x. \<lbrakk>\<And>slots n mi. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap)))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; valid_objs s; s \<turnstile> cap; is_subject aag obj; pas_cap_cur_auth aag cap; \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> (\<exists>capa. caps_of_state s (snd cap) = Some capa \<and> (fst cap \<noteq> NullCap \<longrightarrow> capa \<noteq> fst cap \<longrightarrow> capa = masked_as_full (fst cap) (fst cap))); caps_of_state s (obj, ind) = Some actual_cap; \<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> caps_of_state s slot = Some NullCap \<and> real_cte_at slot s; distinct slots; is_ep_cap cap \<longrightarrow> ep \<noteq> Some (obj_ref_of cap); slots \<noteq> []; s \<turnstile> x; x \<noteq> NullCap; auth_derived x cap; cap \<noteq> NullCap; \<not> is_zombie cap; cap \<noteq> IRQControlCap; actual_cap \<noteq> cap \<longrightarrow> actual_cap = masked_as_full cap cap\<rbrakk> \<Longrightarrow> distinct (tl slots)