theory ArchAcc_AI

lemma set_pd_unmap_mappings:
  "\<lbrace>valid_kernel_mappings and
        obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p
    and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd')
                       \<and> (\<forall>x \<in> kernel_mapping_slots. pd x = pd' x)) p\<rbrace>
     set_pd p pd
   \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>" apply (simp add: set_pd_def) apply (wp set_object_v_ker_map get_object_wp) apply (clarsimp simp: obj_at_def
                 split: kernel_object.split_asm
                        arch_kernel_obj.split_asm) apply (simp add: vs_refs_def) subgoal premises prems for s x r x3 apply (cases "x \<in> kernel_mapping_slots") proof goal_cases case False with prems show ?thesis apply - apply (drule subsetD) apply (rule image_eqI[rotated]) apply (rule pde_graph_ofI[rotated, rotated]) apply ((simp;fail)+)[4] apply (clarsimp simp: valid_kernel_mappings_def
                      dest!: graph_ofD) apply (drule bspec, erule ranI) by (simp add: valid_kernel_mappings_if_pd_def) next case True with prems show ?thesis apply clarsimp apply (bspec x) apply (clarsimp simp: valid_kernel_mappings_def ran_def valid_kernel_mappings_if_pd_def) apply (erule allE[where x="ArchObj (PageDirectory x3)"]) apply clarsimp apply (erule impE) apply (erule exI[where x=p]) apply (erule allE[where x=x], erule allE[where x=r]) by clarsimp+ qed done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_kernel_mappings and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p\<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. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_kernel_mappings and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p) s \<Longrightarrow> valid_kernel_mappings s \<and> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts (arch_state s)))) True (ArchObj (PageDirectory pd)) proof (prove)
goal (1 subgoal):
 1. \<And>s x r pd'. \<lbrakk>valid_kernel_mappings s; vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs (ArchObj (PageDirectory pd')); kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; 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 x r pd'. \<lbrakk>valid_kernel_mappings s; (\<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)) \<subseteq> (\<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)); kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; 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. (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (2 subgoals):
 1. x \<in> kernel_mapping_slots \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)
 2. x \<notin> kernel_mapping_slots \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (state)
goal (2 subgoals):
 1. x \<in> kernel_mapping_slots \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)
 2. x \<notin> kernel_mapping_slots \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (state)
this:
x \<notin> kernel_mapping_slots

goal (2 subgoals):
 1. x \<in> kernel_mapping_slots \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)
 2. x \<notin> kernel_mapping_slots \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (chain)
picking this:
valid_kernel_mappings s
(\<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)) \<subseteq> (\<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 (x3 x))
kheap s p = Some (ArchObj (PageDirectory x3))
\<forall>x\<in>kernel_mapping_slots. pd x = x3 x
pde_ref (pd x) = Some r
x \<notin> kernel_mapping_slots proof (prove)
using this:
valid_kernel_mappings s
(\<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)) \<subseteq> (\<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 (x3 x))
kheap s p = Some (ArchObj (PageDirectory x3))
\<forall>x\<in>kernel_mapping_slots. pd x = x3 x
pde_ref (pd x) = Some r
x \<notin> kernel_mapping_slots

goal (1 subgoal):
 1. (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_kernel_mappings s; (\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> ?c6 \<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))
 2. \<lbrakk>valid_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots; ?c6 \<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 (x3 x))\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> ?x9 \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))
 2. \<lbrakk>valid_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> ?c6 = (case ?x9 of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 3. \<lbrakk>valid_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots; ?c6 \<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 (x3 x))\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> pde_ref ?pde12 = Some ?v12
 2. \<lbrakk>valid_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> pd ?x12 = ?pde12
 3. \<lbrakk>valid_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> ?x12 \<notin> kernel_mapping_slots
 4. \<lbrakk>valid_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> ?c6 = (case (?x12, ?v12) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 5. \<lbrakk>valid_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots; ?c6 \<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 (x3 x))\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> 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 (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x))\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots; pde_ref (x3 x) = Some r; r \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (pd x) = Some r; x \<notin> kernel_mapping_slots; pde_ref (x3 x) = Some r; r \<in> set (arm_global_pts (arch_state s)); valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> False proof (state)
this:
(r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)

goal (1 subgoal):
 1. x \<in> kernel_mapping_slots \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (state)
goal (1 subgoal):
 1. x \<in> kernel_mapping_slots \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (state)
this:
x \<in> kernel_mapping_slots

goal (1 subgoal):
 1. x \<in> kernel_mapping_slots \<Longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (chain)
picking this:
valid_kernel_mappings s
(\<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)) \<subseteq> (\<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 (x3 x))
kheap s p = Some (ArchObj (PageDirectory x3))
\<forall>x\<in>kernel_mapping_slots. pd x = x3 x
pde_ref (pd x) = Some r
x \<in> kernel_mapping_slots proof (prove)
using this:
valid_kernel_mappings s
(\<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)) \<subseteq> (\<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 (x3 x))
kheap s p = Some (ArchObj (PageDirectory x3))
\<forall>x\<in>kernel_mapping_slots. pd x = x3 x
pde_ref (pd x) = Some r
x \<in> kernel_mapping_slots

goal (1 subgoal):
 1. (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_kernel_mappings s; (\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>kernel_mapping_slots. pd x = x3 x; pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> r \<in> set (arm_global_pts (arch_state s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_kernel_mappings s; (\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; pd x = x3 x\<rbrakk> \<Longrightarrow> r \<in> set (arm_global_pts (arch_state s))
 2. \<lbrakk>valid_kernel_mappings s; (\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> r \<in> set (arm_global_pts (arch_state s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x. (\<exists>a. kheap s a = Some x) \<longrightarrow> (case x of ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) | ArchObj _ \<Rightarrow> True | _ \<Rightarrow> True); (\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; pd x = x3 x\<rbrakk> \<Longrightarrow> r \<in> set (arm_global_pts (arch_state s))
 2. \<lbrakk>valid_kernel_mappings s; (\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> r \<in> set (arm_global_pts (arch_state s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; pd x = x3 x; (\<exists>a. kheap s a = Some (ArchObj (PageDirectory x3))) \<longrightarrow> (case ArchObj (PageDirectory x3) of ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) | ArchObj _ \<Rightarrow> True | _ \<Rightarrow> True)\<rbrakk> \<Longrightarrow> r \<in> set (arm_global_pts (arch_state s))
 2. \<lbrakk>valid_kernel_mappings s; (\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> r \<in> set (arm_global_pts (arch_state s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; pd x = x3 x; (\<exists>a. kheap s a = Some (ArchObj (PageDirectory x3))) \<longrightarrow> (\<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))
 2. \<lbrakk>valid_kernel_mappings s; (\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> r \<in> set (arm_global_pts (arch_state s)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; pd x = x3 x\<rbrakk> \<Longrightarrow> \<exists>a. kheap s a = Some (ArchObj (PageDirectory x3))
 2. \<lbrakk>(\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; pd x = x3 x; \<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))
 3. \<lbrakk>valid_kernel_mappings s; (\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> r \<in> set (arm_global_pts (arch_state s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; pd x = x3 x; \<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))
 2. \<lbrakk>valid_kernel_mappings s; (\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> r \<in> set (arm_global_pts (arch_state s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; pd x = x3 x; 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))
 2. \<lbrakk>valid_kernel_mappings s; (\<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)) \<subseteq> (\<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 (x3 x)); kheap s p = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r; x \<in> kernel_mapping_slots; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> r \<in> set (arm_global_pts (arch_state s)) proof (state)
this:
(r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)

goal:
No subgoals! proof (prove)
goal:
No subgoals!