theory TcbAcc_R

lemma setMRs_corres:
  assumes m: "mrs' = mrs"
  shows
  "corres (=) (tcb_at t and case_option \<top> in_user_frame buf)
              (tcb_at' t and case_option \<top> valid_ipc_buffer_ptr' buf)
              (set_mrs t buf mrs) (setMRs t buf mrs')" proof - have setRegister_def2: "setRegister = (\<lambda>r v. modify (\<lambda>s. s ( r := v )))" by ((rule ext)+, simp add: setRegister_def) have S: "\<And>xs ys n m. m - n \<ge> length xs \<Longrightarrow> (zip xs (drop n (take m ys))) = zip xs (drop n ys)" by (simp add: zip_take_triv2 drop_take) have upto_enum_nth_assist4:
    "\<And>i. i < 116 \<Longrightarrow> [(5::machine_word).e.0x78] ! i * 4 = 0x14 + of_nat i * 4" by (subst upto_enum_word, subst upt_lhs_sub_map, simp) note upt.simps[simp del] upt_rec_numeral[simp del] show ?thesis using m unfolding setMRs_def set_mrs_def apply (clarsimp simp: arch_tcb_set_registers_def arch_tcb_get_registers_def cong: option.case_cong split del: if_split) apply (subst bind_assoc[symmetric]) apply (fold thread_set_def[simplified]) apply (subst thread_set_as_user[where f="\<lambda>context. \<lambda>reg.
                      if reg \<in> set (take (length mrs) msg_registers)
                      then mrs ! (the_index msg_registers reg) else context reg",simplified]) apply (cases buf) apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_Nil zipWithM_x_modify
                           take_min_len zip_take_triv2 min.commute) apply (rule corres_guard_imp) apply (rule corres_split_nor[OF asUser_corres']) apply (rule corres_modify') apply (fastforce simp: fold_fun_upd[symmetric] msgRegisters_unfold
                            cong: if_cong simp del: the_index.simps) apply ((wp |simp)+)[6]
    \<comment> \<open>buf = Some a\<close> using if_split[split del] apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_Nil zipWithM_x_modify
                          take_min_len zip_take_triv2 min.commute
                          msgMaxLength_def msgLengthBits_def) apply (simp add: msg_max_length_def) apply (rule corres_guard_imp) apply (rule corres_split_nor[OF asUser_corres']) apply (rule corres_modify') apply (simp only: msgRegisters_unfold cong: if_cong) apply (fastforce simp: fold_fun_upd[symmetric]) apply clarsimp apply (rule corres_split_nor) apply (rule_tac S="{((x, y), (x', y')). y = y' \<and> x' = (a + (of_nat x * 4)) \<and> x < unat max_ipc_words}"
                        in zipWithM_x_corres) apply (fastforce intro: storeWordUser_corres) apply wp+ apply (clarsimp simp add: S msgMaxLength_def msg_max_length_def set_zip) apply (simp add: wordSize_def wordBits_def word_size max_ipc_words
                             upt_Suc_append[symmetric] upto_enum_word) apply simp apply (rule corres_trivial, clarsimp simp: min.commute) apply wp+ apply (wp | clarsimp simp: valid_ipc_buffer_ptr'_def)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (set_mrs t buf mrs) (setMRs t buf mrs') proof (state)
goal (1 subgoal):
 1. corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (set_mrs t buf mrs) (setMRs t buf mrs') proof (prove)
goal (1 subgoal):
 1. setRegister = (\<lambda>r v. modify (\<lambda>s. s(r := v))) proof (state)
this:
setRegister = (\<lambda>r v. modify (\<lambda>s. s(r := v)))

goal (1 subgoal):
 1. corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (set_mrs t buf mrs) (setMRs t buf mrs') proof (prove)
goal (1 subgoal):
 1. \<And>xs ys n m. length xs \<le> m - n \<Longrightarrow> zip xs (drop n (take m ys)) = zip xs (drop n ys) proof (state)
this:
length ?xs \<le> ?m - ?n \<Longrightarrow> zip ?xs (drop ?n (take ?m ?ys)) = zip ?xs (drop ?n ?ys)

goal (1 subgoal):
 1. corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (set_mrs t buf mrs) (setMRs t buf mrs') proof (prove)
goal (1 subgoal):
 1. \<And>i. i < 116 \<Longrightarrow> [5 .e. 0x78] ! i * 4 = 0x14 + word_of_nat i * 4 proof (state)
this:
?i1 < 116 \<Longrightarrow> [5 .e. 0x78] ! ?i1 * 4 = 0x14 + word_of_nat ?i1 * 4

goal (1 subgoal):
 1. corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (set_mrs t buf mrs) (setMRs t buf mrs') proof (state)
this:
[?i..<0] = []
[?i..<Suc ?j] = (if ?i \<le> ?j then [?i..<?j] @ [?j] else [])
[numeral ?m..<numeral ?n] = (if numeral ?m < numeral ?n then numeral ?m # [Suc (numeral ?m)..<numeral ?n] else [])

goal (1 subgoal):
 1. corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (set_mrs t buf mrs) (setMRs t buf mrs') proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (set_mrs t buf mrs) (setMRs t buf mrs') proof (prove)
using this:
mrs' = mrs

goal (1 subgoal):
 1. corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (set_mrs t buf mrs) (setMRs t buf mrs') proof (prove)
using this:
mrs' = mrs

goal (1 subgoal):
 1. corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do tcb <- gets_the $ get_tcb t;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else context reg);
set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) mrs);
case buf of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length mrs)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length mrs) msg_max_length
od
od) (do intSize <- return (fromIntegral wordSize);
hardwareMRs <- return TCB_H.msgRegisters;
bufferMRs <- return (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + PPtr (x * intSize)) [fromIntegral $ length hardwareMRs + 1 .e. msgMaxLength]);
msgLength <- return (min (length mrs') (length hardwareMRs + length bufferMRs));
mrs <- return (take msgLength mrs');
asUser t $ zipWithM_x setRegister hardwareMRs mrs;
zipWithM_x storeWordUser bufferMRs $ drop (length hardwareMRs) mrs;
return $ fromIntegral msgLength
od) proof (prove)
goal (1 subgoal):
 1. mrs' = mrs \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_context_get (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>));
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
goal (1 subgoal):
 1. mrs' = mrs \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_context_get (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>))
od;
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
goal (1 subgoal):
 1. mrs' = mrs \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_context_get (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>) t;
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
goal (1 subgoal):
 1. mrs' = mrs \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else context reg));
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else context reg));
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od)
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else context reg));
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg));
return (word_of_nat (min (length mrs) (Suc (Suc (Suc (Suc 0))))))
od) (do y <- asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs)));
return (word_of_nat (min (length mrs) (Suc (Suc (Suc (Suc 0))))))
od)
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else context reg));
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> corres (=) ?Q7 ?Q'7 (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg));
return (word_of_nat (min (length mrs) (Suc (Suc (Suc (Suc 0))))))
od) (do y <- asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs)));
return (word_of_nat (min (length mrs) (Suc (Suc (Suc (Suc 0))))))
od)
 2. \<And>s. \<lbrakk>mrs' = mrs; buf = None; tcb_at t s\<rbrakk> \<Longrightarrow> ?Q7 s
 3. \<And>s. \<lbrakk>mrs' = mrs; buf = None; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q'7 s
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else context reg));
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs)))
 2. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> corres (=) ?R11 ?R'11 (return (word_of_nat (min (length mrs) (Suc (Suc (Suc (Suc 0))))))) (return (word_of_nat (min (length mrs) (Suc (Suc (Suc (Suc 0)))))))
 3. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q11\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. ?R11\<rbrace>
 4. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. ?R'11\<rbrace>
 5. \<And>s. \<lbrakk>mrs' = mrs; buf = None; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q11) s
 6. \<And>s. \<lbrakk>mrs' = mrs; buf = None; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'11) s
 7. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else context reg));
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
goal (8 subgoals):
 1. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> Id \<longrightarrow> (\<lambda>reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else s reg, foldl (\<lambda>s (r, v). s(r := v)) s' (zip [R2, R3, R4, R5] mrs)) \<in> Id
 2. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> dc () ()
 3. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> corres (=) ?R11 ?R'11 (return (word_of_nat (min (length mrs) (Suc (Suc (Suc (Suc 0))))))) (return (word_of_nat (min (length mrs) (Suc (Suc (Suc (Suc 0)))))))
 4. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q11\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. ?R11\<rbrace>
 5. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. ?R'11\<rbrace>
 6. \<And>s. \<lbrakk>mrs' = mrs; buf = None; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q11) s
 7. \<And>s. \<lbrakk>mrs' = mrs; buf = None; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'11) s
 8. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else context reg));
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> dc () ()
 2. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> corres (=) ?R11 ?R'11 (return (word_of_nat (min (length mrs) (Suc (Suc (Suc (Suc 0))))))) (return (word_of_nat (min (length mrs) (Suc (Suc (Suc (Suc 0)))))))
 3. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q11\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. ?R11\<rbrace>
 4. \<lbrakk>mrs' = mrs; buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. ?R'11\<rbrace>
 5. \<And>s. \<lbrakk>mrs' = mrs; buf = None; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q11) s
 6. \<And>s. \<lbrakk>mrs' = mrs; buf = None; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'11) s
 7. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else context reg));
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else context reg));
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
using this:
?P (if ?Q then ?x else ?y) = ((?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y))

goal (1 subgoal):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else context reg));
case buf of None \<Rightarrow> return (word_of_nat (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) mrs);
return (word_of_nat (min (length mrs) msg_max_length))
od
od) (do y <- asUser t (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t and in_user_frame a) (tcb_at' t and valid_ipc_buffer_ptr' a) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg));
y <- zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<Suc msg_max_length] (drop (Suc (Suc (Suc (Suc 0)))) mrs);
return (word_of_nat (min msg_max_length (length mrs)))
od) (do y <- asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs)));
y <- zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs));
return (word_of_nat (min (length mrs) 120))
od) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t and in_user_frame a) (tcb_at' t and valid_ipc_buffer_ptr' a) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg));
y <- zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs);
return (word_of_nat (min 120 (length mrs)))
od) (do y <- asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs)));
y <- zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs));
return (word_of_nat (min (length mrs) 120))
od) proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?Q94 a) (?Q'94 a) (do y <- as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg));
y <- zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs);
return (word_of_nat (min 120 (length mrs)))
od) (do y <- asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs)));
y <- zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs));
return (word_of_nat (min (length mrs) 120))
od)
 2. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> ?Q94 a s
 3. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> ?Q'94 a s proof (prove)
goal (6 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs)))
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R98 a) (?R'98 a) (do y <- zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs);
return (word_of_nat (min 120 (length mrs)))
od) (do y <- zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs));
return (word_of_nat (min (length mrs) 120))
od)
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. ?R98 a\<rbrace>
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. ?R'98 a\<rbrace>
 5. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
 6. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal (7 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> Id \<longrightarrow> (\<lambda>reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else s reg, foldl (\<lambda>s (r, v). s(r := v)) s' (zip [R2, R3, R4, R5] mrs)) \<in> Id
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> dc () ()
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R98 a) (?R'98 a) (do y <- zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs);
return (word_of_nat (min 120 (length mrs)))
od) (do y <- zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs));
return (word_of_nat (min (length mrs) 120))
od)
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. ?R98 a\<rbrace>
 5. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. ?R'98 a\<rbrace>
 6. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
 7. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal (7 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> Id \<longrightarrow> (\<lambda>reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index [R2, R3, R4, R5] reg else s reg, foldl (\<lambda>s (r, v). s(r := v)) s' (zip [R2, R3, R4, R5] mrs)) \<in> Id
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> dc () ()
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R98 a) (?R'98 a) (do y <- zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs);
return (word_of_nat (min 120 (length mrs)))
od) (do y <- zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs));
return (word_of_nat (min (length mrs) 120))
od)
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. ?R98 a\<rbrace>
 5. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. ?R'98 a\<rbrace>
 6. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
 7. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal (6 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> dc () ()
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R98 a) (?R'98 a) (do y <- zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs);
return (word_of_nat (min 120 (length mrs)))
od) (do y <- zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs));
return (word_of_nat (min (length mrs) 120))
od)
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. ?R98 a\<rbrace>
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. ?R'98 a\<rbrace>
 5. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
 6. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R98 a) (?R'98 a) (do y <- zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs);
return (word_of_nat (min 120 (length mrs)))
od) (do y <- zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs));
return (word_of_nat (min (length mrs) 120))
od)
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. ?R98 a\<rbrace>
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. ?R'98 a\<rbrace>
 4. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
 5. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal (8 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres dc (?P115 a) (?P'115 a) (zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs)) (zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)))
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R115 a) (?R'115 a) (return (word_of_nat (min 120 (length mrs)))) (return (word_of_nat (min (length mrs) 120)))
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 a\<rbrace> zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs) \<lbrace>\<lambda>x. ?R115 a\<rbrace>
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 a\<rbrace> zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)) \<lbrace>\<lambda>x. ?R'115 a\<rbrace>
 5. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. ?P115 a and ?Q115 a\<rbrace>
 6. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. ?P'115 a and ?Q'115 a\<rbrace>
 7. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
 8. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal (12 subgoals):
 1. \<And>a x x' y y'. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); ((x, y), x', y') \<in> {((x, y), x', y'). y = y' \<and> x' = a + word_of_nat x * 4 \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> corres dc (?P115 a) (?P'115 a) (store_word_offs a x y) (storeWordUser x' y')
 2. \<And>a x x' y y'. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); ((x, y), x', y') \<in> {((x, y), x', y'). y = y' \<and> x' = a + word_of_nat x * 4 \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P115 a\<rbrace> store_word_offs a x y \<lbrace>\<lambda>rv. ?P115 a\<rbrace>
 3. \<And>a x x' y y'. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); ((x, y), x', y') \<in> {((x, y), x', y'). y = y' \<and> x' = a + word_of_nat x * 4 \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P'115 a\<rbrace> storeWordUser x' y' \<lbrace>\<lambda>rv. ?P'115 a\<rbrace>
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> set (zip (zip [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs)) (zip (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)))) \<subseteq> {((x, y), x', y'). y = y' \<and> x' = a + word_of_nat x * 4 \<and> x < unat max_ipc_words}
 5. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> length (zip [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs)) = length (zip (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)))
 6. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R115 a) (?R'115 a) (return (word_of_nat (min 120 (length mrs)))) (return (word_of_nat (min (length mrs) 120)))
 7. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 a\<rbrace> zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs) \<lbrace>\<lambda>x. ?R115 a\<rbrace>
 8. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 a\<rbrace> zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)) \<lbrace>\<lambda>x. ?R'115 a\<rbrace>
 9. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. ?P115 a and ?Q115 a\<rbrace>
 10. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. ?P'115 a and ?Q'115 a\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>a x x' y y'. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); ((x, y), x', y') \<in> {((x, y), x', y'). y = y' \<and> x' = a + word_of_nat x * 4 \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>in_user_frame a\<rbrace> store_word_offs a x y \<lbrace>\<lambda>rv. in_user_frame a\<rbrace>
 2. \<And>a x x' y y'. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); ((x, y), x', y') \<in> {((x, y), x', y'). y = y' \<and> x' = a + word_of_nat x * 4 \<and> x < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>valid_ipc_buffer_ptr' a\<rbrace> storeWordUser x' y' \<lbrace>\<lambda>rv. valid_ipc_buffer_ptr' a\<rbrace>
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> set (zip (zip [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs)) (zip (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)))) \<subseteq> {((x, y), x', y'). y = y' \<and> x' = a + word_of_nat x * 4 \<and> x < unat max_ipc_words}
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> length (zip [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs)) = length (zip (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)))
 5. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R115 a) (?R'115 a) (return (word_of_nat (min 120 (length mrs)))) (return (word_of_nat (min (length mrs) 120)))
 6. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 a\<rbrace> zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs) \<lbrace>\<lambda>x. ?R115 a\<rbrace>
 7. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 a\<rbrace> zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)) \<lbrace>\<lambda>x. ?R'115 a\<rbrace>
 8. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. in_user_frame a and ?Q115 a\<rbrace>
 9. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' a and ?Q'115 a\<rbrace>
 10. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> set (zip (zip [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs)) (zip (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)))) \<subseteq> {((x, y), x', y'). y = y' \<and> x' = a + word_of_nat x * 4 \<and> x < unat max_ipc_words}
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> length (zip [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs)) = length (zip (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)))
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R115 a) (?R'115 a) (return (word_of_nat (min 120 (length mrs)))) (return (word_of_nat (min (length mrs) 120)))
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 a\<rbrace> zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs) \<lbrace>\<lambda>x. ?R115 a\<rbrace>
 5. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 a\<rbrace> zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)) \<lbrace>\<lambda>x. ?R'115 a\<rbrace>
 6. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. in_user_frame a and ?Q115 a\<rbrace>
 7. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' a and ?Q'115 a\<rbrace>
 8. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
 9. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal (9 subgoals):
 1. \<And>a i. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); i < 116; i < length mrs - Suc (Suc (Suc (Suc 0)))\<rbrakk> \<Longrightarrow> [5 .e. 0x78] ! i * word_of_nat wordSize = 0x14 + word_of_nat i * 4 \<and> Suc (Suc (Suc (Suc (Suc i)))) < unat max_ipc_words
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> length (zip [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs)) = length (zip (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)))
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R115 a) (?R'115 a) (return (word_of_nat (min 120 (length mrs)))) (return (word_of_nat (min (length mrs) 120)))
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 a\<rbrace> zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs) \<lbrace>\<lambda>x. ?R115 a\<rbrace>
 5. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 a\<rbrace> zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)) \<lbrace>\<lambda>x. ?R'115 a\<rbrace>
 6. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. in_user_frame a and ?Q115 a\<rbrace>
 7. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' a and ?Q'115 a\<rbrace>
 8. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
 9. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal (8 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> length (zip [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs)) = length (zip (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)))
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R115 a) (?R'115 a) (return (word_of_nat (min 120 (length mrs)))) (return (word_of_nat (min (length mrs) 120)))
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 a\<rbrace> zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs) \<lbrace>\<lambda>x. ?R115 a\<rbrace>
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 a\<rbrace> zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)) \<lbrace>\<lambda>x. ?R'115 a\<rbrace>
 5. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. in_user_frame a and ?Q115 a\<rbrace>
 6. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' a and ?Q'115 a\<rbrace>
 7. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
 8. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal (7 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> corres (=) (?R115 a) (?R'115 a) (return (word_of_nat (min 120 (length mrs)))) (return (word_of_nat (min (length mrs) 120)))
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 a\<rbrace> zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs) \<lbrace>\<lambda>x. ?R115 a\<rbrace>
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 a\<rbrace> zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)) \<lbrace>\<lambda>x. ?R'115 a\<rbrace>
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. in_user_frame a and ?Q115 a\<rbrace>
 5. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' a and ?Q'115 a\<rbrace>
 6. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
 7. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal (6 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 a\<rbrace> zipWithM_x (store_word_offs a) [Suc (Suc (Suc (Suc (Suc 0))))..<121] (drop (Suc (Suc (Suc (Suc 0)))) mrs) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 a\<rbrace> zipWithM_x storeWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [5 .e. 0x78]) (drop (Suc (Suc (Suc (Suc 0)))) (take 120 mrs)) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q98 a\<rbrace> as_user t (modify (\<lambda>context reg. if reg \<in> set (take (length mrs) [R2, R3, R4, R5]) then mrs ! the_index msg_registers reg else context reg)) \<lbrace>\<lambda>x. in_user_frame a and ?Q115 a\<rbrace>
 4. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x. valid_ipc_buffer_ptr' a and ?Q'115 a\<rbrace>
 5. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q98 a) s
 6. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 a\<rbrace> asUser t (modify (\<lambda>s. foldl (\<lambda>s (r, v). s(r := v)) s (zip [R2, R3, R4, R5] mrs))) \<lbrace>\<lambda>x s. valid_ipc_buffer_ptr' a s \<and> True\<rbrace>
 2. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at t and in_user_frame a) s\<rbrakk> \<Longrightarrow> (tcb_at t and (\<lambda>s. in_user_frame a s \<and> True)) s
 3. \<And>a s. \<lbrakk>mrs' = mrs; buf = Some a; \<And>P Q x y. P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y)); (tcb_at' t and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'98 a) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres (=) (tcb_at t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (set_mrs t buf mrs) (setMRs t buf mrs')

goal:
No subgoals!