theory ArchFinalise_AI

lemma set_asid_pool_empty_valid_asid_map:
  "\<lbrace>\<lambda>s. valid_asid_map s \<and> asid_pool_at p s
       \<and> (\<forall>asid'. \<not> ([VSRef asid' None] \<rhd> p) s)
       \<and> (\<forall>p'. \<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p') s)\<rbrace>
       set_asid_pool p Map.empty
   \<lbrace>\<lambda>rv s. 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 \<mapsto> p)\<rparr>\<rparr>)\<rbrace>" apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: valid_asid_map_def vspace_at_asid_def
                 dest!: graph_ofD
                 split: Structures_A.kernel_object.split_asm
                        arch_kernel_obj.split_asm) apply (drule bspec, erule graph_ofI) apply (clarsimp dest!: vs_lookup_2ConsD vs_lookup1D) apply (case_tac "p = pa") apply simp apply (clarsimp elim!: vs_lookup_atE) apply (rule vs_lookupI[rotated]) apply (rule r_into_rtrancl) apply (rule_tac p=pa in vs_lookup1I) apply (simp add: obj_at_def) apply assumption apply simp apply (rule vs_asid_refsI) apply clarsimp apply (drule vs_asid_refsI) apply (drule vs_lookupI, rule rtrancl_refl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_asid_map s \<and> typ_at (AArch AASIDPool) p s \<and> (\<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s) \<and> (\<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s)\<rbrace> set_asid_pool p (\<lambda>x. None) \<lbrace>\<lambda>rv s. valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_asid_map s \<and> typ_at (AArch AASIDPool) p s \<and> (\<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s) \<and> (\<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s)\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (ASIDPool (\<lambda>x. None))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>)
od \<lbrace>\<lambda>rv s. valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_asid_map s \<and> typ_at (AArch AASIDPool) p s \<and> (\<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s) \<and> (\<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s) \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))) \<longrightarrow> valid_asid_map (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>)\<lparr>arm_asid_table := (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>) 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> ([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; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, b)\<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 := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<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}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, b); 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>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> pa) s; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p'a) (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> pa) s; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p = pa\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p'a) (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)
 2. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> pa) s; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p'a) (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> pa) s; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p'a) (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p'a) (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> (?ref'52 s ko a aa pa p'a koa, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p'a) \<in> (vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>))\<^sup>*
 2. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> ?ref'52 s ko a aa pa p'a koa \<in> vs_asid_refs (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> (?ref'52 s ko a aa pa p'a koa, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p'a) \<in> vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)
 2. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> ?ref'52 s ko a aa pa p'a koa \<in> vs_asid_refs (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)) proof (prove)
goal (4 subgoals):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> ko_at (?ko57 s ko a aa pa p'a koa) pa (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)
 2. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> (?r57 s ko a aa pa p'a koa, p'a) \<in> vs_refs (?ko57 s ko a aa pa p'a koa)
 3. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = ?r57 s ko a aa pa p'a koa # ?rs57 s ko a aa pa p'a koa
 4. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> (?rs57 s ko a aa pa p'a koa, pa) \<in> vs_asid_refs (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> (?r57 s ko a aa pa p'a koa, p'a) \<in> vs_refs koa
 2. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = ?r57 s ko a aa pa p'a koa # ?rs57 s ko a aa pa p'a koa
 3. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> (?rs57 s ko a aa pa p'a koa, pa) \<in> vs_asid_refs (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<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) # ?rs57 s ko a aa pa p'a koa
 2. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> (?rs57 s ko a aa pa p'a koa, pa) \<in> vs_asid_refs (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], pa) \<in> vs_asid_refs (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of a) = Some pa\<rbrakk> \<Longrightarrow> asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (ASIDPool (\<lambda>x. None))) else kheap s a, arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>) (asid_high_bits_of a) = Some pa proof (prove)
goal (1 subgoal):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_table s (asid_high_bits_of base) = Some pa; asid_high_bits_of a = asid_high_bits_of base\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_high_bits_of a = asid_high_bits_of base; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], pa) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ko a aa pa p'a koa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; typ_at (AArch AASIDPool) p s; \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool (\<lambda>x. None))); arm_asid_map (arch_state s) a = Some (aa, p'a); a \<noteq> 0; ko_at koa pa s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> vs_refs koa; p \<noteq> pa; asid_high_bits_of a = asid_high_bits_of base; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> pa) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!