theory ArchRetype_AI

lemma store_pde_map_global_valid_vspace_objs:
  "\<lbrace>valid_vspace_objs and valid_arch_state and valid_global_objs
        and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs)\<rbrace>
    store_pde p pde
   \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>" apply (simp add: store_pde_def) apply (wp set_pd_vspace_objs_map[where T="{}" and S="{}"]) apply (clarsimp simp: obj_at_def kernel_vsrefs_kernel_mapping_slots[symmetric]) apply (intro conjI) apply (erule vs_refs_add_one'') apply clarsimp apply (drule valid_vspace_objsD, simp add: obj_at_def, simp+) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and valid_arch_state and valid_global_objs and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs)\<rbrace> store_pde p pde \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and valid_arch_state and valid_global_objs and (\<lambda>y. VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs)\<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>rv. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vspace_objs and valid_arch_state and valid_global_objs and (\<lambda>y. VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs)) s \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (valid_vspace_objs and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs ko - {} \<union> {}) (p && ~~ mask pd_bits) and (\<lambda>s. \<forall>x\<in>{}. typ_at (AArch APageTable) (snd x) s) and (\<lambda>s. \<forall>(r, p')\<in>{}. \<forall>ao. (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s) 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)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_vspace_objs s; valid_arch_state s; valid_global_objs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs (ArchObj (PageDirectory pd)) \<and> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>valid_vspace_objs s; valid_arch_state s; valid_global_objs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs (ArchObj (PageDirectory pd))
 2. \<And>s pd. \<lbrakk>valid_vspace_objs s; valid_arch_state s; valid_global_objs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_vspace_objs s; valid_arch_state s; valid_global_objs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s pd x ref. \<lbrakk>valid_vspace_objs s; valid_arch_state s; valid_global_objs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); x \<notin> kernel_mapping_slots; (ref \<rhd> (p && ~~ mask pd_bits)) s\<rbrakk> \<Longrightarrow> (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s pd x. \<lbrakk>valid_vspace_objs s; valid_arch_state s; valid_global_objs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); x \<notin> kernel_mapping_slots; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s\<rbrakk> \<Longrightarrow> x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s proof (prove)
goal:
No subgoals!