theory ArchAcc_AI

lemma store_pde_vspace_objs_unmap:
  "\<lbrace>valid_vspace_objs
    and valid_pde pde
    and K (pde_ref pde = None)\<rbrace>
  store_pde p pde \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" apply (simp add: store_pde_def) apply (wp set_pd_vspace_objs_unmap) apply clarsimp apply (rule conjI) apply clarsimp apply (drule (1) valid_vspace_objsD, fastforce) apply (simp add:) apply (clarsimp simp add: obj_at_def vs_refs_def) apply (rule pair_imageI) apply (simp add: graph_of_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and valid_pde pde and K (pde_ref pde = None)\<rbrace> store_pde p pde \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and valid_pde pde and (\<lambda>y. pde_ref pde = None)\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
set_pd (p && ~~ mask pd_bits) (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))
od \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vspace_objs and valid_pde pde and (\<lambda>y. pde_ref pde = None)) s \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (valid_vspace_objs and (\<lambda>s. (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> valid_vspace_obj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))) s) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s)) \<and> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s)
 2. \<And>s pd. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s proof (prove)
goal (2 subgoals):
 1. \<And>s pd x ref. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s; x \<notin> kernel_mapping_slots; (ref \<rhd> (p && ~~ mask pd_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> valid_pde (pd x) s
 2. \<And>s pd. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s proof (prove)
goal (2 subgoals):
 1. \<And>s pd x ref. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s; x \<notin> kernel_mapping_slots; x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_vspace_obj (PageDirectory pd) s\<rbrakk> \<Longrightarrow> valid_pde (pd x) s
 2. \<And>s pd. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd aa ba. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (aa, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x))\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) proof (prove)
goal (1 subgoal):
 1. \<And>s pd aa ba. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (aa, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x))\<rbrakk> \<Longrightarrow> (aa, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) proof (prove)
goal:
No subgoals!