theory Ipc_IF

lemma aag_has_auth_to_read_captransfer:
  "\<lbrakk> ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer); x \<in> {0..2} \<rbrakk>
     \<Longrightarrow> for_each_byte_of_word (aag_can_read aag)
           (buffer + (2 + (of_nat msg_max_length + of_nat msg_max_extra_caps)) * word_size
                                                                               + x * 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 captransfer_in_ipc_buffer]) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer); x \<in> {0..2}\<rbrakk> \<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + x * word_size) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned buffer msg_align_bits \<and> (\<forall>x\<in>ptr_range buffer msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag); x \<le> 2\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + x * word_size) word_size_bits. aag_can_read aag x proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned buffer msg_align_bits \<and> (\<forall>x\<in>ptr_range buffer msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag); x \<le> 2; xa \<in> ptr_range (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + x * word_size) word_size_bits\<rbrakk> \<Longrightarrow> aag_can_read aag xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned buffer msg_align_bits \<and> (\<forall>x\<in>ptr_range buffer msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag); x \<le> 2; xa \<in> ptr_range (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + x * word_size) word_size_bits\<rbrakk> \<Longrightarrow> (pasSubject aag, Read, pasObjectAbs aag xa) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<le> 2; xa \<in> ptr_range (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + x * word_size) word_size_bits; is_aligned buffer msg_align_bits; \<forall>x\<in>ptr_range buffer msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Read, pasObjectAbs aag xa) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<le> 2; xa \<in> ptr_range (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + x * word_size) word_size_bits; is_aligned buffer msg_align_bits\<rbrakk> \<Longrightarrow> xa \<in> ptr_range buffer msg_align_bits proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>x \<le> 2; xa \<in> ptr_range (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + x * word_size) word_size_bits; is_aligned buffer msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned buffer msg_align_bits
 2. \<And>xa. \<lbrakk>x \<le> 2; xa \<in> ptr_range (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + x * word_size) word_size_bits; is_aligned buffer msg_align_bits\<rbrakk> \<Longrightarrow> ?p12 xa \<in> {0..2}
 3. \<And>xa. \<lbrakk>x \<le> 2; xa \<in> ptr_range (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + x * word_size) word_size_bits; is_aligned buffer msg_align_bits\<rbrakk> \<Longrightarrow> xa \<in> ptr_range (buffer + (2 + (word_of_nat msg_max_length + word_of_nat msg_max_extra_caps)) * word_size + ?p12 xa * word_size) word_size_bits proof (prove)
goal:
No subgoals!