theory ArchVSpace_AI

lemma perform_asid_pool_invs [wp]:
  "\<lbrace>invs and valid_apinv api\<rbrace> perform_asid_pool_invocation api \<lbrace>\<lambda>_. invs\<rbrace>" apply (clarsimp simp: perform_asid_pool_invocation_def split: asid_pool_invocation.splits) apply (wp arch_update_cap_invs_map set_asid_pool_invs_map
            get_cap_wp set_cap_typ_at
            empty_table_lift[unfolded pred_conj_def, OF _ set_cap_obj_at_other]
            set_cap_obj_at_other
               |wpc|simp|wp (once) hoare_vcg_ex_lift)+ apply (clarsimp simp: valid_apinv_def cte_wp_at_caps_of_state is_arch_update_def is_cap_simps cap_master_cap_simps) apply (frule caps_of_state_cteD) apply (drule cte_wp_valid_cap, fastforce) apply (simp add: valid_cap_def cap_aligned_def) apply (clarsimp simp: cap_asid_def split: option.splits) apply (rule conjI) apply (clarsimp simp: vs_cap_ref_def) apply (rule conjI) apply (erule vs_lookup_atE) apply clarsimp apply (drule caps_of_state_cteD) apply (clarsimp simp: cte_wp_at_cases obj_at_def) apply (rule conjI) apply (rule exI) apply (rule conjI, assumption) apply (rule conjI) apply (rule_tac x=a in exI) apply (rule_tac x=b in exI) apply (clarsimp simp: vs_cap_ref_def mask_asid_low_bits_ucast_ucast) apply (clarsimp simp: asid_low_bits_def[symmetric] ucast_ucast_mask
                         word_neq_0_conv[symmetric]) apply (erule notE, rule asid_low_high_bits, simp_all)[1] apply (simp add: asid_high_bits_of_def) apply (rule conjI) apply (erule(1) valid_table_caps_pdD [OF _ invs_pd_caps]) apply (rule conjI) apply clarsimp apply (drule caps_of_state_cteD) apply (clarsimp simp: obj_at_def cte_wp_at_cases a_type_def) apply (clarsimp split: Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_apinv api\<rbrace> perform_asid_pool_invocation api \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b. api = Assign x1 x2 (a, b) \<Longrightarrow> \<lbrace>invs and valid_apinv (Assign x1 x2 (a, b))\<rbrace> get_cap (a, b) >>= case_cap fail (\<lambda>bool word nat1 nat2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word bool set. fail) (\<lambda>word nat list. fail) (\<lambda>word. fail) fail fail (\<lambda>word. fail) (\<lambda>word option nat. fail) (case_arch_cap (\<lambda>word1 word2. fail) fail (\<lambda>bool word set vmpage_size option. fail) (\<lambda>word option. fail) (\<lambda>pd_base x. do pool <- get_asid_pool x2;
y <- set_cap (ArchObjectCap (PageDirectoryCap pd_base (Some x1))) (a, b);
set_asid_pool x2 (pool(UCAST(32 \<rightarrow> 10) x1 \<mapsto> pd_base))
od)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s. \<lbrakk>api = Assign x1 x2 (a, b); invs s \<and> valid_apinv (Assign x1 x2 (a, b)) s\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (a, b) s \<longrightarrow> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (\<forall>xa. (\<exists>xb. x = PageDirectoryCap xa xb) \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x2 s \<longrightarrow> cte_wp_at (is_arch_update (ArchObjectCap (PageDirectoryCap xa (Some x1))) and (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap xa (Some x1))) = Some r)) (a, b) s \<and> s \<turnstile> ArchObjectCap (PageDirectoryCap xa (Some x1)) \<and> x2 \<noteq> a \<and> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap xa (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> xa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> typ_at (AArch APageDirectory) xa s \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) xa s \<and> xa \<noteq> a \<and> pool (UCAST(32 \<rightarrow> 10) x1) = None))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s pool p asid poola. \<lbrakk>api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; cap_asid (ArchObjectCap (PageDirectoryCap p asid)) = None; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p asid)); ako_at (ASIDPool poola) x2 s\<rbrakk> \<Longrightarrow> (\<forall>r. vs_cap_ref (ArchObjectCap (PageDirectoryCap p asid)) = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some r) \<and> s \<turnstile> ArchObjectCap (PageDirectoryCap p (Some x1)) \<and> x2 \<noteq> a \<and> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> typ_at (AArch APageDirectory) p s \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s pool p asid poola. \<lbrakk>api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; cap_asid (ArchObjectCap (PageDirectoryCap p asid)) = None; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p asid)); ako_at (ASIDPool poola) x2 s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid))) (a, b) s\<rbrakk> \<Longrightarrow> (\<forall>r. vs_cap_ref (ArchObjectCap (PageDirectoryCap p asid)) = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some r) \<and> s \<turnstile> ArchObjectCap (PageDirectoryCap p (Some x1)) \<and> x2 \<noteq> a \<and> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> typ_at (AArch APageDirectory) p s \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s pool p asid poola. \<lbrakk>api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; cap_asid (ArchObjectCap (PageDirectoryCap p asid)) = None; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p asid)); ako_at (ASIDPool poola) x2 s; s \<turnstile> ArchObjectCap (PageDirectoryCap p asid)\<rbrakk> \<Longrightarrow> (\<forall>r. vs_cap_ref (ArchObjectCap (PageDirectoryCap p asid)) = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some r) \<and> s \<turnstile> ArchObjectCap (PageDirectoryCap p (Some x1)) \<and> x2 \<noteq> a \<and> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> typ_at (AArch APageDirectory) p s \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s pool p asid poola. \<lbrakk>api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; cap_asid (ArchObjectCap (PageDirectoryCap p asid)) = None; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p asid)); ako_at (ASIDPool poola) x2 s; is_aligned p 14 \<and> 14 < word_bits \<and> typ_at (AArch APageDirectory) p s \<and> (case asid of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrakk> \<Longrightarrow> (\<forall>r. vs_cap_ref (ArchObjectCap (PageDirectoryCap p asid)) = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some r) \<and> x2 \<noteq> a \<and> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> (\<forall>r. vs_cap_ref (ArchObjectCap (PageDirectoryCap p None)) = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some r) \<and> x2 \<noteq> a \<and> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> \<forall>r. vs_cap_ref (ArchObjectCap (PageDirectoryCap p None)) = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some r
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> x2 \<noteq> a \<and> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> x2 \<noteq> a \<and> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> x2 \<noteq> a
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s; asid_table s (asid_high_bits_of x1) = Some x2\<rbrakk> \<Longrightarrow> x2 \<noteq> a
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) a s; api = Assign x1 a (a, b); invs s; ako_at (ASIDPool pool) a s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s; asid_table s (asid_high_bits_of x1) = Some a\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b s pool p poola. \<lbrakk>ako_at (ASIDPool poola) a s; api = Assign x1 a (a, b); invs s; ako_at (ASIDPool pool) a s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s; asid_table s (asid_high_bits_of x1) = Some a; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p None))) (a, b) s\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> (\<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])) \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # x)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> x \<noteq> [VSRef 0 None])
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> (?x337 x1 x2 a b s pool p poola \<rhd> x2) s \<and> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # ?x337 x1 x2 a b s pool p poola)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool) # ?x337 x1 x2 a b s pool p poola)))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> ?x337 x1 x2 a b s pool p poola \<noteq> [VSRef 0 None])
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> (\<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some [VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None]) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None]))) \<and> (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<noteq> [VSRef 0 None])
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some [VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None]) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None]))
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<noteq> [VSRef 0 None]
 3. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> \<exists>ba. (a = a \<and> ba = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some [VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None]) \<and> ((a = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, ba) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None]))
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<noteq> [VSRef 0 None]
 3. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> (a = a \<and> b = b \<longrightarrow> vs_cap_ref (ArchObjectCap (PageDirectoryCap p (Some x1))) = Some [VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None]) \<and> ((a = a \<longrightarrow> b \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None]))
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<noteq> [VSRef 0 None]
 3. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) = 0 \<longrightarrow> [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<noteq> [VSRef 0 None]
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; x1 \<noteq> 0; x1 < 2 ^ local.asid_bits; ([VSRef 0 None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s; x1 && mask local.asid_low_bits = 0; UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; x1 < 2 ^ local.asid_bits; ([VSRef 0 None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s; x1 && mask local.asid_low_bits = 0; UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1) = 0\<rbrakk> \<Longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of 0) = 0
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<and> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> p \<noteq> a \<and> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> p \<noteq> a
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap a None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned a 14; 14 < word_bits; typ_at (AArch APageDirectory) a s\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s pool poola. \<lbrakk>ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned a 14; 14 < word_bits; typ_at (AArch APageDirectory) a s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap a None))) (a, b) s\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b s poola ko. \<lbrakk>kheap s x2 = Some (ArchObj (ASIDPool poola)); api = Assign x1 x2 (a, b); invs s; poola (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned a 14; 14 < word_bits; (\<exists>sz fun. ko = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> fun b = Some (ArchObjectCap (PageDirectoryCap a None))) \<or> (\<exists>tcb. ko = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> ArchObjectCap (PageDirectoryCap a None) = get tcb)); kheap s a = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s pool p poola. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p None)); ako_at (ASIDPool poola) x2 s; api = Assign x1 x2 (a, b); invs s; ako_at (ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s; is_aligned p 14; 14 < word_bits; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> poola (UCAST(32 \<rightarrow> 10) x1) = None proof (prove)
goal:
No subgoals!