theory Finalise_DR

lemma opt_cap_page_table:
  "\<lbrakk> valid_idle s;pd_pt_relation a pt_id x s;ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<rbrakk>
  \<Longrightarrow> opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (cdl_cap.PageTableCap pt_id Fake None)" apply (clarsimp simp :pd_pt_relation_def opt_cap_def transform_def slots_of_def) apply (frule page_directory_at_rev) apply (frule(1) page_directory_not_idle) apply (clarsimp simp: transform_objects_def not_idle_thread_def page_directory_not_idle
                        restrict_map_def object_slots_def) apply (clarsimp simp: transform_page_directory_contents_def unat_map_def | rule conjI )+ apply (clarsimp simp: transform_page_directory_contents_def unat_map_def transform_pde_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 pt_id x s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (cdl_cap.PageTableCap pt_id Fake None) proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && 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) (x && mask pd_bits >> 2)) = PageTablePDE ref u v; pt_id = ptrFromPAddr ref\<rbrakk> \<Longrightarrow> (case transform_objects s a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat (x && mask pd_bits >> 2)) = Some (cdl_cap.PageTableCap (ptrFromPAddr ref) Fake None) proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && 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) (x && mask pd_bits >> 2)) = PageTablePDE ref u v; pt_id = ptrFromPAddr ref; typ_at (AArch APageDirectory) a s\<rbrakk> \<Longrightarrow> (case transform_objects s a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat (x && mask pd_bits >> 2)) = Some (cdl_cap.PageTableCap (ptrFromPAddr ref) Fake None) proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && 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) (x && mask pd_bits >> 2)) = PageTablePDE ref u v; pt_id = ptrFromPAddr ref; typ_at (AArch APageDirectory) a s; not_idle_thread a s\<rbrakk> \<Longrightarrow> (case transform_objects s a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat (x && mask pd_bits >> 2)) = Some (cdl_cap.PageTableCap (ptrFromPAddr ref) Fake None) proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && 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) (x && mask pd_bits >> 2)) = PageTablePDE ref u v; pt_id = ptrFromPAddr ref; typ_at (AArch APageDirectory) a s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> transform_page_directory_contents fun (unat (x && mask pd_bits >> 2)) = Some (cdl_cap.PageTableCap (ptrFromPAddr ref) Fake None) proof (prove)
goal (2 subgoals):
 1. \<And>fun u v ref. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && 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) (x && mask pd_bits >> 2)) = PageTablePDE ref u v; pt_id = ptrFromPAddr ref; typ_at (AArch APageDirectory) a s; a \<noteq> idle_thread s; unat (x && mask pd_bits >> 2) < 4096\<rbrakk> \<Longrightarrow> transform_pde (kernel_pde_mask fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2))) = cdl_cap.PageTableCap (ptrFromPAddr ref) Fake None
 2. \<And>fun u v ref. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && 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) (x && mask pd_bits >> 2)) = PageTablePDE ref u v; pt_id = ptrFromPAddr ref; typ_at (AArch APageDirectory) a s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> unat (x && mask pd_bits >> 2) < 4096 proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && 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) (x && mask pd_bits >> 2)) = PageTablePDE ref u v; pt_id = ptrFromPAddr ref; typ_at (AArch APageDirectory) a s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> unat (x && mask pd_bits >> 2) < 4096 proof (prove)
goal:
No subgoals!