theory ArchInvariants_AI

lemma vs_refs_pdI:
  "\<lbrakk>pd (ucast r) = PageTablePDE x a b;
    ucast r \<notin> kernel_mapping_slots; \<forall>n \<ge> 12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk>
   \<Longrightarrow> (VSRef r (Some APageDirectory), ptrFromPAddr x)
       \<in> vs_refs (ArchObj (PageDirectory pd))" apply (simp add: vs_refs_def) apply (rule image_eqI[rotated]) apply (rule pde_graph_ofI) apply (simp add: pde_ref_def)+ apply (simp add: ucast_ucast_mask) apply (rule word_eqI) apply (simp add: word_size) apply (rule ccontr, auto) 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 \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> (VSRef r (Some APageDirectory), ptrFromPAddr x) \<in> vs_refs (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 \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> (VSRef r (Some APageDirectory), ptrFromPAddr x) \<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)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> ?x5 \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))
 2. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> (VSRef r (Some APageDirectory), ptrFromPAddr x) = (case ?x5 of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> pd ?x8 = ?pde8
 2. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> ?x8 \<notin> kernel_mapping_slots
 3. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> pde_ref ?pde8 = Some ?v8
 4. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> (VSRef r (Some APageDirectory), ptrFromPAddr x) = (case (?x8, ?v8) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> r = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) r) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> r = r && mask 12 proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> n < size r \<longrightarrow> r !! n = (r && mask 12) !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>pd (UCAST(32 \<rightarrow> 12) r) = PageTablePDE x a b; UCAST(32 \<rightarrow> 12) r \<notin> kernel_mapping_slots; \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk> \<Longrightarrow> n < 32 \<longrightarrow> r !! n = (r !! n \<and> n < 12) proof (prove)
goal:
No subgoals!