theory ArchIpc_IF

lemma captransfer_in_ipc_buffer[Ipc_IF_assms]:
  "\<lbrakk> is_aligned (buf :: obj_ref) msg_align_bits; n \<in> {0..2} \<rbrakk>
     \<Longrightarrow> ptr_range (buf + (2 + (of_nat msg_max_length + of_nat msg_max_extra_caps)) * word_size
                                                                                    + n * 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)+ apply (simp add: image_def msg_max_length_def msg_max_extra_caps_def) apply (rule_tac x="(125::nat) + unat n"  in bexI) apply simp+ apply (fastforce intro: unat_less_helper word_leq_minus_one_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned buf msg_align_bits; n \<in> {0..2}\<rbrakk> \<Longrightarrow> ptr_range (buf + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + n * word_size) word_size_bits \<subseteq> ptr_range buf msg_align_bits proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned buf msg_align_bits; n \<in> {0..2}\<rbrakk> \<Longrightarrow> is_aligned buf msg_align_bits
 2. \<lbrakk>is_aligned buf msg_align_bits; n \<in> {0..2}\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 3. \<lbrakk>is_aligned buf msg_align_bits; n \<in> {0..2}\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 4. \<lbrakk>is_aligned buf msg_align_bits; n \<in> {0..2}\<rbrakk> \<Longrightarrow> buf + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + n * word_size \<in> set [buf , buf + word_size .e. buf + 2 ^ msg_align_bits - 1] proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned buf msg_align_bits; n \<in> {0..2}\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 2. \<lbrakk>is_aligned buf msg_align_bits; n \<in> {0..2}\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 3. \<lbrakk>is_aligned buf msg_align_bits; n \<in> {0..2}\<rbrakk> \<Longrightarrow> buf + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + n * word_size \<in> set [buf , buf + word_size .e. buf + 2 ^ msg_align_bits - 1] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned buf msg_align_bits; n \<in> {0..2}\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 2. \<lbrakk>is_aligned buf msg_align_bits; n \<in> {0..2}\<rbrakk> \<Longrightarrow> buf + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + n * word_size \<in> set [buf , buf + word_size .e. buf + 2 ^ msg_align_bits - 1] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned buf msg_align_bits; n \<in> {0..2}\<rbrakk> \<Longrightarrow> buf + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + n * word_size \<in> set [buf , buf + word_size .e. buf + 2 ^ msg_align_bits - 1] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned buf msg_align_bits; n \<le> 2\<rbrakk> \<Longrightarrow> buf + (8 + (word_of_nat msg_max_length * 4 + word_of_nat msg_max_extra_caps * 4)) + n * 4 \<in> set [buf , buf + 4 .e. buf + 2 ^ msg_align_bits - 1] proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned buf msg_align_bits; n \<le> 2\<rbrakk> \<Longrightarrow> is_aligned buf msg_align_bits
 2. \<lbrakk>is_aligned buf msg_align_bits; n \<le> 2\<rbrakk> \<Longrightarrow> msg_align_bits < LENGTH(32)
 3. \<lbrakk>is_aligned buf msg_align_bits; n \<le> 2\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits
 4. \<lbrakk>is_aligned buf msg_align_bits; n \<le> 2\<rbrakk> \<Longrightarrow> buf + (8 + (word_of_nat msg_max_length * 4 + word_of_nat msg_max_extra_caps * 4)) + 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>is_aligned buf 9; n \<le> 2\<rbrakk> \<Longrightarrow> buf + (8 + (word_of_nat msg_max_length * 4 + word_of_nat msg_max_extra_caps * 4)) + n * 4 \<in> (\<lambda>x. buf + word_of_nat x * 4) ` {0..<128} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned buf 9; n \<le> 2\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<128}. 0x1F4 + n * 4 = word_of_nat x * 4 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned buf 9; n \<le> 2\<rbrakk> \<Longrightarrow> 0x1F4 + n * 4 = word_of_nat (125 + unat n) * 4
 2. \<lbrakk>is_aligned buf 9; n \<le> 2\<rbrakk> \<Longrightarrow> 125 + unat n \<in> {0..<128} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned buf 9; n \<le> 2\<rbrakk> \<Longrightarrow> unat n < 3 proof (prove)
goal:
No subgoals!