theory ArchUserOp_IF

lemma data_at_obj_range:
  "\<lbrakk> data_at sz ptr s; pspace_aligned s; valid_objs s \<rbrakk>
     \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz))" apply (clarsimp simp: data_at_def) apply (elim disjE) apply (clarsimp simp: obj_at_def) apply (drule (2) ptr_in_obj_range) apply (clarsimp simp: obj_bits_def obj_range_def) apply fastforce apply (clarsimp simp: obj_at_def) apply (drule (2) ptr_in_obj_range) apply (clarsimp simp: obj_bits_def obj_range_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>data_at sz ptr s; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch (AUserData sz)) ptr s \<or> typ_at (AArch (ADeviceData sz)) ptr s; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned s; valid_objs s; typ_at (AArch (AUserData sz)) ptr s\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz))
 2. \<lbrakk>pspace_aligned s; valid_objs s; typ_at (AArch (ADeviceData sz)) ptr s\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned s; valid_objs s; kheap s ptr = Some (ArchObj (DataPage False sz))\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz))
 2. \<lbrakk>pspace_aligned s; valid_objs s; typ_at (AArch (ADeviceData sz)) ptr s\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned s; kheap s ptr = Some (ArchObj (DataPage False sz)); ptr + (?a7 && mask (obj_bits (ArchObj (DataPage False sz)))) \<in> obj_range ptr (ArchObj (DataPage False sz))\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz))
 2. \<lbrakk>pspace_aligned s; valid_objs s; typ_at (AArch (ADeviceData sz)) ptr s\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned s; kheap s ptr = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + (?a7 && mask (pageBitsForSize sz)); ptr + (?a7 && mask (pageBitsForSize sz)) \<le> ptr + 2 ^ pageBitsForSize sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (offset && mask (pageBitsForSize sz)) \<and> ptr + (offset && mask (pageBitsForSize sz)) \<le> ptr + 2 ^ pageBitsForSize sz - 1
 2. \<lbrakk>pspace_aligned s; valid_objs s; typ_at (AArch (ADeviceData sz)) ptr s\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; valid_objs s; typ_at (AArch (ADeviceData sz)) ptr s\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; valid_objs s; kheap s ptr = Some (ArchObj (DataPage True sz))\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; kheap s ptr = Some (ArchObj (DataPage True sz)); ptr + (?a21 && mask (obj_bits (ArchObj (DataPage True sz)))) \<in> obj_range ptr (ArchObj (DataPage True sz))\<rbrakk> \<Longrightarrow> ptr + (offset && mask (pageBitsForSize sz)) \<in> obj_range ptr (ArchObj (DataPage dev sz)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; kheap s ptr = Some (ArchObj (DataPage True sz)); ptr \<le> ptr + (?a21 && mask (pageBitsForSize sz)); ptr + (?a21 && mask (pageBitsForSize sz)) \<le> ptr + 2 ^ pageBitsForSize sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (offset && mask (pageBitsForSize sz)) \<and> ptr + (offset && mask (pageBitsForSize sz)) \<le> ptr + 2 ^ pageBitsForSize sz - 1 proof (prove)
goal:
No subgoals!