theory Ipc_R

lemma transferCapsToSlots_presM:
  assumes x: "\<And>cap src dest. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) dest s \<and> ex_cte_cap_to' dest s)
                                       \<and> (vo \<longrightarrow> valid_objs' s \<and> valid_cap' cap s \<and> real_cte_at' dest s)
                                       \<and> (drv \<longrightarrow> cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s
                                               \<and> cte_wp_at' (untyped_derived_eq cap o cteCap) src s
                                               \<and> valid_mdb' s)
                                       \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s)\<rbrace>
                                           cteInsert cap src dest \<lbrace>\<lambda>rv. P\<rbrace>"
  assumes eb: "\<And>b n. \<lbrace>P\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. P\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P s
                 \<and> (emx \<longrightarrow> (\<forall>x \<in> set slots. ex_cte_cap_to' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) x s) \<and> distinct slots)
                 \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x \<in> set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) x s)
                           \<and> (\<forall>x \<in> set caps. s \<turnstile>' fst x ) \<and> distinct slots)
                 \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s)
                 \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s
                         \<and> length slots \<le> 1
                         \<and> (\<forall>x \<in> set caps. s \<turnstile>' fst x \<and> (slots \<noteq> []
                              \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace>
                 transferCapsToSlots ep buffer n caps slots mi
              \<lbrace>\<lambda>rv. P\<rbrace>" apply (induct caps arbitrary: slots n mi) apply (simp, wp, simp) apply (simp add: Let_def split_def whenE_def
             cong: if_cong list.case_cong split del: if_split) apply (rule hoare_pre) apply (wp eb hoare_vcg_const_Ball_lift hoare_vcg_const_imp_lift
           | assumption | wpc)+ apply (rule cteInsert_assume_Null) apply (wp x hoare_vcg_const_Ball_lift cteInsert_cte_cap_to' hoare_weak_lift_imp) apply (rule cteInsert_weak_cte_wp_at2,clarsimp) apply (wp hoare_vcg_const_Ball_lift hoare_weak_lift_imp)+ apply (rule cteInsert_weak_cte_wp_at2,clarsimp) apply (wp hoare_vcg_const_Ball_lift cteInsert_cte_wp_at hoare_weak_lift_imp
          deriveCap_derived_foo)+ apply (thin_tac "\<And>slots. PROP P slots" for P) apply (clarsimp simp: cte_wp_at_ctes_of remove_rights_def
                        real_cte_tcb_valid if_apply_def2
             split del: if_split) apply (rule conjI) apply (clarsimp simp:cte_wp_at_ctes_of untyped_derived_eq_def) apply (intro conjI allI) apply (clarsimp simp:Fun.comp_def cte_wp_at_ctes_of)+ apply (clarsimp simp:valid_capAligned) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> 1 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set []. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> 1 \<and> (\<forall>x\<in>set []. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n [] slots mi \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> 1 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set (a # caps). valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> 1 \<and> (\<forall>x\<in>set (a # caps). valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n (a # caps) slots mi \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> 1 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set (a # caps). valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> 1 \<and> (\<forall>x\<in>set (a # caps). valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n (a # caps) slots mi \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> valid_cap' (fst a) s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> valid_cap' (fst a) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst a \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst a) (snd a) s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> constOnFailure (msgExtraCaps_update (\<lambda>_. word_of_nat n) mi) (if isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep then doE y <- liftE (setExtraBadge buffer (capEPBadge (fst a)) n);
liftE (transferCapsToSlots ep buffer (Suc n) caps slots (msgCapsUnwrapped_update (\<lambda>_. msgCapsUnwrapped mi || 2 ^ n) mi))
odE else case slots of [] \<Rightarrow> returnOk (msgExtraCaps_update (\<lambda>_. word_of_nat n) mi) | destSlot # slots' \<Rightarrow> doE cap' <- unifyFailure (global.deriveCap (snd a) (fst a));
y <- if cap' = capability.NullCap then throwError () else returnOk ();
y <- liftE (cteInsert cap' (snd a) destSlot);
liftE (transferCapsToSlots ep buffer (Suc n) caps slots' mi)
odE) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>?Q12 a caps slots n mi\<rbrace> constOnFailure (msgExtraCaps_update (\<lambda>_. word_of_nat n) mi) (if isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep then doE y <- liftE (setExtraBadge buffer (capEPBadge (fst a)) n);
liftE (transferCapsToSlots ep buffer (Suc n) caps slots (msgCapsUnwrapped_update (\<lambda>_. msgCapsUnwrapped mi || 2 ^ n) mi))
odE else case slots of [] \<Rightarrow> returnOk (msgExtraCaps_update (\<lambda>_. word_of_nat n) mi) | destSlot # slots' \<Rightarrow> doE cap' <- unifyFailure (global.deriveCap (snd a) (fst a));
y <- if cap' = capability.NullCap then throwError () else returnOk ();
y <- liftE (cteInsert cap' (snd a) destSlot);
liftE (transferCapsToSlots ep buffer (Suc n) caps slots' mi)
odE) \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>a caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> valid_cap' (fst a) s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> valid_cap' (fst a) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst a \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst a) (snd a) s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrakk> \<Longrightarrow> ?Q12 a caps slots n mi s proof (prove)
goal (4 subgoals):
 1. \<And>a caps slots n mi x21 x22 cap' y. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B116 a caps slots n mi x21 x22 cap' y\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>ya s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set x22. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct x22) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set x22. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct x22) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length x22 \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (x22 \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace>
 2. \<And>a caps slots n mi x21 x22 cap'. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B115 a caps slots n mi x21 x22 cap'\<rbrace> if cap' = capability.NullCap then throwError () else returnOk () \<lbrace>?B116 a caps slots n mi x21 x22 cap'\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a caps slots n mi x21 x22. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R109 a caps slots n mi x21 x22\<rbrace> unifyFailure (global.deriveCap (snd a) (fst a)) \<lbrace>?B115 a caps slots n mi x21 x22\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> valid_cap' (fst a) s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> valid_cap' (fst a) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst a \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst a) (snd a) s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrakk> \<Longrightarrow> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep \<longrightarrow> P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))) \<and> (\<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep) \<longrightarrow> (slots = [] \<longrightarrow> P s) \<and> (\<forall>x xa. slots = x # xa \<longrightarrow> ?R109 a caps slots n mi x xa s)) proof (prove)
goal (4 subgoals):
 1. \<And>a caps slots n mi x21 x22 cap' y. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P249 a caps slots n mi x21 x22 cap' y\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>ya s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set x22. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct x22) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set x22. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct x22) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length x22 \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (x22 \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace>
 2. \<And>a caps slots n mi x21 x22 cap'. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B115 a caps slots n mi x21 x22 cap'\<rbrace> if cap' = capability.NullCap then throwError () else returnOk () \<lbrace>\<lambda>y s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21 s \<longrightarrow> ?P249 a caps slots n mi x21 x22 cap' y s\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>a caps slots n mi x21 x22. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R109 a caps slots n mi x21 x22\<rbrace> unifyFailure (global.deriveCap (snd a) (fst a)) \<lbrace>?B115 a caps slots n mi x21 x22\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> valid_cap' (fst a) s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> valid_cap' (fst a) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst a \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst a) (snd a) s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrakk> \<Longrightarrow> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep \<longrightarrow> P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))) \<and> (\<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep) \<longrightarrow> (slots = [] \<longrightarrow> P s) \<and> (\<forall>x xa. slots = x # xa \<longrightarrow> ?R109 a caps slots n mi x xa s)) proof (prove)
goal (6 subgoals):
 1. \<And>a caps slots n mi x21 x22 cap' y x. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22; x \<in> set x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'258 a caps slots n mi x21 x22 cap' y x\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x\<rbrace>
 2. \<And>a caps slots n mi x21 x22 cap' y. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'256 a caps slots n mi x21 x22 cap' y\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>rv s. distinct x22\<rbrace>
 3. \<And>a caps slots n mi x21 x22 cap' y. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'254 a caps slots n mi x21 x22 cap' y\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>rv s. (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set x22. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct x22) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length x22 \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (x22 \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace>
 4. \<And>a caps slots n mi x21 x22 cap'. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B115 a caps slots n mi x21 x22 cap'\<rbrace> if cap' = capability.NullCap then throwError () else returnOk () \<lbrace>\<lambda>y s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21 s \<longrightarrow> (P s \<and> (emx \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x21 s) \<and> (vo \<longrightarrow> valid_objs' s \<and> valid_cap' cap' s \<and> real_cte_at' x21 s) \<and> (drv \<longrightarrow> cte_wp_at' (is_derived' (ctes_of s) (snd a) cap' \<circ> cteCap) (snd a) s \<and> cte_wp_at' (untyped_derived_eq cap' \<circ> cteCap) (snd a) s \<and> valid_mdb' s) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s)) \<and> (emx \<longrightarrow> (\<forall>x\<in>set x22. (ex_cte_cap_wp_to' (\<lambda>_. True) x and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21) s \<and> ?P'258 a caps slots n mi x21 x22 cap' y x s) \<and> ?P'256 a caps slots n mi x21 x22 cap' y s) \<and> ?P'254 a caps slots n mi x21 x22 cap' y s\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>a caps slots n mi x21 x22. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R109 a caps slots n mi x21 x22\<rbrace> unifyFailure (global.deriveCap (snd a) (fst a)) \<lbrace>?B115 a caps slots n mi x21 x22\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 6. \<And>a caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> valid_cap' (fst a) s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> valid_cap' (fst a) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst a \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst a) (snd a) s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrakk> \<Longrightarrow> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep \<longrightarrow> P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))) \<and> (\<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep) \<longrightarrow> (slots = [] \<longrightarrow> P s) \<and> (\<forall>x xa. slots = x # xa \<longrightarrow> ?R109 a caps slots n mi x xa s)) proof (prove)
goal (5 subgoals):
 1. \<And>a caps slots n mi x21 x22 cap' y. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'256 a caps slots n mi x21 x22 cap' y\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>rv s. distinct x22\<rbrace>
 2. \<And>a caps slots n mi x21 x22 cap' y. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'254 a caps slots n mi x21 x22 cap' y\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>rv s. (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set x22. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct x22) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length x22 \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (x22 \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace>
 3. \<And>a caps slots n mi x21 x22 cap'. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B115 a caps slots n mi x21 x22 cap'\<rbrace> if cap' = capability.NullCap then throwError () else returnOk () \<lbrace>\<lambda>y s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21 s \<longrightarrow> (P s \<and> (emx \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x21 s) \<and> (vo \<longrightarrow> valid_objs' s \<and> valid_cap' cap' s \<and> real_cte_at' x21 s) \<and> (drv \<longrightarrow> cte_wp_at' (is_derived' (ctes_of s) (snd a) cap' \<circ> cteCap) (snd a) s \<and> cte_wp_at' (untyped_derived_eq cap' \<circ> cteCap) (snd a) s \<and> valid_mdb' s) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s)) \<and> (emx \<longrightarrow> (\<forall>x\<in>set x22. (ex_cte_cap_wp_to' (\<lambda>_. True) x and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21) s \<and> (if x = x21 then cap' = capability.NullCap else cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s)) \<and> ?P'256 a caps slots n mi x21 x22 cap' y s) \<and> ?P'254 a caps slots n mi x21 x22 cap' y s\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a caps slots n mi x21 x22. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R109 a caps slots n mi x21 x22\<rbrace> unifyFailure (global.deriveCap (snd a) (fst a)) \<lbrace>?B115 a caps slots n mi x21 x22\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>a caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> valid_cap' (fst a) s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> valid_cap' (fst a) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst a \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst a) (snd a) s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrakk> \<Longrightarrow> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep \<longrightarrow> P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))) \<and> (\<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep) \<longrightarrow> (slots = [] \<longrightarrow> P s) \<and> (\<forall>x xa. slots = x # xa \<longrightarrow> ?R109 a caps slots n mi x xa s)) proof (prove)
goal (6 subgoals):
 1. \<And>a caps slots n mi x21 x22 cap' y x. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22; x \<in> set x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'273 a caps slots n mi x21 x22 cap' y x\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x\<rbrace>
 2. \<And>a caps slots n mi x21 x22 cap' y. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'271 a caps slots n mi x21 x22 cap' y\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>rv s. (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct x22\<rbrace>
 3. \<And>a caps slots n mi x21 x22 cap' y. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'267 a caps slots n mi x21 x22 cap' y\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>rv s. (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length x22 \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (x22 \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace>
 4. \<And>a caps slots n mi x21 x22 cap'. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B115 a caps slots n mi x21 x22 cap'\<rbrace> if cap' = capability.NullCap then throwError () else returnOk () \<lbrace>\<lambda>y s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21 s \<longrightarrow> (P s \<and> (emx \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x21 s) \<and> (vo \<longrightarrow> valid_objs' s \<and> valid_cap' cap' s \<and> real_cte_at' x21 s) \<and> (drv \<longrightarrow> cte_wp_at' (is_derived' (ctes_of s) (snd a) cap' \<circ> cteCap) (snd a) s \<and> cte_wp_at' (untyped_derived_eq cap' \<circ> cteCap) (snd a) s \<and> valid_mdb' s) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s)) \<and> (emx \<longrightarrow> (\<forall>x\<in>set x22. (ex_cte_cap_wp_to' (\<lambda>_. True) x and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21) s \<and> (if x = x21 then cap' = capability.NullCap else cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s)) \<and> distinct x22) \<and> (vo \<longrightarrow> (valid_objs' and valid_cap' cap') s \<and> (\<forall>x\<in>set x22. real_cte_at' x s \<and> ?P'273 a caps slots n mi x21 x22 cap' y x s) \<and> ?P'271 a caps slots n mi x21 x22 cap' y s) \<and> ?P'267 a caps slots n mi x21 x22 cap' y s\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>a caps slots n mi x21 x22. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R109 a caps slots n mi x21 x22\<rbrace> unifyFailure (global.deriveCap (snd a) (fst a)) \<lbrace>?B115 a caps slots n mi x21 x22\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 6. \<And>a caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> valid_cap' (fst a) s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> valid_cap' (fst a) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst a \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst a) (snd a) s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrakk> \<Longrightarrow> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep \<longrightarrow> P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))) \<and> (\<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep) \<longrightarrow> (slots = [] \<longrightarrow> P s) \<and> (\<forall>x xa. slots = x # xa \<longrightarrow> ?R109 a caps slots n mi x xa s)) proof (prove)
goal (5 subgoals):
 1. \<And>a caps slots n mi x21 x22 cap' y. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'271 a caps slots n mi x21 x22 cap' y\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>rv s. (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct x22\<rbrace>
 2. \<And>a caps slots n mi x21 x22 cap' y. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'267 a caps slots n mi x21 x22 cap' y\<rbrace> cteInsert cap' (snd a) x21 \<lbrace>\<lambda>rv s. (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length x22 \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (x22 \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace>
 3. \<And>a caps slots n mi x21 x22 cap'. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B115 a caps slots n mi x21 x22 cap'\<rbrace> if cap' = capability.NullCap then throwError () else returnOk () \<lbrace>\<lambda>y s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21 s \<longrightarrow> (P s \<and> (emx \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x21 s) \<and> (vo \<longrightarrow> valid_objs' s \<and> valid_cap' cap' s \<and> real_cte_at' x21 s) \<and> (drv \<longrightarrow> cte_wp_at' (is_derived' (ctes_of s) (snd a) cap' \<circ> cteCap) (snd a) s \<and> cte_wp_at' (untyped_derived_eq cap' \<circ> cteCap) (snd a) s \<and> valid_mdb' s) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s)) \<and> (emx \<longrightarrow> (\<forall>x\<in>set x22. (ex_cte_cap_wp_to' (\<lambda>_. True) x and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x21) s \<and> (if x = x21 then cap' = capability.NullCap else cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s)) \<and> distinct x22) \<and> (vo \<longrightarrow> (valid_objs' and valid_cap' cap') s \<and> (\<forall>x\<in>set x22. real_cte_at' x s \<and> (if x = x21 then cap' = capability.NullCap else cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s)) \<and> ?P'271 a caps slots n mi x21 x22 cap' y s) \<and> ?P'267 a caps slots n mi x21 x22 cap' y s\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>a caps slots n mi x21 x22. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; \<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep); slots = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R109 a caps slots n mi x21 x22\<rbrace> unifyFailure (global.deriveCap (snd a) (fst a)) \<lbrace>?B115 a caps slots n mi x21 x22\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>a caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> valid_cap' (fst a) s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> valid_cap' (fst a) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst a \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst a) (snd a) s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrakk> \<Longrightarrow> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep \<longrightarrow> P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))) \<and> (\<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep) \<longrightarrow> (slots = [] \<longrightarrow> P s) \<and> (\<forall>x xa. slots = x # xa \<longrightarrow> ?R109 a caps slots n mi x xa s)) proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>\<lambda>s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. P\<rbrace>; P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> valid_cap' (fst a) s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> valid_cap' (fst a) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst a \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst a) (snd a) s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))\<rbrakk> \<Longrightarrow> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep \<longrightarrow> P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))) \<and> (\<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep) \<longrightarrow> (slots = [] \<longrightarrow> P s) \<and> (\<forall>x xa. slots = x # xa \<longrightarrow> P s \<and> True \<and> (\<forall>cap'. (cte_wp_at' (\<lambda>cte. badge_derived' (fst a) (cteCap cte) \<and> capASID (fst a) = capASID (cteCap cte) \<and> cap_asid_base' (fst a) = cap_asid_base' (cteCap cte) \<and> cap_vptr' (fst a) = cap_vptr' (cteCap cte)) (snd a) s \<and> valid_objs' s \<and> cap' \<noteq> capability.NullCap \<longrightarrow> cte_wp_at' (is_derived' (ctes_of s) (snd a) cap' \<circ> cteCap) (snd a) s) \<and> (cte_wp_at' (untyped_derived_eq (fst a) \<circ> cteCap) (snd a) s \<longrightarrow> cte_wp_at' (untyped_derived_eq cap' \<circ> cteCap) (snd a) s) \<and> (valid_cap' (fst a) s \<longrightarrow> valid_cap' cap' s) \<and> (cap' \<noteq> capability.NullCap \<longrightarrow> fst a \<noteq> capability.NullCap) \<longrightarrow> (cap' = capability.NullCap \<longrightarrow> P s \<and> True) \<and> (cap' \<noteq> capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s \<longrightarrow> (P s \<and> (emx \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x s) \<and> (vo \<longrightarrow> valid_objs' s \<and> valid_cap' cap' s \<and> real_cte_at' x s) \<and> (drv \<longrightarrow> cte_wp_at' (is_derived' (ctes_of s) (snd a) cap' \<circ> cteCap) (snd a) s \<and> cte_wp_at' (untyped_derived_eq cap' \<circ> cteCap) (snd a) s \<and> valid_mdb' s) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s)) \<and> (emx \<longrightarrow> (\<forall>xa\<in>set xa. (ex_cte_cap_wp_to' (\<lambda>_. True) xa and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x) s \<and> (if xa = x then cap' = capability.NullCap else cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) xa s)) \<and> distinct xa) \<and> (vo \<longrightarrow> (valid_objs' and valid_cap' cap') s \<and> (\<forall>xa\<in>set xa. real_cte_at' xa s \<and> (if xa = x then cap' = capability.NullCap else cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) xa s)) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct xa) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. snd a \<noteq> x) and K (capAligned cap') and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) (snd a) cap' \<circ> cteCap) (snd a) s)) s \<and> length xa \<le> Suc 0 \<and> (\<forall>xb\<in>set caps. valid_cap' (fst xb) s \<and> (xa \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) (snd a) cap' (cteCap c)) (snd a) s \<and> valid_mdb' s \<and> valid_objs' s \<and> (if snd xb = x then fst xb \<noteq> capability.NullCap \<longrightarrow> cap' = fst xb else cte_wp_at' (\<lambda>c. fst xb \<noteq> capability.NullCap \<longrightarrow> maskedAsFull (cteCap c) cap' = fst xb) (snd xb) s)))))))) proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi s. P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> valid_cap' (fst a) s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> valid_cap' (fst a) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst a \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst a) (snd a) s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s))) \<Longrightarrow> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep \<longrightarrow> P s \<and> (emx \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (vo \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)))) \<and> (\<not> (isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep) \<longrightarrow> (slots = [] \<longrightarrow> P s) \<and> (\<forall>x xa. slots = x # xa \<longrightarrow> P s \<and> True \<and> (\<forall>cap'. (cte_wp_at' (\<lambda>cte. badge_derived' (fst a) (cteCap cte) \<and> capASID (fst a) = capASID (cteCap cte) \<and> cap_asid_base' (fst a) = cap_asid_base' (cteCap cte) \<and> cap_vptr' (fst a) = cap_vptr' (cteCap cte)) (snd a) s \<and> valid_objs' s \<and> cap' \<noteq> capability.NullCap \<longrightarrow> cte_wp_at' (is_derived' (ctes_of s) (snd a) cap' \<circ> cteCap) (snd a) s) \<and> (cte_wp_at' (untyped_derived_eq (fst a) \<circ> cteCap) (snd a) s \<longrightarrow> cte_wp_at' (untyped_derived_eq cap' \<circ> cteCap) (snd a) s) \<and> (valid_cap' (fst a) s \<longrightarrow> valid_cap' cap' s) \<and> (cap' \<noteq> capability.NullCap \<longrightarrow> fst a \<noteq> capability.NullCap) \<longrightarrow> (cap' = capability.NullCap \<longrightarrow> P s \<and> True) \<and> (cap' \<noteq> capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s \<longrightarrow> (P s \<and> (emx \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x s) \<and> (vo \<longrightarrow> valid_objs' s \<and> valid_cap' cap' s \<and> real_cte_at' x s) \<and> (drv \<longrightarrow> cte_wp_at' (is_derived' (ctes_of s) (snd a) cap' \<circ> cteCap) (snd a) s \<and> cte_wp_at' (untyped_derived_eq cap' \<circ> cteCap) (snd a) s \<and> valid_mdb' s) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s)) \<and> (emx \<longrightarrow> (\<forall>xa\<in>set xa. (ex_cte_cap_wp_to' (\<lambda>_. True) xa and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x) s \<and> (if xa = x then cap' = capability.NullCap else cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) xa s)) \<and> distinct xa) \<and> (vo \<longrightarrow> (valid_objs' and valid_cap' cap') s \<and> (\<forall>xa\<in>set xa. real_cte_at' xa s \<and> (if xa = x then cap' = capability.NullCap else cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) xa s)) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct xa) \<and> (pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. snd a \<noteq> x) and K (capAligned cap') and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) (snd a) cap' \<circ> cteCap) (snd a) s)) s \<and> length xa \<le> Suc 0 \<and> (\<forall>xb\<in>set caps. valid_cap' (fst xb) s \<and> (xa \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) (snd a) cap' (cteCap c)) (snd a) s \<and> valid_mdb' s \<and> valid_objs' s \<and> (if snd xb = x then fst xb \<noteq> capability.NullCap \<longrightarrow> cap' = fst xb else cte_wp_at' (\<lambda>c. fst xb \<noteq> capability.NullCap \<longrightarrow> maskedAsFull (cteCap c) cap' = fst xb) (snd xb) s)))))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b caps s x xa cap' cte. \<lbrakk>P s; emx \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<forall>x\<in>set xa. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> x \<notin> set xa \<and> distinct xa; vo \<longrightarrow> valid_objs' s \<and> real_cte_at' x s \<and> (\<forall>x\<in>set xa. real_cte_at' x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> valid_cap' a s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> x \<notin> set xa \<and> distinct xa; pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s; drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> xa = [] \<and> valid_cap' a s \<and> (\<exists>cte. ctes_of s b = Some cte \<and> cteCap cte = a) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (\<exists>cte. ctes_of s (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x))); isEndpointCap a \<longrightarrow> ep = None \<or> capEPPtr a \<noteq> the ep; (\<exists>cte. ctes_of s b = Some cte \<and> badge_derived' a (cteCap cte) \<and> capASID a = capASID (cteCap cte) \<and> cap_asid_base' a = cap_asid_base' (cteCap cte) \<and> cap_vptr' a = cap_vptr' (cteCap cte)) \<and> valid_objs' s \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte)); (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq a (cteCap cte)) \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq cap' (cteCap cte)); valid_cap' a s \<longrightarrow> valid_cap' cap' s; cap' \<noteq> capability.NullCap; ctes_of s x = Some cte; cteCap cte = capability.NullCap; a \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (drv \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte)) \<and> (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq cap' (cteCap cte))) \<and> (emx \<longrightarrow> (\<forall>xa\<in>set xa. if xa = x then False else True)) \<and> (vo \<longrightarrow> (\<forall>xa\<in>set xa. if xa = x then False else True)) \<and> (drv \<longrightarrow> b \<noteq> x \<and> capAligned cap' \<and> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte))) proof (prove)
goal (2 subgoals):
 1. \<And>a b caps s x xa cap' cte. \<lbrakk>P s; emx \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<forall>x\<in>set xa. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> x \<notin> set xa \<and> distinct xa; vo \<longrightarrow> valid_objs' s \<and> real_cte_at' x s \<and> (\<forall>x\<in>set xa. real_cte_at' x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> valid_cap' a s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> x \<notin> set xa \<and> distinct xa; pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s; drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> xa = [] \<and> valid_cap' a s \<and> (\<exists>cte. ctes_of s b = Some cte \<and> cteCap cte = a) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (\<exists>cte. ctes_of s (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x))); isEndpointCap a \<longrightarrow> ep = None \<or> capEPPtr a \<noteq> the ep; (\<exists>cte. ctes_of s b = Some cte \<and> badge_derived' a (cteCap cte) \<and> capASID a = capASID (cteCap cte) \<and> cap_asid_base' a = cap_asid_base' (cteCap cte) \<and> cap_vptr' a = cap_vptr' (cteCap cte)) \<and> valid_objs' s \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte)); (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq a (cteCap cte)) \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq cap' (cteCap cte)); valid_cap' a s \<longrightarrow> valid_cap' cap' s; cap' \<noteq> capability.NullCap; ctes_of s x = Some cte; cteCap cte = capability.NullCap; a \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> drv \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte)) \<and> (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq cap' (cteCap cte))
 2. \<And>a b caps s x xa cap' cte. \<lbrakk>P s; emx \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<forall>x\<in>set xa. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> x \<notin> set xa \<and> distinct xa; vo \<longrightarrow> valid_objs' s \<and> real_cte_at' x s \<and> (\<forall>x\<in>set xa. real_cte_at' x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> valid_cap' a s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> x \<notin> set xa \<and> distinct xa; pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s; drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> xa = [] \<and> valid_cap' a s \<and> (\<exists>cte. ctes_of s b = Some cte \<and> cteCap cte = a) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (\<exists>cte. ctes_of s (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x))); isEndpointCap a \<longrightarrow> ep = None \<or> capEPPtr a \<noteq> the ep; (\<exists>cte. ctes_of s b = Some cte \<and> badge_derived' a (cteCap cte) \<and> capASID a = capASID (cteCap cte) \<and> cap_asid_base' a = cap_asid_base' (cteCap cte) \<and> cap_vptr' a = cap_vptr' (cteCap cte)) \<and> valid_objs' s \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte)); (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq a (cteCap cte)) \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq cap' (cteCap cte)); valid_cap' a s \<longrightarrow> valid_cap' cap' s; cap' \<noteq> capability.NullCap; ctes_of s x = Some cte; cteCap cte = capability.NullCap; a \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (emx \<longrightarrow> (\<forall>xa\<in>set xa. if xa = x then False else True)) \<and> (vo \<longrightarrow> (\<forall>xa\<in>set xa. if xa = x then False else True)) \<and> (drv \<longrightarrow> b \<noteq> x \<and> capAligned cap' \<and> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte))) proof (prove)
goal (1 subgoal):
 1. \<And>a b caps s x xa cap' cte. \<lbrakk>P s; emx \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<forall>x\<in>set xa. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> x \<notin> set xa \<and> distinct xa; vo \<longrightarrow> valid_objs' s \<and> real_cte_at' x s \<and> (\<forall>x\<in>set xa. real_cte_at' x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> valid_cap' a s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> x \<notin> set xa \<and> distinct xa; pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s; drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> xa = [] \<and> valid_cap' a s \<and> (\<exists>cte. ctes_of s b = Some cte \<and> cteCap cte = a) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (\<exists>cte. ctes_of s (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x))); isEndpointCap a \<longrightarrow> ep = None \<or> capEPPtr a \<noteq> the ep; (\<exists>cte. ctes_of s b = Some cte \<and> badge_derived' a (cteCap cte) \<and> capASID a = capASID (cteCap cte) \<and> cap_asid_base' a = cap_asid_base' (cteCap cte) \<and> cap_vptr' a = cap_vptr' (cteCap cte)) \<and> valid_objs' s \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte)); (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq a (cteCap cte)) \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq cap' (cteCap cte)); valid_cap' a s \<longrightarrow> valid_cap' cap' s; cap' \<noteq> capability.NullCap; ctes_of s x = Some cte; cteCap cte = capability.NullCap; a \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (emx \<longrightarrow> (\<forall>xa\<in>set xa. if xa = x then False else True)) \<and> (vo \<longrightarrow> (\<forall>xa\<in>set xa. if xa = x then False else True)) \<and> (drv \<longrightarrow> b \<noteq> x \<and> capAligned cap' \<and> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte))) proof (prove)
goal (3 subgoals):
 1. \<And>a b caps s x xa cap' cte. \<lbrakk>P s; emx \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<forall>x\<in>set xa. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> x \<notin> set xa \<and> distinct xa; vo \<longrightarrow> valid_objs' s \<and> real_cte_at' x s \<and> (\<forall>x\<in>set xa. real_cte_at' x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> valid_cap' a s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> x \<notin> set xa \<and> distinct xa; pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s; drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> xa = [] \<and> valid_cap' a s \<and> (\<exists>cte. ctes_of s b = Some cte \<and> cteCap cte = a) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (\<exists>cte. ctes_of s (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x))); isEndpointCap a \<longrightarrow> ep = None \<or> capEPPtr a \<noteq> the ep; (\<exists>cte. ctes_of s b = Some cte \<and> badge_derived' a (cteCap cte) \<and> capASID a = capASID (cteCap cte) \<and> cap_asid_base' a = cap_asid_base' (cteCap cte) \<and> cap_vptr' a = cap_vptr' (cteCap cte)) \<and> valid_objs' s \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte)); (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq a (cteCap cte)) \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq cap' (cteCap cte)); valid_cap' a s \<longrightarrow> valid_cap' cap' s; cap' \<noteq> capability.NullCap; ctes_of s x = Some cte; cteCap cte = capability.NullCap; a \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> emx \<longrightarrow> (\<forall>xa\<in>set xa. if xa = x then False else True)
 2. \<And>a b caps s x xa cap' cte. \<lbrakk>P s; emx \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<forall>x\<in>set xa. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> x \<notin> set xa \<and> distinct xa; vo \<longrightarrow> valid_objs' s \<and> real_cte_at' x s \<and> (\<forall>x\<in>set xa. real_cte_at' x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> valid_cap' a s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> x \<notin> set xa \<and> distinct xa; pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s; drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> xa = [] \<and> valid_cap' a s \<and> (\<exists>cte. ctes_of s b = Some cte \<and> cteCap cte = a) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (\<exists>cte. ctes_of s (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x))); isEndpointCap a \<longrightarrow> ep = None \<or> capEPPtr a \<noteq> the ep; (\<exists>cte. ctes_of s b = Some cte \<and> badge_derived' a (cteCap cte) \<and> capASID a = capASID (cteCap cte) \<and> cap_asid_base' a = cap_asid_base' (cteCap cte) \<and> cap_vptr' a = cap_vptr' (cteCap cte)) \<and> valid_objs' s \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte)); (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq a (cteCap cte)) \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq cap' (cteCap cte)); valid_cap' a s \<longrightarrow> valid_cap' cap' s; cap' \<noteq> capability.NullCap; ctes_of s x = Some cte; cteCap cte = capability.NullCap; a \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> vo \<longrightarrow> (\<forall>xa\<in>set xa. if xa = x then False else True)
 3. \<And>a b caps s x xa cap' cte. \<lbrakk>P s; emx \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<forall>x\<in>set xa. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> x \<notin> set xa \<and> distinct xa; vo \<longrightarrow> valid_objs' s \<and> real_cte_at' x s \<and> (\<forall>x\<in>set xa. real_cte_at' x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap)) \<and> valid_cap' a s \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> x \<notin> set xa \<and> distinct xa; pad \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s; drv \<longrightarrow> vo \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> xa = [] \<and> valid_cap' a s \<and> (\<exists>cte. ctes_of s b = Some cte \<and> cteCap cte = a) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (\<exists>cte. ctes_of s (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x))); isEndpointCap a \<longrightarrow> ep = None \<or> capEPPtr a \<noteq> the ep; (\<exists>cte. ctes_of s b = Some cte \<and> badge_derived' a (cteCap cte) \<and> capASID a = capASID (cteCap cte) \<and> cap_asid_base' a = cap_asid_base' (cteCap cte) \<and> cap_vptr' a = cap_vptr' (cteCap cte)) \<and> valid_objs' s \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte)); (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq a (cteCap cte)) \<longrightarrow> (\<exists>cte. ctes_of s b = Some cte \<and> untyped_derived_eq cap' (cteCap cte)); valid_cap' a s \<longrightarrow> valid_cap' cap' s; cap' \<noteq> capability.NullCap; ctes_of s x = Some cte; cteCap cte = capability.NullCap; a \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> drv \<longrightarrow> b \<noteq> x \<and> capAligned cap' \<and> (\<exists>cte. ctes_of s b = Some cte \<and> is_derived' (ctes_of s) b cap' (cteCap cte)) proof (prove)
goal (1 subgoal):
 1. \<And>b caps s x cap' cte ctea. \<lbrakk>P s; emx \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x s; isEndpointCap (cteCap ctea) \<longrightarrow> ep = None \<or> capEPPtr (cteCap ctea) \<noteq> the ep; is_derived' (ctes_of s) b cap' (cteCap ctea); untyped_derived_eq (cteCap ctea) (cteCap ctea) \<longrightarrow> untyped_derived_eq cap' (cteCap ctea); cap' \<noteq> capability.NullCap; ctes_of s x = Some cte; cteCap cte = capability.NullCap; cteCap ctea \<noteq> capability.NullCap; drv; vo; pspace_aligned' s; pspace_distinct' s; valid_mdb' s; \<forall>x\<in>set caps. \<exists>cte. ctes_of s (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x); ctes_of s b = Some ctea; valid_objs' s; real_cte_at' x s; valid_cap' (cteCap ctea) s; \<forall>x\<in>set caps. valid_cap' (fst x) s; valid_cap' cap' s\<rbrakk> \<Longrightarrow> b \<noteq> x \<and> capAligned cap' proof (prove)
goal:
No subgoals!