theory ArchIpc_IF

lemma cptrs_in_ipc_buffer[Ipc_IF_assms]:
  "\<lbrakk> n \<in> set [buffer_cptr_index ..< buffer_cptr_index + unat (mi_extra_caps mi)];
     is_aligned (p :: obj_ref) msg_align_bits;
     buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits) \<rbrakk>
     \<Longrightarrow> ptr_range (p + of_nat n * of_nat word_size) word_size_bits \<subseteq> ptr_range p msg_align_bits" apply (rule ptr_range_subset) apply assumption apply (simp add: msg_align_bits') apply (simp add: msg_align_bits' word_size_bits_def word_bits_def) apply (simp add: word_size_def) apply (subst upto_enum_step_shift_red[where us=2, simplified]) apply (simp add: msg_align_bits' word_bits_def word_size_bits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits \<subseteq> ptr_range p msg_align_bits proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> is_aligned p msg_align_bits
 2. \<lbrakk>n \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 3. \<lbrakk>n \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 4. \<lbrakk>n \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> p + word_of_nat n * word_of_nat word_size \<in> set [p , p + word_size .e. p + 2 ^ msg_align_bits - 1] proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 2. \<lbrakk>n \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 3. \<lbrakk>n \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> p + word_of_nat n * word_of_nat word_size \<in> set [p , p + word_size .e. p + 2 ^ msg_align_bits - 1] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 2. \<lbrakk>n \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> p + word_of_nat n * word_of_nat word_size \<in> set [p , p + word_size .e. p + 2 ^ msg_align_bits - 1] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> p + word_of_nat n * word_of_nat word_size \<in> set [p , p + word_size .e. p + 2 ^ msg_align_bits - 1] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>buffer_cptr_index \<le> n \<and> n < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> p + word_of_nat n * 4 \<in> set [p , p + 4 .e. p + 2 ^ msg_align_bits - 1] proof (prove)
goal (4 subgoals):
 1. \<lbrakk>buffer_cptr_index \<le> n \<and> n < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> is_aligned p msg_align_bits
 2. \<lbrakk>buffer_cptr_index \<le> n \<and> n < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < LENGTH(32)
 3. \<lbrakk>buffer_cptr_index \<le> n \<and> n < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits
 4. \<lbrakk>buffer_cptr_index \<le> n \<and> n < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned p msg_align_bits; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> p + word_of_nat n * 4 \<in> set (map (\<lambda>x. p + word_of_nat x * 4) [0..<2 ^ (msg_align_bits - 2)]) proof (prove)
goal:
No subgoals!