theory Ipc_IF

lemma aag_has_auth_to_read_mrs:
  "\<lbrakk> aag_can_read_or_affect_ipc_buffer aag l (Some buf);
     n \<in> set [length msg_registers + 1..<Suc n'];
     n' < 2 ^ (msg_align_bits - word_size_bits) \<rbrakk>
     \<Longrightarrow> for_each_byte_of_word
           (\<lambda>x. aag_can_read_label aag (pasObjectAbs aag x) \<or> aag_can_affect aag l x)
           (buf + of_nat n * of_nat word_size)" apply (simp add: for_each_byte_of_word_def2 aag_can_read_or_affect_ipc_buffer_def) apply (rule ballI) apply (erule conjE) apply (erule bspec) apply (rule subsetD[OF mrs_in_ipc_buffer[where n=n and n'=n']]) apply (clarsimp split: if_splits) apply assumption apply assumption apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aag_can_read_or_affect_ipc_buffer aag l (Some buf); n \<in> set [length msg_registers + 1..<Suc n']; n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> for_each_byte_of_word (aag_can_read_or_affect aag l) (buf + word_of_nat n * word_of_nat word_size) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned buf msg_align_bits \<and> (\<forall>x\<in>ptr_range buf msg_align_bits. aag_can_read_or_affect aag l x); Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits. aag_can_read_or_affect aag l x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned buf msg_align_bits \<and> (\<forall>x\<in>ptr_range buf msg_align_bits. aag_can_read_or_affect aag l x); Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits; \<forall>x\<in>ptr_range buf msg_align_bits. aag_can_read_or_affect aag l x\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits\<rbrakk> \<Longrightarrow> x \<in> ptr_range buf msg_align_bits proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits\<rbrakk> \<Longrightarrow> n \<in> set [length msg_registers + 1..<Suc n']
 2. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned buf msg_align_bits
 3. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits\<rbrakk> \<Longrightarrow> n' < 2 ^ (msg_align_bits - word_size_bits)
 4. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits\<rbrakk> \<Longrightarrow> x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned buf msg_align_bits
 2. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits\<rbrakk> \<Longrightarrow> n' < 2 ^ (msg_align_bits - word_size_bits)
 3. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits\<rbrakk> \<Longrightarrow> x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits\<rbrakk> \<Longrightarrow> n' < 2 ^ (msg_align_bits - word_size_bits)
 2. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits\<rbrakk> \<Longrightarrow> x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Suc (length msg_registers) \<le> n' \<and> (n = n' \<or> Suc (length msg_registers) \<le> n \<and> n < n'); n' < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned buf msg_align_bits\<rbrakk> \<Longrightarrow> x \<in> ptr_range (buf + word_of_nat n * word_of_nat word_size) word_size_bits proof (prove)
goal:
No subgoals!