theory ArchKHeap_AI

lemma valid_global_vspace_mappings_pres:
  "\<lbrakk> valid_global_vspace_mappings s;
     \<And>pd. ko_at (ArchObj (PageDirectory pd)) (arm_global_pd (arch_state s)) s
            \<Longrightarrow> ko_at (ArchObj (PageDirectory pd)) (arm_global_pd (arch_state s)) s';
     \<And>pt p. \<lbrakk> ko_at (ArchObj (PageTable pt)) p s;
               valid_global_objs s \<Longrightarrow> p \<in> set (arm_global_pts (arch_state s)) \<rbrakk>
            \<Longrightarrow> ko_at (ArchObj (PageTable pt)) p s';
     arm_global_pd (arch_state s') = arm_global_pd (arch_state s);
     arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s) \<rbrakk>
        \<Longrightarrow> valid_global_vspace_mappings s'" apply atomize apply (clarsimp simp: valid_global_vspace_mappings_def obj_at_def) apply (clarsimp simp: valid_pd_kernel_mappings_def
                 split: kernel_object.split_asm arch_kernel_obj.split_asm) apply (drule_tac x=x in spec) apply (clarsimp simp: valid_pde_kernel_mappings_def obj_at_def
                        valid_pt_kernel_mappings_def pde_ref_def
                 split: pde.split_asm) apply (simp split: kernel_object.split_asm
                     arch_kernel_obj.split_asm) apply (drule spec, drule spec, drule(1) mp) apply (drule mp) apply (clarsimp simp: valid_global_objs_def obj_at_def empty_table_def) apply (drule_tac x=x in spec) apply (simp add: pde_ref_def second_level_tables_def)[1] apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_vspace_mappings s; \<And>pd. ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s \<Longrightarrow> ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s'; \<And>pt p. \<lbrakk>ako_at (PageTable pt) p s; valid_global_objs s \<Longrightarrow> p \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> ako_at (PageTable pt) p s'; arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s)\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_vspace_mappings s; \<forall>pd. ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s \<longrightarrow> ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s'; \<forall>pt p. ako_at (PageTable pt) p s \<longrightarrow> (valid_global_objs s \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<longrightarrow> ako_at (PageTable pt) p s'; arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s)\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings s' proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>\<forall>pd. ko = ArchObj (PageDirectory pd) \<longrightarrow> kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); \<forall>pt p. kheap s p = Some (ArchObj (PageTable pt)) \<longrightarrow> (valid_global_objs s \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<longrightarrow> kheap s' p = Some (ArchObj (PageTable pt)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some ko; valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s' (arm_global_pd (arch_state s)) = Some ko \<and> valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s' ko proof (prove)
goal (1 subgoal):
 1. \<And>x3 x. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); \<forall>pt p. kheap s p = Some (ArchObj (PageTable pt)) \<longrightarrow> (valid_global_objs s \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<longrightarrow> kheap s' p = Some (ArchObj (PageTable pt)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); \<forall>x. valid_pde_kernel_mappings (x3 x) (UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) (arm_kernel_vspace (arch_state s)) s\<rbrakk> \<Longrightarrow> valid_pde_kernel_mappings (x3 x) (UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) (arm_kernel_vspace (arch_state s)) s' proof (prove)
goal (1 subgoal):
 1. \<And>x3 x. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); \<forall>pt p. kheap s p = Some (ArchObj (PageTable pt)) \<longrightarrow> (valid_global_objs s \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<longrightarrow> kheap s' p = Some (ArchObj (PageTable pt)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); valid_pde_kernel_mappings (x3 x) (UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) (arm_kernel_vspace (arch_state s)) s\<rbrakk> \<Longrightarrow> valid_pde_kernel_mappings (x3 x) (UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) (arm_kernel_vspace (arch_state s)) s' proof (prove)
goal (1 subgoal):
 1. \<And>x3 x x21 x22 x23 ko. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); \<forall>pt p. kheap s p = Some (ArchObj (PageTable pt)) \<longrightarrow> (valid_global_objs s \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<longrightarrow> kheap s' p = Some (ArchObj (PageTable pt)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); x3 x = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some ko; case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>xa. valid_pte_kernel_mappings (pt xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s' (ptrFromPAddr x21) = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>xa. valid_pte_kernel_mappings (pt xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>x3 x x21 x22 x23 ko x5 x2. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); \<forall>pt p. kheap s p = Some (ArchObj (PageTable pt)) \<longrightarrow> (valid_global_objs s \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<longrightarrow> kheap s' p = Some (ArchObj (PageTable pt)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); x3 x = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2)); ko = ArchObj (PageTable x2); x5 = PageTable x2; \<forall>xa. valid_pte_kernel_mappings (x2 xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s))\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s' (ptrFromPAddr x21) = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>xa. valid_pte_kernel_mappings (pt xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>x3 x x21 x22 x23 ko x5 x2. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); x3 x = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2)); ko = ArchObj (PageTable x2); x5 = PageTable x2; \<forall>xa. valid_pte_kernel_mappings (x2 xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)); (valid_global_objs s \<longrightarrow> ptrFromPAddr x21 \<in> set (arm_global_pts (arch_state s))) \<longrightarrow> kheap s' (ptrFromPAddr x21) = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s' (ptrFromPAddr x21) = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>xa. valid_pte_kernel_mappings (pt xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>x3 x x21 x22 x23 ko x5 x2. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); x3 x = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2)); ko = ArchObj (PageTable x2); x5 = PageTable x2; \<forall>xa. valid_pte_kernel_mappings (x2 xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s))\<rbrakk> \<Longrightarrow> valid_global_objs s \<longrightarrow> ptrFromPAddr x21 \<in> set (arm_global_pts (arch_state s))
 2. \<And>x3 x x21 x22 x23 ko x5 x2. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); x3 x = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2)); ko = ArchObj (PageTable x2); x5 = PageTable x2; \<forall>xa. valid_pte_kernel_mappings (x2 xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)); kheap s' (ptrFromPAddr x21) = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s' (ptrFromPAddr x21) = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>xa. valid_pte_kernel_mappings (pt xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>x3 x x21 x22 x23 x2. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); x3 x = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2)); \<forall>xa. valid_pte_kernel_mappings (x2 xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)); valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>x. (\<forall>r. pde_ref (x3 x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (x3 x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> x3 x = InvalidPDE); \<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))\<rbrakk> \<Longrightarrow> ptrFromPAddr x21 \<in> set (arm_global_pts (arch_state s))
 2. \<And>x3 x x21 x22 x23 ko x5 x2. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); x3 x = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2)); ko = ArchObj (PageTable x2); x5 = PageTable x2; \<forall>xa. valid_pte_kernel_mappings (x2 xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)); kheap s' (ptrFromPAddr x21) = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s' (ptrFromPAddr x21) = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>xa. valid_pte_kernel_mappings (pt xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>x3 x x21 x22 x23 x2. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); x3 x = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2)); \<forall>xa. valid_pte_kernel_mappings (x2 xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)); 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>r. pde_ref (x3 x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (x3 x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> x3 x = InvalidPDE)\<rbrakk> \<Longrightarrow> ptrFromPAddr x21 \<in> set (arm_global_pts (arch_state s))
 2. \<And>x3 x x21 x22 x23 ko x5 x2. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); x3 x = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2)); ko = ArchObj (PageTable x2); x5 = PageTable x2; \<forall>xa. valid_pte_kernel_mappings (x2 xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)); kheap s' (ptrFromPAddr x21) = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s' (ptrFromPAddr x21) = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>xa. valid_pte_kernel_mappings (pt xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>x3 x x21 x22 x23 ko x5 x2. \<lbrakk>kheap s' (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); arm_global_pd (arch_state s') = arm_global_pd (arch_state s); arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory x3)); x3 x = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2)); ko = ArchObj (PageTable x2); x5 = PageTable x2; \<forall>xa. valid_pte_kernel_mappings (x2 xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)); kheap s' (ptrFromPAddr x21) = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s' (ptrFromPAddr x21) = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>xa. valid_pte_kernel_mappings (pt xa) ((UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + (UCAST(8 \<rightarrow> 32) xa << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal:
No subgoals!