theory ArchVSpace_AI

lemma mapM_invalidate:
  "\<lbrace>[VSRef (ucast (asid_high_bits_of base)) None] \<rhd> ptr and
    ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) ptr and
    valid_asid_map and K (is_aligned base asid_low_bits)\<rbrace>
       mapM (\<lambda>offset. when (\<exists>y. pool (ucast offset) = Some y)
                       (do y \<leftarrow> flush_space (base + offset);
                           invalidate_asid_entry (base + offset)
                        od))
        [0.e.2 ^ asid_low_bits - 1]
       \<lbrace>\<lambda>rv s. \<forall>x\<le>2 ^ asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None\<rbrace>" proof - have ball: "\<And>P w::word32. (\<forall>x\<le>w. P x) = (\<forall>x \<in> set [0.e.w]. P x)" by simp show ?thesis apply (subst ball) apply (rule mapM_set) apply (wp, simp) apply (wp |
            simp add: invalidate_asid_entry_def invalidate_asid_def
                      invalidate_hw_asid_entry_def
                 cong: if_cong)+ apply clarsimp apply (rule ccontr) apply clarsimp apply (clarsimp simp: valid_asid_map_def) apply (drule bspec, erule graph_ofI) apply (erule vs_lookup_atE) apply (clarsimp simp: vspace_at_asid_def) apply (drule vs_lookup_2ConsD) apply clarsimp apply (erule vs_lookup_atE) apply (drule vs_lookup1D) apply clarsimp apply (subgoal_tac "p' = ptr") apply (clarsimp simp: obj_at_def vs_refs_def graph_of_def) apply (subgoal_tac "base + x && mask asid_low_bits = x") apply (simp add: ucast_ucast_mask) apply (subgoal_tac "aa && mask 32 = aa") apply simp apply (rule word_eqI) apply (simp add: word_size) apply (subst add_mask_eq, assumption+) apply (simp add: asid_low_bits_def word_bits_def) apply (rule refl) apply (subst (asm) asid_high_bits_of_add, assumption+) apply simp apply (wp invalidate_asid_entry_asid_map_None_inv) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits)\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>rv s. \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits)\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>rv s. \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P w. (\<forall>x\<le>w. P x) = (\<forall>x\<in>set [0 .e. w]. P x) proof (state)
this:
(\<forall>x\<le>?w. ?P x) = (\<forall>x\<in>set [0 .e. ?w]. ?P x)

goal (1 subgoal):
 1. \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits)\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>rv s. \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits)\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>rv s. \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits)\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>rv s. \<forall>x\<in>set [0 .e. 2 ^ local.asid_low_bits - 1]. arm_asid_map (arch_state s) (base + x) = None\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1] \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv. [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits)\<rbrace>
 2. \<And>x. x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1] \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + x) = None\<rbrace>
 3. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1] \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + x) = None\<rbrace>
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr) s \<and> ako_at (ASIDPool pool) ptr s \<and> valid_asid_map s \<and> is_aligned base local.asid_low_bits\<rbrakk> \<Longrightarrow> pool (UCAST(32 \<rightarrow> 10) x) = None \<longrightarrow> arm_asid_map (arch_state s) (base + x) = None
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr) s; ako_at (ASIDPool pool) ptr s; valid_asid_map s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) (base + x) = None
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr) s; ako_at (ASIDPool pool) ptr s; valid_asid_map s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) \<noteq> None\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr) s; ako_at (ASIDPool pool) ptr s; valid_asid_map s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b)\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr) s; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr) s; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; case (base + x, a, b) of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; case (base + x, a, b) of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; asid_table s (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; ([VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of (base + x))) None] \<rhd> b) s; base + x \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; \<exists>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of (base + x))) None] \<rhd> p') s \<and> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of (base + x))) None], p'), [VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of (base + x))) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b p'. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of (base + x))) None] \<rhd> p') s; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of (base + x))) None], p'), [VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of (base + x))) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b p'. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of (base + x))) None], p'), [VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of (base + x))) None], b) \<in> vs_lookup1 s; asid_table s (asid_high_bits_of (base + x)) = Some p'\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b p'. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; \<exists>rs r p p'a ko. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of (base + x))) None], p') = (rs, p) \<and> ([VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of (base + x))) None], b) = (r # rs, p'a) \<and> ko_at ko p s \<and> (r, p'a) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' = ptr\<rbrakk> \<Longrightarrow> False
 2. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 3. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x s a aa ba. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some ptr; pool aa = Some ba; base + x && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> False
 2. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 3. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x s a aa ba. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some ptr; pool aa = Some ba; base + x && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa; base + x && mask local.asid_low_bits = x\<rbrakk> \<Longrightarrow> False
 2. \<And>x s a aa ba. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some ptr; pool aa = Some ba; base + x && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> base + x && mask local.asid_low_bits = x
 3. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 4. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x s a aa ba. \<lbrakk>UCAST(10 \<rightarrow> 32) aa \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (aa && mask 32) = None; arm_asid_map (arch_state s) (base + UCAST(10 \<rightarrow> 32) aa) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + UCAST(10 \<rightarrow> 32) aa \<noteq> 0; asid_table s (asid_high_bits_of (base + UCAST(10 \<rightarrow> 32) aa)) = Some ptr; pool aa = Some ba; x = UCAST(10 \<rightarrow> 32) aa; base + UCAST(10 \<rightarrow> 32) aa && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> False
 2. \<And>x s a aa ba. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some ptr; pool aa = Some ba; base + x && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> base + x && mask local.asid_low_bits = x
 3. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 4. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x s a aa ba. \<lbrakk>UCAST(10 \<rightarrow> 32) aa \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (aa && mask 32) = None; arm_asid_map (arch_state s) (base + UCAST(10 \<rightarrow> 32) aa) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + UCAST(10 \<rightarrow> 32) aa \<noteq> 0; asid_table s (asid_high_bits_of (base + UCAST(10 \<rightarrow> 32) aa)) = Some ptr; pool aa = Some ba; x = UCAST(10 \<rightarrow> 32) aa; base + UCAST(10 \<rightarrow> 32) aa && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa; aa && mask 32 = aa\<rbrakk> \<Longrightarrow> False
 2. \<And>x s a aa ba. \<lbrakk>UCAST(10 \<rightarrow> 32) aa \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (aa && mask 32) = None; arm_asid_map (arch_state s) (base + UCAST(10 \<rightarrow> 32) aa) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + UCAST(10 \<rightarrow> 32) aa \<noteq> 0; asid_table s (asid_high_bits_of (base + UCAST(10 \<rightarrow> 32) aa)) = Some ptr; pool aa = Some ba; x = UCAST(10 \<rightarrow> 32) aa; base + UCAST(10 \<rightarrow> 32) aa && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> aa && mask 32 = aa
 3. \<And>x s a aa ba. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some ptr; pool aa = Some ba; base + x && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> base + x && mask local.asid_low_bits = x
 4. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 5. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x s a aa ba. \<lbrakk>UCAST(10 \<rightarrow> 32) aa \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (aa && mask 32) = None; arm_asid_map (arch_state s) (base + UCAST(10 \<rightarrow> 32) aa) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + UCAST(10 \<rightarrow> 32) aa \<noteq> 0; asid_table s (asid_high_bits_of (base + UCAST(10 \<rightarrow> 32) aa)) = Some ptr; pool aa = Some ba; x = UCAST(10 \<rightarrow> 32) aa; base + UCAST(10 \<rightarrow> 32) aa && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> aa && mask 32 = aa
 2. \<And>x s a aa ba. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some ptr; pool aa = Some ba; base + x && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> base + x && mask local.asid_low_bits = x
 3. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 4. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x s a aa ba n. \<lbrakk>UCAST(10 \<rightarrow> 32) aa \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (aa && mask 32) = None; arm_asid_map (arch_state s) (base + UCAST(10 \<rightarrow> 32) aa) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + UCAST(10 \<rightarrow> 32) aa \<noteq> 0; asid_table s (asid_high_bits_of (base + UCAST(10 \<rightarrow> 32) aa)) = Some ptr; pool aa = Some ba; x = UCAST(10 \<rightarrow> 32) aa; base + UCAST(10 \<rightarrow> 32) aa && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> n < size (aa && mask 32) \<longrightarrow> (aa && mask 32) !! n = aa !! n
 2. \<And>x s a aa ba. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some ptr; pool aa = Some ba; base + x && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> base + x && mask local.asid_low_bits = x
 3. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 4. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x s a aa ba. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some ptr; pool aa = Some ba; base + x && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> base + x && mask local.asid_low_bits = x
 2. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 3. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x s a aa ba. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some ptr; pool aa = Some ba; base + x && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> local.asid_low_bits < LENGTH(32)
 2. \<And>x s a aa ba. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some ptr; pool aa = Some ba; base + x && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> x = x
 3. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 4. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x s a aa ba. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; kheap s ptr = Some (ArchObj (ASIDPool pool)); is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, ba); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some ptr; pool aa = Some ba; base + x && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> x = x
 2. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 3. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of (base + x)) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s a b p' ko. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; ako_at (ASIDPool pool) ptr s; is_aligned base local.asid_low_bits; pool (UCAST(32 \<rightarrow> 10) x) = None; arm_asid_map (arch_state s) (base + x) = Some (a, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; asid_table s (asid_high_bits_of base) = Some ptr; base + x \<noteq> 0; asid_table s (asid_high_bits_of base) = Some p'; ko_at ko p' s; (VSRef (base + x && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> p' = ptr
 2. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)\<rbrace> when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y) (do y <- flush_space (base + x);
invalidate_asid_entry (base + x)
od) \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) (base + y) = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x y s. \<lbrakk>x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; y \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits) and (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)) s\<rbrakk> \<Longrightarrow> (if \<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y then \<lambda>s. arm_asid_map (arch_state s) (base + y) = None else (\<lambda>s. arm_asid_map (arch_state s) (base + y) = None)) s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>[VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> ptr and ako_at (ASIDPool pool) ptr and valid_asid_map and K (is_aligned base local.asid_low_bits)\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>rv s. \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None\<rbrace>

goal:
No subgoals!