theory TcbAcc_R

lemma storeWordUser_corres:
  assumes y: "y < unat max_ipc_words"
  shows "corres dc (in_user_frame a) (valid_ipc_buffer_ptr' a)
                   (store_word_offs a y w) (storeWordUser (a + of_nat y * 4) w)" apply (simp add: storeWordUser_def bind_assoc[symmetric]
                   store_word_offs_def word_size_def) apply (rule corres_guard2_imp) apply (rule_tac F = "is_aligned a msg_align_bits" in corres_gen_asm2) apply (rule corres_guard1_imp) apply (rule_tac r'=dc in corres_split) apply (simp add: stateAssert_def) apply (rule_tac r'=dc in corres_split) apply (rule corres_trivial) apply simp apply (rule corres_assert) apply wp+ apply (rule corres_machine_op) apply (rule corres_Id [OF refl]) apply simp apply (rule no_fail_pre) apply (wp no_fail_storeWord) apply (erule_tac n=msg_align_bits in aligned_add_aligned) apply (rule is_aligned_mult_triv2 [where n = 2, simplified]) apply (simp add: word_bits_conv msg_align_bits)+ apply wp+ apply (simp add: in_user_frame_eq[OF y]) apply simp apply (rule conjI) apply (frule (1) valid_ipc_buffer_ptr'D [OF y]) apply (simp add: valid_ipc_buffer_ptr'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (in_user_frame a) (valid_ipc_buffer_ptr' a) (store_word_offs a y w) (storeWordUser (a + word_of_nat y * 4) w) proof (prove)
goal (1 subgoal):
 1. corres dc (in_user_frame a) (valid_ipc_buffer_ptr' a) (do ya <- do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od;
do_machine_op (storeWord (a + word_of_nat y * 4) w)
od) (do ya <- stateAssert (pointerInUserData (a + word_of_nat y * 4)) [];
doMachineOp (storeWord (a + word_of_nat y * 4) w)
od) proof (prove)
goal (2 subgoals):
 1. corres dc (in_user_frame a) ?Q' (do ya <- do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od;
do_machine_op (storeWord (a + word_of_nat y * 4) w)
od) (do ya <- stateAssert (pointerInUserData (a + word_of_nat y * 4)) [];
doMachineOp (storeWord (a + word_of_nat y * 4) w)
od)
 2. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ?Q' s proof (prove)
goal (2 subgoals):
 1. is_aligned a msg_align_bits \<Longrightarrow> corres dc (in_user_frame a) ?P'3 (do ya <- do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od;
do_machine_op (storeWord (a + word_of_nat y * 4) w)
od) (do ya <- stateAssert (pointerInUserData (a + word_of_nat y * 4)) [];
doMachineOp (storeWord (a + word_of_nat y * 4) w)
od)
 2. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> (?P'3 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (3 subgoals):
 1. is_aligned a msg_align_bits \<Longrightarrow> corres dc ?Q4 ?P'3 (do ya <- do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od;
do_machine_op (storeWord (a + word_of_nat y * 4) w)
od) (do ya <- stateAssert (pointerInUserData (a + word_of_nat y * 4)) [];
doMachineOp (storeWord (a + word_of_nat y * 4) w)
od)
 2. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> (?P'3 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (6 subgoals):
 1. is_aligned a msg_align_bits \<Longrightarrow> corres dc ?P7 ?P'7 (do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od) (stateAssert (pointerInUserData (a + word_of_nat y * 4)) [])
 2. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R7 rv) (?R'7 rv') (do_machine_op (storeWord (a + word_of_nat y * 4) w)) (doMachineOp (storeWord (a + word_of_nat y * 4) w))
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>?R7\<rbrace>
 4. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>?R'7\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> (?P7 and ?Q7) s
 6. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> (?P'7 and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (6 subgoals):
 1. is_aligned a msg_align_bits \<Longrightarrow> corres dc ?P7 ?P'7 (do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od) (do s <- get;
assert (pointerInUserData (a + word_of_nat y * 4) s)
od)
 2. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R7 rv) (?R'7 rv') (do_machine_op (storeWord (a + word_of_nat y * 4) w)) (doMachineOp (storeWord (a + word_of_nat y * 4) w))
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>?R7\<rbrace>
 4. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>?R'7\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> (?P7 and ?Q7) s
 6. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> (?P'7 and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (9 subgoals):
 1. is_aligned a msg_align_bits \<Longrightarrow> corres dc ?P9 ?P'9 get get
 2. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R9 rv) (?R'9 rv') (assert (in_user_frame (a + word_of_nat y * 4) rv)) (assert (pointerInUserData (a + word_of_nat y * 4) rv'))
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q9\<rbrace> get \<lbrace>?R9\<rbrace>
 4. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'9\<rbrace> get \<lbrace>?R'9\<rbrace>
 5. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R7 rv) (?R'7 rv') (do_machine_op (storeWord (a + word_of_nat y * 4) w)) (doMachineOp (storeWord (a + word_of_nat y * 4) w))
 6. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>?R7\<rbrace>
 7. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>?R'7\<rbrace>
 8. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> (?P9 and ?Q9 and ?Q7) s
 9. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> (?P'9 and ?Q'9 and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (9 subgoals):
 1. is_aligned a msg_align_bits \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) get get
 2. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R9 rv) (?R'9 rv') (assert (in_user_frame (a + word_of_nat y * 4) rv)) (assert (pointerInUserData (a + word_of_nat y * 4) rv'))
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q9\<rbrace> get \<lbrace>?R9\<rbrace>
 4. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'9\<rbrace> get \<lbrace>?R'9\<rbrace>
 5. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R7 rv) (?R'7 rv') (do_machine_op (storeWord (a + word_of_nat y * 4) w)) (doMachineOp (storeWord (a + word_of_nat y * 4) w))
 6. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>?R7\<rbrace>
 7. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>?R'7\<rbrace>
 8. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q9 and ?Q7) s
 9. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and ?Q'9 and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R9 rv) (?R'9 rv') (assert (in_user_frame (a + word_of_nat y * 4) rv)) (assert (pointerInUserData (a + word_of_nat y * 4) rv'))
 2. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q9\<rbrace> get \<lbrace>?R9\<rbrace>
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'9\<rbrace> get \<lbrace>?R'9\<rbrace>
 4. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R7 rv) (?R'7 rv') (do_machine_op (storeWord (a + word_of_nat y * 4) w)) (doMachineOp (storeWord (a + word_of_nat y * 4) w))
 5. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>?R7\<rbrace>
 6. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>?R'7\<rbrace>
 7. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q9 and ?Q7) s
 8. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and ?Q'9 and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (7 subgoals):
 1. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q9\<rbrace> get \<lbrace>\<lambda>rv _. in_user_frame (a + word_of_nat y * 4) rv\<rbrace>
 2. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'9\<rbrace> get \<lbrace>\<lambda>rv' _. pointerInUserData (a + word_of_nat y * 4) rv'\<rbrace>
 3. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R7 rv) (?R'7 rv') (do_machine_op (storeWord (a + word_of_nat y * 4) w)) (doMachineOp (storeWord (a + word_of_nat y * 4) w))
 4. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>?R7\<rbrace>
 5. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>?R'7\<rbrace>
 6. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q9 and ?Q7) s
 7. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and ?Q'9 and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R7 rv) (?R'7 rv') (do_machine_op (storeWord (a + word_of_nat y * 4) w)) (doMachineOp (storeWord (a + word_of_nat y * 4) w))
 2. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>?R7\<rbrace>
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>?R'7\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and in_user_frame (a + word_of_nat y * 4) and ?Q7) s
 5. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and pointerInUserData (a + word_of_nat y * 4) and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (storeWord (a + word_of_nat y * 4) w) (storeWord (a + word_of_nat y * 4) w)
 2. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and in_user_frame (a + word_of_nat y * 4) and ?Q7) s
 5. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and pointerInUserData (a + word_of_nat y * 4) and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' rva. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'\<rbrakk> \<Longrightarrow> dc rva rva
 2. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (storeWord (a + word_of_nat y * 4) w)
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 4. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>\<lambda>rv' _. True\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and in_user_frame (a + word_of_nat y * 4) and ?Q7) s
 6. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and pointerInUserData (a + word_of_nat y * 4) and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (storeWord (a + word_of_nat y * 4) w)
 2. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and in_user_frame (a + word_of_nat y * 4) and ?Q7) s
 5. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and pointerInUserData (a + word_of_nat y * 4) and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?P28 rv rv') (storeWord (a + word_of_nat y * 4) w)
 2. \<And>rv rv' s. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'; True; True\<rbrakk> \<Longrightarrow> ?P28 rv rv' s
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 4. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>\<lambda>rv' _. True\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and in_user_frame (a + word_of_nat y * 4) and ?Q7) s
 6. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and pointerInUserData (a + word_of_nat y * 4) and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' s. \<lbrakk>is_aligned a msg_align_bits; dc rv rv'; True; True\<rbrakk> \<Longrightarrow> is_aligned (a + word_of_nat y * 4) 2
 2. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and in_user_frame (a + word_of_nat y * 4) and ?Q7) s
 5. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and pointerInUserData (a + word_of_nat y * 4) and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' s. \<lbrakk>dc rv rv'; True; True\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat y * 4) 2
 2. \<And>rv rv' s. \<lbrakk>dc rv rv'; True; True\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 4. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>\<lambda>rv' _. True\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and in_user_frame (a + word_of_nat y * 4) and ?Q7) s
 6. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and pointerInUserData (a + word_of_nat y * 4) and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' s. \<lbrakk>dc rv rv'; True; True\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits
 2. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 3. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and in_user_frame (a + word_of_nat y * 4) and ?Q7) s
 5. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and pointerInUserData (a + word_of_nat y * 4) and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (4 subgoals):
 1. is_aligned a 9 \<Longrightarrow> \<lbrace>?Q7\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat y * 4) s)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 2. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>?Q'7\<rbrace> stateAssert (pointerInUserData (a + word_of_nat y * 4)) [] \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and in_user_frame (a + word_of_nat y * 4) and ?Q7) s
 4. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and pointerInUserData (a + word_of_nat y * 4) and ?Q'7 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned a msg_align_bits; in_user_frame a s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and in_user_frame (a + word_of_nat y * 4) and (\<lambda>s. in_user_frame (a + word_of_nat y * 4) s \<longrightarrow> True)) s
 2. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and pointerInUserData (a + word_of_nat y * 4) and (\<lambda>s. pointerInUserData (a + word_of_nat y * 4) s \<longrightarrow> True) and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and pointerInUserData (a + word_of_nat y * 4) and (\<lambda>s. pointerInUserData (a + word_of_nat y * 4) s \<longrightarrow> True) and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> pointerInUserData (a + word_of_nat y * 4) s \<and> is_aligned a msg_align_bits proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> pointerInUserData (a + word_of_nat y * 4) s
 2. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> is_aligned a msg_align_bits proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> is_aligned a msg_align_bits proof (prove)
goal:
No subgoals!