theory ArchAcc_AI

lemma set_pd_asid_map [wp]:
  "\<lbrace>valid_asid_map\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: a_type_def simp del: fun_upd_apply
                  split: kernel_object.splits
                         arch_kernel_obj.splits) apply (clarsimp simp: valid_asid_map_def) apply (drule bspec, blast) apply (clarsimp simp: vspace_at_asid_def obj_at_def) apply (erule vs_lookupE) apply (rule vs_lookupI, simp) apply (clarsimp simp: vs_asid_refs_def dest!: graph_ofD) apply (frule vs_lookup1_trans_is_append) apply clarsimp apply (drule rtranclD) apply clarsimp apply (drule tranclD) apply clarsimp apply (drule vs_lookup1D) apply clarsimp apply (rule rtrancl_trans) apply (rule r_into_rtrancl) apply (rule vs_lookup1I) apply (clarsimp simp: obj_at_def) apply (rule conjI, clarsimp) prefer 2 apply clarsimp apply (rule refl) apply clarsimp apply (clarsimp simp: vs_refs_def) apply (drule vs_lookup1_trans_is_append) apply clarsimp apply assumption apply (rule refl) apply (frule vs_lookup1_trans_is_append, clarsimp) apply (drule rtranclD) apply (erule disjE, clarsimp) apply clarsimp apply (drule tranclD) apply clarsimp apply (drule vs_lookup1D) apply clarsimp apply (drule vs_lookup1_trans_is_append, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory pd)));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
od \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_asid_map s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory pd)) \<longrightarrow> valid_asid_map (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x3. \<lbrakk>valid_asid_map s; ako_at (PageDirectory x3) p s\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b. \<lbrakk>ako_at (PageDirectory x3) p 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 := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b. \<lbrakk>ako_at (PageDirectory x3) p 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 := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); (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 := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ref' p'. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); (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; (ref', p') \<in> vs_asid_refs (asid_table s); ((ref', 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)\<^sup>*\<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 := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ref' p'. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); (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; (ref', p') \<in> vs_asid_refs (asid_table s); ((ref', 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)\<^sup>*\<rbrakk> \<Longrightarrow> ((ref', 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 := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [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)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [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 := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [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)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; \<exists>zs. [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] = zs @ [VSRef (UCAST(7 \<rightarrow> 32) ab) None]\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [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 := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; ([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba) = ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<or> ([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba) \<noteq> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; \<exists>z. (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), z) \<in> vs_lookup1 s \<and> (z, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba ac bb. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), ac, bb) \<in> vs_lookup1 s; ((ac, bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba ac bb. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; ((ac, bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; \<exists>rs r p p' ko. ([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba) = (rs, p) \<and> (ac, bb) = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), ?y86 s x3 a aa b ab ba bb r ko) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>*
 2. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?y86 s x3 a aa b ab ba bb r ko, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), ?y86 s x3 a aa b ab ba bb r ko) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?y86 s x3 a aa b ab ba bb r ko, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (4 subgoals):
 1. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ko_at (?ko91 s x3 a aa b ab ba bb r ko) ba (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko) \<in> vs_refs (?ko91 s x3 a aa b ab ba bb r ko)
 3. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ?rs'91 s x3 a aa b ab ba bb r ko = [?r91 s x3 a aa b ab ba bb r ko, VSRef (UCAST(7 \<rightarrow> 32) ab) None]
 4. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((?rs'91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (4 subgoals):
 1. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (ba = p \<longrightarrow> ArchObj (PageDirectory pd) = ?ko91 s x3 a aa b ab p bb r ko) \<and> (ba \<noteq> p \<longrightarrow> ko = ?ko91 s x3 a aa b ab ba bb r ko)
 2. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko) \<in> vs_refs (?ko91 s x3 a aa b ab ba bb r ko)
 3. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ?rs'91 s x3 a aa b ab ba bb r ko = [?r91 s x3 a aa b ab ba bb r ko, VSRef (UCAST(7 \<rightarrow> 32) ab) None]
 4. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((?rs'91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (5 subgoals):
 1. \<And>s x3 a aa b ab bb r. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some p; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; kheap s p = Some (ArchObj (PageDirectory x3)); (r, bb) \<in> vs_refs (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> ArchObj (PageDirectory pd) = ?ko91 s x3 a aa b ab p bb r (ArchObj (PageDirectory x3))
 2. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ba \<noteq> p \<longrightarrow> ko = ?ko91 s x3 a aa b ab ba bb r ko
 3. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko) \<in> vs_refs (?ko91 s x3 a aa b ab ba bb r ko)
 4. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ?rs'91 s x3 a aa b ab ba bb r ko = [?r91 s x3 a aa b ab ba bb r ko, VSRef (UCAST(7 \<rightarrow> 32) ab) None]
 5. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((?rs'91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (5 subgoals):
 1. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ba \<noteq> p \<longrightarrow> ko = ?ko91 s x3 a aa b ab ba bb r ko
 2. \<And>s x3 a aa b ab bb r. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some p; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; kheap s p = Some (ArchObj (PageDirectory x3)); (r, bb) \<in> vs_refs (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> ArchObj (PageDirectory pd) = ?ko91 s x3 a aa b ab p bb r (ArchObj (PageDirectory x3))
 3. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko) \<in> vs_refs (?ko91 s x3 a aa b ab ba bb r ko)
 4. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ?rs'91 s x3 a aa b ab ba bb r ko = [?r91 s x3 a aa b ab ba bb r ko, VSRef (UCAST(7 \<rightarrow> 32) ab) None]
 5. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((?rs'91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (5 subgoals):
 1. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; kheap s ba = Some ko; (r, bb) \<in> vs_refs ko; ba \<noteq> p\<rbrakk> \<Longrightarrow> ko = ?ko91 s x3 a aa b ab ba bb r ko
 2. \<And>s x3 a aa b ab bb r. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some p; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; kheap s p = Some (ArchObj (PageDirectory x3)); (r, bb) \<in> vs_refs (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> ArchObj (PageDirectory pd) = ?ko91 s x3 a aa b ab p bb r (ArchObj (PageDirectory x3))
 3. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko) \<in> vs_refs (?ko91 s x3 a aa b ab ba bb r ko)
 4. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ?rs'91 s x3 a aa b ab ba bb r ko = [?r91 s x3 a aa b ab ba bb r ko, VSRef (UCAST(7 \<rightarrow> 32) ab) None]
 5. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((?rs'91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (4 subgoals):
 1. \<And>s x3 a aa b ab bb r. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some p; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; kheap s p = Some (ArchObj (PageDirectory x3)); (r, bb) \<in> vs_refs (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> ArchObj (PageDirectory pd) = ArchObj (PageDirectory x3)
 2. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko) \<in> vs_refs ko
 3. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ?rs'91 s x3 a aa b ab ba bb r ko = [?r91 s x3 a aa b ab ba bb r ko, VSRef (UCAST(7 \<rightarrow> 32) ab) None]
 4. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((?rs'91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (4 subgoals):
 1. \<And>s x3 a aa b ab bb r. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some p; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; kheap s p = Some (ArchObj (PageDirectory x3)); (r, bb) \<in> vs_refs (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> pd = x3
 2. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko) \<in> vs_refs ko
 3. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ?rs'91 s x3 a aa b ab ba bb r ko = [?r91 s x3 a aa b ab ba bb r ko, VSRef (UCAST(7 \<rightarrow> 32) ab) None]
 4. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((?rs'91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (4 subgoals):
 1. \<And>s x3 a aa b ab ac ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some p; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; kheap s p = Some (ArchObj (PageDirectory x3)); (ac, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x))\<rbrakk> \<Longrightarrow> pd = x3
 2. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko) \<in> vs_refs ko
 3. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ?rs'91 s x3 a aa b ab ba bb r ko = [?r91 s x3 a aa b ab ba bb r ko, VSRef (UCAST(7 \<rightarrow> 32) ab) None]
 4. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((?rs'91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (4 subgoals):
 1. \<And>s x3 a aa b ab ac ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some p; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; kheap s p = Some (ArchObj (PageDirectory x3)); (ac, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)); \<exists>zs. [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None] = zs @ [VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), VSRef (UCAST(7 \<rightarrow> 32) ab) None]\<rbrakk> \<Longrightarrow> pd = x3
 2. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko) \<in> vs_refs ko
 3. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ?rs'91 s x3 a aa b ab ba bb r ko = [?r91 s x3 a aa b ab ba bb r ko, VSRef (UCAST(7 \<rightarrow> 32) ab) None]
 4. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((?rs'91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko) \<in> vs_refs ko
 2. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ?rs'91 s x3 a aa b ab ba bb r ko = [?r91 s x3 a aa b ab ba bb r ko, VSRef (UCAST(7 \<rightarrow> 32) ab) None]
 3. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((?rs'91 s x3 a aa b ab ba bb r ko, ?p'91 s x3 a aa b ab ba bb r ko), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ?rs'91 s x3 a aa b ab ba bb r ko = [r, VSRef (UCAST(7 \<rightarrow> 32) ab) None]
 2. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ((?rs'91 s x3 a aa b ab ba bb r ko, bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba bb r ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (r, bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([r, VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba bb ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), bb) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba bb ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), bb) \<in> vs_refs ko; ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb) = ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<or> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb) \<noteq> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<and> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba bb ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), bb) \<in> vs_refs ko; ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb) \<noteq> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<and> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba bb ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), bb) \<in> vs_refs ko; bb \<noteq> b; (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba bb ko. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), bb) \<in> vs_refs ko; bb \<noteq> b; \<exists>z. (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), z) \<in> vs_lookup1 s \<and> (z, [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba bb ko ac bc. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), bb) \<in> vs_refs ko; bb \<noteq> b; (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), ac, bc) \<in> vs_lookup1 s; ((ac, bc), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba bb ko ac bc. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), bb) \<in> vs_refs ko; bb \<noteq> b; ((ac, bc), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; \<exists>rs r p p' ko. ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb) = (rs, p) \<and> (ac, bc) = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x3 a aa b ab ba bb ko bc r koa. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; arm_asid_map (arch_state s) a = Some (aa, b); asid_table s ab = Some ba; UCAST(7 \<rightarrow> 32) (asid_high_bits_of a) = UCAST(7 \<rightarrow> 32) ab; ko_at ko ba s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), bb) \<in> vs_refs ko; bb \<noteq> b; (([r, VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bc), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at koa bb s; (r, bc) \<in> vs_refs koa\<rbrakk> \<Longrightarrow> (([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<^sup>* proof (prove)
goal:
No subgoals!