theory Arch_AC

lemma store_word_offs_integrity_autarch:
  "\<lbrace>\<lambda>s. integrity aag X st s \<and> is_subject aag thread \<and>
        ipc_buffer_has_auth aag thread (Some buf) \<and>
        r < 2 ^ (msg_align_bits - word_size_bits)\<rbrace>
   store_word_offs buf r v
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: store_word_offs_def) apply (rule hoare_pre) apply (wp dmo_storeWord_respects_Write) apply clarsimp apply (drule (1) ipc_buffer_has_auth_wordE) apply (simp add: word_size_word_size_bits is_aligned_mult_triv2) apply (simp add: msg_align_bits') apply (erule mul_word_size_lt_msg_align_bits_ofnat) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> is_subject aag thread \<and> ipc_buffer_has_auth aag thread (Some buf) \<and> r < 2 ^ (msg_align_bits - word_size_bits)\<rbrace> store_word_offs buf r v \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> is_subject aag thread \<and> ipc_buffer_has_auth aag thread (Some buf) \<and> r < 2 ^ (msg_align_bits - word_size_bits)\<rbrace> do s <- get;
y <- assert (in_user_frame (buf + word_of_nat r * word_of_nat word_size) s);
do_machine_op (storeWord (buf + word_of_nat r * word_of_nat word_size) v)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do s <- get;
y <- assert (in_user_frame (buf + word_of_nat r * word_of_nat word_size) s);
do_machine_op (storeWord (buf + word_of_nat r * word_of_nat word_size) v)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. integrity aag X st s \<and> is_subject aag thread \<and> ipc_buffer_has_auth aag thread (Some buf) \<and> r < 2 ^ (msg_align_bits - word_size_bits) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity aag X st s \<and> is_subject aag thread \<and> ipc_buffer_has_auth aag thread (Some buf) \<and> r < 2 ^ (msg_align_bits - word_size_bits) \<Longrightarrow> in_user_frame (buf + word_of_nat r * word_of_nat word_size) s \<longrightarrow> (integrity aag X st and K (\<forall>p'\<in>ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits. (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag)) s proof (prove)
goal (1 subgoal):
 1. \<And>s p'. \<lbrakk>integrity aag X st s; is_subject aag thread; ipc_buffer_has_auth aag thread (Some buf); r < 2 ^ (msg_align_bits - word_size_bits); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; p' \<in> ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag proof (prove)
goal (4 subgoals):
 1. \<And>s p'. \<lbrakk>integrity aag X st s; is_subject aag thread; r < 2 ^ (msg_align_bits - word_size_bits); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; p' \<in> ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) word_size_bits
 2. \<And>s p'. \<lbrakk>integrity aag X st s; is_subject aag thread; r < 2 ^ (msg_align_bits - word_size_bits); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; p' \<in> ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 3. \<And>s p'. \<lbrakk>integrity aag X st s; is_subject aag thread; r < 2 ^ (msg_align_bits - word_size_bits); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; p' \<in> ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> word_of_nat r * word_of_nat word_size < 2 ^ msg_align_bits
 4. \<And>s p'. \<lbrakk>integrity aag X st s; is_subject aag thread; r < 2 ^ (msg_align_bits - word_size_bits); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; p' \<in> ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits; (pasObjectAbs aag thread, Write, pasObjectAbs aag p') \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>s p'. \<lbrakk>integrity aag X st s; is_subject aag thread; r < 2 ^ (msg_align_bits - word_size_bits); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; p' \<in> ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 2. \<And>s p'. \<lbrakk>integrity aag X st s; is_subject aag thread; r < 2 ^ (msg_align_bits - word_size_bits); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; p' \<in> ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> word_of_nat r * word_of_nat word_size < 2 ^ msg_align_bits
 3. \<And>s p'. \<lbrakk>integrity aag X st s; is_subject aag thread; r < 2 ^ (msg_align_bits - word_size_bits); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; p' \<in> ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits; (pasObjectAbs aag thread, Write, pasObjectAbs aag p') \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s p'. \<lbrakk>integrity aag X st s; is_subject aag thread; r < 2 ^ (msg_align_bits - word_size_bits); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; p' \<in> ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> word_of_nat r * word_of_nat word_size < 2 ^ msg_align_bits
 2. \<And>s p'. \<lbrakk>integrity aag X st s; is_subject aag thread; r < 2 ^ (msg_align_bits - word_size_bits); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; p' \<in> ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits; (pasObjectAbs aag thread, Write, pasObjectAbs aag p') \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s p'. \<lbrakk>integrity aag X st s; is_subject aag thread; r < 2 ^ (msg_align_bits - word_size_bits); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; p' \<in> ptr_range (buf + word_of_nat r * word_of_nat word_size) word_size_bits; (pasObjectAbs aag thread, Write, pasObjectAbs aag p') \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag proof (prove)
goal:
No subgoals!