theory ArchAcc_AI

lemma store_pde_lookup_pd:
  "\<lbrace>\<exists>\<rhd> pd and page_directory_at pd and valid_vspace_objs
     and (\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s)\<rbrace>
  store_pde p pde \<lbrace>\<lambda>_. \<exists>\<rhd> pd\<rbrace>" apply (simp add: store_pde_def set_pd_def set_object_def) apply (wp get_object_wp) apply clarsimp apply (clarsimp simp: obj_at_def) apply (erule vs_lookupE) apply (clarsimp simp: vs_asid_refs_def graph_of_def) apply (drule rtranclD) apply (erule disjE) apply clarsimp apply (rule exI) apply (rule vs_lookup_atI) apply simp apply clarsimp apply (frule (1) valid_asid_tableD) apply (frule vs_lookup_atI) apply (frule (2) stronger_vspace_objsD) apply (clarsimp simp: obj_at_def a_type_def) apply (case_tac ao, simp_all, clarsimp) apply (drule tranclD) apply clarsimp apply (drule rtranclD) apply (erule disjE) apply clarsimp apply (rule_tac x=ref in exI) apply (rule vs_lookup_step) apply (rule vs_lookup_atI) apply simp apply (clarsimp simp: vs_lookup1_def) apply (clarsimp simp: obj_at_def vs_refs_def graph_of_def) apply clarsimp apply (drule (1) vs_lookup_step) apply (frule (2) stronger_vspace_objsD) apply clarsimp apply (drule vs_lookup1D) apply clarsimp apply (erule obj_atE)+ apply (clarsimp simp: vs_refs_def graph_of_def) apply (drule bspec, blast) apply (erule obj_atE)+ apply clarsimp apply (drule tranclD) apply clarsimp apply (drule rtranclD) apply clarsimp apply (drule vs_lookup1D) apply clarsimp apply (erule obj_atE)+ apply (clarsimp simp: vs_refs_def graph_of_def) apply (erule_tac x=ab in ballE) apply (case_tac "pdb ab", simp_all add: pde_ref_def split: if_split_asm) apply (erule obj_atE) apply clarsimp apply (erule disjE) apply (clarsimp simp: a_type_def) apply clarsimp apply (drule tranclD) apply clarsimp apply (drule vs_lookup1D) apply clarsimp apply (erule obj_atE)+ apply (clarsimp simp: vs_refs_def graph_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and valid_vspace_objs and (\<lambda>s. valid_asid_table (asid_table s) s)\<rbrace> store_pde p pde \<lbrace>\<lambda>_ s. \<exists>ref. (ref \<rhd> pd) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and valid_vspace_objs and (\<lambda>s. valid_asid_table (asid_table s) s)\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
kobj <- get_object (p && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>)
od \<lbrace>\<lambda>_ s. \<exists>ref. (ref \<rhd> pd) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and valid_vspace_objs and (\<lambda>s. valid_asid_table (asid_table s) s)) s \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (p && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<longrightarrow> (\<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref ko. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; valid_vspace_objs s; valid_asid_table (asid_table s) s; ako_at (PageDirectory pda) (p && ~~ mask pd_bits) s; ko_at ko (p && ~~ mask pd_bits) s; a_type ko = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa. \<lbrakk>(ref \<rhd> pd) s; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa ref' p'. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); (ref', p') \<in> vs_asid_refs (asid_table s); ((ref', p'), ref, pd) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>*; asid_table s a = Some b\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) = (ref, pd) \<or> ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) \<noteq> (ref, pd) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) = (ref, pd)\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) \<noteq> (ref, pd) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda pdaa a. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some pd\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) \<noteq> (ref, pd) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda pdaa a. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some pd\<rbrakk> \<Longrightarrow> (?ref41 s pda pdaa a \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) \<noteq> (ref, pd) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda pdaa a. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some pd\<rbrakk> \<Longrightarrow> asid_table (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) (?a43 s pda pdaa a) = Some pd
 2. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) \<noteq> (ref, pd) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) \<noteq> (ref, pd) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; typ_at (AArch AASIDPool) b s\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; typ_at (AArch AASIDPool) b s; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; typ_at (AArch AASIDPool) b s; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; \<exists>ao. ako_at ao b s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b ao. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (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) = AASIDPool; kheap s b = Some (ArchObj ao); valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; \<exists>z. (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), z) \<in> vs_lookup1 s \<and> (z, ref, pd) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; (aa, ba) = (ref, pd) \<or> (aa, ba) \<noteq> (ref, pd) \<and> ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; (aa, ba) = (ref, pd)\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; (aa, ba) \<noteq> (ref, pd) \<and> ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 3. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref pdaa a b x1. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; (aa, ba) \<noteq> (ref, pd) \<and> ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 3. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref pdaa a b x1. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; (aa, ba) \<noteq> (ref, pd) \<and> ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 3. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref pdaa a b x1. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (?ref80 s pda ref pdaa a b x1 \<rhd> ?p80 s pda ref pdaa a b x1) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b x1. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((?ref80 s pda ref pdaa a b x1, ?p80 s pda ref pdaa a b x1), ref, pd) \<in> vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 3. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; (aa, ba) \<noteq> (ref, pd) \<and> ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 4. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref pdaa a b x1. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> asid_table (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) (?a83 s pda ref pdaa a b x1) = Some (?p80 s pda ref pdaa a b x1)
 2. \<And>s pda ref pdaa a b x1. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (?a83 s pda ref pdaa a b x1)) None], ?p80 s pda ref pdaa a b x1), ref, pd) \<in> vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 3. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; (aa, ba) \<noteq> (ref, pd) \<and> ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 4. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref pdaa a b x1. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> vs_lookup1 (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; (aa, ba) \<noteq> (ref, pd) \<and> ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 3. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s pda pdaa a b x1 ko r. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; ko_at ko b s; (r, pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> \<exists>ko. ko_at ko b (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) \<and> (r, pd) \<in> vs_refs ko
 2. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; (aa, ba) \<noteq> (ref, pd) \<and> ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 3. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; (aa, ba) \<noteq> (ref, pd) \<and> ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; aa = ref \<longrightarrow> ba \<noteq> pd; ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; aa = ref \<longrightarrow> ba \<noteq> pd; ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; (aa \<rhd> ba) s\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; aa = ref \<longrightarrow> ba \<noteq> pd; ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; (aa \<rhd> ba) s; \<exists>ao. ako_at ao ba s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa ba ao. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), aa, ba) \<in> vs_lookup1 s; aa = ref \<longrightarrow> ba \<noteq> pd; ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; (aa \<rhd> ba) s; ako_at ao ba s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa ba ao. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; aa = ref \<longrightarrow> ba \<noteq> pd; ((aa, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; (aa \<rhd> ba) s; ako_at ao ba s; valid_vspace_obj ao s; \<exists>rs r p p' ko. ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) = (rs, p) \<and> (aa, ba) = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 ba ao r ko. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; [r, VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ba \<noteq> pd; (([r, VSRef (UCAST(7 \<rightarrow> 32) a) None], ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([r, VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> ba) s; ako_at ao ba s; valid_vspace_obj ao s; ko_at ko b s; (r, ba) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 ba ao r ko koa kob. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; kheap s b = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; [r, VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ba \<noteq> pd; (([r, VSRef (UCAST(7 \<rightarrow> 32) a) None], ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([r, VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> ba) s; valid_vspace_obj ao s; (r, ba) \<in> vs_refs ko; kheap s ba = Some koa; ArchObj ao = koa; kheap s b = Some kob; ko = kob\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 ao aa bb. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; (([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bb), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; valid_vspace_obj ao s; kheap s bb = Some (ArchObj ao); kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 ao aa bb. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; (([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bb), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; valid_vspace_obj ao s; kheap s bb = Some (ArchObj ao); kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; typ_at (AArch APageDirectory) bb s\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 ao aa bb ko. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; (([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bb), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; valid_vspace_obj ao s; kheap s bb = Some (ArchObj ao); kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some ko; a_type ko = AArch APageDirectory\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; (([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bb), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdb x) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb))\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdb x) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); \<exists>z. (([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bb), z) \<in> vs_lookup1 s \<and> (z, ref, pd) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdb x) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); (([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bb), ab, ba) \<in> vs_lookup1 s; ((ab, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdb x) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); (([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bb), ab, ba) \<in> vs_lookup1 s; (ab, ba) = (ref, pd) \<or> (ab, ba) \<noteq> (ref, pd) \<and> ((ab, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdb x) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); (([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bb), ab, ba) \<in> vs_lookup1 s; ab = ref \<and> ba = pd \<or> (ab = ref \<longrightarrow> ba \<noteq> pd) \<and> ((ab, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdb x) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab = ref \<and> ba = pd \<or> (ab = ref \<longrightarrow> ba \<noteq> pd) \<and> ((ab, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; \<exists>rs r p p' ko. ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bb) = (rs, p) \<and> (ab, ba) = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ba r ko. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdb x) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); [r, VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<and> ba = pd \<or> ([r, VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ba \<noteq> pd) \<and> (([r, VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ko_at ko bb s; (r, ba) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ba r ko koa. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdb x) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); [r, VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<and> ba = pd \<or> ([r, VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ba \<noteq> pd) \<and> (([r, VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; (r, ba) \<in> vs_refs ko; kheap s bb = Some koa; ko = koa\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab bc. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdb x) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<and> bc = pd \<or> ([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bc \<noteq> pd) \<and> (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bc), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; kheap s bb = Some (ArchObj (PageDirectory pdb)); (if ab \<in> kernel_mapping_slots then None else pde_ref (pdb ab)) = Some bc\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab bc. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<and> bc = pd \<or> ([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bc \<noteq> pd) \<and> (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bc), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; kheap s bb = Some (ArchObj (PageDirectory pdb)); (if ab \<in> kernel_mapping_slots then None else pde_ref (pdb ab)) = Some bc; valid_pde (pdb ab) s\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b x1 aa bb pdb ab bc. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<and> bc = pd \<or> ([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bc \<noteq> pd) \<and> (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bc), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; kheap s bb = Some (ArchObj (PageDirectory pdb)); (if ab \<in> kernel_mapping_slots then None else pde_ref (pdb ab)) = Some bc; ab \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 3. \<And>s pda ref pdaa a b ao x41 x42. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> b) s; (if x41 then ADeviceData x42 else AUserData x42) = AASIDPool; kheap s b = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab bc x21 x22 x23. \<lbrakk>typ_at (AArch APageTable) bc s; pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<and> bc = pd \<or> ([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bc \<noteq> pd) \<and> (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bc), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; ptrFromPAddr x21 = bc\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab bc x21 x22 x23 ko. \<lbrakk>pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<and> bc = pd \<or> ([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bc \<noteq> pd) \<and> (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], bc), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; ptrFromPAddr x21 = bc; kheap s bc = Some ko; a_type ko = AArch APageTable\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab x21 x22 x23 pt. \<lbrakk>pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<and> ptrFromPAddr x21 = pd \<or> ([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ptrFromPAddr x21 \<noteq> pd) \<and> (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr x21), ref, pd) \<in> (vs_lookup1 s)\<^sup>+; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab x21 x22 x23 pt. \<lbrakk>pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<and> ptrFromPAddr x21 = pd\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>)
 2. \<And>s pda ref pdaa a b x1 aa bb pdb ab x21 x22 x23 pt. \<lbrakk>pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); ([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ptrFromPAddr x21 \<noteq> pd) \<and> (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr x21), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab x21 x22 x23 pt. \<lbrakk>pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); ([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ptrFromPAddr x21 \<noteq> pd) \<and> (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr x21), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab x21 x22 x23 pt. \<lbrakk>pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ptrFromPAddr x21 \<noteq> pd; (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr x21), ref, pd) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab x21 x22 x23 pt. \<lbrakk>pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ptrFromPAddr x21 \<noteq> pd; \<exists>z. (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr x21), z) \<in> vs_lookup1 s \<and> (z, ref, pd) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab x21 x22 x23 pt ac ba. \<lbrakk>pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ptrFromPAddr x21 \<noteq> pd; (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr x21), ac, ba) \<in> vs_lookup1 s; ((ac, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab x21 x22 x23 pt ac ba. \<lbrakk>pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ptrFromPAddr x21 \<noteq> pd; ((ac, ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>*; \<exists>rs r p p' ko. ([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr x21) = (rs, p) \<and> (ac, ba) = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab x21 x22 x23 pt ba r ko. \<lbrakk>pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ptrFromPAddr x21 \<noteq> pd; (([r, VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko (ptrFromPAddr x21) s; (r, ba) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref pdaa a b x1 aa bb pdb ab x21 x22 x23 pt ba r ko koa. \<lbrakk>pdb ab = PageTablePDE x21 x22 x23; valid_vspace_objs s; valid_asid_table (asid_table s) s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); asid_table s a = Some b; [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> b \<noteq> pd; [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> bb \<noteq> pd; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> bb) s; kheap s b = Some (ArchObj (ASIDPool x1)); x1 aa = Some bb; kheap s bb = Some (ArchObj (PageDirectory pdb)); ab \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref \<longrightarrow> ptrFromPAddr x21 \<noteq> pd; (([r, VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ba), ref, pd) \<in> (vs_lookup1 s)\<^sup>*; (r, ba) \<in> vs_refs ko; kheap s (ptrFromPAddr x21) = Some koa; ko = koa\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pd) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pda a))) else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!