theory TcbAcc_R

lemma copyMRs_corres:
  "corres (=) (tcb_at s and tcb_at r
               and case_option \<top> in_user_frame sb
               and case_option \<top> in_user_frame rb
               and K (unat n \<le> msg_max_length))
              (tcb_at' s and tcb_at' r
               and case_option \<top> valid_ipc_buffer_ptr' sb
               and case_option \<top> valid_ipc_buffer_ptr' rb)
              (copy_mrs s sb r rb n) (copyMRs s sb r rb n)" proof - have U: "unat n \<le> msg_max_length \<Longrightarrow>
           map (toEnum :: nat \<Rightarrow> word32) [7 ..< Suc (unat n)] = map of_nat [7 ..< Suc (unat n)]" unfolding msg_max_length_def by auto note R'=msgRegisters_unfold[THEN meta_eq_to_obj_eq, THEN arg_cong[where f=length]] note R=R'[simplified] have as_user_bit:
    "\<And>v :: word32. corres dc (tcb_at s and tcb_at r) (tcb_at' s and tcb_at' r)
           (mapM
             (\<lambda>ra. do v \<leftarrow> as_user s (getRegister ra);
                      as_user r (setRegister ra v)
                   od)
             (take (unat n) msg_registers))
           (mapM
             (\<lambda>ra. do v \<leftarrow> asUser s (getRegister ra);
                      asUser r (setRegister ra v)
                   od)
             (take (unat n) msgRegisters))" apply (rule corres_guard_imp) apply (rule_tac S=Id in corres_mapM, simp+) apply (rule corres_split_eqr[OF asUser_getRegister_corres asUser_setRegister_corres]) apply (wp | clarsimp simp: msg_registers_def msgRegisters_def)+ done have wordSize[simp]: "of_nat wordSize = 4" by (simp add: wordSize_def wordBits_def word_size) show ?thesis apply (rule corres_assume_pre) apply (simp add: copy_mrs_def copyMRs_def word_size
               cong: option.case_cong
          split del: if_split del: upt.simps) apply (cases sb) apply (simp add: R) apply (rule corres_guard_imp) apply (rule corres_split_nor[OF as_user_bit]) apply (rule corres_trivial, simp) apply wp+ apply simp apply simp apply (cases rb) apply (simp add: R) apply (rule corres_guard_imp) apply (rule corres_split_nor[OF as_user_bit]) apply (rule corres_trivial, simp) apply wp+ apply simp apply simp apply (simp add: R del: upt.simps) apply (rule corres_guard_imp) apply (rename_tac sb_ptr rb_ptr) apply (rule corres_split_nor[OF as_user_bit]) apply (rule corres_split_eqr) apply (rule_tac S="{(x, y). y = of_nat x \<and> x < unat max_ipc_words}"
                   in corres_mapM, simp+) apply (rule corres_split_eqr) apply (rule loadWordUser_corres) apply simp apply (rule storeWordUser_corres) apply simp apply (wp hoare_vcg_all_lift | simp)+ apply (clarsimp simp: upto_enum_def) apply arith apply (subst set_zip) apply (simp add: upto_enum_def U del: upt.simps) apply (clarsimp simp del: upt.simps) apply (clarsimp simp: msg_max_length_def word_le_nat_alt nth_append
                                 max_ipc_words) apply (erule order_less_trans) apply simp apply (rule corres_trivial, simp) apply (wp hoare_vcg_all_lift mapM_wp'
                | simp add: valid_ipc_buffer_ptr'_def)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat n \<le> msg_max_length)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (copy_mrs s sb r rb n) (copyMRs s sb r rb n) proof (state)
goal (1 subgoal):
 1. corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat n \<le> msg_max_length)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (copy_mrs s sb r rb n) (copyMRs s sb r rb n) proof (prove)
goal (1 subgoal):
 1. unat n \<le> msg_max_length \<Longrightarrow> map toEnum [7..<Suc (unat n)] = map word_of_nat [7..<Suc (unat n)] proof (prove)
goal (1 subgoal):
 1. unat n \<le> 120 \<Longrightarrow> map toEnum [7..<Suc (unat n)] = map word_of_nat [7..<Suc (unat n)] proof (state)
this:
unat n \<le> msg_max_length \<Longrightarrow> map toEnum [7..<Suc (unat n)] = map word_of_nat [7..<Suc (unat n)]

goal (1 subgoal):
 1. corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat n \<le> msg_max_length)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (copy_mrs s sb r rb n) (copyMRs s sb r rb n) proof (state)
this:
length TCB_H.msgRegisters = length (map Register ARM.msgRegisters)
length msg_registers = length ARM.msgRegisters
length ARM.msgRegisters = length [R2, R3, R4, R5]

goal (1 subgoal):
 1. corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat n \<le> msg_max_length)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (copy_mrs s sb r rb n) (copyMRs s sb r rb n) proof (state)
this:
length TCB_H.msgRegisters = length ARM.msgRegisters
length msg_registers = length ARM.msgRegisters
length ARM.msgRegisters = Suc (Suc (Suc (Suc 0)))

goal (1 subgoal):
 1. corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat n \<le> msg_max_length)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (copy_mrs s sb r rb n) (copyMRs s sb r rb n) proof (prove)
goal (1 subgoal):
 1. \<And>v. corres dc (tcb_at s and tcb_at r) (tcb_at' s and tcb_at' r) (mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers)) (mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters)) proof (prove)
goal (3 subgoals):
 1. \<And>v. corres dc (?Q v) (?Q' v) (mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers)) (mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters))
 2. \<And>v sa. (tcb_at s and tcb_at r) sa \<Longrightarrow> ?Q v sa
 3. \<And>v sa. (tcb_at' s and tcb_at' r) sa \<Longrightarrow> ?Q' v sa proof (prove)
goal (7 subgoals):
 1. \<And>v x. corres (?r'4 v) (?Q v) (?Q' v) (do v <- as_user s (getRegister x);
as_user r (setRegister x v)
od) (do v <- asUser s (getRegister x);
asUser r (setRegister x v)
od)
 2. \<And>v x y. (x, y) \<in> Id \<Longrightarrow> \<lbrace>?Q v\<rbrace> do v <- as_user s (getRegister x);
as_user r (setRegister x v)
od \<lbrace>\<lambda>rv. ?Q v\<rbrace>
 3. \<And>v x y. (x, y) \<in> Id \<Longrightarrow> \<lbrace>?Q' v\<rbrace> do v <- asUser s (getRegister y);
asUser r (setRegister y v)
od \<lbrace>\<lambda>rv. ?Q' v\<rbrace>
 4. \<And>v. length (take (unat n) msg_registers) = length (take (unat n) TCB_H.msgRegisters)
 5. \<And>v. set (zip (take (unat n) msg_registers) (take (unat n) TCB_H.msgRegisters)) \<subseteq> Id
 6. \<And>v sa. (tcb_at s and tcb_at r) sa \<Longrightarrow> ?Q v sa
 7. \<And>v sa. (tcb_at' s and tcb_at' r) sa \<Longrightarrow> ?Q' v sa proof (prove)
goal (8 subgoals):
 1. \<And>v x. \<lbrace>?Q10 v\<rbrace> as_user s (getRegister x) \<lbrace>\<lambda>v. tcb_at r\<rbrace>
 2. \<And>v x. \<lbrace>?Q'12 v\<rbrace> asUser s (getRegister x) \<lbrace>\<lambda>v. tcb_at' r\<rbrace>
 3. \<And>v x y. (x, y) \<in> Id \<Longrightarrow> \<lbrace>tcb_at s and ?Q10 v\<rbrace> do v <- as_user s (getRegister x);
as_user r (setRegister x v)
od \<lbrace>\<lambda>rv. tcb_at s and ?Q10 v\<rbrace>
 4. \<And>v x y. (x, y) \<in> Id \<Longrightarrow> \<lbrace>tcb_at' s and ?Q'12 v\<rbrace> do v <- asUser s (getRegister y);
asUser r (setRegister y v)
od \<lbrace>\<lambda>rv. tcb_at' s and ?Q'12 v\<rbrace>
 5. \<And>v. length (take (unat n) msg_registers) = length (take (unat n) TCB_H.msgRegisters)
 6. \<And>v. set (zip (take (unat n) msg_registers) (take (unat n) TCB_H.msgRegisters)) \<subseteq> Id
 7. \<And>v sa. (tcb_at s and tcb_at r) sa \<Longrightarrow> (tcb_at s and ?Q10 v) sa
 8. \<And>v sa. (tcb_at' s and tcb_at' r) sa \<Longrightarrow> (tcb_at' s and ?Q'12 v) sa proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (tcb_at s and tcb_at r) (tcb_at' s and tcb_at' r) (mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers)) (mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters))

goal (1 subgoal):
 1. corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat n \<le> msg_max_length)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (copy_mrs s sb r rb n) (copyMRs s sb r rb n) proof (prove)
goal (1 subgoal):
 1. of_nat wordSize = (4::'a) proof (state)
this:
of_nat wordSize = (4::?'a1)

goal (1 subgoal):
 1. corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat n \<le> msg_max_length)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (copy_mrs s sb r rb n) (copyMRs s sb r rb n) proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat n \<le> msg_max_length)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (copy_mrs s sb r rb n) (copyMRs s sb r rb n) proof (prove)
goal (1 subgoal):
 1. \<And>sa s'. \<lbrakk>(tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat n \<le> msg_max_length)) sa; (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s'; (sa, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat n \<le> msg_max_length)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (copy_mrs s sb r rb n) (copyMRs s sb r rb n) proof (prove)
goal (1 subgoal):
 1. \<And>sa s'. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (2 subgoals):
 1. \<And>sa s'. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od)
 2. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (2 subgoals):
 1. \<And>sa s'. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) (tcb_at' s and tcb_at' r and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n))))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n))))
od)
 2. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (4 subgoals):
 1. \<And>sa s'. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None\<rbrakk> \<Longrightarrow> corres (=) (?Q8 sa s') (?Q'8 sa s') (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n))))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n))))
od)
 2. \<And>sa s' saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None; (tcb_at s and tcb_at r and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) saa\<rbrakk> \<Longrightarrow> ?Q8 sa s' saa
 3. \<And>sa s' saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None; (tcb_at' s and tcb_at' r and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) saa\<rbrakk> \<Longrightarrow> ?Q'8 sa s' saa
 4. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (6 subgoals):
 1. \<And>sa s'. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None\<rbrakk> \<Longrightarrow> corres (=) (?R12 sa s') (?R'12 sa s') (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n))))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)))))
 2. \<And>sa s'. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 sa s'\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. ?R12 sa s'\<rbrace>
 3. \<And>sa s'. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'12 sa s'\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. ?R'12 sa s'\<rbrace>
 4. \<And>sa s' saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None; (tcb_at s and tcb_at r and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q12 sa s') saa
 5. \<And>sa s' saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None; (tcb_at' s and tcb_at' r and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'12 sa s') saa
 6. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (5 subgoals):
 1. \<And>sa s'. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 sa s'\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>sa s'. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'12 sa s'\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>sa s' saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None; (tcb_at s and tcb_at r and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q12 sa s') saa
 4. \<And>sa s' saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None; (tcb_at' s and tcb_at' r and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'12 sa s') saa
 5. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (3 subgoals):
 1. \<And>sa s' saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None; (tcb_at s and tcb_at r and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and (\<lambda>s. True)) saa
 2. \<And>sa s' saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None; (tcb_at' s and tcb_at' r and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and (\<lambda>s. True)) saa
 3. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (2 subgoals):
 1. \<And>sa s' saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = None; (tcb_at' s and tcb_at' r and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and (\<lambda>s. True)) saa
 2. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (2 subgoals):
 1. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a; rb = None\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od)
 2. \<And>sa s' a aa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (2 subgoals):
 1. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and in_user_frame a) (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n))))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n))))
od)
 2. \<And>sa s' a aa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (4 subgoals):
 1. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None\<rbrakk> \<Longrightarrow> corres (=) (?Q29 sa s' a) (?Q'29 sa s' a) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n))))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n))))
od)
 2. \<And>sa s' a saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None; (tcb_at s and tcb_at r and in_user_frame a) saa\<rbrakk> \<Longrightarrow> ?Q29 sa s' a saa
 3. \<And>sa s' a saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a) saa\<rbrakk> \<Longrightarrow> ?Q'29 sa s' a saa
 4. \<And>sa s' a aa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (6 subgoals):
 1. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None\<rbrakk> \<Longrightarrow> corres (=) (?R33 sa s' a) (?R'33 sa s' a) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n))))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)))))
 2. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 sa s' a\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. ?R33 sa s' a\<rbrace>
 3. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 sa s' a\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. ?R'33 sa s' a\<rbrace>
 4. \<And>sa s' a saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None; (tcb_at s and tcb_at r and in_user_frame a) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q33 sa s' a) saa
 5. \<And>sa s' a saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'33 sa s' a) saa
 6. \<And>sa s' a aa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (5 subgoals):
 1. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 sa s' a\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>sa s' a. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 sa s' a\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>sa s' a saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None; (tcb_at s and tcb_at r and in_user_frame a) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q33 sa s' a) saa
 4. \<And>sa s' a saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'33 sa s' a) saa
 5. \<And>sa s' a aa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (3 subgoals):
 1. \<And>sa s' a saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None; (tcb_at s and tcb_at r and in_user_frame a) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and (\<lambda>s. True)) saa
 2. \<And>sa s' a saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and (\<lambda>s. True)) saa
 3. \<And>sa s' a aa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (2 subgoals):
 1. \<And>sa s' a saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s'; (sa, s') \<in> state_relation; sb = Some a; rb = None; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and (\<lambda>s. True)) saa
 2. \<And>sa s' a aa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>sa s' a aa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (length msg_registers)..<Suc (unat n)];
return (min n (word_of_nat (min (length msg_registers) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * 4) >>= storeWordUser (rbPtr + x * 4)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>sa s' a aa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> corres (=) (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- mapM (\<lambda>x. load_word_offs a x >>= store_word_offs aa x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)];
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- mapM (\<lambda>x. loadWordUser (a + x * 4) >>= storeWordUser (aa + x * 4)) [5 .e. n];
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length bufferMRs)))
od) proof (prove)
goal (3 subgoals):
 1. \<And>sa s' a aa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> corres (=) (?Q49 sa s' a aa) (?Q'49 sa s' a aa) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- mapM (\<lambda>x. load_word_offs a x >>= store_word_offs aa x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)];
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- mapM (\<lambda>x. loadWordUser (a + x * 4) >>= storeWordUser (aa + x * 4)) [5 .e. n];
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length bufferMRs)))
od)
 2. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> ?Q49 sa s' a aa saa
 3. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> ?Q'49 sa s' a aa saa proof (prove)
goal (3 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?Q49 sa s' sb_ptr rb_ptr) (?Q'49 sa s' sb_ptr rb_ptr) (do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)];
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))
od) (do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n];
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length bufferMRs)))
od)
 2. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> ?Q49 sa s' a aa saa
 3. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> ?Q'49 sa s' a aa saa proof (prove)
goal (5 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R53 sa s' sb_ptr rb_ptr) (?R'53 sa s' sb_ptr rb_ptr) (do buf_mrs <- mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)];
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))
od) (do bufferMRs <- mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n];
return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length bufferMRs)))
od)
 2. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. ?R53 sa s' sb_ptr rb_ptr\<rbrace>
 3. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. ?R'53 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 5. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal (8 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?P57 sa s' sb_ptr rb_ptr) (?P'57 sa s' sb_ptr rb_ptr) (mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)]) (mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n])
 2. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 3. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. ?P57 sa s' sb_ptr rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. ?P'57 sa s' sb_ptr rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
 7. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 8. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal (12 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> corres (?r'62 sa s' sb_ptr rb_ptr) (?P57 sa s' sb_ptr rb_ptr) (?P'57 sa s' sb_ptr rb_ptr) (load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) (loadWordUser (sb_ptr + word_of_nat x * 4) >>= storeWordUser (rb_ptr + word_of_nat x * 4))
 2. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P57 sa s' sb_ptr rb_ptr\<rbrace> load_word_offs sb_ptr x >>= store_word_offs rb_ptr x \<lbrace>\<lambda>rv. ?P57 sa s' sb_ptr rb_ptr\<rbrace>
 3. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P'57 sa s' sb_ptr rb_ptr\<rbrace> loadWordUser (sb_ptr + y * 4) >>= storeWordUser (rb_ptr + y * 4) \<lbrace>\<lambda>rv. ?P'57 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> length [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] = length [5 .e. n]
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> set (zip [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] [5 .e. n]) \<subseteq> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}
 6. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 7. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 8. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 9. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. ?P57 sa s' sb_ptr rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 10. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. ?P'57 sa s' sb_ptr rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
A total of 12 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> corres (=) (?P65 sa s' sb_ptr rb_ptr) (?P'67 sa s' sb_ptr rb_ptr) (load_word_offs sb_ptr x) (loadWordUser (sb_ptr + word_of_nat x * 4))
 2. \<And>sa s' sb_ptr rb_ptr x rv. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> corres (?r'62 sa s' sb_ptr rb_ptr) (?R64 sa s' sb_ptr rb_ptr x rv) (?R'64 sa s' sb_ptr rb_ptr x rv) (store_word_offs rb_ptr x rv) (storeWordUser (rb_ptr + word_of_nat x * 4) rv)
 3. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 sa s' sb_ptr rb_ptr\<rbrace> load_word_offs sb_ptr x \<lbrace>?R64 sa s' sb_ptr rb_ptr x\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 sa s' sb_ptr rb_ptr\<rbrace> loadWordUser (sb_ptr + word_of_nat x * 4) \<lbrace>?R'64 sa s' sb_ptr rb_ptr x\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P65 sa s' sb_ptr rb_ptr and ?Q66 sa s' sb_ptr rb_ptr\<rbrace> load_word_offs sb_ptr x >>= store_word_offs rb_ptr x \<lbrace>\<lambda>rv. ?P65 sa s' sb_ptr rb_ptr and ?Q66 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P'67 sa s' sb_ptr rb_ptr and ?Q'68 sa s' sb_ptr rb_ptr\<rbrace> loadWordUser (sb_ptr + y * 4) >>= storeWordUser (rb_ptr + y * 4) \<lbrace>\<lambda>rv. ?P'67 sa s' sb_ptr rb_ptr and ?Q'68 sa s' sb_ptr rb_ptr\<rbrace>
 7. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> length [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] = length [5 .e. n]
 8. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> set (zip [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] [5 .e. n]) \<subseteq> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}
 9. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 10. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> x < unat max_ipc_words
 2. \<And>sa s' sb_ptr rb_ptr x rv. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> corres (?r'62 sa s' sb_ptr rb_ptr) (?R64 sa s' sb_ptr rb_ptr x rv) (?R'64 sa s' sb_ptr rb_ptr x rv) (store_word_offs rb_ptr x rv) (storeWordUser (rb_ptr + word_of_nat x * 4) rv)
 3. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 sa s' sb_ptr rb_ptr\<rbrace> load_word_offs sb_ptr x \<lbrace>?R64 sa s' sb_ptr rb_ptr x\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 sa s' sb_ptr rb_ptr\<rbrace> loadWordUser (sb_ptr + word_of_nat x * 4) \<lbrace>?R'64 sa s' sb_ptr rb_ptr x\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>_. True) and ?Q66 sa s' sb_ptr rb_ptr\<rbrace> load_word_offs sb_ptr x >>= store_word_offs rb_ptr x \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q66 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>valid_ipc_buffer_ptr' sb_ptr and ?Q'68 sa s' sb_ptr rb_ptr\<rbrace> loadWordUser (sb_ptr + y * 4) >>= storeWordUser (rb_ptr + y * 4) \<lbrace>\<lambda>rv. valid_ipc_buffer_ptr' sb_ptr and ?Q'68 sa s' sb_ptr rb_ptr\<rbrace>
 7. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> length [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] = length [5 .e. n]
 8. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> set (zip [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] [5 .e. n]) \<subseteq> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}
 9. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 10. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr x rv. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> corres (?r'62 sa s' sb_ptr rb_ptr) (?R64 sa s' sb_ptr rb_ptr x rv) (?R'64 sa s' sb_ptr rb_ptr x rv) (store_word_offs rb_ptr x rv) (storeWordUser (rb_ptr + word_of_nat x * 4) rv)
 2. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 sa s' sb_ptr rb_ptr\<rbrace> load_word_offs sb_ptr x \<lbrace>?R64 sa s' sb_ptr rb_ptr x\<rbrace>
 3. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 sa s' sb_ptr rb_ptr\<rbrace> loadWordUser (sb_ptr + word_of_nat x * 4) \<lbrace>?R'64 sa s' sb_ptr rb_ptr x\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>_. True) and ?Q66 sa s' sb_ptr rb_ptr\<rbrace> load_word_offs sb_ptr x >>= store_word_offs rb_ptr x \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q66 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>valid_ipc_buffer_ptr' sb_ptr and ?Q'68 sa s' sb_ptr rb_ptr\<rbrace> loadWordUser (sb_ptr + y * 4) >>= storeWordUser (rb_ptr + y * 4) \<lbrace>\<lambda>rv. valid_ipc_buffer_ptr' sb_ptr and ?Q'68 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> length [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] = length [5 .e. n]
 7. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> set (zip [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] [5 .e. n]) \<subseteq> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}
 8. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 9. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 10. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr x rv. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> x < unat max_ipc_words
 2. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 sa s' sb_ptr rb_ptr\<rbrace> load_word_offs sb_ptr x \<lbrace>\<lambda>rv. in_user_frame rb_ptr\<rbrace>
 3. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 sa s' sb_ptr rb_ptr\<rbrace> loadWordUser (sb_ptr + word_of_nat x * 4) \<lbrace>\<lambda>rv. valid_ipc_buffer_ptr' rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>_. True) and ?Q66 sa s' sb_ptr rb_ptr\<rbrace> load_word_offs sb_ptr x >>= store_word_offs rb_ptr x \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q66 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>valid_ipc_buffer_ptr' sb_ptr and ?Q'68 sa s' sb_ptr rb_ptr\<rbrace> loadWordUser (sb_ptr + y * 4) >>= storeWordUser (rb_ptr + y * 4) \<lbrace>\<lambda>rv. valid_ipc_buffer_ptr' sb_ptr and ?Q'68 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> length [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] = length [5 .e. n]
 7. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> set (zip [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] [5 .e. n]) \<subseteq> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}
 8. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 9. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 10. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 sa s' sb_ptr rb_ptr\<rbrace> load_word_offs sb_ptr x \<lbrace>\<lambda>rv. in_user_frame rb_ptr\<rbrace>
 2. \<And>sa s' sb_ptr rb_ptr x. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 sa s' sb_ptr rb_ptr\<rbrace> loadWordUser (sb_ptr + word_of_nat x * 4) \<lbrace>\<lambda>rv. valid_ipc_buffer_ptr' rb_ptr\<rbrace>
 3. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>_. True) and ?Q66 sa s' sb_ptr rb_ptr\<rbrace> load_word_offs sb_ptr x >>= store_word_offs rb_ptr x \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q66 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr x y. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; (x, y) \<in> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>valid_ipc_buffer_ptr' sb_ptr and ?Q'68 sa s' sb_ptr rb_ptr\<rbrace> loadWordUser (sb_ptr + y * 4) >>= storeWordUser (rb_ptr + y * 4) \<lbrace>\<lambda>rv. valid_ipc_buffer_ptr' sb_ptr and ?Q'68 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> length [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] = length [5 .e. n]
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> set (zip [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] [5 .e. n]) \<subseteq> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}
 7. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 8. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 9. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 10. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q66 sa s' sb_ptr rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
A total of 13 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> Suc (Suc (Suc (Suc (Suc 0)))) \<le> unat n \<longrightarrow> Suc (unat n - Suc (Suc (Suc (Suc (Suc 0))))) = unat n - 4
 2. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> set (zip [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] [5 .e. n]) \<subseteq> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}
 3. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. (\<lambda>_. True) and in_user_frame rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 7. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' sb_ptr and valid_ipc_buffer_ptr' rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
 8. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 9. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal (9 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>(sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; tcb_at s sa; tcb_at' s s'; tcb_at r sa; tcb_at' r s'; in_user_frame sb_ptr sa; valid_ipc_buffer_ptr' sb_ptr s'; valid_ipc_buffer_ptr' rb_ptr s'; in_user_frame rb_ptr sa; unat n \<le> msg_max_length; Suc (Suc (Suc (Suc (Suc 0)))) \<le> unat n\<rbrakk> \<Longrightarrow> Suc (unat n - Suc (Suc (Suc (Suc (Suc 0))))) = unat n - 4
 2. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> set (zip [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] [5 .e. n]) \<subseteq> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}
 3. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. (\<lambda>_. True) and in_user_frame rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 7. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' sb_ptr and valid_ipc_buffer_ptr' rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
 8. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 9. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal (8 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> set (zip [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] [5 .e. n]) \<subseteq> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}
 2. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 3. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. (\<lambda>_. True) and in_user_frame rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' sb_ptr and valid_ipc_buffer_ptr' rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
 7. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 8. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal (8 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> {([Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] ! i, [5 .e. n] ! i) |i. i < min (length [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)]) (length [5 .e. n])} \<subseteq> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}
 2. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 3. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. (\<lambda>_. True) and in_user_frame rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' sb_ptr and valid_ipc_buffer_ptr' rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
 7. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 8. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal (8 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> {([Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] ! i, map toEnum [5..<Suc (unat n)] ! i) |i. i < unat n - Suc (Suc (Suc (Suc 0)))} \<subseteq> {(x, y). y = word_of_nat x \<and> x < unat max_ipc_words}
 2. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 3. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. (\<lambda>_. True) and in_user_frame rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' sb_ptr and valid_ipc_buffer_ptr' rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
 7. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 8. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal (8 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr i. \<lbrakk>(sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; tcb_at s sa; tcb_at' s s'; i < unat n - Suc (Suc (Suc (Suc 0))); tcb_at r sa; tcb_at' r s'; in_user_frame sb_ptr sa; valid_ipc_buffer_ptr' sb_ptr s'; valid_ipc_buffer_ptr' rb_ptr s'; in_user_frame rb_ptr sa; unat n \<le> msg_max_length\<rbrakk> \<Longrightarrow> toEnum (5 + i) = 5 + word_of_nat i \<and> Suc (Suc (Suc (Suc (Suc i)))) < unat max_ipc_words
 2. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 3. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. (\<lambda>_. True) and in_user_frame rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' sb_ptr and valid_ipc_buffer_ptr' rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
 7. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 8. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal (8 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr i. \<lbrakk>(sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; tcb_at s sa; tcb_at' s s'; i < unat n - Suc (Suc (Suc (Suc 0))); tcb_at r sa; tcb_at' r s'; in_user_frame sb_ptr sa; valid_ipc_buffer_ptr' sb_ptr s'; valid_ipc_buffer_ptr' rb_ptr s'; in_user_frame rb_ptr sa; unat n \<le> 120\<rbrakk> \<Longrightarrow> i < 123
 2. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 3. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. (\<lambda>_. True) and in_user_frame rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' sb_ptr and valid_ipc_buffer_ptr' rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
 7. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 8. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal (8 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr i. \<lbrakk>(sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr; tcb_at s sa; tcb_at' s s'; tcb_at r sa; tcb_at' r s'; in_user_frame sb_ptr sa; valid_ipc_buffer_ptr' sb_ptr s'; valid_ipc_buffer_ptr' rb_ptr s'; in_user_frame rb_ptr sa; unat n \<le> 120\<rbrakk> \<Longrightarrow> unat n - Suc (Suc (Suc (Suc 0))) < 123
 2. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 3. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. (\<lambda>_. True) and in_user_frame rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' sb_ptr and valid_ipc_buffer_ptr' rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
 7. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 8. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal (7 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr buf_mrs. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> corres (=) (?R57 sa s' sb_ptr rb_ptr buf_mrs) (?R'57 sa s' sb_ptr rb_ptr buf_mrs) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs)))) (return (min n (word_of_nat (min (Suc (Suc (Suc (Suc 0)))) (unat n)) + word_of_nat (length buf_mrs))))
 2. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>?R57 sa s' sb_ptr rb_ptr\<rbrace>
 3. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>?R'57 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. (\<lambda>_. True) and in_user_frame rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' sb_ptr and valid_ipc_buffer_ptr' rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
 6. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 7. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal (6 subgoals):
 1. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc (unat n)] \<lbrace>\<lambda>buf_mrs _. True\<rbrace>
 2. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>x. loadWordUser (sb_ptr + x * 4) >>= storeWordUser (rb_ptr + x * 4)) [5 .e. n] \<lbrace>\<lambda>buf_mrs _. True\<rbrace>
 3. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x. (\<lambda>_. True) and in_user_frame rb_ptr and ?Q57 sa s' sb_ptr rb_ptr\<rbrace>
 4. \<And>sa s' sb_ptr rb_ptr. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame sb_ptr sa \<and> in_user_frame rb_ptr sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' sb_ptr s' \<and> valid_ipc_buffer_ptr' rb_ptr s'; (sa, s') \<in> state_relation; sb = Some sb_ptr; rb = Some rb_ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 sa s' sb_ptr rb_ptr\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' sb_ptr and valid_ipc_buffer_ptr' rb_ptr and ?Q'57 sa s' sb_ptr rb_ptr\<rbrace>
 5. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at s and tcb_at r and in_user_frame a and in_user_frame aa) saa\<rbrakk> \<Longrightarrow> (tcb_at s and tcb_at r and ?Q53 sa s' a aa) saa
 6. \<And>sa s' a aa saa. \<lbrakk>tcb_at s sa \<and> tcb_at r sa \<and> in_user_frame a sa \<and> in_user_frame aa sa \<and> unat n \<le> msg_max_length; tcb_at' s s' \<and> tcb_at' r s' \<and> valid_ipc_buffer_ptr' a s' \<and> valid_ipc_buffer_ptr' aa s'; (sa, s') \<in> state_relation; sb = Some a; rb = Some aa; (tcb_at' s and tcb_at' r and valid_ipc_buffer_ptr' a and valid_ipc_buffer_ptr' aa) saa\<rbrakk> \<Longrightarrow> (tcb_at' s and tcb_at' r and ?Q'53 sa s' a aa) saa proof (prove)
goal:
No subgoals! proof (state)
this:
corres (=) (tcb_at s and tcb_at r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat n \<le> msg_max_length)) (tcb_at' s and tcb_at' r and (case sb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case rb of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (copy_mrs s sb r rb n) (copyMRs s sb r rb n)

goal:
No subgoals!