theory ArchAcc_AI

lemma kernel_mapping_slots_empty_pdeI:
  "\<lbrakk>equal_kernel_mappings s; valid_global_objs s; valid_arch_state s;
    kheap s p = Some (ArchObj (PageDirectory pd)); x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow>
   (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd x)" apply (clarsimp simp: invs_def valid_state_def equal_kernel_mappings_def valid_global_objs_def) apply (erule_tac x=p in allE, erule_tac x="arm_global_pd (arch_state s)" in allE) including unfold_objects apply clarsimp by (simp add: empty_table_def valid_arch_state_def a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equal_kernel_mappings s; valid_global_objs s; valid_arch_state s; kheap s p = Some (ArchObj (PageDirectory pd)); x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y pd pd'. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w); valid_arch_state s; kheap s p = Some (ArchObj (PageDirectory pd)); x \<in> kernel_mapping_slots; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_state s; kheap s p = Some (ArchObj (PageDirectory pd)); x \<in> kernel_mapping_slots; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); \<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') (arm_global_pd (arch_state s)) s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrakk> \<Longrightarrow> (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_state s; kheap s p = Some (ArchObj (PageDirectory pd)); x \<in> kernel_mapping_slots; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); \<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') (arm_global_pd (arch_state s)) s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrakk> \<Longrightarrow> (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd x) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_arch_state s; kheap s p = Some (ArchObj (PageDirectory pd)); x \<in> kernel_mapping_slots; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); \<forall>pd'. ko = ArchObj (PageDirectory pd') \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w); kheap s (arm_global_pd (arch_state s)) = Some ko; empty_table (set (second_level_tables (arch_state s))) ko\<rbrakk> \<Longrightarrow> (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd x)