theory ArchIpc_IF

lemma mrs_in_ipc_buffer[Ipc_IF_assms]:
  "\<lbrakk> n \<in> set [length msg_registers + 1 ..< Suc n'];
     is_aligned (buf :: obj_ref) msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits) \<rbrakk>
     \<Longrightarrow> ptr_range (buf + of_nat n * of_nat word_size) word_size_bits \<subseteq> ptr_range buf 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 word_size_bits_def)+ apply (simp add: image_def) apply (rule_tac x=n in bexI) apply (rule refl) apply (fastforce split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> set [length msg_registers + 1..<Suc n']; is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits \<subseteq> ptr_range buf msg_align_bits proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<in> set [length msg_registers + 1..<Suc n']; is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> is_aligned buf msg_align_bits
 2. \<lbrakk>n \<in> set [length msg_registers + 1..<Suc n']; is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 3. \<lbrakk>n \<in> set [length msg_registers + 1..<Suc n']; is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 4. \<lbrakk>n \<in> set [length msg_registers + 1..<Suc n']; is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> buf + word_of_nat n * word_of_nat word_size \<in> set [buf , buf + word_size .e. buf + 2 ^ msg_align_bits - 1] proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<in> set [length msg_registers + 1..<Suc n']; is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 2. \<lbrakk>n \<in> set [length msg_registers + 1..<Suc n']; is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 3. \<lbrakk>n \<in> set [length msg_registers + 1..<Suc n']; is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> buf + word_of_nat n * word_of_nat word_size \<in> set [buf , buf + word_size .e. buf + 2 ^ msg_align_bits - 1] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<in> set [length msg_registers + 1..<Suc n']; is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 2. \<lbrakk>n \<in> set [length msg_registers + 1..<Suc n']; is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> buf + word_of_nat n * word_of_nat word_size \<in> set [buf , buf + word_size .e. buf + 2 ^ msg_align_bits - 1] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> set [length msg_registers + 1..<Suc n']; is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> buf + word_of_nat n * word_of_nat word_size \<in> set [buf , buf + word_size .e. buf + 2 ^ msg_align_bits - 1] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> buf + word_of_nat n * 4 \<in> set [buf , buf + 4 .e. buf + 2 ^ msg_align_bits - 1] proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> is_aligned buf msg_align_bits
 2. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> msg_align_bits < LENGTH(32)
 3. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits
 4. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> buf + word_of_nat n * 4 \<in> set (map (\<lambda>x. buf + word_of_nat x * 4) [0..<2 ^ (msg_align_bits - 2)]) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); is_aligned buf 9; n' < 128\<rbrakk> \<Longrightarrow> buf + word_of_nat n * 4 \<in> (\<lambda>x. buf + word_of_nat x * 4) ` {0..<128} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); is_aligned buf 9; n' < 128\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<128}. word_of_nat n * 4 = word_of_nat x * 4 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); is_aligned buf 9; n' < 128\<rbrakk> \<Longrightarrow> word_of_nat n * 4 = word_of_nat n * 4
 2. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); is_aligned buf 9; n' < 128\<rbrakk> \<Longrightarrow> n \<in> {0..<128} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); is_aligned buf 9; n' < 128\<rbrakk> \<Longrightarrow> n \<in> {0..<128} proof (prove)
goal:
No subgoals!