theory ArchAInvsPre

lemma some_get_page_info_kmapsD:
  "\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r);
    p \<in> kernel_mappings; valid_global_vspace_mappings s; equal_kernel_mappings s\<rbrakk>
   \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a) \<and> r = {}" apply (clarsimp simp: get_page_info_def get_pd_entry_def get_arch_obj_def
                         kernel_mappings_slots_eq
                  split: option.splits Structures_A.kernel_object.splits
                         arch_kernel_obj.splits) apply (erule valid_global_pd_mappingsE) apply (clarsimp simp: equal_kernel_mappings_def obj_at_def) apply (drule_tac x=pd_ref in spec,
          drule_tac x="arm_global_pd (arch_state s)" in spec, simp) apply (drule bspec, assumption) apply (clarsimp simp: valid_pd_kernel_mappings_def pde_mapping_bits_def) apply (drule_tac x="ucast (p >> 20)" in spec) apply (clarsimp simp: get_page_info_def get_pd_entry_def get_arch_obj_def
                         get_pt_info_def get_pt_entry_def
                         kernel_mappings_slots_eq
                  split: option.splits Structures_A.kernel_object.splits
                         arch_kernel_obj.splits
                         pde.splits pte.splits) apply (rule conjI, rule_tac x=ARMLargePage in exI, simp) apply (simp add: valid_pde_kernel_mappings_def obj_at_def
                       valid_pt_kernel_mappings_def) apply (drule_tac x="ucast ((p >> 12) && mask 8)" in spec) apply (clarsimp simp: valid_pte_kernel_mappings_def) apply (rule conjI, rule_tac x=ARMSmallPage in exI, simp) apply (simp add: valid_pde_kernel_mappings_def obj_at_def
                      valid_pt_kernel_mappings_def) apply (drule_tac x="ucast ((p >> 12) && mask 8)" in spec) apply (clarsimp simp: valid_pte_kernel_mappings_def) apply (rule conjI, rule_tac x=ARMSection in exI, simp) apply (simp add: valid_pde_kernel_mappings_def) apply (rule conjI, rule_tac x=ARMSuperSection in exI, simp) apply (simp add: valid_pde_kernel_mappings_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r); p \<in> kernel_mappings; valid_global_vspace_mappings s; equal_kernel_mappings s\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a) \<and> r = {} proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; valid_global_vspace_mappings s; equal_kernel_mappings s\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a) \<and> r = {} proof (prove)
goal (1 subgoal):
 1. \<And>x3 pd. \<lbrakk>kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; equal_kernel_mappings s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); \<forall>x. valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a) \<and> r = {} proof (prove)
goal (1 subgoal):
 1. \<And>x3 pd. \<lbrakk>kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; \<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); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a) \<and> r = {} proof (prove)
goal (1 subgoal):
 1. \<And>x3 pd. \<lbrakk>kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case pd (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s (ArchObj (PageDirectory pd)); \<forall>w\<in>kernel_mapping_slots. x3 w = pd w\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a) \<and> r = {} proof (prove)
goal (1 subgoal):
 1. \<And>x3 pd. \<lbrakk>kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case pd (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = pd (UCAST(32 \<rightarrow> 12) (p >> 20))\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a) \<and> r = {} proof (prove)
goal (1 subgoal):
 1. \<And>x3 pd. \<lbrakk>kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case pd (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); \<forall>x. valid_pde_kernel_mappings (pd x) (UCAST(12 \<rightarrow> 32) x << 20) (arm_kernel_vspace (arch_state s)) s; x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = pd (UCAST(32 \<rightarrow> 12) (p >> 20))\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a) \<and> r = {} proof (prove)
goal (1 subgoal):
 1. \<And>x3 pd. \<lbrakk>kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case pd (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = pd (UCAST(32 \<rightarrow> 12) (p >> 20)); valid_pde_kernel_mappings (pd (UCAST(32 \<rightarrow> 12) (p >> 20))) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a) \<and> r = {} proof (prove)
goal (4 subgoals):
 1. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; valid_pde_kernel_mappings (PageTablePDE x21 x22 x23) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = LargePagePTE b attr r; a = 16\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 16) \<and> r = {}
 2. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; valid_pde_kernel_mappings (PageTablePDE x21 x22 x23) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 12) \<and> r = {}
 3. \<And>x3 pd x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; valid_pde_kernel_mappings (SectionPDE b attr x33 r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 20) \<and> r = {}
 4. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 24) \<and> r = {} proof (prove)
goal (4 subgoals):
 1. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; valid_pde_kernel_mappings (PageTablePDE x21 x22 x23) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = LargePagePTE b attr r; a = 16\<rbrakk> \<Longrightarrow> r = {}
 2. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; valid_pde_kernel_mappings (PageTablePDE x21 x22 x23) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 12) \<and> r = {}
 3. \<And>x3 pd x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; valid_pde_kernel_mappings (SectionPDE b attr x33 r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 20) \<and> r = {}
 4. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 24) \<and> r = {} proof (prove)
goal (4 subgoals):
 1. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; \<forall>x. valid_pte_kernel_mappings (x2c x) ((UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) + (UCAST(8 \<rightarrow> 32) x << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)); kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = LargePagePTE b attr r; a = 16\<rbrakk> \<Longrightarrow> r = {}
 2. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; valid_pde_kernel_mappings (PageTablePDE x21 x22 x23) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 12) \<and> r = {}
 3. \<And>x3 pd x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; valid_pde_kernel_mappings (SectionPDE b attr x33 r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 20) \<and> r = {}
 4. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 24) \<and> r = {} proof (prove)
goal (4 subgoals):
 1. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = LargePagePTE b attr r; a = 16; valid_pte_kernel_mappings (x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8))) ((UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) << pte_mapping_bits)) (arm_kernel_vspace (arch_state s))\<rbrakk> \<Longrightarrow> r = {}
 2. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; valid_pde_kernel_mappings (PageTablePDE x21 x22 x23) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 12) \<and> r = {}
 3. \<And>x3 pd x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; valid_pde_kernel_mappings (SectionPDE b attr x33 r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 20) \<and> r = {}
 4. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 24) \<and> r = {} proof (prove)
goal (3 subgoals):
 1. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; valid_pde_kernel_mappings (PageTablePDE x21 x22 x23) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 12) \<and> r = {}
 2. \<And>x3 pd x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; valid_pde_kernel_mappings (SectionPDE b attr x33 r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 20) \<and> r = {}
 3. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 24) \<and> r = {} proof (prove)
goal (3 subgoals):
 1. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; valid_pde_kernel_mappings (PageTablePDE x21 x22 x23) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> r = {}
 2. \<And>x3 pd x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; valid_pde_kernel_mappings (SectionPDE b attr x33 r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 20) \<and> r = {}
 3. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 24) \<and> r = {} proof (prove)
goal (3 subgoals):
 1. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; \<forall>x. valid_pte_kernel_mappings (x2c x) ((UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) + (UCAST(8 \<rightarrow> 32) x << pte_mapping_bits)) (arm_kernel_vspace (arch_state s)); kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> r = {}
 2. \<And>x3 pd x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; valid_pde_kernel_mappings (SectionPDE b attr x33 r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 20) \<and> r = {}
 3. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 24) \<and> r = {} proof (prove)
goal (3 subgoals):
 1. \<And>x3 pd x21 x22 x23 x2c. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable x2c)); x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12; valid_pte_kernel_mappings (x2c (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8))) ((UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) << pte_mapping_bits)) (arm_kernel_vspace (arch_state s))\<rbrakk> \<Longrightarrow> r = {}
 2. \<And>x3 pd x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; valid_pde_kernel_mappings (SectionPDE b attr x33 r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 20) \<and> r = {}
 3. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 24) \<and> r = {} proof (prove)
goal (2 subgoals):
 1. \<And>x3 pd x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; valid_pde_kernel_mappings (SectionPDE b attr x33 r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 20) \<and> r = {}
 2. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 24) \<and> r = {} proof (prove)
goal (2 subgoals):
 1. \<And>x3 pd x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; valid_pde_kernel_mappings (SectionPDE b attr x33 r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> r = {}
 2. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 24) \<and> r = {} proof (prove)
goal (1 subgoal):
 1. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = 24) \<and> r = {} proof (prove)
goal (1 subgoal):
 1. \<And>x3 pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; valid_pde_kernel_mappings (SuperSectionPDE b attr r) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20)) << 20) (arm_kernel_vspace (arch_state s)) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> r = {} proof (prove)
goal:
No subgoals!