theory Ipc_IF

lemma aag_has_auth_to_read_msg:
  "\<lbrakk> n = msg_max_length \<or> n < msg_max_length;
     ipc_buffer_has_read_auth aag (pasSubject aag) (Some p);
     unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits) \<rbrakk>
     \<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (p + of_nat n * of_nat word_size)" apply (simp add: for_each_byte_of_word_def2 ipc_buffer_has_read_auth_def) apply (rule ballI) apply (rule reads_read) apply (clarify) apply (erule bspec) apply (rule subsetD[OF msg_in_ipc_buffer[where n=n]]) apply assumption apply assumption apply assumption apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; ipc_buffer_has_read_auth aag (pasSubject aag) (Some p); unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (p + word_of_nat n * word_of_nat word_size) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits \<and> (\<forall>x\<in>ptr_range p msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag); unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits. aag_can_read aag x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits \<and> (\<forall>x\<in>ptr_range p msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag); unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> aag_can_read aag x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits \<and> (\<forall>x\<in>ptr_range p msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag); unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits; \<forall>x\<in>ptr_range p msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> x \<in> ptr_range p msg_align_bits proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> n = msg_max_length \<or> n < msg_max_length
 2. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned p msg_align_bits
 3. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> unat (mi_length (?mi12 x)) < 2 ^ (msg_align_bits - word_size_bits)
 4. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned p msg_align_bits
 2. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> unat (mi_length (?mi12 x)) < 2 ^ (msg_align_bits - word_size_bits)
 3. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> unat (mi_length (?mi12 x)) < 2 ^ (msg_align_bits - word_size_bits)
 2. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n = msg_max_length \<or> n < msg_max_length; unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits); x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits; is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> x \<in> ptr_range (p + word_of_nat n * word_of_nat word_size) word_size_bits proof (prove)
goal:
No subgoals!