theory ArchRetype_AI

lemma store_pde_valid_kernel_mappings_map_global:
  "\<lbrace>valid_kernel_mappings and valid_arch_state and valid_global_objs
     and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)
                \<in> kernel_vsrefs)
     and (\<lambda>s. \<forall>p. pde_ref pde = Some p
             \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))\<rbrace>
     store_pde p pde
   \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>" apply (simp add: store_pde_def) apply (wp set_pd_valid_kernel_mappings_map) apply (clarsimp simp: obj_at_def) apply (rule conjI, rule glob_vs_refs_add_one') apply (clarsimp simp: ucast_ucast_mask_shift_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_kernel_mappings and valid_arch_state and valid_global_objs and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs) and (\<lambda>s. \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))\<rbrace> store_pde p pde \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_kernel_mappings and valid_arch_state and valid_global_objs and (\<lambda>y. VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs) and (\<lambda>s. \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))\<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_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_kernel_mappings and valid_arch_state and valid_global_objs and (\<lambda>y. VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs) and (\<lambda>s. \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))) s \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (valid_kernel_mappings and obj_at (\<lambda>ko. glob_vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = glob_vs_refs ko - ?T2 pd \<union> ?S2 pd) (p && ~~ mask pd_bits) and (\<lambda>s. \<forall>(r, p)\<in>?S2 pd. (r \<in> kernel_vsrefs) = (p \<in> set (arm_global_pts (arch_state s))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_kernel_mappings s; valid_arch_state s; valid_global_objs s; VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> glob_vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = glob_vs_refs (ArchObj (PageDirectory pd)) - ?T2 pd \<union> ?S2 pd \<and> (\<forall>x\<in>?S2 pd. case x of (r, p) \<Rightarrow> (r \<in> kernel_vsrefs) = (p \<in> set (arm_global_pts (arch_state s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_kernel_mappings s; valid_arch_state s; valid_global_objs s; VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>x\<in>Pair (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory)) ` set_option (pde_ref pde). case x of (r, p) \<Rightarrow> (r \<in> kernel_vsrefs) = (p \<in> set (arm_global_pts (arch_state s))) proof (prove)
goal:
No subgoals!