theory ArchAInvsPre

lemma (* ptable_rights_imp_frame *)[AInvsPre_asms]:
  assumes "valid_state s"
  shows "ptable_rights t s x \<noteq> {} \<Longrightarrow>
         ptable_lift t s x = Some (addrFromPPtr y) \<Longrightarrow>
         in_user_frame y s \<or> in_device_frame y s" apply (clarsimp simp: ptable_rights_def ptable_lift_def in_user_frame_def
                        in_device_frame_def data_at_def
                 split: option.splits) apply (rename_tac b a r) apply (case_tac "x \<in> kernel_mappings") apply (frule (1) some_get_page_info_kmapsD) using assms apply (clarsimp simp add: valid_state_def) using assms apply (clarsimp simp add: valid_state_def) apply simp apply (frule some_get_page_info_umapsD) apply (rule get_pd_of_thread_reachable) apply clarsimp apply (frule get_page_info_gpd_kmaps[rotated 2]) using assms apply (simp_all add: valid_state_def valid_pspace_def
                               valid_arch_state_def) apply clarsimp apply (frule is_aligned_add_helper[OF _ and_mask_less',
                                     THEN conjunct2, of _ _ x]) apply (simp only: pbfs_less_wb'[simplified word_bits_def]) apply (clarsimp simp: ptrFromPAddr_def addrFromPPtr_def
                        field_simps) apply (rule_tac x=sz in exI) apply (drule_tac x = sz in spec) apply (subst add.assoc[symmetric]) apply (frule is_aligned_add_helper[OF aligned_add_aligned[OF _ is_aligned_pptrBaseOffset]]) apply (rule le_refl) apply (rule_tac w = x in and_mask_less') apply (case_tac sz, simp_all add: word_bits_conv)[1] apply (clarsimp simp: field_simps simp: data_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptable_rights t s x \<noteq> {}; ptable_lift t s x = Some (addrFromPPtr y)\<rbrakk> \<Longrightarrow> in_user_frame y s \<or> in_device_frame y s proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (a, aa, ab, b); b \<noteq> {}; a + (x && mask aa) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (2 subgoals):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s
 2. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (4 subgoals):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings s
 2. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> equal_kernel_mappings s
 3. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings; (\<exists>sz. pageBitsForSize sz = b) \<and> r = {}\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s
 4. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
using this:
valid_state s

goal (4 subgoals):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings s
 2. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> equal_kernel_mappings s
 3. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings; (\<exists>sz. pageBitsForSize sz = b) \<and> r = {}\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s
 4. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (3 subgoals):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> equal_kernel_mappings s
 2. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings; (\<exists>sz. pageBitsForSize sz = b) \<and> r = {}\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s
 3. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
using this:
valid_state s

goal (3 subgoals):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> equal_kernel_mappings s
 2. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings; (\<exists>sz. pageBitsForSize sz = b) \<and> r = {}\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s
 3. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (2 subgoals):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<in> kernel_mappings; (\<exists>sz. pageBitsForSize sz = b) \<and> r = {}\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s
 2. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (7 subgoals):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> get_pd_of_thread (kheap s) (arch_state s) t) s
 2. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> x \<notin> kernel_mappings
 3. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 4. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> pspace_aligned s
 5. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s
 6. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_objs s
 7. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; \<exists>sz. pageBitsForSize sz = b \<and> is_aligned aa b \<and> data_at sz (ptrFromPAddr aa) s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (7 subgoals):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> get_pd_of_thread (kheap s) (arch_state s) t \<noteq> arm_global_pd (arch_state s)
 2. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> x \<notin> kernel_mappings
 3. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 4. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> pspace_aligned s
 5. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s
 6. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_objs s
 7. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; \<exists>sz. pageBitsForSize sz = b \<and> is_aligned aa b \<and> data_at sz (ptrFromPAddr aa) s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (7 subgoals):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) t = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> x \<notin> kernel_mappings
 3. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 4. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> pspace_aligned s
 5. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s
 6. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_objs s
 7. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; \<exists>sz. pageBitsForSize sz = b \<and> is_aligned aa b \<and> data_at sz (ptrFromPAddr aa) s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (9 subgoals):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) t = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> valid_global_objs s
 2. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) t = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) t = arm_global_pd (arch_state s); x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> x \<notin> kernel_mappings
 5. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 6. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> pspace_aligned s
 7. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s
 8. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_objs s
 9. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; \<exists>sz. pageBitsForSize sz = b \<and> is_aligned aa b \<and> data_at sz (ptrFromPAddr aa) s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
using this:
valid_state s

goal (9 subgoals):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) t = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> valid_global_objs s
 2. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) t = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) t = arm_global_pd (arch_state s); x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> x \<notin> kernel_mappings
 5. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 6. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> pspace_aligned s
 7. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s
 8. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> valid_objs s
 9. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; \<exists>sz. pageBitsForSize sz = b \<and> is_aligned aa b \<and> data_at sz (ptrFromPAddr aa) s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>aa b a r. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, b, a, r); r \<noteq> {}; aa + (x && mask b) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; \<exists>sz. pageBitsForSize sz = b \<and> is_aligned aa b \<and> data_at sz (ptrFromPAddr aa) s; valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_asid_table (asid_table s) s \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s \<and> valid_global_pts s \<and> is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)) \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; aa + (x && mask (pageBitsForSize sz)) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (ptrFromPAddr aa) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (2 subgoals):
 1. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; aa + (x && mask (pageBitsForSize sz)) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (ptrFromPAddr aa) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s\<rbrakk> \<Longrightarrow> pageBitsForSize sz < LENGTH(32)
 2. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; aa + (x && mask (pageBitsForSize sz)) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (ptrFromPAddr aa) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; aa + (x && mask (pageBitsForSize sz)) = addrFromPPtr y; \<forall>sz. \<not> typ_at (AArch (ADeviceData sz)) (y && ~~ mask (pageBitsForSize sz)) s; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (ptrFromPAddr aa) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; \<forall>sza. \<not> typ_at (AArch (ADeviceData sza)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sza)) s; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz)))\<rbrakk> \<Longrightarrow> \<exists>sza. typ_at (AArch (AUserData sza)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sza)) s proof (prove)
goal (1 subgoal):
 1. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; \<forall>sza. \<not> typ_at (AArch (ADeviceData sza)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sza)) s; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz)))\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))); \<not> typ_at (AArch (ADeviceData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))); \<not> typ_at (AArch (ADeviceData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) (aa + pptrBaseOffset + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (3 subgoals):
 1. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))); \<not> typ_at (AArch (ADeviceData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> pageBitsForSize (?sz102 aa a r sz) \<le> pageBitsForSize sz
 2. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))); \<not> typ_at (AArch (ADeviceData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> ?d102 aa a r sz < 2 ^ pageBitsForSize (?sz102 aa a r sz)
 3. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))); \<not> typ_at (AArch (ADeviceData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s; aa + pptrBaseOffset + ?d102 aa a r sz && mask (pageBitsForSize (?sz102 aa a r sz)) = ?d102 aa a r sz \<and> aa + pptrBaseOffset + ?d102 aa a r sz && ~~ mask (pageBitsForSize (?sz102 aa a r sz)) = aa + pptrBaseOffset\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) (aa + pptrBaseOffset + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (2 subgoals):
 1. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))); \<not> typ_at (AArch (ADeviceData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> ?d102 aa a r sz < 2 ^ pageBitsForSize sz
 2. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))); \<not> typ_at (AArch (ADeviceData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s; aa + pptrBaseOffset + ?d102 aa a r sz && mask (pageBitsForSize sz) = ?d102 aa a r sz \<and> aa + pptrBaseOffset + ?d102 aa a r sz && ~~ mask (pageBitsForSize sz) = aa + pptrBaseOffset\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) (aa + pptrBaseOffset + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (2 subgoals):
 1. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))); \<not> typ_at (AArch (ADeviceData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> pageBitsForSize sz < LENGTH(32)
 2. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))); \<not> typ_at (AArch (ADeviceData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s; aa + pptrBaseOffset + (x && mask (pageBitsForSize sz)) && mask (pageBitsForSize sz) = x && mask (pageBitsForSize sz) \<and> aa + pptrBaseOffset + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa + pptrBaseOffset\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) (aa + pptrBaseOffset + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>aa a r sz. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) x = Some (aa, pageBitsForSize sz, a, r); r \<noteq> {}; x \<notin> kernel_mappings; valid_objs s; pspace_aligned s; is_aligned aa (pageBitsForSize sz); data_at sz (aa + pptrBaseOffset) s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; aa + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa; y = aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))); \<not> typ_at (AArch (ADeviceData sz)) (aa + (pptrBaseOffset + (x && mask (pageBitsForSize sz))) && ~~ mask (pageBitsForSize sz)) s; aa + pptrBaseOffset + (x && mask (pageBitsForSize sz)) && mask (pageBitsForSize sz) = x && mask (pageBitsForSize sz) \<and> aa + pptrBaseOffset + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = aa + pptrBaseOffset\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) (aa + pptrBaseOffset + (x && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal:
No subgoals!