theory Ipc_IF

lemma ptr_in_obj_range:
  "\<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj\<rbrakk>
  \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<in> obj_range ptr obj" apply (simp add: obj_range_def) apply (rule context_conjI) apply (frule(1) pspace_alignedD) apply (erule is_aligned_no_wrap') apply (rule and_mask_less') apply (drule valid_obj_sizes) apply fastforce apply (simp add: word_bits_def) apply (simp add: p_assoc_help) apply (rule word_plus_mono_right) apply (rule word_less_sub_1) apply (drule valid_obj_sizes) apply fastforce apply (simp add: word_bits_def and_mask_less') apply (rule is_aligned_no_overflow') apply (erule(1) pspace_alignedD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj\<rbrakk> \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<in> obj_range ptr obj proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (a && mask (obj_bits obj)) \<and> ptr + (a && mask (obj_bits obj)) \<le> ptr + 2 ^ obj_bits obj - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (a && mask (obj_bits obj))
 2. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<le> ptr + 2 ^ obj_bits obj - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; is_aligned ptr (obj_bits obj)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (a && mask (obj_bits obj))
 2. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<le> ptr + 2 ^ obj_bits obj - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj\<rbrakk> \<Longrightarrow> a && mask (obj_bits obj) < 2 ^ obj_bits obj
 2. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<le> ptr + 2 ^ obj_bits obj - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj\<rbrakk> \<Longrightarrow> obj_bits obj < LENGTH(32)
 2. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<le> ptr + 2 ^ obj_bits obj - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pspace_aligned s; kheap s ptr = Some obj\<rbrakk> \<Longrightarrow> ?ko10 \<in> ran (kheap s)
 2. \<lbrakk>pspace_aligned s; kheap s ptr = Some obj; obj_bits ?ko10 < word_bits\<rbrakk> \<Longrightarrow> obj_bits obj < LENGTH(32)
 3. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<le> ptr + 2 ^ obj_bits obj - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned s; kheap s ptr = Some obj; obj_bits obj < word_bits\<rbrakk> \<Longrightarrow> obj_bits obj < LENGTH(32)
 2. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<le> ptr + 2 ^ obj_bits obj - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<le> ptr + 2 ^ obj_bits obj - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<le> ptr + (2 ^ obj_bits obj - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> a && mask (obj_bits obj) \<le> 2 ^ obj_bits obj - 1
 2. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ obj_bits obj - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> a && mask (obj_bits obj) < 2 ^ obj_bits obj
 2. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ obj_bits obj - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ?ko21 \<in> ran (kheap s)
 2. \<lbrakk>pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj)); obj_bits ?ko21 < word_bits\<rbrakk> \<Longrightarrow> a && mask (obj_bits obj) < 2 ^ obj_bits obj
 3. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ obj_bits obj - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj)); obj_bits obj < word_bits\<rbrakk> \<Longrightarrow> a && mask (obj_bits obj) < 2 ^ obj_bits obj
 2. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ obj_bits obj - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ obj_bits obj - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj; ptr \<le> ptr + (a && mask (obj_bits obj))\<rbrakk> \<Longrightarrow> is_aligned ptr (obj_bits obj) proof (prove)
goal:
No subgoals!