theory ArchVSpace_AI

lemma set_pd_valid_kernel_mappings_map:
  "\<lbrace>valid_kernel_mappings and
     obj_at (\<lambda>ko. glob_vs_refs (ArchObj (PageDirectory pd)) = glob_vs_refs ko - T \<union> S) p and
     (\<lambda>s. \<forall>(r,p) \<in> S. (r \<in> kernel_vsrefs)
                         = (p \<in> set (arm_global_pts (arch_state s))))\<rbrace>
     set_pd p pd
   \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>" apply (simp add: set_pd_def) including unfold_objects apply (wpsimp wp: set_object_v_ker_map[THEN hoare_set_object_weaken_pre]
              simp: a_type_def valid_kernel_mappings_def) apply (drule bspec, erule ranI) apply (clarsimp simp: valid_kernel_mappings_if_pd_def
                        kernel_vsrefs_def) apply (drule_tac f="\<lambda>S. (VSRef (ucast x) (Some APageDirectory), r) \<in> S"
               in arg_cong) apply (simp add: glob_vs_refs_def) apply (drule iffD1) apply (rule image_eqI[rotated]) apply (erule global_pde_graph_ofI[rotated]) apply simp+ apply (elim conjE disjE) apply (clarsimp dest!: graph_ofD) apply (drule(1) bspec) apply (clarsimp simp: kernel_base_shift_cast_le
                        kernel_mapping_slots_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_kernel_mappings and obj_at (\<lambda>ko. glob_vs_refs (ArchObj (PageDirectory pd)) = glob_vs_refs ko - T \<union> S) p and (\<lambda>s. \<forall>(r, p)\<in>S. (r \<in> kernel_vsrefs) = (p \<in> set (arm_global_pts (arch_state s))))\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_kernel_mappings and obj_at (\<lambda>ko. glob_vs_refs (ArchObj (PageDirectory pd)) = glob_vs_refs ko - T \<union> S) p and (\<lambda>s. \<forall>x\<in>S. case x of (r, p) \<Rightarrow> (r \<in> kernel_vsrefs) = (p \<in> set (arm_global_pts (arch_state s))))\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_kernel_mappings and obj_at (\<lambda>ko. glob_vs_refs (ArchObj (PageDirectory pd)) = glob_vs_refs ko - T \<union> S) p and (\<lambda>s. \<forall>x\<in>S. case x of (r, p) \<Rightarrow> (r \<in> kernel_vsrefs) = (p \<in> set (arm_global_pts (arch_state s))))\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; \<forall>x\<in>S. case x of (r, p) \<Rightarrow> (r \<in> kernel_vsrefs) = (p \<in> set (arm_global_pts (arch_state s))); glob_vs_refs (ArchObj (PageDirectory pd)) = glob_vs_refs (ArchObj (PageDirectory x3)) - T \<union> S; kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (r \<in> kernel_vsrefs) = (p \<in> set (arm_global_pts (arch_state s))); glob_vs_refs (ArchObj (PageDirectory pd)) = glob_vs_refs (ArchObj (PageDirectory x3)) - T \<union> S; kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); glob_vs_refs (ArchObj (PageDirectory pd)) = glob_vs_refs (ArchObj (PageDirectory x3)) - T \<union> S; kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots); ((VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> glob_vs_refs (ArchObj (PageDirectory pd))) = ((VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> glob_vs_refs (ArchObj (PageDirectory x3)) - T \<union> S)\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots); ((VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd)) = ((VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (pde_ref \<circ> x3) \<and> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<notin> T \<or> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> S)\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (2 subgoals):
 1. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd)
 2. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots); (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (pde_ref \<circ> x3) \<and> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<notin> T \<or> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> S\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (3 subgoals):
 1. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)\<rbrakk> \<Longrightarrow> ?x69 s x3 x r \<in> graph_of (pde_ref \<circ> pd)
 2. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) = (case ?x69 s x3 x r of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 3. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots); (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (pde_ref \<circ> x3) \<and> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<notin> T \<or> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> S\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (3 subgoals):
 1. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)\<rbrakk> \<Longrightarrow> pd (?x72 s x3 x r) = pd x
 2. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) = (case (?x72 s x3 x r, r) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 3. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots); (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (pde_ref \<circ> x3) \<and> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<notin> T \<or> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> S\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots); (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> x3) \<and> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<notin> T \<or> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> S\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (2 subgoals):
 1. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots); (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> x3); (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<notin> T\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)
 2. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots); (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> S\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>\<forall>x\<in>S. case x of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s))); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots); (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> S\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (pd x) = Some r; \<forall>x r. pde_ref (x3 x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots); (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) \<in> S; case (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r) of (r, p) \<Rightarrow> (case r of VSRef x y \<Rightarrow> kernel_base >> 20 \<le> x) = (p \<in> set (arm_global_pts (arch_state s)))\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal:
No subgoals!