theory ArchIpc_IF

lemma msg_in_ipc_buffer[Ipc_IF_assms]:
  "\<lbrakk> n = msg_max_length \<or> n < msg_max_length;  is_aligned p msg_align_bits;
     unat (mi_length 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 :: obj_ref) msg_align_bits" apply (rule ptr_range_subset) apply assumption apply (simp add: msg_align_bits') apply (simp add: msg_align_bits 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)+ apply (simp add: image_def) apply (rule_tac x=n in bexI) apply (rule refl) apply (auto simp: msg_max_length_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length 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 = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> is_aligned p msg_align_bits
 2. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 3. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 4. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length 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 = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 2. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 3. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length 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 = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 2. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length 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 = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length 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 = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length 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>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> is_aligned p msg_align_bits
 2. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < LENGTH(32)
 3. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits
 4. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits; unat (mi_length 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 (1 subgoal):
 1. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p 9; unat (mi_length mi) < 2 ^ (9 - word_size_bits)\<rbrakk> \<Longrightarrow> p + word_of_nat n * 4 \<in> (\<lambda>x. p + word_of_nat x * 4) ` {0..<128} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p 9; unat (mi_length mi) < 2 ^ (9 - word_size_bits)\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<128}. word_of_nat n * 4 = word_of_nat x * 4 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p 9; unat (mi_length mi) < 2 ^ (9 - word_size_bits)\<rbrakk> \<Longrightarrow> word_of_nat n * 4 = word_of_nat n * 4
 2. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p 9; unat (mi_length mi) < 2 ^ (9 - word_size_bits)\<rbrakk> \<Longrightarrow> n \<in> {0..<128} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p 9; unat (mi_length mi) < 2 ^ (9 - word_size_bits)\<rbrakk> \<Longrightarrow> n \<in> {0..<128} proof (prove)
goal:
No subgoals!