theory ArchVSpace_AI

lemma valid_asid_map_unmap:
  "valid_asid_map s \<and> is_aligned base asid_low_bits \<and> base \<le> mask asid_bits \<and>
   (\<forall>x \<in> set [0.e.2^asid_low_bits - 1]. arm_asid_map (arch_state s) (base + x) = None) \<longrightarrow>
   valid_asid_map(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(asid_high_bits_of base := None)\<rparr>\<rparr>)" apply (clarsimp simp: valid_asid_map_def vspace_at_asid_def) apply (drule bspec, blast) apply clarsimp apply (erule vs_lookupE) apply (clarsimp simp: vs_asid_refs_def dest!: graph_ofD) apply (frule vs_lookup1_trans_is_append, clarsimp) apply (drule ucast_up_inj, simp) apply clarsimp apply (rule_tac ref'="([VSRef (ucast (asid_high_bits_of a)) None],ba)" in vs_lookupI) apply (simp add: vs_asid_refs_def) apply (simp add: graph_of_def) apply (rule_tac x="(asid_high_bits_of a, ba)" in image_eqI) apply simp apply clarsimp apply (subgoal_tac "a \<le> mask asid_bits") prefer 2 apply fastforce apply (drule_tac asid=a in ex_asid_high_bits_plus) apply (clarsimp simp: asid_high_bits_shl) apply (drule rtranclD, simp) apply (drule tranclD) apply clarsimp apply (drule vs_lookup1D) apply clarsimp apply (frule vs_lookup1_trans_is_append, clarsimp) apply (drule vs_lookup_trans_ptr_eq, clarsimp) apply (rule r_into_rtrancl) apply (rule vs_lookup1I) apply simp apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_map s \<and> is_aligned base local.asid_low_bits \<and> base \<le> mask local.asid_bits \<and> (\<forall>x\<in>set [0 .e. 2 ^ local.asid_low_bits - 1]. arm_asid_map (arch_state s) (base + x) = None) \<longrightarrow> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); 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> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; case (a, aa, b) of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; ([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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ref' p'. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba\<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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None] \<rhd> b) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; asid_high_bits_of a = ab\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None] \<rhd> b) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], ba) \<in> vs_asid_refs (asid_table (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))
 2. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], ba) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` (graph_of (asid_table s) - {asid_high_bits_of base} \<times> UNIV)
 2. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], ba) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` ({(x, y). asid_table s x = Some y} - {asid_high_bits_of base} \<times> UNIV)
 2. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], ba) = (case (asid_high_bits_of a, ba) of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p))
 2. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (asid_high_bits_of a, ba) \<in> {(x, y). asid_table s x = Some y} - {asid_high_bits_of base} \<times> UNIV
 3. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (asid_high_bits_of a, ba) \<in> {(x, y). asid_table s x = Some y} - {asid_high_bits_of base} \<times> UNIV
 2. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], b) \<in> (vs_lookup1 s)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of base) = Some ba; asid_high_bits_of a = asid_high_bits_of base\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], b) \<in> (vs_lookup1 s)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of base) = Some ba; asid_high_bits_of a = asid_high_bits_of base; a \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], b) \<in> (vs_lookup1 s)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of base) = Some ba; asid_high_bits_of a = asid_high_bits_of base\<rbrakk> \<Longrightarrow> a \<le> mask local.asid_bits
 3. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], b) \<in> (vs_lookup1 s)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of base) = Some ba; asid_high_bits_of a = asid_high_bits_of base\<rbrakk> \<Longrightarrow> a \<le> mask local.asid_bits
 2. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], b) \<in> (vs_lookup1 s)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of base) = Some ba; asid_high_bits_of a = asid_high_bits_of base; a \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], b) \<in> (vs_lookup1 s)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of base) = Some ba; asid_high_bits_of a = asid_high_bits_of base; a \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], b) \<in> (vs_lookup1 s)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of base) = Some ba; asid_high_bits_of a = asid_high_bits_of base; \<exists>x\<le>2 ^ local.asid_low_bits - 1. a = (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) << local.asid_low_bits) + x\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; \<exists>z. (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba ab bb. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], ba), ab, bb) \<in> vs_lookup1 s; ((ab, 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) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba ab bb. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; ((ab, 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) (asid_high_bits_of a)) None], ba) = (rs, p) \<and> (ab, bb) = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba bb r ko. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; (([r, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba bb ko. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba ko. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba ko. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) 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>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ba ko. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ko_at (?ko86 a aa b ba ko) ba (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>)
 2. \<And>a aa b ba ko. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r86 a aa b ba ko, b) \<in> vs_refs (?ko86 a aa b ba ko)
 3. \<And>a aa b ba ko. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = [?r86 a aa b ba ko, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba ko. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r86 a aa b ba ko, b) \<in> vs_refs ko
 2. \<And>a aa b ba ko. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = [?r86 a aa b ba ko, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba ko. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s (asid_high_bits_of a) = Some ba; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] proof (prove)
goal:
No subgoals!