theory ArchADT_AC

lemma ptr_offset_in_ptr_range:
  "\<lbrakk> invs s; x \<notin> kernel_mappings;
     get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s);
     get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
                   (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r) \<rbrakk>
     \<Longrightarrow> ptrFromPAddr base + (x && mask sz) \<in> ptr_range (ptrFromPAddr base) sz" apply (simp add: ptr_range_def mask_def) apply (rule conjI) apply (rule_tac b="2 ^ sz - 1" in word_plus_mono_right2) apply (frule some_get_page_info_umapsD) apply (clarsimp simp: get_pd_of_thread_reachable invs_vspace_objs
                                invs_psp_aligned invs_valid_asid_table invs_valid_objs)+ apply (drule is_aligned_ptrFromPAddr_n) apply (simp add: pageBitsForSize_def split: vmpage_size.splits) apply (clarsimp simp: is_aligned_no_overflow' word_and_le1)+ apply (subst p_assoc_help) apply (rule word_plus_mono_right) apply (rule word_and_le1) apply (frule some_get_page_info_umapsD) apply (clarsimp simp: get_pd_of_thread_reachable invs_vspace_objs
                              invs_psp_aligned invs_valid_asid_table invs_valid_objs)+ apply (drule is_aligned_ptrFromPAddr_n) apply (simp add: pageBitsForSize_def split: vmpage_size.splits) apply (clarsimp simp: is_aligned_no_overflow') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base + (x && mask sz) \<in> ptr_range (ptrFromPAddr base) sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (x && 2 ^ sz - 1) \<and> ptrFromPAddr base + (x && 2 ^ sz - 1) \<le> ptrFromPAddr base + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (x && 2 ^ sz - 1)
 2. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base + (x && 2 ^ sz - 1) \<le> ptrFromPAddr base + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (2 ^ sz - 1)
 2. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> x && 2 ^ sz - 1 \<le> 2 ^ sz - 1
 3. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base + (x && 2 ^ sz - 1) \<le> ptrFromPAddr base + 2 ^ sz - 1 proof (prove)
goal (9 subgoals):
 1. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> get_pd_of_thread (kheap s) (arch_state s) tcb) s
 2. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> x \<notin> kernel_mappings
 3. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 4. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> pspace_aligned s
 5. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s
 6. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> valid_objs s
 7. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); \<exists>sza. pageBitsForSize sza = sz \<and> is_aligned base sz \<and> data_at sza (ptrFromPAddr base) s\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (2 ^ sz - 1)
 8. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> x && 2 ^ sz - 1 \<le> 2 ^ sz - 1
 9. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base + (x && 2 ^ sz - 1) \<le> ptrFromPAddr base + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<And>sza. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, pageBitsForSize sza, attr, r); sz = pageBitsForSize sza; is_aligned base (pageBitsForSize sza); data_at sza (ptrFromPAddr base) s\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (2 ^ pageBitsForSize sza - 1)
 2. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> x && 2 ^ sz - 1 \<le> 2 ^ sz - 1
 3. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base + (x && 2 ^ sz - 1) \<le> ptrFromPAddr base + 2 ^ sz - 1 proof (prove)
goal (4 subgoals):
 1. \<And>sza. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, pageBitsForSize sza, attr, r); sz = pageBitsForSize sza; data_at sza (ptrFromPAddr base) s\<rbrakk> \<Longrightarrow> pageBitsForSize sza \<le> 24
 2. \<And>sza. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, pageBitsForSize sza, attr, r); sz = pageBitsForSize sza; data_at sza (ptrFromPAddr base) s; is_aligned (ptrFromPAddr base) (pageBitsForSize sza)\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (2 ^ pageBitsForSize sza - 1)
 3. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> x && 2 ^ sz - 1 \<le> 2 ^ sz - 1
 4. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base + (x && 2 ^ sz - 1) \<le> ptrFromPAddr base + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<And>sza. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, pageBitsForSize sza, attr, r); sz = pageBitsForSize sza; data_at sza (ptrFromPAddr base) s; is_aligned (ptrFromPAddr base) (pageBitsForSize sza)\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (2 ^ pageBitsForSize sza - 1)
 2. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> x && 2 ^ sz - 1 \<le> 2 ^ sz - 1
 3. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base + (x && 2 ^ sz - 1) \<le> ptrFromPAddr base + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base + (x && 2 ^ sz - 1) \<le> ptrFromPAddr base + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base + (x && 2 ^ sz - 1) \<le> ptrFromPAddr base + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> x && 2 ^ sz - 1 \<le> 2 ^ sz - 1
 2. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (2 ^ sz - 1) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> get_pd_of_thread (kheap s) (arch_state s) tcb) s
 2. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> x \<notin> kernel_mappings
 3. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 4. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> pspace_aligned s
 5. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s
 6. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r)\<rbrakk> \<Longrightarrow> valid_objs s
 7. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); \<exists>sza. pageBitsForSize sza = sz \<and> is_aligned base sz \<and> data_at sza (ptrFromPAddr base) s\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>sza. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, pageBitsForSize sza, attr, r); sz = pageBitsForSize sza; is_aligned base (pageBitsForSize sza); data_at sza (ptrFromPAddr base) s\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (2 ^ pageBitsForSize sza - 1) proof (prove)
goal (2 subgoals):
 1. \<And>sza. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, pageBitsForSize sza, attr, r); sz = pageBitsForSize sza; data_at sza (ptrFromPAddr base) s\<rbrakk> \<Longrightarrow> pageBitsForSize sza \<le> 24
 2. \<And>sza. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, pageBitsForSize sza, attr, r); sz = pageBitsForSize sza; data_at sza (ptrFromPAddr base) s; is_aligned (ptrFromPAddr base) (pageBitsForSize sza)\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (2 ^ pageBitsForSize sza - 1) proof (prove)
goal (1 subgoal):
 1. \<And>sza. \<lbrakk>invs s; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, pageBitsForSize sza, attr, r); sz = pageBitsForSize sza; data_at sza (ptrFromPAddr base) s; is_aligned (ptrFromPAddr base) (pageBitsForSize sza)\<rbrakk> \<Longrightarrow> ptrFromPAddr base \<le> ptrFromPAddr base + (2 ^ pageBitsForSize sza - 1) proof (prove)
goal:
No subgoals!