theory CNodeInv_AI

lemma cap_swap_mdb [wp]:
  "\<lbrace>valid_mdb and
  cte_wp_at (weak_derived c) a and
  cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c) a and
  cte_wp_at (weak_derived c') b and K (a \<noteq> b) and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c') b\<rbrace>
  cap_swap c a c' b
  \<lbrace>\<lambda>_. valid_mdb\<rbrace>" apply (simp add: valid_mdb_def2 cap_swap_def set_cdt_def bind_assoc set_original_def) apply (wp | simp del: fun_upd_apply split del: if_split)+ apply (fold swap_mdb_def [simplified Let_def]) apply (wp set_cap_caps_of_state2 get_cap_wp)+ apply (clarsimp simp: cte_wp_at_caps_of_state simp del: fun_upd_apply) apply (subgoal_tac "mdb_swap_abs_invs (cdt s) a b s cap capb c c'") prefer 2 apply (rule mdb_swap_abs_invs.intro) apply (rule mdb_swap_abs.intro) apply (simp add: valid_mdb_def2) apply (fastforce simp: cte_wp_at_caps_of_state) apply (fastforce simp: cte_wp_at_caps_of_state) apply (rule refl) apply assumption apply (erule (3) mdb_swap_abs_invs_axioms.intro) apply (unfold swap_mdb_def Let_def) apply (simp add: mdb_swap_abs_invs.no_mloop_n
                   mdb_swap_abs_invs.untyped_mdb_n
                   mdb_swap_abs_invs.mdb_cte_n
                   mdb_swap_abs_invs.reply_mdb_n
              del: fun_upd_apply
              split del: if_split) apply (rule conjI) apply (erule mdb_swap_abs_invs.descendants_inc_n) apply (rule conjI) apply (erule mdb_swap_abs_invs.untyped_inc_n) apply (clarsimp simp:cte_wp_at_caps_of_state)+ apply (rule conjI) apply (simp add: ut_revocable_def weak_derived_ranges del: split_paired_All) apply (rule conjI) apply (simp add: irq_revocable_def del: split_paired_All) apply (intro conjI impI allI) apply (simp del: split_paired_All) apply (simp del: split_paired_All) apply (simp add: reply_master_revocable_def weak_derived_replies
              del: split_paired_All) apply (clarsimp simp: valid_arch_mdb_cap_swap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb and cte_wp_at (weak_derived c) a and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c) a and cte_wp_at (weak_derived c') b and K (a \<noteq> b) and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c') b\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) and cte_wp_at (weak_derived c) a and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c) a and cte_wp_at (weak_derived c') b and (\<lambda>y. a \<noteq> b) and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c') b\<rbrace> do y <- set_cap c' a;
y <- set_cap c b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
x <- get;
y <- put (x\<lparr>cdt := (\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a)\<rparr>);
y <- do_extended_op (cap_swap_ext a b slot1_p slot2_p);
is_original <- gets is_original_cap;
x <- gets is_original_cap;
y <- modify (is_original_cap_update (\<lambda>_. x(a := is_original b)));
r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(b := is_original a)))
od \<lbrace>\<lambda>_ s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B1 ()\<rbrace> set_cap c b \<lbrace>\<lambda>ya s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) \<and> untyped_mdb ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) (caps_of_state s) \<and> descendants_inc ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) (caps_of_state s) \<and> no_mloop ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) \<and> untyped_inc ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) (caps_of_state s) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) (caps_of_state s) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) (caps_of_state s) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) (caps_of_state s) \<and> reply_mdb ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) (caps_of_state s) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) (caps_of_state s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 3. \<And>s. ((\<lambda>s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) and cte_wp_at (weak_derived c) a and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c) a and cte_wp_at (weak_derived c') b and (\<lambda>y. a \<noteq> b) and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B1 ()\<rbrace> set_cap c b \<lbrace>\<lambda>ya s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) (caps_of_state s) \<and> descendants_inc (swap_mdb (cdt s) a b) (caps_of_state s) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) (caps_of_state s) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) (caps_of_state s) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) (caps_of_state s) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) (caps_of_state s) \<and> reply_mdb (swap_mdb (cdt s) a b) (caps_of_state s) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) (caps_of_state s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 3. \<And>s. ((\<lambda>s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) and cte_wp_at (weak_derived c) a and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c) a and cte_wp_at (weak_derived c') b and (\<lambda>y. a \<noteq> b) and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) and cte_wp_at (weak_derived c) a and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c) a and cte_wp_at (weak_derived c') b and (\<lambda>y. a \<noteq> b) and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = c') b) s \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c))
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> mdb_swap_abs_invs (cdt s) a b s cap capb c c' proof (prove)
goal (2 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> mdb_swap_abs_invs (cdt s) a b s cap capb c c'
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (3 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> mdb_swap_abs (cdt s) a b s
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> mdb_swap_abs_invs_axioms a b s cap capb c c'
 3. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (7 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) a s
 3. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) b s
 4. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> cdt s = cdt s
 5. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> a \<noteq> b
 6. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> mdb_swap_abs_invs_axioms a b s cap capb c c'
 7. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (6 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) a s
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) b s
 3. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> cdt s = cdt s
 4. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> a \<noteq> b
 5. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> mdb_swap_abs_invs_axioms a b s cap capb c c'
 6. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (5 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) b s
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> cdt s = cdt s
 3. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> a \<noteq> b
 4. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> mdb_swap_abs_invs_axioms a b s cap capb c c'
 5. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (4 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> cdt s = cdt s
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> a \<noteq> b
 3. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> mdb_swap_abs_invs_axioms a b s cap capb c c'
 4. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (3 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> a \<noteq> b
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> mdb_swap_abs_invs_axioms a b s cap capb c c'
 3. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'\<rbrakk> \<Longrightarrow> mdb_swap_abs_invs_axioms a b s cap capb c c'
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) (swap_mdb (cdt s) a b) \<and> untyped_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop (swap_mdb (cdt s) a b) \<and> untyped_inc (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb (swap_mdb (cdt s) a b) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>ca. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some ca \<and> NullCap \<noteq> ca) ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) \<and> untyped_mdb ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> descendants_inc ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> no_mloop ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) \<and> untyped_inc ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_mdb ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> descendants_inc ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> untyped_inc ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> descendants_inc ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c))
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> untyped_inc ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> untyped_inc ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> untyped_inc ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c))
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (3 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; is_untyped_cap cap\<rbrakk> \<Longrightarrow> c = cap
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; is_untyped_cap capb\<rbrakk> \<Longrightarrow> c' = capb
 3. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c))
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c))
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); \<forall>p. caps_of_state s p = Some IRQControlCap \<longrightarrow> is_original_cap s p; reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> \<forall>p. (p = a \<longrightarrow> c' = IRQControlCap \<longrightarrow> is_original_cap s b) \<and> (p \<noteq> a \<longrightarrow> p = b \<longrightarrow> c = IRQControlCap \<longrightarrow> is_original_cap s a)
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (3 subgoals):
 1. \<And>s cap capb p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); \<forall>p. caps_of_state s p = Some IRQControlCap \<longrightarrow> is_original_cap s p; reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'; p = a; c' = IRQControlCap\<rbrakk> \<Longrightarrow> is_original_cap s b
 2. \<And>s cap capb p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); \<forall>p. caps_of_state s p = Some IRQControlCap \<longrightarrow> is_original_cap s p; reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'; p \<noteq> a; p = b; c = IRQControlCap\<rbrakk> \<Longrightarrow> is_original_cap s a
 3. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capb p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); \<forall>p. caps_of_state s p = Some IRQControlCap \<longrightarrow> is_original_cap s p; reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'; p \<noteq> a; p = b; c = IRQControlCap\<rbrakk> \<Longrightarrow> is_original_cap s a
 2. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) \<and> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); \<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> is_original_cap s p; reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); weak_derived c cap; caps_of_state s a = Some cap; is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; weak_derived c' capb; caps_of_state s b = Some capb; is_untyped_cap capb \<longrightarrow> capb = c'; mdb_swap_abs_invs (cdt s) a b s cap capb c c'\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(a := is_original_cap s b, b := is_original_cap s a)) ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) proof (prove)
goal:
No subgoals!