theory Finalise_DR

lemma slot_with_pd_pt_relation:
  "\<lbrakk>valid_idle s; pd_pt_relation a b y s; ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow>
  (a, unat (y && mask pd_bits >> 2)) \<in>
    (slots_with (\<lambda>x. \<exists>asid. x = cdl_cap.PageTableCap b Fake asid)) (transform s)" apply (clarsimp simp :pd_pt_relation_def) apply (frule page_directory_at_rev) apply (frule(1) page_directory_not_idle) apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def) apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def) apply (clarsimp simp:has_slots_def object_slots_def) apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base) apply (simp add:mask_pd_bits_less) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; pd_pt_relation a b y s; UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (a, unat (y && mask pd_bits >> 2)) \<in> slots_with (\<lambda>x. \<exists>asid. x = cdl_cap.PageTableCap b Fake asid) (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); typ_at (AArch APageTable) (ptrFromPAddr ref) s; fun (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = PageTablePDE ref u v; b = ptrFromPAddr ref\<rbrakk> \<Longrightarrow> (a, unat (y && mask pd_bits >> 2)) \<in> slots_with (\<lambda>x. \<exists>asid. x = cdl_cap.PageTableCap (ptrFromPAddr ref) Fake asid) (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); typ_at (AArch APageTable) (ptrFromPAddr ref) s; fun (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = PageTablePDE ref u v; b = ptrFromPAddr ref; typ_at (AArch APageDirectory) a s\<rbrakk> \<Longrightarrow> (a, unat (y && mask pd_bits >> 2)) \<in> slots_with (\<lambda>x. \<exists>asid. x = cdl_cap.PageTableCap (ptrFromPAddr ref) Fake asid) (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); typ_at (AArch APageTable) (ptrFromPAddr ref) s; fun (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = PageTablePDE ref u v; b = ptrFromPAddr ref; typ_at (AArch APageDirectory) a s; not_idle_thread a s\<rbrakk> \<Longrightarrow> (a, unat (y && mask pd_bits >> 2)) \<in> slots_with (\<lambda>x. \<exists>asid. x = cdl_cap.PageTableCap (ptrFromPAddr ref) Fake asid) (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>u v ref pd pt. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = PageTablePDE ref u v; b = ptrFromPAddr ref; not_idle_thread a s; kheap s (ptrFromPAddr ref) = Some (ArchObj (arch_kernel_obj.PageTable pt))\<rbrakk> \<Longrightarrow> \<exists>x. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) a = Some x \<and> has_slots x \<and> (\<exists>c. object_slots x (unat (y && mask pd_bits >> 2)) = Some c \<and> (\<exists>asid. c = cdl_cap.PageTableCap (ptrFromPAddr ref) Fake asid)) proof (prove)
goal (1 subgoal):
 1. \<And>u v ref pd pt. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = PageTablePDE ref u v; b = ptrFromPAddr ref; a \<noteq> idle_thread s; kheap s (ptrFromPAddr ref) = Some (ArchObj (arch_kernel_obj.PageTable pt))\<rbrakk> \<Longrightarrow> has_slots (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr>) \<and> (\<exists>c. object_slots (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr>) (unat (y && mask pd_bits >> 2)) = Some c \<and> (\<exists>asid. c = cdl_cap.PageTableCap (ptrFromPAddr ref) Fake asid)) proof (prove)
goal (1 subgoal):
 1. \<And>u v ref pd pt. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = PageTablePDE ref u v; b = ptrFromPAddr ref; a \<noteq> idle_thread s; kheap s (ptrFromPAddr ref) = Some (ArchObj (arch_kernel_obj.PageTable pt))\<rbrakk> \<Longrightarrow> \<exists>c. transform_page_directory_contents pd (unat (y && mask pd_bits >> 2)) = Some c \<and> (\<exists>asid. c = cdl_cap.PageTableCap (ptrFromPAddr ref) Fake asid) proof (prove)
goal (1 subgoal):
 1. \<And>u v ref pd pt. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = PageTablePDE ref u v; b = ptrFromPAddr ref; a \<noteq> idle_thread s; kheap s (ptrFromPAddr ref) = Some (ArchObj (arch_kernel_obj.PageTable pt))\<rbrakk> \<Longrightarrow> unat (y && mask pd_bits >> 2) < 4096 proof (prove)
goal:
No subgoals!