theory ArchArch_AC

lemma vs_refs_no_global_pts_pdI:
  "\<lbrakk> pd (ucast r) = PageTablePDE x a b; (ucast r :: 12 word) < ucast (kernel_base >> 20) \<rbrakk>
     \<Longrightarrow> (ptrFromPAddr x, r && mask 12, APageDirectory, Control) \<in>
           vs_refs_no_global_pts (ArchObj (PageDirectory pd))" apply (clarsimp simp: vs_refs_no_global_pts_def) apply (drule_tac f=pde_ref2 in arg_cong, simp add: pde_ref_simps o_def) apply (rule rev_bexI, rule DiffI, erule graph_ofI) apply simp apply (clarsimp simp: ucast_ucast_mask) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)\<rbrakk> \<Longrightarrow> (ptrFromPAddr x, r && mask 12, APageDirectory, Control) \<in> vs_refs_no_global_pts (ArchObj (PageDirectory pd)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptrFromPAddr x, r && mask 12, APageDirectory, Control) \<in> (case xa of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST(32 \<rightarrow> 12) r < UCAST(32 \<rightarrow> 12) (kernel_base >> 20); pde_ref2 (pd (UCAST(32 \<rightarrow> 12) r)) = Some (ptrFromPAddr x, 0, {Control})\<rbrakk> \<Longrightarrow> \<exists>xa\<in>graph_of (\<lambda>x. pde_ref2 (pd x)) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptrFromPAddr x, r && mask 12, APageDirectory, Control) \<in> (case xa of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>UCAST(32 \<rightarrow> 12) r < UCAST(32 \<rightarrow> 12) (kernel_base >> 20); pde_ref2 (pd (UCAST(32 \<rightarrow> 12) r)) = Some (ptrFromPAddr x, 0, {Control})\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) r, ptrFromPAddr x, 0, {Control}) \<notin> {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}
 2. \<lbrakk>UCAST(32 \<rightarrow> 12) r < UCAST(32 \<rightarrow> 12) (kernel_base >> 20); pde_ref2 (pd (UCAST(32 \<rightarrow> 12) r)) = Some (ptrFromPAddr x, 0, {Control})\<rbrakk> \<Longrightarrow> (ptrFromPAddr x, r && mask 12, APageDirectory, Control) \<in> (case (UCAST(32 \<rightarrow> 12) r, ptrFromPAddr x, 0, {Control}) of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST(32 \<rightarrow> 12) r < UCAST(32 \<rightarrow> 12) (kernel_base >> 20); pde_ref2 (pd (UCAST(32 \<rightarrow> 12) r)) = Some (ptrFromPAddr x, 0, {Control})\<rbrakk> \<Longrightarrow> (ptrFromPAddr x, r && mask 12, APageDirectory, Control) \<in> (case (UCAST(32 \<rightarrow> 12) r, ptrFromPAddr x, 0, {Control}) of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal:
No subgoals!