theory Finalise_DR

lemma opt_cap_section:
  "\<lbrakk>valid_idle s;pd_section_relation a pg x s \<or> pd_super_section_relation a pg x s;
    ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow>
  \<exists>f sz. (opt_cap (a, unat (x && mask pd_bits >> 2) ) (transform s))
    = Some (cdl_cap.FrameCap False pg f sz Fake None)" apply (erule disjE) apply (clarsimp simp: pd_section_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 split:ARM_A.pte.split_asm | 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) apply (clarsimp simp: pd_super_section_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 split:ARM_A.pte.split_asm | 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_section_relation a pg x s \<or> pd_super_section_relation a pg x s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<exists>f sz. opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (FrameCap False pg f sz Fake None) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pd_section_relation a pg x s\<rbrakk> \<Longrightarrow> \<exists>f sz. opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (FrameCap False pg f sz Fake None)
 2. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pd_super_section_relation a pg x s\<rbrakk> \<Longrightarrow> \<exists>f sz. opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (FrameCap False pg f sz Fake None) proof (prove)
goal (2 subgoals):
 1. \<And>fun u v ref1 ref2. \<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)); pg = ptrFromPAddr ref1; fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SectionPDE ref1 u ref2 v\<rbrakk> \<Longrightarrow> \<exists>f sz. (case transform_objects s a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat (x && mask pd_bits >> 2)) = Some (FrameCap False (ptrFromPAddr ref1) f sz Fake None)
 2. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pd_super_section_relation a pg x s\<rbrakk> \<Longrightarrow> \<exists>f sz. opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (FrameCap False pg f sz Fake None) proof (prove)
goal (2 subgoals):
 1. \<And>fun u v ref1 ref2. \<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)); pg = ptrFromPAddr ref1; fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SectionPDE ref1 u ref2 v; typ_at (AArch APageDirectory) a s\<rbrakk> \<Longrightarrow> \<exists>f sz. (case transform_objects s a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat (x && mask pd_bits >> 2)) = Some (FrameCap False (ptrFromPAddr ref1) f sz Fake None)
 2. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pd_super_section_relation a pg x s\<rbrakk> \<Longrightarrow> \<exists>f sz. opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (FrameCap False pg f sz Fake None) proof (prove)
goal (2 subgoals):
 1. \<And>fun u v ref1 ref2. \<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)); pg = ptrFromPAddr ref1; fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SectionPDE ref1 u ref2 v; typ_at (AArch APageDirectory) a s; not_idle_thread a s\<rbrakk> \<Longrightarrow> \<exists>f sz. (case transform_objects s a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat (x && mask pd_bits >> 2)) = Some (FrameCap False (ptrFromPAddr ref1) f sz Fake None)
 2. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pd_super_section_relation a pg x s\<rbrakk> \<Longrightarrow> \<exists>f sz. opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (FrameCap False pg f sz Fake None) proof (prove)
goal (2 subgoals):
 1. \<And>fun u v ref1 ref2. \<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)); pg = ptrFromPAddr ref1; fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SectionPDE ref1 u ref2 v; typ_at (AArch APageDirectory) a s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<exists>f sz. transform_page_directory_contents fun (unat (x && mask pd_bits >> 2)) = Some (FrameCap False (ptrFromPAddr ref1) f sz Fake None)
 2. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pd_super_section_relation a pg x s\<rbrakk> \<Longrightarrow> \<exists>f sz. opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (FrameCap False pg f sz Fake None) proof (prove)
goal (3 subgoals):
 1. \<And>fun u v ref1 ref2. \<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)); pg = ptrFromPAddr ref1; fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SectionPDE ref1 u ref2 v; typ_at (AArch APageDirectory) a s; a \<noteq> idle_thread s; unat (x && mask pd_bits >> 2) < 4096\<rbrakk> \<Longrightarrow> \<exists>f sz. transform_pde (kernel_pde_mask fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2))) = FrameCap False (ptrFromPAddr ref1) f sz Fake None
 2. \<And>fun u v ref1 ref2. \<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)); pg = ptrFromPAddr ref1; fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SectionPDE ref1 u ref2 v; typ_at (AArch APageDirectory) a s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> unat (x && mask pd_bits >> 2) < 4096
 3. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pd_super_section_relation a pg x s\<rbrakk> \<Longrightarrow> \<exists>f sz. opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (FrameCap False pg f sz Fake None) proof (prove)
goal (2 subgoals):
 1. \<And>fun u v ref1 ref2. \<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)); pg = ptrFromPAddr ref1; fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SectionPDE ref1 u ref2 v; typ_at (AArch APageDirectory) a s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> unat (x && mask pd_bits >> 2) < 4096
 2. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pd_super_section_relation a pg x s\<rbrakk> \<Longrightarrow> \<exists>f sz. opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (FrameCap False pg f sz Fake None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pd_super_section_relation a pg x s\<rbrakk> \<Longrightarrow> \<exists>f sz. opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (FrameCap False pg f sz Fake None) proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref1. \<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)); fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; pg = ptrFromPAddr ref1\<rbrakk> \<Longrightarrow> \<exists>f sz. (case transform_objects s a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat (x && mask pd_bits >> 2)) = Some (FrameCap False (ptrFromPAddr ref1) f sz Fake None) proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref1. \<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)); fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; pg = ptrFromPAddr ref1; typ_at (AArch APageDirectory) a s\<rbrakk> \<Longrightarrow> \<exists>f sz. (case transform_objects s a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat (x && mask pd_bits >> 2)) = Some (FrameCap False (ptrFromPAddr ref1) f sz Fake None) proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref1. \<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)); fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; pg = ptrFromPAddr ref1; typ_at (AArch APageDirectory) a s; not_idle_thread a s\<rbrakk> \<Longrightarrow> \<exists>f sz. (case transform_objects s a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat (x && mask pd_bits >> 2)) = Some (FrameCap False (ptrFromPAddr ref1) f sz Fake None) proof (prove)
goal (1 subgoal):
 1. \<And>fun u v ref1. \<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)); fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; pg = ptrFromPAddr ref1; typ_at (AArch APageDirectory) a s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<exists>f sz. transform_page_directory_contents fun (unat (x && mask pd_bits >> 2)) = Some (FrameCap False (ptrFromPAddr ref1) f sz Fake None) proof (prove)
goal (2 subgoals):
 1. \<And>fun u v ref1. \<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)); fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; pg = ptrFromPAddr ref1; typ_at (AArch APageDirectory) a s; a \<noteq> idle_thread s; unat (x && mask pd_bits >> 2) < 4096\<rbrakk> \<Longrightarrow> \<exists>f sz. transform_pde (kernel_pde_mask fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2))) = FrameCap False (ptrFromPAddr ref1) f sz Fake None
 2. \<And>fun u v ref1. \<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)); fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; pg = ptrFromPAddr ref1; 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 ref1. \<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)); fun (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; pg = ptrFromPAddr ref1; 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!