theory ArchAcc_AI

lemma set_asid_pool_restrict_asid_map:
  "\<lbrace>valid_asid_map and ko_at (ArchObj (ASIDPool ap)) p and
    (\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> ucast asid \<notin> S \<longrightarrow>
                arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow>
                arm_asid_map (arch_state s) asid = None)\<rbrace>
  set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: set_asid_pool_def valid_asid_map_def set_object_def) apply (wp get_object_wp) apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits
                  simp del: fun_upd_apply) apply (drule(1) bspec) apply (clarsimp simp: vspace_at_asid_def obj_at_def graph_of_def) apply (drule subsetD, erule domI) apply simp apply (drule spec, drule(1) mp) apply simp apply (erule vs_lookupE) apply (rule vs_lookupI, simp) apply (clarsimp simp: vs_asid_refs_def graph_of_def) apply (drule rtranclD) apply (erule disjE, clarsimp) apply clarsimp apply (drule tranclD) apply clarsimp apply (rule r_into_rtrancl) apply (drule vs_lookup1D) apply clarsimp apply (subst vs_lookup1_def) apply (clarsimp simp: obj_at_def) apply (erule rtranclE) apply (clarsimp simp: vs_refs_def graph_of_def) apply (rule image_eqI[where x="(_, _)"]) apply (simp add: split_def) apply (clarsimp simp: restrict_map_def) apply (drule ucast_up_inj, simp) apply (simp add: mask_asid_low_bits_ucast_ucast) apply (drule ucast_up_inj, simp) apply clarsimp apply clarsimp apply (drule vs_lookup1_trans_is_append) apply clarsimp apply (drule vs_lookup1D) by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and ako_at (ASIDPool ap) p and (\<lambda>s. \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None)\<rbrace> set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0)) and ako_at (ASIDPool ap) p and (\<lambda>s. \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None)\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (ASIDPool (ap |` S))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>)
od \<lbrace>\<lambda>_ s. dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0)) and ako_at (ASIDPool ap) p and (\<lambda>s. \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None)) s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (ASIDPool (ap |` S))) \<longrightarrow> dom (arm_asid_map (arch_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>))) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>))). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) \<and> asid \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a aa b. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; ako_at (ASIDPool ap) p s; \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (ap |` S))); (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> vspace_at_asid a b (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s ko a aa b. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; ako_at (ASIDPool ap) p s; \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (ap |` S))); (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); case (a, aa, b) of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> vspace_at_asid a b (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; kheap s p = Some (ArchObj (ASIDPool ap)); \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None; a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None; a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0; a \<in> {0..mask local.asid_bits}\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None; a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0; a \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) = Some p \<longrightarrow> arm_asid_map (arch_state s) a = None\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ref' p'. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; (ref', p') \<in> vs_asid_refs (asid_table s); ((ref', p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ref' p'. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; (ref', p') \<in> vs_asid_refs (asid_table s); ((ref', p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> ((ref', p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>*; asid_table s ab = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; ([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba) = ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<or> ([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba) \<noteq> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; ([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba) \<noteq> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; \<exists>z. (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), z) \<in> vs_lookup1 s \<and> (z, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba ac bb. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), ac, bb) \<in> vs_lookup1 s; ((ac, bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba ac bb. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), ac, bb) \<in> vs_lookup1 s; ((ac, bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba ac bb. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; ((ac, bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>*; \<exists>rs r p p' ko. ([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba) = (rs, p) \<and> (ac, bb) = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> {((rs, pa), rs', p'). \<exists>ko r. ko_at ko pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (ap |` S)))\<rparr>) \<and> rs' = r # rs \<and> (r, p') \<in> vs_refs ko} proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 s)\<^sup>*; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (2 subgoals):
 1. \<And>s a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; ([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb) = ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b)\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko)
 2. \<And>s a aa b ab ba bb r ko y. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (2 subgoals):
 1. \<And>s a aa ab ac ba. \<lbrakk>a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, ba); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some p; kheap s p = Some (ArchObj (ASIDPool ap)); UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) (asid_high_bits_of a); ap ac = Some ba; a && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ac\<rbrakk> \<Longrightarrow> (VSRef (UCAST(10 \<rightarrow> 32) ac) (Some AASIDPool), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). (ap |` S) x = Some y}
 2. \<And>s a aa b ab ba bb r ko y. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (3 subgoals):
 1. \<And>s a aa ab ac ba. \<lbrakk>a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, ba); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some p; kheap s p = Some (ArchObj (ASIDPool ap)); UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) (asid_high_bits_of a); ap ac = Some ba; a && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ac\<rbrakk> \<Longrightarrow> (VSRef (UCAST(10 \<rightarrow> 32) ac) (Some AASIDPool), ba) = (case (?uu88 s a aa ab ac ba, ?uua88 s a aa ab ac ba) of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x))
 2. \<And>s a aa ab ac ba. \<lbrakk>a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, ba); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some p; kheap s p = Some (ArchObj (ASIDPool ap)); UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) (asid_high_bits_of a); ap ac = Some ba; a && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ac\<rbrakk> \<Longrightarrow> (?uu88 s a aa ab ac ba, ?uua88 s a aa ab ac ba) \<in> {(x, y). (ap |` S) x = Some y}
 3. \<And>s a aa b ab ba bb r ko y. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (2 subgoals):
 1. \<And>s a aa ab ac ba. \<lbrakk>a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, ba); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some p; kheap s p = Some (ArchObj (ASIDPool ap)); UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) (asid_high_bits_of a); ap ac = Some ba; a && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ac\<rbrakk> \<Longrightarrow> (ac, ba) \<in> {(x, y). (ap |` S) x = Some y}
 2. \<And>s a aa b ab ba bb r ko y. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (2 subgoals):
 1. \<And>s a aa ab ac ba. \<lbrakk>a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. if x \<in> S then ap x else None))); arm_asid_map (arch_state s) a = Some (aa, ba); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some p; kheap s p = Some (ArchObj (ASIDPool ap)); UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) (asid_high_bits_of a); ap ac = Some ba; a && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ac\<rbrakk> \<Longrightarrow> ac \<in> S
 2. \<And>s a aa b ab ba bb r ko y. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (2 subgoals):
 1. \<And>s a aa ab ac ba. \<lbrakk>a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. if x \<in> S then ap x else None))); arm_asid_map (arch_state s) a = Some (aa, ba); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some p; kheap s p = Some (ArchObj (ASIDPool ap)); ap ac = Some ba; a && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ac; ab = asid_high_bits_of a\<rbrakk> \<Longrightarrow> ac \<in> S
 2. \<And>s a aa b ab ba bb r ko y. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (2 subgoals):
 1. \<And>s a aa ab ac ba. \<lbrakk>a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. if x \<in> S then ap x else None))); arm_asid_map (arch_state s) a = Some (aa, ba); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<in> S; asid_table s (asid_high_bits_of a) = Some p; kheap s p = Some (ArchObj (ASIDPool ap)); ap ac = Some ba; UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) a) = UCAST(10 \<rightarrow> 32) ac; ab = asid_high_bits_of a\<rbrakk> \<Longrightarrow> ac \<in> S
 2. \<And>s a aa b ab ba bb r ko y. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (2 subgoals):
 1. \<And>s a aa ab ac ba. \<lbrakk>a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (\<lambda>x. if x \<in> S then ap x else None))); arm_asid_map (arch_state s) a = Some (aa, ba); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<in> S; asid_table s (asid_high_bits_of a) = Some p; kheap s p = Some (ArchObj (ASIDPool ap)); ap ac = Some ba; ab = asid_high_bits_of a; UCAST(32 \<rightarrow> 10) a = ac\<rbrakk> \<Longrightarrow> ac \<in> S
 2. \<And>s a aa b ab ba bb r ko y. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba bb r ko y. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba bb r ko ac bc. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), ac, bc) \<in> (vs_lookup1 s)\<^sup>*; ((ac, bc), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba bb r ko ac bc. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; ((ac, bc), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s; \<exists>zs. ac = zs @ [r, VSRef (UCAST(7 \<rightarrow> 32) ab) None]\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba bb r ko bc zs. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; ((zs @ [r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bc), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ab ba bb r ko bc zs. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool ap)); a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool (ap |` S))); arm_asid_map (arch_state s) a = Some (aa, b); a \<noteq> 0; a \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) a \<notin> S \<longrightarrow> asid_table s (asid_high_bits_of a) \<noteq> Some p; asid_table s ab = Some ba; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; \<exists>rs ra p p' ko. (zs @ [r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bc) = (rs, p) \<and> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) = (ra # rs, p') \<and> ko_at ko p s \<and> (ra, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (ap |` S)))) \<and> (ba \<noteq> p \<longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab \<and> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko)