theory ArchIpc_AC

lemma store_word_offs_respects_in_ipc[Ipc_AC_assms]:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
    K ((\<not> is_subject aag receiver \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits)
        \<and> is_aligned buf msg_align_bits \<and> r < 2 ^ (msg_align_bits - word_size_bits))\<rbrace>
   store_word_offs buf r v
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" apply (simp add: store_word_offs_def storeWord_def pred_conj_def) apply (rule hoare_pre) apply (wp dmo_wp) apply (unfold integrity_tcb_in_ipc_def) apply (elim conjE) apply (intro impI conjI) apply assumption+ apply clarsimp apply (erule integrity_trans) apply (clarsimp simp: ptr_range_off_off_mems integrity_def is_aligned_mask[symmetric]) apply (intro conjI impI) apply (subst (asm) ptr_range_off_off_mems; clarsimp simp: word_size_def)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and K ((pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits) \<and> is_aligned buf msg_align_bits \<and> r < 2 ^ (msg_align_bits - word_size_bits))\<rbrace> store_word_offs buf r v \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. integrity_tcb_in_ipc aag X receiver epptr TRContext st x \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits) \<and> is_aligned buf msg_align_bits \<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 (do y <- assert (buf + word_of_nat r * word_of_nat word_size && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)))
od)
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> do s <- get;
y <- assert (in_user_frame (buf + word_of_nat r * word_of_nat word_size) s);
do_machine_op (do y <- assert (buf + word_of_nat r * word_of_nat word_size && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)))
od)
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>
 2. \<And>s. integrity_tcb_in_ipc aag X receiver epptr TRContext st s \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits) \<and> is_aligned buf msg_align_bits \<and> r < 2 ^ (msg_align_bits - word_size_bits) \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity_tcb_in_ipc aag X receiver epptr TRContext st s \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits) \<and> is_aligned buf msg_align_bits \<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> buf + word_of_nat r * word_of_nat word_size && mask 2 = 0 \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRContext st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. (pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits) \<and> is_aligned buf msg_align_bits \<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> buf + word_of_nat r * word_of_nat word_size && mask 2 = 0 \<longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s), kheap := (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>)\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>) receiver) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> in_user_frame (buf + word_of_nat r * word_of_nat word_size) s \<longrightarrow> buf + word_of_nat r * word_of_nat word_size && mask 2 = 0 \<longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s), kheap := (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>)\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>) receiver) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag
 2. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> pas_refined aag st
 3. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s), kheap := (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>)\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>)) p\<rparr>\<rparr>)
 4. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>) receiver) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s), kheap := (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>)\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>)) p\<rparr>\<rparr>)
 2. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>) receiver) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> ptr_range buf msg_align_bits then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> ptr_range buf msg_align_bits then underlying_memory (machine_state st) p else if p = buf + word_of_nat r * word_of_nat word_size + 3 then word_rsplit v ! 0 else if p = buf + word_of_nat r * word_of_nat word_size + 2 then word_rsplit v ! Suc 0 else if p = buf + word_of_nat r * word_of_nat word_size + 1 then word_rsplit v ! 2 else if p = buf + word_of_nat r * word_of_nat word_size then word_rsplit v ! 3 else underlying_memory (machine_state s) p\<rparr>\<rparr>)
 2. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>) receiver) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> integrity aag X (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> ptr_range buf msg_align_bits then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> ptr_range buf msg_align_bits then underlying_memory (machine_state st) p else if p = buf + word_of_nat r * word_of_nat word_size + 3 then word_rsplit v ! 0 else if p = buf + word_of_nat r * word_of_nat word_size + 2 then word_rsplit v ! Suc 0 else if p = buf + word_of_nat r * word_of_nat word_size + 1 then word_rsplit v ! 2 else if p = buf + word_of_nat r * word_of_nat word_size then word_rsplit v ! 3 else underlying_memory (machine_state s) p\<rparr>\<rparr>)
 2. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>) receiver) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; is_aligned (buf + word_of_nat r * word_of_nat word_size) 2; x \<noteq> buf + word_of_nat r * word_of_nat word_size\<rbrakk> \<Longrightarrow> (x = buf + word_of_nat r * word_of_nat word_size + 1 \<longrightarrow> buf + word_of_nat r * word_of_nat word_size + 1 \<notin> ptr_range buf msg_align_bits \<longrightarrow> memory_integrity X aag (buf + word_of_nat r * word_of_nat word_size + 1) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> ptr_range buf msg_align_bits then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) (underlying_memory (machine_state s) (buf + word_of_nat r * word_of_nat word_size + 1)) (word_rsplit v ! 2)) \<and> (x \<noteq> buf + word_of_nat r * word_of_nat word_size + 1 \<longrightarrow> (x = buf + word_of_nat r * word_of_nat word_size + 2 \<longrightarrow> buf + word_of_nat r * word_of_nat word_size + 2 \<notin> ptr_range buf msg_align_bits \<longrightarrow> memory_integrity X aag (buf + word_of_nat r * word_of_nat word_size + 2) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> ptr_range buf msg_align_bits then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) (underlying_memory (machine_state s) (buf + word_of_nat r * word_of_nat word_size + 2)) (word_rsplit v ! Suc 0)) \<and> (x \<noteq> buf + word_of_nat r * word_of_nat word_size + 2 \<longrightarrow> x = buf + word_of_nat r * word_of_nat word_size + 3 \<longrightarrow> buf + word_of_nat r * word_of_nat word_size + 3 \<notin> ptr_range buf msg_align_bits \<longrightarrow> memory_integrity X aag (buf + word_of_nat r * word_of_nat word_size + 3) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> ptr_range buf msg_align_bits then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) (underlying_memory (machine_state s) (buf + word_of_nat r * word_of_nat word_size + 3)) (word_rsplit v ! 0)))
 2. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>) receiver) proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; is_aligned (buf + word_of_nat r * word_of_nat word_size) 2; x \<noteq> buf + word_of_nat r * word_of_nat word_size; x = buf + word_of_nat r * word_of_nat word_size + 1; buf + word_of_nat r * word_of_nat word_size + 1 \<notin> ptr_range buf msg_align_bits\<rbrakk> \<Longrightarrow> memory_integrity X aag (buf + word_of_nat r * word_of_nat word_size + 1) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> ptr_range buf msg_align_bits then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) (underlying_memory (machine_state s) (buf + word_of_nat r * word_of_nat word_size + 1)) (word_rsplit v ! 2)
 2. \<And>s x. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; is_aligned (buf + word_of_nat r * word_of_nat word_size) 2; x \<noteq> buf + word_of_nat r * word_of_nat word_size; x \<noteq> buf + word_of_nat r * word_of_nat word_size + 1; x = buf + word_of_nat r * word_of_nat word_size + 2; buf + word_of_nat r * word_of_nat word_size + 2 \<notin> ptr_range buf msg_align_bits\<rbrakk> \<Longrightarrow> memory_integrity X aag (buf + word_of_nat r * word_of_nat word_size + 2) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> ptr_range buf msg_align_bits then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) (underlying_memory (machine_state s) (buf + word_of_nat r * word_of_nat word_size + 2)) (word_rsplit v ! Suc 0)
 3. \<And>s x. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; is_aligned (buf + word_of_nat r * word_of_nat word_size) 2; x \<noteq> buf + word_of_nat r * word_of_nat word_size; x \<noteq> buf + word_of_nat r * word_of_nat word_size + 1; x \<noteq> buf + word_of_nat r * word_of_nat word_size + 2; x = buf + word_of_nat r * word_of_nat word_size + 3; buf + word_of_nat r * word_of_nat word_size + 3 \<notin> ptr_range buf msg_align_bits\<rbrakk> \<Longrightarrow> memory_integrity X aag (buf + word_of_nat r * word_of_nat word_size + 3) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> ptr_range buf msg_align_bits then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) (underlying_memory (machine_state s) (buf + word_of_nat r * word_of_nat word_size + 3)) (word_rsplit v ! 0)
 4. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>) receiver) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits; pas_refined aag st; is_aligned buf msg_align_bits; r < 2 ^ (msg_align_bits - word_size_bits); integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); in_user_frame (buf + word_of_nat r * word_of_nat word_size) s; buf + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(buf + word_of_nat r * word_of_nat word_size := word_rsplit v ! 3, buf + word_of_nat r * word_of_nat word_size + 1 := word_rsplit v ! 2, buf + word_of_nat r * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, buf + word_of_nat r * word_of_nat word_size + 3 := word_rsplit v ! 0)) (machine_state s)\<rparr>) receiver) proof (prove)
goal:
No subgoals!