theory Ipc_IF

lemma aag_has_auth_to_read_cptrs:
  "\<lbrakk> x \<in> set [buffer_cptr_index ..< buffer_cptr_index + unat (mi_extra_caps mi)];
     ipc_buffer_has_read_auth aag (pasSubject aag) (Some a);
     buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits) \<rbrakk>
     \<Longrightarrow> for_each_byte_of_word (\<lambda> y. aag_can_read aag y) (a + of_nat x * 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 cptrs_in_ipc_buffer]) apply fastforce apply assumption apply assumption apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]; ipc_buffer_has_read_auth aag (pasSubject aag) (Some a); buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (a + word_of_nat x * word_of_nat word_size) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>buffer_cptr_index \<le> x \<and> x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits \<and> (\<forall>x\<in>ptr_range a msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag); buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits. aag_can_read aag x proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>buffer_cptr_index \<le> x \<and> x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits \<and> (\<forall>x\<in>ptr_range a msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag); buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> aag_can_read aag xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>buffer_cptr_index \<le> x \<and> x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits \<and> (\<forall>x\<in>ptr_range a msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag); buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat 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>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits; \<forall>x\<in>ptr_range a 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>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits\<rbrakk> \<Longrightarrow> xa \<in> ptr_range a msg_align_bits proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits\<rbrakk> \<Longrightarrow> ?n13 xa \<in> set [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (?mi13 xa))]
 2. \<And>xa. \<lbrakk>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned a msg_align_bits
 3. \<And>xa. \<lbrakk>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits\<rbrakk> \<Longrightarrow> buffer_cptr_index + unat (mi_extra_caps (?mi13 xa)) < 2 ^ (msg_align_bits - word_size_bits)
 4. \<And>xa. \<lbrakk>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits\<rbrakk> \<Longrightarrow> xa \<in> ptr_range (a + word_of_nat (?n13 xa) * word_of_nat word_size) word_size_bits proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned a msg_align_bits
 2. \<And>xa. \<lbrakk>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits\<rbrakk> \<Longrightarrow> buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)
 3. \<And>xa. \<lbrakk>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits\<rbrakk> \<Longrightarrow> xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits\<rbrakk> \<Longrightarrow> buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)
 2. \<And>xa. \<lbrakk>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits\<rbrakk> \<Longrightarrow> xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits; buffer_cptr_index \<le> x; x < buffer_cptr_index + unat (mi_extra_caps mi); is_aligned a msg_align_bits\<rbrakk> \<Longrightarrow> xa \<in> ptr_range (a + word_of_nat x * word_of_nat word_size) word_size_bits proof (prove)
goal:
No subgoals!