theory CSpace1_R

lemma is_derived_eq:
  "\<lbrakk> cap_relation c c'; cap_relation d d';
     cdt_relation (swp cte_at s) (cdt s) (ctes_of s'); cte_at p s \<rbrakk> \<Longrightarrow>
  is_derived (cdt s) p c d = is_derived' (ctes_of s') (cte_map p) c' d'" unfolding cdt_relation_def apply (erule allE, erule impE, simp) apply (clarsimp simp: is_derived_def is_derived'_def badge_derived'_def) apply (rule conjI) apply (clarsimp simp: is_cap_simps isCap_simps) apply (cases c, auto simp: isCap_simps cap_master_cap_def capMasterCap_def)[1] apply (simp add:vsCapRef_def) apply (simp add:vs_cap_ref_def) apply (case_tac "isIRQControlCap d'") apply (frule(1) master_cap_relation) apply (clarsimp simp: isCap_simps cap_master_cap_def
                         is_zombie_def is_reply_cap_def is_master_reply_cap_def
                  split: cap_relation_split_asm arch_cap.split_asm)[1] apply (frule(1) master_cap_relation) apply (frule(1) cap_badge_relation) apply (frule cap_asid_cap_relation) apply (frule(1) capBadge_ordering_relation) apply (case_tac d) apply (simp_all add: isCap_simps is_cap_simps cap_master_cap_def
     vs_cap_ref_def vsCapRef_def capMasterCap_def
     split: cap_relation_split_asm arch_cap.split_asm) apply fastforce apply ((auto split:arch_cap.splits arch_capability.splits)[3]) apply (clarsimp split:option.splits arch_cap.splits arch_capability.splits) apply (intro conjI|clarsimp)+ apply fastforce apply clarsimp+ apply (clarsimp split:option.splits arch_cap.splits arch_capability.splits) apply (intro conjI|clarsimp)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cte_wp_at (\<lambda>_. True) p s\<rbrakk> \<Longrightarrow> is_derived (cdt s) p c d = is_derived' (ctes_of s') (cte_map p) c' d' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; \<forall>c. swp (cte_wp_at (\<lambda>_. True)) s c \<longrightarrow> cte_map ` descendants_of c (cdt s) = descendants_of' (cte_map c) (ctes_of s'); cte_wp_at (\<lambda>_. True) p s\<rbrakk> \<Longrightarrow> is_derived (cdt s) p c d = is_derived' (ctes_of s') (cte_map p) c' d' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s')\<rbrakk> \<Longrightarrow> is_derived (cdt s) p c d = is_derived' (ctes_of s') (cte_map p) c' d' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s')\<rbrakk> \<Longrightarrow> (is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> descendants_of p (cdt s) = {} \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))) \<and> (\<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s')\<rbrakk> \<Longrightarrow> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> descendants_of p (cdt s) = {} \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 2. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s')\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (2 subgoals):
 1. \<And>dev r bits f. \<lbrakk>cap_relation c c'; d' = capability.UntypedCap dev r bits f; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); d = cap.UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> (c \<noteq> cap.NullCap \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap (cap.UntypedCap dev r bits f) = cap_master_cap c \<and> descendants_of p (cdt s) = {} \<and> (\<forall>x R. c \<noteq> cap.ReplyCap x False R) \<and> ((\<exists>p asid. c = cap.ArchObjectCap (arch_cap.PageTableCap p asid)) \<longrightarrow> cap_asid c = None \<and> (\<exists>y. cap_asid c = Some y)) \<and> ((\<exists>p asid. c = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid)) \<longrightarrow> cap_asid c = None \<and> (\<exists>y. cap_asid c = Some y)) \<and> vs_cap_ref c = vs_cap_ref (cap.UntypedCap dev r bits f) \<and> (\<forall>x R. c \<noteq> cap.ReplyCap x True R)) = (c' \<noteq> capability.NullCap \<and> c' \<noteq> capability.IRQControlCap \<and> capability.UntypedCap dev r bits 0 = capMasterCap c' \<and> descendants_of' (cte_map p) (ctes_of s') = {} \<and> (\<forall>v0 v1 v2. c' \<noteq> capability.ReplyCap v0 v1 v2) \<and> ((\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef (capability.UntypedCap dev r bits f) = vsCapRef c' \<or> isArchCap isPageCap c'))
 2. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s')\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (3 subgoals):
 1. \<And>f x21 x22 x23 x24. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; d' = capability.UntypedCap x21 x22 x23 f; cte_wp_at (\<lambda>_. True) p s; {} = descendants_of' (cte_map p) (ctes_of s'); d = cap.UntypedCap x21 x22 x23 f; c = cap.UntypedCap x21 x22 x23 x24; descendants_of p (cdt s) = {}; vs_cap_ref (cap.UntypedCap x21 x22 x23 x24) = vs_cap_ref (cap.UntypedCap x21 x22 x23 f)\<rbrakk> \<Longrightarrow> vsCapRef (capability.UntypedCap x21 x22 x23 f) = vsCapRef (capability.UntypedCap x21 x22 x23 x24)
 2. \<And>f x21 x22 x23 x24. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; d' = capability.UntypedCap x21 x22 x23 f; cte_wp_at (\<lambda>_. True) p s; descendants_of p (cdt s) = {}; d = cap.UntypedCap x21 x22 x23 f; c = cap.UntypedCap x21 x22 x23 x24; descendants_of' (cte_map p) (ctes_of s') = {}; vsCapRef (capability.UntypedCap x21 x22 x23 f) = vsCapRef (capability.UntypedCap x21 x22 x23 x24)\<rbrakk> \<Longrightarrow> vs_cap_ref (cap.UntypedCap x21 x22 x23 x24) = vs_cap_ref (cap.UntypedCap x21 x22 x23 f)
 3. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s')\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (2 subgoals):
 1. \<And>f x21 x22 x23 x24. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; d' = capability.UntypedCap x21 x22 x23 f; cte_wp_at (\<lambda>_. True) p s; descendants_of p (cdt s) = {}; d = cap.UntypedCap x21 x22 x23 f; c = cap.UntypedCap x21 x22 x23 x24; descendants_of' (cte_map p) (ctes_of s') = {}; vsCapRef (capability.UntypedCap x21 x22 x23 f) = vsCapRef (capability.UntypedCap x21 x22 x23 x24)\<rbrakk> \<Longrightarrow> vs_cap_ref (cap.UntypedCap x21 x22 x23 x24) = vs_cap_ref (cap.UntypedCap x21 x22 x23 f)
 2. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s')\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s')\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); isIRQControlCap d'\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 2. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c)\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 2. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c)\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c)\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c; ((capBadge c', capBadge c') \<in> capBadge_ordering ?f1141) = ((cap_badge c, cap_badge c) \<in> capBadge_ordering ?f1141)\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y))) proof (prove)
goal (12 subgoals):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c; ((capBadge c', capBadge c') \<in> capBadge_ordering ?f1141) = ((cap_badge c, cap_badge c) \<in> capBadge_ordering ?f1141); d = cap.NullCap\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c; ((capBadge c', capBadge c') \<in> capBadge_ordering ?f1141) = ((cap_badge c, cap_badge c) \<in> capBadge_ordering ?f1141); d = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 3. \<And>x31 x32 x33. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c; ((capBadge c', capBadge c') \<in> capBadge_ordering ?f1141) = ((cap_badge c, cap_badge c) \<in> capBadge_ordering ?f1141); d = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 4. \<And>x41 x42 x43. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c; ((capBadge c', capBadge c') \<in> capBadge_ordering ?f1141) = ((cap_badge c, cap_badge c) \<in> capBadge_ordering ?f1141); d = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 5. \<And>x51 x52 x53. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c; ((capBadge c', capBadge c') \<in> capBadge_ordering ?f1141) = ((cap_badge c, cap_badge c) \<in> capBadge_ordering ?f1141); d = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 6. \<And>x61 x62 x63. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c; ((capBadge c', capBadge c') \<in> capBadge_ordering ?f1141) = ((cap_badge c, cap_badge c) \<in> capBadge_ordering ?f1141); d = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 7. \<And>x7. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c; ((capBadge c', capBadge c') \<in> capBadge_ordering ?f1141) = ((cap_badge c, cap_badge c) \<in> capBadge_ordering ?f1141); d = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 8. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c; ((capBadge c', capBadge c') \<in> capBadge_ordering ?f1141) = ((cap_badge c, cap_badge c) \<in> capBadge_ordering ?f1141); d = cap.DomainCap\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 9. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c; ((capBadge c', capBadge c') \<in> capBadge_ordering ?f1141) = ((cap_badge c, cap_badge c) \<in> capBadge_ordering ?f1141); d = cap.IRQControlCap\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
 10. \<And>x10. \<lbrakk>cap_relation c c'; cap_relation d d'; cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); \<not> isIRQControlCap d'; (capMasterCap c' = capMasterCap c') = (cap_master_cap c = cap_master_cap c); (capBadge c' = capBadge c') = (cap_badge c = cap_badge c); capASID c' = cap_asid c; ((capBadge c', capBadge c') \<in> capBadge_ordering ?f1141) = ((cap_badge c, cap_badge c) \<in> capBadge_ordering ?f1141); d = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap d \<longrightarrow> (c \<noteq> cap.NullCap \<and> \<not> is_zombie d \<and> c \<noteq> cap.IRQControlCap \<and> cap_master_cap d = cap_master_cap c \<and> (cap_badge d, cap_badge c) \<in> capBadge_ordering False \<and> is_master_reply_cap d = is_reply_cap c \<and> (is_pt_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (is_pd_cap c \<longrightarrow> cap_asid c = cap_asid d \<and> (\<exists>y. cap_asid c = Some y)) \<and> (vs_cap_ref c = vs_cap_ref d \<or> is_pg_cap d) \<and> \<not> is_reply_cap d \<and> \<not> is_master_reply_cap c) = (c' \<noteq> capability.NullCap \<and> \<not> isZombie d' \<and> \<not> isIRQControlCap c' \<and> capMasterCap d' = capMasterCap c' \<and> (capBadge d', capBadge c') \<in> capBadge_ordering False \<and> (isUntypedCap d' \<longrightarrow> descendants_of' (cte_map p) (ctes_of s') = {}) \<and> isReplyCap d' = isReplyCap c' \<and> (isReplyCap d' \<longrightarrow> capReplyMaster d') \<and> (isReplyCap c' \<longrightarrow> \<not> capReplyMaster c') \<and> (vsCapRef d' = vsCapRef c' \<or> isArchCap isPageCap c') \<and> (isArchCap isPageTableCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)) \<and> (isArchCap isPageDirectoryCap d' \<longrightarrow> capASID d' = capASID c' \<and> (\<exists>y. capASID d' = Some y)))
A total of 12 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>x51 x52 x53 x51a x52a x53a. \<lbrakk>d' = capability.ReplyCap x51 x52 (AllowGrant \<in> x53); cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); d = cap.ReplyCap x51 x52 x53; c = cap.ReplyCap x51a x52a x53a; c' = capability.ReplyCap x51a x52a (AllowGrant \<in> x53a)\<rbrakk> \<Longrightarrow> (x51 = x51a \<and> x52 = (\<not> x52a) \<and> x52 \<and> \<not> x52a) = (x51 = x51a \<and> x52 \<and> \<not> x52a)
 2. \<And>x12 x12a a' x11 x12b. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.ASIDPoolCap x11 x12b); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.ASIDPoolCap x11 x12b; c' = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12b)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.ASIDPoolCap x11 0 \<and> (Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x12b)) None] = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.ASIDPoolCap x11 0 \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x12b)) None] \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = None \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = None \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)))
 3. \<And>x12 x12a a'. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap arch_cap.ASIDControlCap; acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.ASIDControlCap; c' = capability.ArchObjectCap arch_capability.ASIDControlCap\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.ASIDControlCap \<and> (None = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.ASIDControlCap \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = None \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = None \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = None \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)))
 4. \<And>x12 x12a a' x31 x32 x33 x34 x35. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35)) = cap_asid (cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.PageCap x31 x32 x33 x34 x35; c' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageCap x31 x32 UNIV x34 None \<and> ((case x34 of ARMSection \<Rightarrow> case x35 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ARMSuperSection \<Rightarrow> case x35 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> case x35 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageCap x31 x32 VMReadWrite x34 None \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)))
 5. \<And>x12 x12a a' x41 x42. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageTableCap x41 x42); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.PageTableCap x41 x42; c' = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageTableCap x41 None \<and> cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) = cap_asid (cap.ArchObjectCap x12) \<and> (\<exists>y. cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) = Some y) \<and> ((case x42 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageTableCap x41 None \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x42 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)))
 6. \<And>x12 x12a a' x51 x52. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.PageDirectoryCap x51 x52; c' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageDirectoryCap x51 None \<and> cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap x12) \<and> (\<exists>y. cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = Some y) \<and> ((case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageDirectoryCap x51 None \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y))) proof (prove)
goal (5 subgoals):
 1. \<And>x12 x12a a' x11 x12b. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.ASIDPoolCap x11 x12b); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.ASIDPoolCap x11 x12b; c' = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12b)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.ASIDPoolCap x11 0 \<and> (Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x12b)) None] = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.ASIDPoolCap x11 0 \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x12b)) None] \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = None \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = None \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)))
 2. \<And>x12 x12a a'. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap arch_cap.ASIDControlCap; acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.ASIDControlCap; c' = capability.ArchObjectCap arch_capability.ASIDControlCap\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.ASIDControlCap \<and> (None = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.ASIDControlCap \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = None \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = None \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = None \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)))
 3. \<And>x12 x12a a' x31 x32 x33 x34 x35. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35)) = cap_asid (cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.PageCap x31 x32 x33 x34 x35; c' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageCap x31 x32 UNIV x34 None \<and> ((case x34 of ARMSection \<Rightarrow> case x35 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ARMSuperSection \<Rightarrow> case x35 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> case x35 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageCap x31 x32 VMReadWrite x34 None \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)))
 4. \<And>x12 x12a a' x41 x42. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageTableCap x41 x42); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.PageTableCap x41 x42; c' = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageTableCap x41 None \<and> cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) = cap_asid (cap.ArchObjectCap x12) \<and> (\<exists>y. cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) = Some y) \<and> ((case x42 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageTableCap x41 None \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x42 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)))
 5. \<And>x12 x12a a' x51 x52. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.PageDirectoryCap x51 x52; c' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageDirectoryCap x51 None \<and> cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap x12) \<and> (\<exists>y. cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = Some y) \<and> ((case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageDirectoryCap x51 None \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y))) proof (prove)
goal (2 subgoals):
 1. \<And>x12 x12a a' x41 x42. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageTableCap x41 x42); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.PageTableCap x41 x42; c' = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageTableCap x41 None \<and> cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) = cap_asid (cap.ArchObjectCap x12) \<and> (\<exists>y. cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) = Some y) \<and> ((case x42 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageTableCap x41 None \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x42 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)))
 2. \<And>x12 x12a a' x51 x52. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.PageDirectoryCap x51 x52; c' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageDirectoryCap x51 None \<and> cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap x12) \<and> (\<exists>y. cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = Some y) \<and> ((case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageDirectoryCap x51 None \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y))) proof (prove)
goal (2 subgoals):
 1. \<And>x12 a' x41 x42. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageTableCap x41 x42); acap_relation x12 a'; d' = capability.ArchObjectCap a'; c' = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)\<rbrakk> \<Longrightarrow> ((\<exists>x11 x12. a' = arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> (\<forall>x41a a b. x12 = arch_cap.PageTableCap x41a (Some (a, b)) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> aa && mask local.asid_low_bits = a && mask local.asid_low_bits \<longrightarrow> ba >> 20 = b >> 20 \<longrightarrow> x41a = x41 \<longrightarrow> aa \<noteq> a))) \<and> (a' = arch_capability.ASIDControlCap \<longrightarrow> (\<forall>x41a a b. x12 = arch_cap.PageTableCap x41a (Some (a, b)) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> aa && mask local.asid_low_bits = a && mask local.asid_low_bits \<longrightarrow> ba >> 20 = b >> 20 \<longrightarrow> x41a = x41 \<longrightarrow> aa \<noteq> a))) \<and> ((\<exists>x31 x32 x33 x34 x35. a' = arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> (\<forall>x41a a b. x12 = arch_cap.PageTableCap x41a (Some (a, b)) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> aa && mask local.asid_low_bits = a && mask local.asid_low_bits \<longrightarrow> ba >> 20 = b >> 20 \<longrightarrow> x41a = x41 \<longrightarrow> aa \<noteq> a))) \<and> (\<forall>x41a x42a. (x42a = None \<longrightarrow> a' = arch_capability.PageTableCap x41a None \<longrightarrow> (\<forall>x41a a b. x12 = arch_cap.PageTableCap x41a (Some (a, b)) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> aa && mask local.asid_low_bits = a && mask local.asid_low_bits \<longrightarrow> ba >> 20 = b >> 20 \<longrightarrow> x41a = x41 \<longrightarrow> aa \<noteq> a))) \<and> (\<forall>a b. x42a = Some (a, b) \<longrightarrow> a' = arch_capability.PageTableCap x41a (Some (a, b)) \<longrightarrow> ((\<exists>x11 x12a. x12 = arch_cap.ASIDPoolCap x11 x12a) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> b >> 20 = ba >> 20 \<and> a && mask local.asid_low_bits = aa && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of aa) \<longrightarrow> x41a = x41 \<longrightarrow> a \<noteq> aa)) \<and> (x12 = arch_cap.ASIDControlCap \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> b >> 20 = ba >> 20 \<and> a && mask local.asid_low_bits = aa && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of aa) \<longrightarrow> x41a = x41 \<longrightarrow> a \<noteq> aa)) \<and> ((\<exists>x31 x32 x33 x34 x35. x12 = arch_cap.PageCap x31 x32 x33 x34 x35) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> b >> 20 = ba >> 20 \<and> a && mask local.asid_low_bits = aa && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of aa) \<longrightarrow> x41a = x41 \<longrightarrow> a \<noteq> aa)) \<and> (\<forall>x41b x42a. (x42a = None \<longrightarrow> x12 = arch_cap.PageTableCap x41b None \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> b >> 20 = ba >> 20 \<and> a && mask local.asid_low_bits = aa && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of aa) \<longrightarrow> x41a = x41 \<longrightarrow> a \<noteq> aa)) \<and> (\<forall>aa ba. x42a = Some (aa, ba) \<longrightarrow> x12 = arch_cap.PageTableCap x41b (Some (aa, ba)) \<longrightarrow> (\<forall>ab bb. x42 = Some (ab, bb) \<longrightarrow> (x41b = x41 \<and> ab = aa \<and> bb >> 20 = ba >> 20 \<and> ab && mask local.asid_low_bits = aa && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of ab) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of aa)) = (x41a = x41 \<and> b >> 20 = bb >> 20 \<and> a && mask local.asid_low_bits = ab && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of ab) \<and> a = ab)))) \<and> ((\<exists>x51 x52. x12 = arch_cap.PageDirectoryCap x51 x52) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> b >> 20 = ba >> 20 \<and> a && mask local.asid_low_bits = aa && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of aa) \<longrightarrow> x41a = x41 \<longrightarrow> a \<noteq> aa)))) \<and> ((\<exists>x51 x52. a' = arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> (\<forall>x41a a b. x12 = arch_cap.PageTableCap x41a (Some (a, b)) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> aa && mask local.asid_low_bits = a && mask local.asid_low_bits \<longrightarrow> ba >> 20 = b >> 20 \<longrightarrow> x41a = x41 \<longrightarrow> aa \<noteq> a)))
 2. \<And>x12 x12a a' x51 x52. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.PageDirectoryCap x51 x52; c' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageDirectoryCap x51 None \<and> cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap x12) \<and> (\<exists>y. cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = Some y) \<and> ((case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageDirectoryCap x51 None \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y))) proof (prove)
goal (4 subgoals):
 1. \<And>x41 a b x41b ab bb. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); d = cap.ArchObjectCap (arch_cap.PageTableCap x41b (Some (a, b))); c = cap.ArchObjectCap (arch_cap.PageTableCap x41 (Some (ab, bb))); d' = capability.ArchObjectCap (arch_capability.PageTableCap x41b (Some (a, b))); c' = capability.ArchObjectCap (arch_capability.PageTableCap x41 (Some (ab, bb)))\<rbrakk> \<Longrightarrow> (x41b = x41 \<and> ab = a \<and> bb >> 20 = b >> 20 \<and> ab && mask local.asid_low_bits = a && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of ab) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) = (x41b = x41 \<and> b >> 20 = bb >> 20 \<and> a && mask local.asid_low_bits = ab && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of ab) \<and> a = ab)
 2. \<And>x12 x41 x42 x41a a b. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageTableCap x41 x42); acap_relation x12 (arch_capability.PageTableCap x41a (Some (a, b))); d' = capability.ArchObjectCap (arch_capability.PageTableCap x41a (Some (a, b))); c' = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)\<rbrakk> \<Longrightarrow> (\<exists>x51 x52. x12 = arch_cap.PageDirectoryCap x51 x52) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> b >> 20 = ba >> 20 \<and> a && mask local.asid_low_bits = aa && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of aa) \<longrightarrow> x41a = x41 \<longrightarrow> a \<noteq> aa)
 3. \<And>x12 a' x41 x42. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageTableCap x41 x42); acap_relation x12 a'; d' = capability.ArchObjectCap a'; c' = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)\<rbrakk> \<Longrightarrow> (\<exists>x51 x52. a' = arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> (\<forall>x41a a b. x12 = arch_cap.PageTableCap x41a (Some (a, b)) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> aa && mask local.asid_low_bits = a && mask local.asid_low_bits \<longrightarrow> ba >> 20 = b >> 20 \<longrightarrow> x41a = x41 \<longrightarrow> aa \<noteq> a))
 4. \<And>x12 x12a a' x51 x52. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.PageDirectoryCap x51 x52; c' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageDirectoryCap x51 None \<and> cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap x12) \<and> (\<exists>y. cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = Some y) \<and> ((case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageDirectoryCap x51 None \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y))) proof (prove)
goal (3 subgoals):
 1. \<And>x12 x41 x42 x41a a b. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageTableCap x41 x42); acap_relation x12 (arch_capability.PageTableCap x41a (Some (a, b))); d' = capability.ArchObjectCap (arch_capability.PageTableCap x41a (Some (a, b))); c' = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)\<rbrakk> \<Longrightarrow> (\<exists>x51 x52. x12 = arch_cap.PageDirectoryCap x51 x52) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> b >> 20 = ba >> 20 \<and> a && mask local.asid_low_bits = aa && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of aa) \<longrightarrow> x41a = x41 \<longrightarrow> a \<noteq> aa)
 2. \<And>x12 a' x41 x42. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) = cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageTableCap x41 x42); acap_relation x12 a'; d' = capability.ArchObjectCap a'; c' = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)\<rbrakk> \<Longrightarrow> (\<exists>x51 x52. a' = arch_capability.PageDirectoryCap x51 x52) \<longrightarrow> (\<forall>x41a a b. x12 = arch_cap.PageTableCap x41a (Some (a, b)) \<longrightarrow> (\<forall>aa ba. x42 = Some (aa, ba) \<longrightarrow> aa && mask local.asid_low_bits = a && mask local.asid_low_bits \<longrightarrow> ba >> 20 = b >> 20 \<longrightarrow> x41a = x41 \<longrightarrow> aa \<noteq> a))
 3. \<And>x12 x12a a' x51 x52. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); acap_relation x12 a'; d' = capability.ArchObjectCap a'; x12a = arch_cap.PageDirectoryCap x51 x52; c' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageDirectoryCap x51 None \<and> cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap x12) \<and> (\<exists>y. cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = Some y) \<and> ((case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageDirectoryCap x51 None \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y))) proof (prove)
goal (1 subgoal):
 1. \<And>x12 a' x51 x52. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); acap_relation x12 a'; d' = capability.ArchObjectCap a'; c' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)\<rbrakk> \<Longrightarrow> ((case x12 of arch_cap.ASIDPoolCap pool asid \<Rightarrow> arch_cap.ASIDPoolCap pool 0 | arch_cap.ASIDControlCap \<Rightarrow> x12 | arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> arch_cap.PageCap dev ref UNIV sz None | arch_cap.PageTableCap ptr data \<Rightarrow> arch_cap.PageTableCap ptr None | arch_cap.PageDirectoryCap ptr data \<Rightarrow> arch_cap.PageDirectoryCap ptr None) = arch_cap.PageDirectoryCap x51 None \<and> cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap x12) \<and> (\<exists>y. cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) = Some y) \<and> ((case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x12 of arch_cap.ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.ASIDControlCap \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageCap dev obj_ref rights _ None \<Rightarrow> None | arch_cap.PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageTableCap obj_ref None \<Rightarrow> None | arch_cap.PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_cap.PageDirectoryCap obj_ref None \<Rightarrow> None | arch_cap.PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>dev p R sz m. x12 = arch_cap.PageCap dev p R sz m))) = ((case a' of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> a' | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) = arch_capability.PageDirectoryCap x51 None \<and> (case a' of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = (case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((\<exists>v0 v1. a' = arch_capability.PageTableCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y)) \<and> ((\<exists>v0 v1. a' = arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> capASID (capability.ArchObjectCap a') = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) \<and> (\<exists>y. capASID (capability.ArchObjectCap a') = Some y))) proof (prove)
goal (1 subgoal):
 1. \<And>x12 a' x51 x52. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); capASID (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) = cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); d = cap.ArchObjectCap x12; c = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); acap_relation x12 a'; d' = capability.ArchObjectCap a'; c' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)\<rbrakk> \<Longrightarrow> ((\<exists>x11 x12. a' = arch_capability.ASIDPoolCap x11 x12) \<longrightarrow> (\<forall>x51a x2. x12 = arch_cap.PageDirectoryCap x51a (Some x2) \<longrightarrow> (\<forall>x2a. x52 = Some x2a \<longrightarrow> x2a && mask local.asid_low_bits = x2 && mask local.asid_low_bits \<longrightarrow> x51a = x51 \<longrightarrow> x2a \<noteq> x2))) \<and> (a' = arch_capability.ASIDControlCap \<longrightarrow> (\<forall>x51a x2. x12 = arch_cap.PageDirectoryCap x51a (Some x2) \<longrightarrow> (\<forall>x2a. x52 = Some x2a \<longrightarrow> x2a && mask local.asid_low_bits = x2 && mask local.asid_low_bits \<longrightarrow> x51a = x51 \<longrightarrow> x2a \<noteq> x2))) \<and> ((\<exists>x31 x32 x33 x34 x35. a' = arch_capability.PageCap x31 x32 x33 x34 x35) \<longrightarrow> (\<forall>x51a x2. x12 = arch_cap.PageDirectoryCap x51a (Some x2) \<longrightarrow> (\<forall>x2a. x52 = Some x2a \<longrightarrow> x2a && mask local.asid_low_bits = x2 && mask local.asid_low_bits \<longrightarrow> x51a = x51 \<longrightarrow> x2a \<noteq> x2))) \<and> ((\<exists>x41 x42. a' = arch_capability.PageTableCap x41 x42) \<longrightarrow> (\<forall>x51a x2. x12 = arch_cap.PageDirectoryCap x51a (Some x2) \<longrightarrow> (\<forall>x2a. x52 = Some x2a \<longrightarrow> x2a && mask local.asid_low_bits = x2 && mask local.asid_low_bits \<longrightarrow> x51a = x51 \<longrightarrow> x2a \<noteq> x2))) \<and> (\<forall>x51a x52a. (x52a = None \<longrightarrow> a' = arch_capability.PageDirectoryCap x51a None \<longrightarrow> (\<forall>x51a x2. x12 = arch_cap.PageDirectoryCap x51a (Some x2) \<longrightarrow> (\<forall>x2a. x52 = Some x2a \<longrightarrow> x2a && mask local.asid_low_bits = x2 && mask local.asid_low_bits \<longrightarrow> x51a = x51 \<longrightarrow> x2a \<noteq> x2))) \<and> (\<forall>x2. x52a = Some x2 \<longrightarrow> a' = arch_capability.PageDirectoryCap x51a (Some x2) \<longrightarrow> ((\<exists>x11 x12a. x12 = arch_cap.ASIDPoolCap x11 x12a) \<longrightarrow> (\<forall>x2a. x52 = Some x2a \<longrightarrow> x2 && mask local.asid_low_bits = x2a && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2a) \<longrightarrow> x51a = x51 \<longrightarrow> x2 \<noteq> x2a)) \<and> (x12 = arch_cap.ASIDControlCap \<longrightarrow> (\<forall>x2a. x52 = Some x2a \<longrightarrow> x2 && mask local.asid_low_bits = x2a && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2a) \<longrightarrow> x51a = x51 \<longrightarrow> x2 \<noteq> x2a)) \<and> ((\<exists>x31 x32 x33 x34 x35. x12 = arch_cap.PageCap x31 x32 x33 x34 x35) \<longrightarrow> (\<forall>x2a. x52 = Some x2a \<longrightarrow> x2 && mask local.asid_low_bits = x2a && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2a) \<longrightarrow> x51a = x51 \<longrightarrow> x2 \<noteq> x2a)) \<and> ((\<exists>x41 x42. x12 = arch_cap.PageTableCap x41 x42) \<longrightarrow> (\<forall>x2a. x52 = Some x2a \<longrightarrow> x2 && mask local.asid_low_bits = x2a && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2a) \<longrightarrow> x51a = x51 \<longrightarrow> x2 \<noteq> x2a)) \<and> (\<forall>x51b x52a. (x52a = None \<longrightarrow> x12 = arch_cap.PageDirectoryCap x51b None \<longrightarrow> (\<forall>x2a. x52 = Some x2a \<longrightarrow> x2 && mask local.asid_low_bits = x2a && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2a) \<longrightarrow> x51a = x51 \<longrightarrow> x2 \<noteq> x2a)) \<and> (\<forall>x2a. x52a = Some x2a \<longrightarrow> x12 = arch_cap.PageDirectoryCap x51b (Some x2a) \<longrightarrow> (\<forall>x2b. x52 = Some x2b \<longrightarrow> (x51b = x51 \<and> x2b = x2a \<and> x2b && mask local.asid_low_bits = x2a && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2b) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2a)) = (x51a = x51 \<and> x2 && mask local.asid_low_bits = x2b && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2b) \<and> x2 = x2b)))))) proof (prove)
goal (1 subgoal):
 1. \<And>x51 x2 x51b x2b. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s'); d = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51b (Some x2)); c = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x2b)); d' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51b (Some x2)); c' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 (Some x2b))\<rbrakk> \<Longrightarrow> (x51b = x51 \<and> x2b = x2 \<and> x2b && mask local.asid_low_bits = x2 && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2b) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2)) = (x51b = x51 \<and> x2 && mask local.asid_low_bits = x2b && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2b) \<and> x2 = x2b) proof (prove)
goal:
No subgoals!