theory ArchAInvsPre

lemma get_page_info_gpd_kmaps:
  "\<lbrakk>valid_global_objs s; valid_arch_state s;
    get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
                  (arm_global_pd (arch_state s)) p = Some (b, a, attr, r)\<rbrakk>
   \<Longrightarrow> p \<in> kernel_mappings" apply (clarsimp simp: valid_global_objs_def valid_arch_state_def) apply (thin_tac "Ball x y" for x y) apply (clarsimp simp add: obj_at_def valid_ao_at_def) apply (clarsimp simp: empty_table_def kernel_mappings_slots_eq) apply (drule_tac x="ucast (p >> 20)" in spec) apply (rule ccontr, simp) apply (clarsimp simp: get_page_info_def get_pd_entry_def get_arch_obj_def
                  split: option.splits arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_objs s; valid_arch_state s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) p = Some (b, a, attr, r)\<rbrakk> \<Longrightarrow> p \<in> kernel_mappings proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) p = Some (b, a, attr, r); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table 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)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> p \<in> kernel_mappings proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) p = Some (b, a, attr, r); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> p \<in> kernel_mappings proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) p = Some (b, a, attr, r); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> p \<in> kernel_mappings proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) p = Some (b, a, attr, r); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) p = Some (b, a, attr, r); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); (\<forall>r. pde_ref (pd (UCAST(32 \<rightarrow> 12) (p >> 20))) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd (UCAST(32 \<rightarrow> 12) (p >> 20))) \<and> (UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots \<longrightarrow> pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = InvalidPDE)\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) p = Some (b, a, attr, r); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); (\<forall>r. pde_ref (pd (UCAST(32 \<rightarrow> 12) (p >> 20))) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd (UCAST(32 \<rightarrow> 12) (p >> 20))) \<and> pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = InvalidPDE; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!