theory ArchFinalise_AI

lemma delete_asid_invs[wp]:
  "\<lbrace>invs and K (asid \<le> mask asid_bits)\<rbrace>
     delete_asid asid pd
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: delete_asid_def cong: option.case_cong) apply (wp set_asid_pool_invs_unmap | wpc)+ apply (simp add: invalidate_asid_entry_def invalidate_asid_def invalidate_hw_asid_entry_def) apply (wp load_hw_asid_wp)+ apply (simp add: flush_space_def) apply (wp load_hw_asid_wp|wpc)+ apply (clarsimp simp del: fun_upd_apply) apply (subgoal_tac "valid_asid_table (arm_asid_table (arch_state s)) s") prefer 2 apply fastforce apply (clarsimp simp: valid_asid_table_def) apply (rule conjI) apply clarsimp apply (subgoal_tac "asid_high_bits_of asid = asid_high_bits_of asida") prefer 2 apply (fastforce elim!: inj_onD) apply (drule asid_low_high_bits', simp) apply (simp add: mask_def) apply (simp add: mask_def) apply blast apply clarsimp apply (subgoal_tac "asid_high_bits_of asid = asid_high_bits_of asida") prefer 2 apply (fastforce elim!: inj_onD) apply (drule asid_low_high_bits', simp) apply (simp add: mask_def) apply (simp add: mask_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (asid \<le> mask local.asid_bits)\<rbrace> delete_asid asid pd \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>y. asid \<le> mask local.asid_bits)\<rbrace> do asid_table <- gets (arm_asid_table \<circ> arch_state);
case asid_table (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>asid_tablea x2 pool y. \<lbrakk>asid_tablea (asid_high_bits_of asid) = Some x2; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?P'34 asid_tablea x2 pool y\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. \<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x2 \<longrightarrow> arm_asid_map (arch_state s) asida = None\<rbrace>
 2. \<And>asid_table x2 pool. \<lbrakk>asid_table (asid_high_bits_of asid) = Some x2; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?Q22 asid_table x2 pool\<rbrace> flush_space asid \<lbrace>\<lambda>y s. invs s \<and> ako_at (ASIDPool pool) x2 s \<and> ?P'34 asid_table x2 pool y s\<rbrace>
 3. \<And>asid_table x2. asid_table (asid_high_bits_of asid) = Some x2 \<Longrightarrow> \<lbrace>?R15 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) asid) = Some pd then ?Q22 asid_table x2 pool else invs\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of asid) = None \<longrightarrow> invs s) \<and> (\<forall>x. asid_table (asid_high_bits_of asid) = Some x \<longrightarrow> ?R15 asid_table x s)\<rbrace>
 5. \<And>s. (invs and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (5 subgoals):
 1. \<And>asid_tablea x2 pool. \<lbrakk>asid_tablea (asid_high_bits_of asid) = Some x2; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?P'34 asid_tablea x2 pool ()\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
y <- when (\<exists>y. maybe_hw_asid = Some y) (do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(the maybe_hw_asid := None)\<rparr>\<rparr>)
od);
asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(asid := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>rv s. \<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x2 \<longrightarrow> arm_asid_map (arch_state s) asida = None\<rbrace>
 2. \<And>asid_table x2 pool. \<lbrakk>asid_table (asid_high_bits_of asid) = Some x2; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?Q22 asid_table x2 pool\<rbrace> flush_space asid \<lbrace>\<lambda>y s. invs s \<and> ako_at (ASIDPool pool) x2 s \<and> ?P'34 asid_table x2 pool y s\<rbrace>
 3. \<And>asid_table x2. asid_table (asid_high_bits_of asid) = Some x2 \<Longrightarrow> \<lbrace>?R15 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) asid) = Some pd then ?Q22 asid_table x2 pool else invs\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of asid) = None \<longrightarrow> invs s) \<and> (\<forall>x. asid_table (asid_high_bits_of asid) = Some x \<longrightarrow> ?R15 asid_table x s)\<rbrace>
 5. \<And>s. (invs and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>asid_tablea x2 pool. \<lbrakk>asid_tablea (asid_high_bits_of asid) = Some x2; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?P'57 asid_tablea x2 pool\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. (if \<exists>y. map_option fst (arm_asid_map (arch_state s) asid) = Some y then \<lambda>sa. \<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>, arch_state := arch_state (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>)\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>))(asid := None)\<rparr>\<rparr>) (asid_high_bits_of asida) = Some x2 \<longrightarrow> arm_asid_map (arch_state (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>, arch_state := arch_state (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>)\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>))(asid := None)\<rparr>\<rparr>)) asida = None else (\<lambda>s. \<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid := None)\<rparr>\<rparr>) (asid_high_bits_of asida) = Some x2 \<longrightarrow> arm_asid_map (arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid := None)\<rparr>\<rparr>)) asida = None)) s\<rbrace>
 2. \<And>asid_table x2. asid_table (asid_high_bits_of asid) = Some x2 \<Longrightarrow> \<lbrace>?R15 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) asid) = Some pd then \<lambda>s. invs s \<and> ako_at (ASIDPool pool) x2 s \<and> ?P'57 asid_table x2 pool s else invs\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of asid) = None \<longrightarrow> invs s) \<and> (\<forall>x. asid_table (asid_high_bits_of asid) = Some x \<longrightarrow> ?R15 asid_table x s)\<rbrace>
 4. \<And>s. (invs and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>asid_tablea x2 pool. \<lbrakk>asid_tablea (asid_high_bits_of asid) = Some x2; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?P'57 asid_tablea x2 pool\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
y <- do_machine_op cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op $ invalidateLocalTLB_ASID hw_asid
od \<lbrace>\<lambda>rv s. ((\<exists>y b. arm_asid_map (arch_state s) asid = Some (y, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x2 \<longrightarrow> arm_asid_map (arch_state s) asida = None)) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x2 \<longrightarrow> arm_asid_map (arch_state s) asida = None))\<rbrace>
 2. \<And>asid_table x2. asid_table (asid_high_bits_of asid) = Some x2 \<Longrightarrow> \<lbrace>?R15 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) asid) = Some pd then \<lambda>s. invs s \<and> ako_at (ASIDPool pool) x2 s \<and> ?P'57 asid_table x2 pool s else invs\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of asid) = None \<longrightarrow> invs s) \<and> (\<forall>x. asid_table (asid_high_bits_of asid) = Some x \<longrightarrow> ?R15 asid_table x s)\<rbrace>
 4. \<And>s. (invs and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> ((arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = None \<longrightarrow> invs s) \<and> (\<forall>x. (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = Some x \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x s \<longrightarrow> (if pool (UCAST(32 \<rightarrow> 10) asid) = Some pd then \<lambda>s. invs s \<and> ako_at (ASIDPool pool) x s \<and> (map_option fst (arm_asid_map (arch_state s) asid) = None \<longrightarrow> ((\<exists>y b. arm_asid_map (arch_state s) asid = Some (y, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None))) \<and> (\<forall>xa. map_option fst (arm_asid_map (arch_state s) asid) = Some xa \<longrightarrow> ((\<exists>y b. arm_asid_map (arch_state s) asid = Some (y, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None))) else invs) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s\<rbrakk> \<Longrightarrow> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) \<and> ((\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None))) proof (prove)
goal (2 subgoals):
 1. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) \<and> ((\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)))
 2. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s proof (prove)
goal (2 subgoals):
 1. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s
 2. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) \<and> ((\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None))) proof (prove)
goal (1 subgoal):
 1. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) \<and> ((\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None))) proof (prove)
goal (1 subgoal):
 1. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) \<and> ((\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None))) proof (prove)
goal (2 subgoals):
 1. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)
 2. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) proof (prove)
goal (2 subgoals):
 1. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None
 2. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) proof (prove)
goal (3 subgoals):
 1. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None
 2. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x\<rbrakk> \<Longrightarrow> asid_high_bits_of asid = asid_high_bits_of asida
 3. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) proof (prove)
goal (3 subgoals):
 1. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x\<rbrakk> \<Longrightarrow> asid_high_bits_of asid = asid_high_bits_of asida
 2. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None
 3. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) proof (prove)
goal (2 subgoals):
 1. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None
 2. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) proof (prove)
goal (4 subgoals):
 1. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> asida \<le> 2 ^ local.asid_bits - 1
 2. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> asid \<le> 2 ^ local.asid_bits - 1
 3. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida; asida = asid\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None
 4. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) proof (prove)
goal (3 subgoals):
 1. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> asid \<le> 2 ^ local.asid_bits - 1
 2. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida; asida = asid\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None
 3. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) proof (prove)
goal (2 subgoals):
 1. \<And>s x pool asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = None; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida; asida = asid\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None
 2. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) proof (prove)
goal (1 subgoal):
 1. \<And>s x pool. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (\<exists>x b. arm_asid_map (arch_state s) asid = Some (x, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x \<longrightarrow> arm_asid_map (arch_state s) asida = None)) proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (2 subgoals):
 1. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None
 2. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x\<rbrakk> \<Longrightarrow> asid_high_bits_of asid = asid_high_bits_of asida proof (prove)
goal (2 subgoals):
 1. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x\<rbrakk> \<Longrightarrow> asid_high_bits_of asid = asid_high_bits_of asida
 2. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (3 subgoals):
 1. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> asida \<le> 2 ^ local.asid_bits - 1
 2. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> asid \<le> 2 ^ local.asid_bits - 1
 3. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida; asida = asid\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (2 subgoals):
 1. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> asid \<le> 2 ^ local.asid_bits - 1
 2. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida; asida = asid\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa b asida. \<lbrakk>invs s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); arm_asid_map (arch_state s) asid = Some (xa, b); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some x; asid_high_bits_of asid = asid_high_bits_of asida; asida = asid\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal:
No subgoals!