theory ArchCNodeInv_AI

lemma swap_of_caps_valid_arch_caps [CNodeInv_AI_assms]:
  "\<lbrace>valid_arch_caps and
    cte_wp_at (weak_derived c) a and
    cte_wp_at (weak_derived c') b\<rbrace>
   do
     y \<leftarrow> set_cap c b;
     set_cap c' a
   od
   \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" apply (rule hoare_pre) apply (simp add: valid_arch_caps_def
                    valid_vs_lookup_def valid_table_caps_def pred_conj_def
               del: split_paired_Ex split_paired_All imp_disjL) apply (wp hoare_vcg_all_lift hoare_convert_imp[OF set_cap.vs_lookup_pages]
             hoare_vcg_disj_lift hoare_convert_imp[OF set_cap_caps_of_state]
             hoare_use_eq[OF set_cap_arch set_cap_obj_at_impossible[where P="\<lambda>x. x"]]) apply (clarsimp simp: valid_arch_caps_def cte_wp_at_caps_of_state
              simp del: split_paired_Ex split_paired_All imp_disjL) apply (frule weak_derived_obj_refs[where dcap=c]) apply (frule weak_derived_obj_refs[where dcap=c']) apply (frule weak_derived_pd_pt_asid[where c=c]) apply (frule weak_derived_pd_pt_asid[where c=c']) apply (intro conjI) apply (simp add: valid_vs_lookup_def del: split_paired_Ex split_paired_All) apply (elim allEI) apply (intro impI disjCI2) apply (simp del: split_paired_Ex split_paired_All) apply (elim conjE) apply (erule exfEI[where f="id (a := b, b := a)"]) apply (auto dest!: weak_derived_vs_cap_ref)[1] apply (simp add: valid_table_caps_def empty_table_caps_of
                del: split_paired_Ex split_paired_All imp_disjL) apply (simp add: unique_table_caps_def
               del: split_paired_Ex split_paired_All imp_disjL
                    split del: if_split) apply (erule allfEI[where f="id (a := b, b := a)"]) apply (erule allfEI[where f="id (a := b, b := a)"]) apply (clarsimp split del: if_split split: if_split_asm) apply (simp add: unique_table_refs_def
              del: split_paired_All split del: if_split) apply (erule allfEI[where f="id (a := b, b := a)"]) apply (erule allfEI[where f="id (a := b, b := a)"]) apply (clarsimp split del: if_split split: if_split_asm dest!:vs_cap_ref_to_table_cap_ref
                      dest!: weak_derived_table_cap_ref) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace> do y <- set_cap c b;
set_cap c' a
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- set_cap c b;
set_cap c' a
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>
 2. \<And>s. (valid_arch_caps and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- set_cap c b;
set_cap c' a
od \<lbrace>\<lambda>rv x. (\<forall>p ref. (ref \<unrhd> p) x \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state x p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) \<and> (\<forall>r p cap. caps_of_state x p = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state x)))) r x) \<and> unique_table_caps (caps_of_state x) \<and> unique_table_refs (caps_of_state x)\<rbrace>
 2. \<And>s. (valid_arch_caps and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_arch_caps and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> (\<forall>x xa. (xa \<unrhd> x) s \<longrightarrow> xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. ((caps_of_state s)(b \<mapsto> c, a \<mapsto> c')) p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa)) \<and> (\<forall>x xa xb. ((caps_of_state s)(b \<mapsto> c, a \<mapsto> c')) xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> (obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (\<forall>x. empty_table (set (second_level_tables (arch_state s))) x \<longrightarrow> caps_of x = {})) \<and> unique_table_caps ((caps_of_state s)(b \<mapsto> c, a \<mapsto> c')) \<and> unique_table_refs ((caps_of_state s)(b \<mapsto> c, a \<mapsto> c')) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa\<rbrakk> \<Longrightarrow> (\<forall>x xa. (xa \<unrhd> x) s \<longrightarrow> xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p'. (p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs c \<and> vs_cap_ref c = Some xa)) \<and> (p' \<noteq> b \<longrightarrow> (p' = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))))) \<and> (\<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))) \<and> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) \<and> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap\<rbrakk> \<Longrightarrow> (\<forall>x xa. (xa \<unrhd> x) s \<longrightarrow> xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p'. (p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs c \<and> vs_cap_ref c = Some xa)) \<and> (p' \<noteq> b \<longrightarrow> (p' = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))))) \<and> (\<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))) \<and> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) \<and> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa\<rbrakk> \<Longrightarrow> (\<forall>x xa. (xa \<unrhd> x) s \<longrightarrow> xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p'. (p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs c \<and> vs_cap_ref c = Some xa)) \<and> (p' \<noteq> b \<longrightarrow> (p' = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))))) \<and> (\<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))) \<and> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) \<and> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap\<rbrakk> \<Longrightarrow> (\<forall>x xa. (xa \<unrhd> x) s \<longrightarrow> xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p'. (p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs c \<and> vs_cap_ref c = Some xa)) \<and> (p' \<noteq> b \<longrightarrow> (p' = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))))) \<and> (\<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))) \<and> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) \<and> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> (\<forall>x xa. (xa \<unrhd> x) s \<longrightarrow> xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p'. (p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs c \<and> vs_cap_ref c = Some xa)) \<and> (p' \<noteq> b \<longrightarrow> (p' = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))))) \<and> (\<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))) \<and> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) \<and> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (4 subgoals):
 1. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>x xa. (xa \<unrhd> x) s \<longrightarrow> xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p'. (p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs c \<and> vs_cap_ref c = Some xa)) \<and> (p' \<noteq> b \<longrightarrow> (p' = a \<longrightarrow> x \<in> obj_refs c' \<and> vs_cap_ref c' = Some xa) \<and> (p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))))
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))
 3. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d)
 4. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (4 subgoals):
 1. \<And>s cap capa. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>x xa. (xa \<unrhd> x) s \<longrightarrow> (\<exists>p'. (p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref c = Some xa)) \<and> (p' \<noteq> b \<longrightarrow> (p' = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> (p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))))
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))
 3. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d)
 4. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (4 subgoals):
 1. \<And>s cap capa x xa. \<lbrakk>valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa; (xa \<unrhd> x) s \<longrightarrow> xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa)\<rbrakk> \<Longrightarrow> (xa \<unrhd> x) s \<longrightarrow> (\<exists>p'. (p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref c = Some xa)) \<and> (p' \<noteq> b \<longrightarrow> (p' = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> (p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))))
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))
 3. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d)
 4. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (4 subgoals):
 1. \<And>s cap capa x xa. \<lbrakk>valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa; (xa \<unrhd> x) s \<longrightarrow> xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa); (xa \<unrhd> x) s\<rbrakk> \<Longrightarrow> \<exists>p'. (p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref c = Some xa)) \<and> (p' \<noteq> b \<longrightarrow> (p' = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> (p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa)))
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))
 3. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d)
 4. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (4 subgoals):
 1. \<And>s cap capa x xa. \<lbrakk>valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa); (xa \<unrhd> x) s\<rbrakk> \<Longrightarrow> \<exists>p'. (p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref c = Some xa)) \<and> (p' \<noteq> b \<longrightarrow> (p' = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> (p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa)))
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))
 3. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d)
 4. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (4 subgoals):
 1. \<And>s cap capa x xa. \<lbrakk>valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; (xa \<unrhd> x) s; cap_asid c = cap_asid cap; cap_asid c' = cap_asid capa; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; \<exists>p' cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa; is_pt_cap c = is_pt_cap cap; is_pd_cap c = is_pd_cap cap; is_pt_cap c' = is_pt_cap capa; is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<exists>p'. (p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref c = Some xa)) \<and> (p' \<noteq> b \<longrightarrow> (p' = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> (p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa)))
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))
 3. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d)
 4. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (4 subgoals):
 1. \<And>s cap capa x xa p'. \<lbrakk>valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; (xa \<unrhd> x) s; cap_asid c = cap_asid cap; cap_asid c' = cap_asid capa; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; is_pt_cap c = is_pt_cap cap; is_pd_cap c = is_pd_cap cap; is_pt_cap c' = is_pt_cap capa; is_pd_cap c' = is_pd_cap capa; \<exists>cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa\<rbrakk> \<Longrightarrow> ((id(a := b, b := a)) p' = b \<longrightarrow> (b = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> (b \<noteq> a \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref c = Some xa)) \<and> ((id(a := b, b := a)) p' \<noteq> b \<longrightarrow> ((id(a := b, b := a)) p' = a \<longrightarrow> x \<in> obj_refs capa \<and> vs_cap_ref c' = Some xa) \<and> ((id(a := b, b := a)) p' \<noteq> a \<longrightarrow> (\<exists>cap. caps_of_state s ((id(a := b, b := a)) p') = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa)))
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))
 3. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d)
 4. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (3 subgoals):
 1. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>x xa. (xa = b \<longrightarrow> (b = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (b \<noteq> a \<longrightarrow> is_pd_cap c \<or> is_pt_cap c \<longrightarrow> cap_asid c = None \<longrightarrow> x \<in> obj_refs c \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))) \<and> (xa \<noteq> b \<longrightarrow> (xa = a \<longrightarrow> is_pd_cap c' \<or> is_pt_cap c' \<longrightarrow> cap_asid c' = None \<longrightarrow> x \<in> obj_refs c' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {})) \<and> (xa \<noteq> a \<longrightarrow> (\<forall>xb. caps_of_state s xa = Some xb \<longrightarrow> is_pd_cap xb \<or> is_pt_cap xb \<longrightarrow> cap_asid xb = None \<longrightarrow> x \<in> obj_refs xb \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}))))
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d)
 3. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d)
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; \<forall>p p' cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>p p' cap. (if p = a then Some c' else if p = b then Some c else caps_of_state s p) = Some cap \<longrightarrow> (\<forall>cap'. (if p' = a then Some c' else if p' = b then Some c else caps_of_state s p') = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p))
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capa p. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa; \<forall>p' cap. caps_of_state s ((id(a := b, b := a)) p) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = (id(a := b, b := a)) p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = (id(a := b, b := a)) p))\<rbrakk> \<Longrightarrow> \<forall>p' cap. (if p = a then Some c' else if p = b then Some c else caps_of_state s p) = Some cap \<longrightarrow> (\<forall>cap'. (if p' = a then Some c' else if p' = b then Some c else caps_of_state s p') = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p))
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capa p p'. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa; \<forall>cap. caps_of_state s ((id(a := b, b := a)) p) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s ((id(a := b, b := a)) p') = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> (id(a := b, b := a)) p' = (id(a := b, b := a)) p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> (id(a := b, b := a)) p' = (id(a := b, b := a)) p))\<rbrakk> \<Longrightarrow> \<forall>cap. (if p = a then Some c' else if p = b then Some c else caps_of_state s p) = Some cap \<longrightarrow> (\<forall>cap'. (if p' = a then Some c' else if p' = b then Some c else caps_of_state s p') = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p))
 2. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>d. if d = a then Some c' else if d = b then Some c else caps_of_state s d) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); \<forall>p p' cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa\<rbrakk> \<Longrightarrow> \<forall>p p' cap. (if p = a then Some c' else if p = b then Some c else caps_of_state s p) = Some cap \<longrightarrow> (\<forall>cap'. (if p' = a then Some c' else if p' = b then Some c else caps_of_state s p') = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa p. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa; \<forall>p' cap. caps_of_state s ((id(a := b, b := a)) p) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap)\<rbrakk> \<Longrightarrow> \<forall>p' cap. (if p = a then Some c' else if p = b then Some c else caps_of_state s p) = Some cap \<longrightarrow> (\<forall>cap'. (if p' = a then Some c' else if p' = b then Some c else caps_of_state s p') = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa p p'. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; obj_refs c = obj_refs cap; obj_refs c' = obj_refs capa; cap_asid c = cap_asid cap \<and> is_pt_cap c = is_pt_cap cap \<and> is_pd_cap c = is_pd_cap cap; cap_asid c' = cap_asid capa \<and> is_pt_cap c' = is_pt_cap capa \<and> is_pd_cap c' = is_pd_cap capa; \<forall>cap. caps_of_state s ((id(a := b, b := a)) p) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s ((id(a := b, b := a)) p') = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap)\<rbrakk> \<Longrightarrow> \<forall>cap. (if p = a then Some c' else if p = b then Some c else caps_of_state s p) = Some cap \<longrightarrow> (\<forall>cap'. (if p' = a then Some c' else if p' = b then Some c else caps_of_state s p') = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) proof (prove)
goal:
No subgoals!