theory ArchVSpace_AI

lemma store_pde_pd_at_asid:
  "\<lbrace>vspace_at_asid asid pd\<rbrace>
  store_pde p pde \<lbrace>\<lambda>_. vspace_at_asid asid pd\<rbrace>" apply (simp add: store_pde_def set_pd_def set_object_def vspace_at_asid_def) apply (wp get_object_wp) apply clarsimp apply (clarsimp simp: obj_at_def) apply (drule vs_lookup_2ConsD) apply clarsimp apply (erule vs_lookup_atE) apply (drule vs_lookup1D) apply clarsimp apply (rule_tac ref'="([VSRef (ucast (asid_high_bits_of asid)) None],p')" in vs_lookupI) apply (fastforce simp: vs_asid_refs_def graph_of_def) apply (rule r_into_rtrancl) apply (rule_tac ko=ko in vs_lookup1I) prefer 3 apply (rule refl) prefer 2 apply assumption apply (clarsimp simp: obj_at_def vs_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>vspace_at_asid asid pd\<rbrace> store_pde p pde \<lbrace>\<lambda>_. vspace_at_asid asid pd\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>[VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd\<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>_. [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) 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> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<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 ko. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) 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> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<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. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) 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))))\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<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. \<lbrakk>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)))); \<exists>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> p') s \<and> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<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 p'. \<lbrakk>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)))); ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> p') s; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<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 p'. \<lbrakk>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)))); (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> vs_lookup1 s; asid_table s (asid_high_bits_of asid) = Some p'\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<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 p'. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; \<exists>rs r p p'a ko. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p') = (rs, p) \<and> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) = (r # rs, p'a) \<and> ko_at ko p s \<and> (r, p'a) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<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 p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<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 p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p') \<in> vs_asid_refs (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>))
 2. \<And>s pda p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], 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>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s pda p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], 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>))\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s pda p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], 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>) proof (prove)
goal (3 subgoals):
 1. \<And>s pda p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ko_at ko p' (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 p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r34 s pda p' ko, pd) \<in> vs_refs ko
 3. \<And>s pda p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] = [?r34 s pda p' ko, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] proof (prove)
goal (3 subgoals):
 1. \<And>s pda p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] = [?r34 s pda p' ko, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]
 2. \<And>s pda p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ko_at ko p' (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 p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (?r34 s pda p' ko, pd) \<in> vs_refs ko proof (prove)
goal (2 subgoals):
 1. \<And>s pda p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ko_at ko p' (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 p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko proof (prove)
goal (2 subgoals):
 1. \<And>s pda p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko
 2. \<And>s pda p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ko_at ko p' (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 p' ko. \<lbrakk>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)))); asid_table s (asid_high_bits_of asid) = Some p'; ko_at ko p' s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ko_at ko p' (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!