theory ArchVSpace_AI

lemma set_pd_vspace_objs_map:
  notes valid_vspace_obj.simps[simp del] and a_type_elims[rule del]
  shows
  "\<lbrace>valid_vspace_objs and
   obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T \<union> S) p and
   (\<lambda>s. \<forall>x \<in> S. page_table_at (snd x) s) and
   (\<lambda>s. \<forall>(r,p') \<in> S. \<forall>ao. (\<exists>\<rhd>p) s \<longrightarrow> ko_at (ArchObj ao) p' s
                      \<longrightarrow> valid_vspace_obj ao s) and
   (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd) s)\<rbrace>
  set_pd p pd \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" apply (simp add: set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def valid_vspace_objs_def a_type_simps
              simp del: fun_upd_apply
                 split: Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (frule (1) vs_lookup_map_some_pdes.intro, simp add: obj_at_def) apply (frule vs_lookup_map_some_pdes.vs_lookup2) apply (drule(1) subsetD) apply (erule UnE) apply (simp only: fun_upd_apply split: if_split_asm) apply (rule valid_vspace_obj_same_type) apply fastforce apply assumption apply (clarsimp simp add: a_type_def) apply (rule valid_vspace_obj_same_type) apply fastforce apply assumption apply (clarsimp simp: a_type_def) apply (clarsimp simp add: vs_lookup_map_some_pdes.new_lookups_def) apply (drule(1) bspec)+ apply (clarsimp simp add: a_type_simps  split: if_split_asm) apply (drule mp, erule exI)+ apply (erule(1) valid_vspace_obj_same_type) apply (simp add: a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T \<union> S) p and (\<lambda>s. \<forall>x\<in>S. typ_at (AArch APageTable) (snd x) s) and (\<lambda>s. \<forall>(r, p')\<in>S. \<forall>ao. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s)\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T \<union> S) p and (\<lambda>s. \<forall>x\<in>S. typ_at (AArch APageTable) (snd x) s) and (\<lambda>s. \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s)\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory pd)));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
od \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vspace_objs and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T \<union> S) p and (\<lambda>s. \<forall>x\<in>S. typ_at (AArch APageTable) (snd x) s) and (\<lambda>s. \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s)) s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory pd)) \<longrightarrow> valid_vspace_objs (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) \<subseteq> vs_lookup s \<union> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs, pa) \<in> vs_lookup s \<union> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs, pa) \<in> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> p) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj ao)\<rparr>); pa = p; Some (ArchObj (PageDirectory pd)) = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj ao)\<rparr>)
 2. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 3. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs, pa) \<in> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> p) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj ao)\<rparr>); pa = p; Some (ArchObj (PageDirectory pd)) = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> p) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj ao)\<rparr>); pa = p; Some (ArchObj (PageDirectory pd)) = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> kheap s p = Some (?ko56 s pda pa rs ao)
 3. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> p) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj ao)\<rparr>); pa = p; Some (ArchObj (PageDirectory pd)) = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> a_type (ArchObj ao) = a_type (?ko56 s pda pa rs ao)
 4. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 5. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs, pa) \<in> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> p) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj ao)\<rparr>); pa = p; Some (ArchObj (PageDirectory pd)) = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> kheap s p = Some (?ko56 s pda pa rs ao)
 2. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> p) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj ao)\<rparr>); pa = p; Some (ArchObj (PageDirectory pd)) = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> a_type (ArchObj ao) = a_type (?ko56 s pda pa rs ao)
 3. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 4. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs, pa) \<in> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> p) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj ao)\<rparr>); pa = p; Some (ArchObj (PageDirectory pd)) = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> a_type (ArchObj ao) = a_type (ArchObj (PageDirectory pda))
 2. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 3. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs, pa) \<in> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs, pa) \<in> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> kheap s p = Some (?ko71 s pda pa rs ao)
 3. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory pd)) = a_type (?ko71 s pda pa rs ao)
 4. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs, pa) \<in> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> kheap s p = Some (?ko71 s pda pa rs ao)
 2. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory pd)) = a_type (?ko71 s pda pa rs ao)
 3. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs, pa) \<in> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda pa rs ao. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (rs \<rhd> pa) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory pda))
 2. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs, pa) \<in> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda pa rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ((kheap s)(p \<mapsto> ArchObj (PageDirectory pd))) pa = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (rs, pa) \<in> vs_lookup_map_some_pdes.new_lookups p S `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda pa ao a r. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); ((r # a) \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); (if pa = p then Some (ArchObj (PageDirectory pd)) else kheap s pa) = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (a \<rhd> p) s; (r, pa) \<in> S\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda pa ao a r. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); ((r # a) \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); (if pa = p then Some (ArchObj (PageDirectory pd)) else kheap s pa) = Some (ArchObj ao); vs_lookup_map_some_pdes pda p s S T pd; (a \<rhd> p) s; (r, pa) \<in> S; \<exists>ko. kheap s (snd (r, pa)) = Some ko \<and> a_type ko = AArch APageTable; case (r, pa) of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda pa a r pt. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (a \<rhd> p) s; (r, pa) \<in> S; (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageTable pt) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s; kheap s p = Some (ArchObj (PageDirectory pda)); ((r # a) \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> valid_vspace_obj (PageTable pt) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda pa a r pt. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (a \<rhd> p) s; (r, pa) \<in> S; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; kheap s p = Some (ArchObj (PageDirectory pda)); ((r # a) \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj (PageTable pt)); valid_vspace_obj (PageTable pt) s; valid_vspace_obj (PageDirectory pd) s\<rbrakk> \<Longrightarrow> valid_vspace_obj (PageTable pt) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda pa a r pt. \<lbrakk>vs_lookup_map_some_pdes pda p s S T pd; (a \<rhd> p) s; (r, pa) \<in> S; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; kheap s p = Some (ArchObj (PageDirectory pda)); ((r # a) \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); pa \<noteq> p; kheap s pa = Some (ArchObj (PageTable pt)); valid_vspace_obj (PageDirectory pd) s\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory pda)) proof (prove)
goal:
No subgoals!