theory ArchUntyped_AI

lemma copy_global_mappings_nonempty_table:
  "is_aligned pd pd_bits \<Longrightarrow>
   \<lbrace>\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \<and>
        valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace>
   copy_global_mappings pd
   \<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table
                        (set (second_level_tables (arch_state s)))) r s) \<and>
           valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace>" apply (simp add: copy_global_mappings_def) apply (rule hoare_seq_ext [OF _ gets_sp]) apply (rule hoare_strengthen_post) apply (rule mapM_x_wp[where S="{x. kernel_base >> 20 \<le> x \<and>
                                      x < 2 ^ (pd_bits - 2)}"]) apply (wp get_pde_wp hoare_vcg_ball_lift
              store_pde_weaken[THEN iffD2,OF store_pde_nonempty_table]
              store_pde_weaken[THEN iffD2,OF store_pde_global_global_objs]
           | simp)+ apply clarsimp apply (subst (asm) is_aligned_add_helper[THEN conjunct2]) apply (clarsimp simp: valid_arch_state_def pspace_aligned_def dom_def
                            obj_at_def) apply (drule_tac x="arm_global_pd (arch_state s)" in spec, erule impE,
             fastforce) apply (simp add: pd_bits_def pageBits_def) apply (erule shiftl_less_t2n) apply (simp add: pd_bits_def pageBits_def) apply (clarsimp simp: valid_arch_state_def valid_global_objs_def obj_at_def
                          empty_table_def second_level_tables_def) apply (simp add: kernel_mapping_slots_def) apply (subst is_aligned_add_helper[THEN conjunct1], assumption) apply (erule shiftl_less_t2n) apply (simp add: pd_bits_def pageBits_def) apply (simp add: kernel_base_shift_cast_le[symmetric] ucast_ucast_mask) apply (subst shiftl_shiftr_id) apply simp apply (simp add: word_less_nat_alt pd_bits_def pageBits_def) apply (subst less_mask_eq) apply (simp add: pd_bits_def pageBits_def) apply assumption apply (clarsimp simp: pd_bits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>rv s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace> do global_pd <- gets (arm_global_pd \<circ> arch_state);
mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]
od \<lbrace>\<lambda>rv s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>\<lambda>rv s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>?Q4 global_pd\<rbrace>
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ?Q4 global_pd rv s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; x \<in> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>rv. (\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)\<rbrace>
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (arm_global_pd (arch_state s) + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> (\<forall>rf. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))) \<and> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2)))
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s; ako_at (PageDirectory pda) (arm_global_pd (arch_state s) + (x << 2) && ~~ mask pd_bits) s; typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (\<forall>rf. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))) \<and> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2)))
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (5 subgoals):
 1. \<And>x s pda. \<lbrakk>typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s; is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned (arm_global_pd (arch_state s)) pd_bits
 2. \<And>x s pda. \<lbrakk>typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s; is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ pd_bits
 3. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (\<forall>rf. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))) \<and> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2)))
 4. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 5. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (5 subgoals):
 1. \<And>x s pda pdaa. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (second_level_tables (arch_state s))) ko; valid_global_objs s; \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> is_aligned x (obj_bits (the (kheap s x))); valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> is_aligned (arm_global_pd (arch_state s)) pd_bits
 2. \<And>x s pda. \<lbrakk>typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s; is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ pd_bits
 3. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (\<forall>rf. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))) \<and> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2)))
 4. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 5. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (5 subgoals):
 1. \<And>x s pda pdaa. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (second_level_tables (arch_state s))) ko; valid_global_objs s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdaa)); is_aligned (arm_global_pd (arch_state s)) (obj_bits (the (kheap s (arm_global_pd (arch_state s)))))\<rbrakk> \<Longrightarrow> is_aligned (arm_global_pd (arch_state s)) pd_bits
 2. \<And>x s pda. \<lbrakk>typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s; is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ pd_bits
 3. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (\<forall>rf. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))) \<and> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2)))
 4. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 5. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (4 subgoals):
 1. \<And>x s pda. \<lbrakk>typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s; is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ pd_bits
 2. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (\<forall>rf. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))) \<and> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2)))
 3. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 4. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (4 subgoals):
 1. \<And>x s pda. \<lbrakk>typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s; is_aligned pd pd_bits; kernel_base >> 20 \<le> x; \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 2. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (\<forall>rf. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))) \<and> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2)))
 3. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 4. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; valid_global_objs s; valid_arch_state s; pspace_aligned s; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (pd + (x << 2) && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (\<forall>rf. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))) \<and> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2)))
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2)
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (4 subgoals):
 1. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ pd_bits
 2. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (x << 2 >> 2)
 3. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 4. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (4 subgoals):
 1. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 2. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (x << 2 >> 2)
 3. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 4. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (x << 2 >> 2)
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> (x << 2 >> 2) && mask 12
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (5 subgoals):
 1. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - 2)
 3. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> x && mask 12
 4. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 5. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (4 subgoals):
 1. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - 2)
 2. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> x && mask 12
 3. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 4. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> x && mask 12
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (4 subgoals):
 1. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> x < 2 ^ 12
 2. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> x
 3. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 4. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>x s pda pdb. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ko. kheap s r = Some ko \<longrightarrow> \<not> nonempty_table (set (arm_global_pts (arch_state s))) ko; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pdb)); valid_vso_at (arm_global_pd (arch_state s)) s; valid_asid_table (asid_table s) s; kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); \<forall>x. (\<forall>r. pde_ref (pdb x) = Some r \<longrightarrow> r \<in> set (arm_global_pts (arch_state s))) \<and> valid_pde_mappings (pdb x) \<and> (\<not> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> pdb x = InvalidPDE); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> x
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (2 subgoals):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal (1 subgoal):
 1. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s proof (prove)
goal:
No subgoals!