theory ArchRetype_AI

lemma store_pde_map_global_valid_arch_caps:
  "\<lbrace>valid_arch_caps and valid_objs and valid_vspace_objs
     and valid_arch_state and valid_global_objs
     and K (valid_pde_mappings pde)
     and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)
                \<in> kernel_vsrefs)
     and (\<lambda>s. \<forall>p. pde_ref pde = Some p
             \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))\<rbrace>
      store_pde p pde
   \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>" apply (simp add: store_pde_def) apply (wp set_pd_valid_arch_caps
            [where T="{}" and S="{}" and T'="{}" and S'="{}"]) apply (clarsimp simp: obj_at_def kernel_vsrefs_kernel_mapping_slots[symmetric]) apply (intro conjI) apply (erule vs_refs_add_one'') apply (rule set_eqI) apply (clarsimp simp add:  vs_refs_pages_def graph_of_def image_def) apply (rule arg_cong[where f=Ex], rule ext, fastforce) apply clarsimp apply (rule conjI, clarsimp) apply (drule valid_vspace_objsD, simp add: obj_at_def, simp+)[1] apply (rule impI, rule disjI2) apply (simp add: empty_table_def second_level_tables_def) apply clarsimp apply (rule conjI, clarsimp) apply (thin_tac "All P" for P) apply clarsimp apply (frule_tac ref'="VSRef (ucast c) (Some APageDirectory) # r" and
                    p'=q in vs_lookup_pages_step) apply (clarsimp simp: vs_lookup_pages1_def vs_refs_pages_def
                          obj_at_def graph_of_def image_def) apply (clarsimp simp: valid_arch_caps_def valid_vs_lookup_def) apply clarsimp apply (rule conjI, clarsimp) apply (thin_tac "All P" for P) apply clarsimp apply (drule_tac ref'="VSRef (ucast c) (Some APageDirectory) # r" and
                   p'=q in vs_lookup_pages_step) apply (clarsimp simp: vs_lookup_pages1_def vs_refs_pages_def
                         obj_at_def graph_of_def image_def) apply (drule_tac ref'="VSRef (ucast d) (Some APageTable) #
                         VSRef (ucast c) (Some APageDirectory) # r" and
                   p'=q' in vs_lookup_pages_step) apply (fastforce simp: vs_lookup_pages1_def vs_refs_pages_def
                         obj_at_def graph_of_def image_def) apply (clarsimp simp: valid_arch_caps_def valid_vs_lookup_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and valid_objs and valid_vspace_objs and valid_arch_state and valid_global_objs and K (valid_pde_mappings pde) and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs) and (\<lambda>s. \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))\<rbrace> store_pde p pde \<lbrace>\<lambda>_. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and valid_objs and valid_vspace_objs and valid_arch_state and valid_global_objs and (\<lambda>y. valid_pde_mappings pde) and (\<lambda>y. VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs) and (\<lambda>s. \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
set_pd (p && ~~ mask pd_bits) (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))
od \<lbrace>\<lambda>_. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_arch_caps and valid_objs and valid_vspace_objs and valid_arch_state and valid_global_objs and (\<lambda>y. valid_pde_mappings pde) and (\<lambda>y. VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs) and (\<lambda>s. \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))) s \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (valid_arch_caps and valid_arch_state and valid_vspace_objs and valid_objs and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs ko - {} \<union> {}) (p && ~~ mask pd_bits) and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages ko - {} \<union> {}) (p && ~~ mask pd_bits) and (\<lambda>s. \<forall>x\<in>{}. typ_at (AArch APageTable) (snd x) s) and (\<lambda>s. \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> {}) and (\<lambda>s. \<forall>(r, p')\<in>{}. \<forall>ao. (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s) and (\<lambda>s. (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> valid_vspace_obj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))) s) and (\<lambda>s. (\<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> cap_asid cap \<noteq> None) \<or> (obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))))) and (\<lambda>s. \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) c) = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))) and (\<lambda>s. \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) c) = Some q \<longrightarrow> (\<forall>q' pt d. ako_at (PageTable pt) q s \<longrightarrow> pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs (ArchObj (PageDirectory pd)) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) \<and> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s))) \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) \<and> (\<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<and> (\<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))))) proof (prove)
goal (6 subgoals):
 1. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs (ArchObj (PageDirectory pd))
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd))
 3. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s))
 4. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 5. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))
 6. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (5 subgoals):
 1. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd))
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s))
 3. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 4. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))
 5. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (5 subgoals):
 1. \<And>s pd x. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (x \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) = (x \<in> vs_refs_pages (ArchObj (PageDirectory pd)))
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s))
 3. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 4. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))
 5. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (5 subgoals):
 1. \<And>s pd a b. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>aa. aa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<and> (aa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> aa \<notin> kernel_mapping_slots \<and> (aa \<notin> kernel_mapping_slots \<longrightarrow> pde_ref_pages (pd aa) = Some b \<and> a = VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory)))) = (\<exists>aa. aa \<notin> kernel_mapping_slots \<and> (aa \<notin> kernel_mapping_slots \<longrightarrow> pde_ref_pages (pd aa) = Some b \<and> a = VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory)))
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s))
 3. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 4. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))
 5. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (4 subgoals):
 1. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s))
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 3. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))
 4. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (4 subgoals):
 1. \<And>s pd x ref. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); x \<notin> kernel_mapping_slots; (ref \<rhd> (p && ~~ mask pd_bits)) s\<rbrakk> \<Longrightarrow> (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde pde s) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s)
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 3. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))
 4. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (4 subgoals):
 1. \<And>s pd x ref. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); x \<notin> kernel_mapping_slots; (ref \<rhd> (p && ~~ mask pd_bits)) s\<rbrakk> \<Longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 3. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))
 4. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (3 subgoals):
 1. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))
 3. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (3 subgoals):
 1. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))
 3. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd r c. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (r \<unrhd> (p && ~~ mask pd_bits)) s; c \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages pde = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd r c. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (r \<unrhd> (p && ~~ mask pd_bits)) s; c \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd r c. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (r \<unrhd> (p && ~~ mask pd_bits)) s; c \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd r c q. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (r \<unrhd> (p && ~~ mask pd_bits)) s; c \<notin> kernel_mapping_slots; c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref_pages (pd c) = Some q\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (3 subgoals):
 1. \<And>s pd r c q. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (r \<unrhd> (p && ~~ mask pd_bits)) s; c \<notin> kernel_mapping_slots; c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref_pages (pd c) = Some q\<rbrakk> \<Longrightarrow> ((r, p && ~~ mask pd_bits), VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r, q) \<in> vs_lookup_pages1 s
 2. \<And>s pd r c q. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (r \<unrhd> (p && ~~ mask pd_bits)) s; c \<notin> kernel_mapping_slots; c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref_pages (pd c) = Some q; ((VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 3. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd r c q. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (r \<unrhd> (p && ~~ mask pd_bits)) s; c \<notin> kernel_mapping_slots; c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref_pages (pd c) = Some q; ((VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd r c. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (r \<unrhd> (p && ~~ mask pd_bits)) s; c \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (c = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref pde = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) (Some APageDirectory) # r)))))) \<and> (c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd r c. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>p. pde_ref pde = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (r \<unrhd> (p && ~~ mask pd_bits)) s; c \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd r c. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (r \<unrhd> (p && ~~ mask pd_bits)) s; c \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd r c q q' pt d. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (r \<unrhd> (p && ~~ mask pd_bits)) s; c \<notin> kernel_mapping_slots; c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref (pd c) = Some q; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) proof (prove)
goal (2 subgoals):
 1. \<And>s pd r c q q' pt d. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref (pd c) = Some q; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'\<rbrakk> \<Longrightarrow> ((r, p && ~~ mask pd_bits), VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r, q) \<in> vs_lookup_pages1 s
 2. \<And>s pd r c q q' pt d. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref (pd c) = Some q; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; ((VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) proof (prove)
goal (1 subgoal):
 1. \<And>s pd r c q q' pt d. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref (pd c) = Some q; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; ((VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) proof (prove)
goal (2 subgoals):
 1. \<And>s pd r c q q' pt d. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref (pd c) = Some q; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'\<rbrakk> \<Longrightarrow> ((VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r, q), VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r, q') \<in> vs_lookup_pages1 s
 2. \<And>s pd r c q q' pt d. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref (pd c) = Some q; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; ((VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q') s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) proof (prove)
goal (1 subgoal):
 1. \<And>s pd r c q q' pt d. \<lbrakk>valid_arch_caps s; valid_objs s; valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_pde_mappings pde; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; c \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref (pd c) = Some q; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; ((VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q') s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) proof (prove)
goal:
No subgoals!