theory TcbAcc_R

lemma loadWordUser_corres:
  assumes y: "y < unat max_ipc_words"
  shows "corres (=) \<top> (valid_ipc_buffer_ptr' a) (load_word_offs a y) (loadWordUser (a + of_nat y * 4))" unfolding loadWordUser_def apply (rule corres_stateAssert_assume [rotated]) apply (erule valid_ipc_buffer_ptr'D[OF y]) apply (rule corres_guard_imp) apply (simp add: load_word_offs_def word_size_def) apply (rule_tac F = "is_aligned a msg_align_bits" in corres_gen_asm2) apply (rule corres_machine_op) apply (rule corres_Id [OF refl refl]) apply (rule no_fail_pre) apply wp apply (erule aligned_add_aligned) apply (rule is_aligned_mult_triv2 [where n = 2, simplified]) apply (simp add: word_bits_conv msg_align_bits)+ apply (simp add: valid_ipc_buffer_ptr'_def msg_align_bits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (valid_ipc_buffer_ptr' a) (load_word_offs a y) (loadWordUser (a + word_of_nat y * 4)) proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (valid_ipc_buffer_ptr' a) (load_word_offs a y) (do stateAssert (pointerInUserData (a + word_of_nat y * 4)) [];
doMachineOp $ loadWord (a + word_of_nat y * 4)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> pointerInUserData (a + word_of_nat y * 4) s
 2. corres (=) (\<lambda>_. True) (valid_ipc_buffer_ptr' a) (load_word_offs a y) (K_bind (doMachineOp $ loadWord (a + word_of_nat y * 4)) ()) proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (valid_ipc_buffer_ptr' a) (load_word_offs a y) (K_bind (doMachineOp $ loadWord (a + word_of_nat y * 4)) ()) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q4 ?Q'4 (load_word_offs a y) (K_bind (doMachineOp $ loadWord (a + word_of_nat y * 4)) ())
 2. \<And>s. True \<Longrightarrow> ?Q4 s
 3. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ?Q'4 s proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q4 ?Q'4 (do_machine_op (loadWord (a + word_of_nat y * 4))) (doMachineOp (loadWord (a + word_of_nat y * 4)))
 2. \<And>s. True \<Longrightarrow> ?Q4 s
 3. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ?Q'4 s proof (prove)
goal (3 subgoals):
 1. is_aligned a msg_align_bits \<Longrightarrow> corres (=) ?Q4 ?P'8 (do_machine_op (loadWord (a + word_of_nat y * 4))) (doMachineOp (loadWord (a + word_of_nat y * 4)))
 2. \<And>s. True \<Longrightarrow> ?Q4 s
 3. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> (?P'8 and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (3 subgoals):
 1. is_aligned a msg_align_bits \<Longrightarrow> corres_underlying Id False True (=) (\<lambda>_. True) (\<lambda>_. True) (loadWord (a + word_of_nat y * 4)) (loadWord (a + word_of_nat y * 4))
 2. \<And>s. True \<Longrightarrow> True
 3. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned a msg_align_bits; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (loadWord (a + word_of_nat y * 4))
 2. \<And>s. True \<Longrightarrow> True
 3. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned a msg_align_bits; True\<rbrakk> \<Longrightarrow> no_fail ?P17 (loadWord (a + word_of_nat y * 4))
 2. \<And>s. \<lbrakk>is_aligned a msg_align_bits; True; True\<rbrakk> \<Longrightarrow> ?P17 s
 3. \<And>s. True \<Longrightarrow> True
 4. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>is_aligned a msg_align_bits; True; True\<rbrakk> \<Longrightarrow> is_aligned (a + word_of_nat y * 4) 2
 2. \<And>s. True \<Longrightarrow> True
 3. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat y * 4) 2
 2. \<And>s. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits
 3. \<And>s. True \<Longrightarrow> True
 4. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned a msg_align_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits
 2. \<And>s. True \<Longrightarrow> True
 3. \<And>s. valid_ipc_buffer_ptr' a s \<Longrightarrow> ((\<lambda>_. 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> is_aligned a 9 proof (prove)
goal:
No subgoals!