theory ArchVSpace_AI

lemma set_asid_pool_asid_map:
  "\<lbrace>valid_asid_map and ko_at (ArchObj (ASIDPool pool)) ap
    and K (pool asid = None)\<rbrace>
  set_asid_pool ap (pool(asid \<mapsto> pd))
  \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>" apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: a_type_def) apply (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm) apply (clarsimp simp: obj_at_def) apply (clarsimp simp: valid_asid_map_def) apply (drule bspec, blast) 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 (case_tac "p'=ap") apply (clarsimp simp: obj_at_def) apply (rule vs_lookupI) apply (clarsimp simp: vs_asid_refs_def graph_of_def) apply fastforce apply (rule r_into_rtrancl) apply (rule_tac r="VSRef (a && mask asid_low_bits) (Some AASIDPool)" in vs_lookup1I) apply (simp add: obj_at_def) apply (simp add: vs_refs_def graph_of_def) apply fastforce apply simp apply (rule vs_lookupI) apply (clarsimp simp: vs_asid_refs_def graph_of_def) apply fastforce apply (rule r_into_rtrancl) apply (rule vs_lookup1I) apply (simp add: obj_at_def) apply simp apply (simp split: if_splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and ako_at (ASIDPool pool) ap and K (pool asid = None)\<rbrace> set_asid_pool ap (pool(asid \<mapsto> pd)) \<lbrace>\<lambda>rv. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and ako_at (ASIDPool pool) ap and (\<lambda>y. pool asid = None)\<rbrace> do kobj <- get_object ap;
y <- assert (a_type kobj = a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
od \<lbrace>\<lambda>rv. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_asid_map and ako_at (ASIDPool pool) ap and (\<lambda>y. pool asid = None)) s \<Longrightarrow> \<forall>ko. ko_at ko ap s \<longrightarrow> a_type ko = a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) \<longrightarrow> valid_asid_map (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ko_at ko ap s; (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 AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x11 x12. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ko_at (CNode x11 x12) ap s; (if well_formed_cnode_n x11 x12 then ACapTable x11 else AGarbage (cte_level_bits + x11)) = AArch AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x1. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 3. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> vspace_at_asid a b (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) \<and> a \<noteq> 0
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; case (a, aa, b) of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> vspace_at_asid a b (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) \<and> a \<noteq> 0
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; \<exists>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p') s \<and> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b p'. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p') s; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b p'. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s; asid_table s (asid_high_bits_of a) = Some p'\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b p'. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; \<exists>rs r p p'a ko. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p') = (rs, p) \<and> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) = (r # rs, p'a) \<and> ko_at ko p s \<and> (r, p'a) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' = ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 3. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 3. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> ?ref'104 s a aa b \<in> vs_asid_refs (asid_table (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>))
 2. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> (?ref'104 s a aa b, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>))\<^sup>*
 3. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 4. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; arm_asid_map (arch_state s) a = Some (aa, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> ?ref'104 s a aa b \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` {(x, y). asid_table s x = Some y}
 2. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> (?ref'104 s a aa b, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>))\<^sup>*
 3. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 4. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], ap), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>))\<^sup>*
 2. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 3. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], ap), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 3. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> ko_at (?ko119 s a aa b) ap (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (?ko119 s a aa b)
 3. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]
 4. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 5. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a)))
 2. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]
 3. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 4. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; arm_asid_map (arch_state s) a = Some (aa, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). pool x = Some y}\<rbrakk> \<Longrightarrow> (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). (if x = asid then Some pd else pool x) = Some y}
 2. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]
 3. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 4. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s a aa b. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some ap; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]
 2. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 3. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ?ref'141 s x1 a aa b p' ko \<in> vs_asid_refs (asid_table (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>))
 2. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> (?ref'141 s x1 a aa b p' ko, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>))\<^sup>*
 3. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; arm_asid_map (arch_state s) a = Some (aa, b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ?ref'141 s x1 a aa b p' ko \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` {(x, y). asid_table s x = Some y}
 2. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> (?ref'141 s x1 a aa b p' ko, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>))\<^sup>*
 3. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>))\<^sup>*
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> ko_at (?ko156 s x1 a aa b p' ko) p' (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>)
 2. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> (?r156 s x1 a aa b p' ko, b) \<in> vs_refs (?ko156 s x1 a aa b p' ko)
 3. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = [?r156 s x1 a aa b p' ko, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]
 4. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> (?r156 s x1 a aa b p' ko, b) \<in> vs_refs ko
 2. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = [?r156 s x1 a aa b p' ko, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]
 3. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 a aa b p' ko. \<lbrakk>ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (ASIDPool x1) ap s; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; p' \<noteq> ap\<rbrakk> \<Longrightarrow> [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]
 2. \<And>s x41 x42. \<lbrakk>valid_asid_map s; ako_at (ASIDPool pool) ap s; pool asid = None; ako_at (DataPage x41 x42) ap s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!