theory ArchFinalise_AI

lemma obj_at_empty_tableI:
  "invs s \<and>
  (\<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow>
      pde_wp_at (\<lambda>pde. pde = InvalidPDE) p x s)
  \<Longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s" apply safe apply (simp add: obj_at_def empty_table_def pde_wp_at_def) 
  (* Boring cases *)
   apply (case_tac "\<exists>ko. kheap s p = Some ko") apply (erule exE) apply (rule_tac x=ko in exI) apply (rule conjI) apply assumption apply (case_tac ko) apply ((erule_tac x="ucast (kernel_base >> 20) - 1" in allE,
         simp add: kernel_base_def kernel_mapping_slots_def)+)[4] apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj) defer 3 apply ((erule_tac x="ucast (kernel_base >> 20) - 1" in allE,
         simp add: kernel_base_def kernel_mapping_slots_def)+)[4] 
   (* Interesting case *)
   apply (rename_tac "fun") apply clarsimp apply (erule_tac x=x in allE) apply (case_tac "x \<notin> kernel_mapping_slots") apply (simp add:valid_pde_mappings_def pde_ref_def) apply simp apply (rule conjI) apply (simp add: invs_def valid_state_def valid_kernel_mappings_def
                    valid_kernel_mappings_if_pd_def) apply (erule conjE)+ apply (erule_tac x="ArchObj (PageDirectory fun)" in ballE) apply simp apply (simp add: ran_def) apply (clarsimp simp: invs_def valid_state_def valid_arch_state_def
                        valid_global_objs_def equal_kernel_mappings_def
                        obj_at_def a_type_simps) apply (erule_tac x=p in allE,
          erule_tac x="arm_global_pd (arch_state s)" in allE) apply (erule_tac x="fun" in allE, erule_tac x="pd" in allE) apply (simp add: empty_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<and> (\<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> pde_wp_at (\<lambda>pde. pde = InvalidPDE) p x s) \<Longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> pde_wp_at (\<lambda>pde. pde = InvalidPDE) p x s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); \<exists>ko. kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False)
 2. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); \<nexists>ko. kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False)
 2. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); \<nexists>ko. kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko\<rbrakk> \<Longrightarrow> kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False)
 2. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); \<nexists>ko. kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (3 subgoals):
 1. \<And>ko. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko\<rbrakk> \<Longrightarrow> kheap s p = Some ko
 2. \<And>ko. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 3. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); \<nexists>ko. kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 2. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); \<nexists>ko. kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (6 subgoals):
 1. \<And>ko x11 x12. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = CNode x11 x12\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 2. \<And>ko x2. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = TCB x2\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 3. \<And>ko x3. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = Endpoint x3\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 4. \<And>ko x4. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = Notification x4\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 5. \<And>ko x5. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj x5\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 6. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); \<nexists>ko. kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>ko x5. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj x5\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 2. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); \<nexists>ko. kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>ko arch_kernel_obj. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 2. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); \<nexists>ko. kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (5 subgoals):
 1. \<And>ko arch_kernel_obj x1. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj; arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 2. \<And>ko arch_kernel_obj x2. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj; arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 3. \<And>ko arch_kernel_obj x3. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 4. \<And>ko arch_kernel_obj x41 x42. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 5. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); \<nexists>ko. kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (5 subgoals):
 1. \<And>ko arch_kernel_obj x1. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj; arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 2. \<And>ko arch_kernel_obj x2. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj; arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 3. \<And>ko arch_kernel_obj x41 x42. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 4. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); \<nexists>ko. kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False)
 5. \<And>ko arch_kernel_obj x3. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko arch_kernel_obj x3. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko arch_kernel_obj x3. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko arch_kernel_obj fun. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> (case kheap s p of None \<Rightarrow> False | Some (ArchObj (PageDirectory pd)) \<Rightarrow> pd x = InvalidPDE | Some (ArchObj _) \<Rightarrow> False | Some _ \<Rightarrow> False); kheap s p = Some ko; ko = ArchObj arch_kernel_obj; arch_kernel_obj = PageDirectory fun\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>fun x. \<lbrakk>invs s; \<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow> fun x = InvalidPDE; kheap s p = Some (ArchObj (PageDirectory fun))\<rbrakk> \<Longrightarrow> (\<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (fun x) proof (prove)
goal (1 subgoal):
 1. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<notin> kernel_mapping_slots \<longrightarrow> fun x = InvalidPDE\<rbrakk> \<Longrightarrow> (\<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (fun x) proof (prove)
goal (2 subgoals):
 1. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<notin> kernel_mapping_slots \<longrightarrow> fun x = InvalidPDE; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (\<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (fun x)
 2. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<notin> kernel_mapping_slots \<longrightarrow> fun x = InvalidPDE; \<not> x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (\<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (fun x) proof (prove)
goal (1 subgoal):
 1. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<notin> kernel_mapping_slots \<longrightarrow> fun x = InvalidPDE; \<not> x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (\<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (fun x) proof (prove)
goal (1 subgoal):
 1. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (\<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (fun x) proof (prove)
goal (2 subgoals):
 1. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))
 2. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_pde_mappings (fun x) proof (prove)
goal (2 subgoals):
 1. \<And>fun x. \<lbrakk>valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> Ball (ran (kheap s)) (case_kernel_object (\<lambda>nat fun. True) (\<lambda>tcb_ext. True) (\<lambda>endpoint. True) (\<lambda>notification_ext. True) (case_arch_kernel_obj (\<lambda>pool. True) (\<lambda>pt. True) (\<lambda>pd. \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)) (\<lambda>dev s. True))) \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))
 2. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_pde_mappings (fun x) proof (prove)
goal (2 subgoals):
 1. \<And>fun x. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; Ball (ran (kheap s)) (case_kernel_object (\<lambda>nat fun. True) (\<lambda>tcb_ext. True) (\<lambda>endpoint. True) (\<lambda>notification_ext. True) (case_arch_kernel_obj (\<lambda>pool. True) (\<lambda>pt. True) (\<lambda>pd. \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots)) (\<lambda>dev s. True))); equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> \<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))
 2. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_pde_mappings (fun x) proof (prove)
goal (3 subgoals):
 1. \<And>fun x. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; case ArchObj (PageDirectory fun) of ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) | ArchObj _ \<Rightarrow> True | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> \<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))
 2. \<And>fun x. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ArchObj (PageDirectory fun) \<notin> ran (kheap s)\<rbrakk> \<Longrightarrow> \<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))
 3. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_pde_mappings (fun x) proof (prove)
goal (2 subgoals):
 1. \<And>fun x. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ArchObj (PageDirectory fun) \<notin> ran (kheap s)\<rbrakk> \<Longrightarrow> \<forall>r. pde_ref (fun x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))
 2. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_pde_mappings (fun x) proof (prove)
goal (1 subgoal):
 1. \<And>fun x. \<lbrakk>invs s; kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_pde_mappings (fun x) proof (prove)
goal (1 subgoal):
 1. \<And>fun x pd. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs 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)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps 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)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); valid_kernel_mappings s; \<forall>x y pd pd'. kheap s x = Some (ArchObj (PageDirectory pd)) \<and> kheap s y = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w); valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> valid_pde_mappings (fun x) proof (prove)
goal (1 subgoal):
 1. \<And>fun x pd. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs 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)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps 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)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>pd pd'. kheap s p = Some (ArchObj (PageDirectory pd)) \<and> kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrakk> \<Longrightarrow> valid_pde_mappings (fun x) proof (prove)
goal (1 subgoal):
 1. \<And>fun x pd. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory fun)); x \<in> kernel_mapping_slots; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs 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)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps 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)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; kheap s p = Some (ArchObj (PageDirectory fun)) \<and> kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. fun w = pd w)\<rbrakk> \<Longrightarrow> valid_pde_mappings (fun x) proof (prove)
goal:
No subgoals!