theory Tcb_C

lemma getMRs_rel_context:
  "\<lbrakk>getMRs_rel args buffer s;
    (cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer) s;
    ko_at' ko t s ; t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow>
  getMRs_rel args buffer (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)" apply (clarsimp simp: getMRs_rel_def) apply (rule exI, erule conjI) apply (subst (asm) det_wp_use, rule det_wp_getMRs) apply (simp add: cur_tcb'_def) apply (subst det_wp_use, rule det_wp_getMRs) apply (simp add: cur_tcb'_def) apply (rule conjI) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs
                          objBits_simps ps_clear_def split: if_split) apply (clarsimp simp: valid_ipc_buffer_ptr'_def split: option.splits) apply (clarsimp simp: typ_at'_def ko_wp_at'_def projectKOs obj_at'_real_def
                         objBits_simps ps_clear_def split: if_split) apply (clarsimp simp: getMRs_def in_monad) apply (frule use_valid, rule asUser_inv [where P="(=) s"]) apply (wp mapM_wp' getRegister_inv)[1] apply simp apply clarsimp apply (drule (1) asUser_context) apply (wp mapM_wp' getRegister_inv)[1] apply assumption apply (intro exI) apply (erule conjI) apply (cases buffer) apply (clarsimp simp: return_def) apply clarsimp apply (drule mapM_upd_inv [rotated -1]) prefer 3 apply fastforce prefer 2 apply wp apply (clarsimp simp: loadWordUser_def in_monad stateAssert_def word_size
                  simp del: fun_upd_apply) apply (rule conjI) apply (clarsimp simp: pointerInUserData_def typ_at'_def ko_wp_at'_def
                         projectKOs ps_clear_def obj_at'_real_def
                  split: if_split) apply (erule doMachineOp_context) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>getMRs_rel args buffer s; (cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; ko_at' ko t s; t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow> getMRs_rel args buffer (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; msgLength mi \<le> msgMaxLength; fst (getMRs (ksCurThread s) buffer mi s) = {(args, s)}\<rbrakk> \<Longrightarrow> \<exists>mi. msgLength mi \<le> msgMaxLength \<and> fst (getMRs (ksCurThread s) buffer mi (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) = {(args, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)} proof (prove)
goal (1 subgoal):
 1. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; fst (getMRs (ksCurThread s) buffer mi s) = {(args, s)}\<rbrakk> \<Longrightarrow> fst (getMRs (ksCurThread s) buffer mi (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) = {(args, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)} proof (prove)
goal (2 subgoals):
 1. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s\<rbrakk> \<Longrightarrow> (tcb_at' (ksCurThread s) and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s
 2. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> fst (getMRs (ksCurThread s) buffer mi (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) = {(args, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)} proof (prove)
goal (1 subgoal):
 1. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> fst (getMRs (ksCurThread s) buffer mi (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) = {(args, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)} proof (prove)
goal (2 subgoals):
 1. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> (tcb_at' (ksCurThread s) and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)
 2. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> (args, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (getMRs (ksCurThread s) buffer mi (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; tcb_at' (ksCurThread s) s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> tcb_at' (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)
 2. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> (args, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (getMRs (ksCurThread s) buffer mi (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; tcb_at' (ksCurThread s) s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> tcb_at' (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)
 2. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; tcb_at' (ksCurThread s) s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)
 3. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> (args, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (getMRs (ksCurThread s) buffer mi (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; tcb_at' (ksCurThread s) s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)
 2. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> (args, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (getMRs (ksCurThread s) buffer mi (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>mi x2. \<lbrakk>(args, s) \<in> fst (getMRs (ksCurThread s) (Some x2) mi s); ko_at' ko t s; t \<noteq> ksCurThread s; tcb_at' (ksCurThread s) s; buffer = Some x2; is_aligned x2 msg_align_bits; typ_at' UserDataT (x2 && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x2 && ~~ mask pageBits) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)
 2. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> (args, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (getMRs (ksCurThread s) buffer mi (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>mi. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (args, s) \<in> fst (getMRs (ksCurThread s) buffer mi s)\<rbrakk> \<Longrightarrow> (args, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (getMRs (ksCurThread s) buffer mi (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>mi s'' hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (hardwareMRValues, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) s); (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s''); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues\<rbrakk> \<Longrightarrow> \<exists>s'' hardwareMRValuesa. (hardwareMRValuesa, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s'') \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValuesa @ take (unat (msgLength mi) - length hardwareMRValuesa) bufferMRValuesa) proof (prove)
goal (3 subgoals):
 1. \<And>mi s'' hardwareMRValues bufferMRValues P. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (hardwareMRValues, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) s); (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s''); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM getRegister TCB_H.msgRegisters \<lbrace>\<lambda>x. P\<rbrace>
 2. \<And>mi s'' hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (hardwareMRValues, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) s); (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s''); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues\<rbrakk> \<Longrightarrow> s = s
 3. \<And>mi s'' hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (hardwareMRValues, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) s); (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s''); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' hardwareMRValuesa. (hardwareMRValuesa, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s'') \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValuesa @ take (unat (msgLength mi) - length hardwareMRValuesa) bufferMRValuesa) proof (prove)
goal (2 subgoals):
 1. \<And>mi s'' hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (hardwareMRValues, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) s); (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s''); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues\<rbrakk> \<Longrightarrow> s = s
 2. \<And>mi s'' hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (hardwareMRValues, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) s); (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s''); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' hardwareMRValuesa. (hardwareMRValuesa, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s'') \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValuesa @ take (unat (msgLength mi) - length hardwareMRValuesa) bufferMRValuesa) proof (prove)
goal (1 subgoal):
 1. \<And>mi s'' hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (hardwareMRValues, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) s); (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s''); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' hardwareMRValuesa. (hardwareMRValuesa, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s'') \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValuesa @ take (unat (msgLength mi) - length hardwareMRValuesa) bufferMRValuesa) proof (prove)
goal (1 subgoal):
 1. \<And>mi hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (hardwareMRValues, s) \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) s); (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues\<rbrakk> \<Longrightarrow> \<exists>s'' hardwareMRValuesa. (hardwareMRValuesa, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s'') \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValuesa @ take (unat (msgLength mi) - length hardwareMRValuesa) bufferMRValuesa) proof (prove)
goal (3 subgoals):
 1. \<And>mi hardwareMRValues bufferMRValues sa. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM getRegister TCB_H.msgRegisters \<lbrace>\<lambda>_. (=) sa\<rbrace>
 2. \<And>mi hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues\<rbrakk> \<Longrightarrow> t \<noteq> ksCurThread s
 3. \<And>mi hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; (hardwareMRValues, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st76 mi hardwareMRValues bufferMRValues) (tcbArch ko)) ko))\<rparr>) \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st76 mi hardwareMRValues bufferMRValues) (tcbArch ko)) ko))\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>s'' hardwareMRValuesa. (hardwareMRValuesa, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s'') \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValuesa @ take (unat (msgLength mi) - length hardwareMRValuesa) bufferMRValuesa) proof (prove)
goal (2 subgoals):
 1. \<And>mi hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues\<rbrakk> \<Longrightarrow> t \<noteq> ksCurThread s
 2. \<And>mi hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; (hardwareMRValues, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st76 mi hardwareMRValues bufferMRValues) (tcbArch ko)) ko))\<rparr>) \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st76 mi hardwareMRValues bufferMRValues) (tcbArch ko)) ko))\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>s'' hardwareMRValuesa. (hardwareMRValuesa, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s'') \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValuesa @ take (unat (msgLength mi) - length hardwareMRValuesa) bufferMRValuesa) proof (prove)
goal (1 subgoal):
 1. \<And>mi hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; (hardwareMRValues, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st76 mi hardwareMRValues bufferMRValues) (tcbArch ko)) ko))\<rparr>) \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st76 mi hardwareMRValues bufferMRValues) (tcbArch ko)) ko))\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>s'' hardwareMRValuesa. (hardwareMRValuesa, s'') \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s'') \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValuesa @ take (unat (msgLength mi) - length hardwareMRValuesa) bufferMRValuesa) proof (prove)
goal (1 subgoal):
 1. \<And>mi hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; (hardwareMRValues, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st76 mi hardwareMRValues bufferMRValues) (tcbArch ko)) ko))\<rparr>) \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st76 mi hardwareMRValues bufferMRValues) (tcbArch ko)) ko))\<rparr>))\<rbrakk> \<Longrightarrow> (?hardwareMRValues87 mi hardwareMRValues bufferMRValues, ?s''86 mi hardwareMRValues bufferMRValues) \<in> fst (asUser (ksCurThread s) (mapM getRegister TCB_H.msgRegisters) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) (?s''86 mi hardwareMRValues bufferMRValues)) \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) (?hardwareMRValues87 mi hardwareMRValues bufferMRValues) @ take (unat (msgLength mi) - length (?hardwareMRValues87 mi hardwareMRValues bufferMRValues)) bufferMRValuesa) proof (prove)
goal (1 subgoal):
 1. \<And>mi hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues\<rbrakk> \<Longrightarrow> \<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValuesa proof (prove)
goal (2 subgoals):
 1. \<And>mi hardwareMRValues bufferMRValues. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = None\<rbrakk> \<Longrightarrow> \<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValuesa
 2. \<And>mi hardwareMRValues bufferMRValues a. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a\<rbrakk> \<Longrightarrow> \<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValuesa proof (prove)
goal (1 subgoal):
 1. \<And>mi hardwareMRValues bufferMRValues a. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (bufferMRValues, s) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a\<rbrakk> \<Longrightarrow> \<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst ((case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValuesa proof (prove)
goal (1 subgoal):
 1. \<And>mi hardwareMRValues bufferMRValues a. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; (bufferMRValues, s) \<in> fst (mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) s); args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a\<rbrakk> \<Longrightarrow> \<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi) - length hardwareMRValues) bufferMRValuesa proof (prove)
goal (3 subgoals):
 1. \<And>mi hardwareMRValues bufferMRValues a x rv. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a; (rv, s) \<in> fst (loadWordUser x s); x \<in> set (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength])\<rbrakk> \<Longrightarrow> (rv, ?g91 mi hardwareMRValues bufferMRValues a s) \<in> fst (loadWordUser x (?g91 mi hardwareMRValues bufferMRValues a s))
 2. \<And>mi hardwareMRValues bufferMRValues a x. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> loadWordUser x \<lbrace>\<lambda>_. (=) s\<rbrace>
 3. \<And>mi hardwareMRValues bufferMRValues a. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a; (bufferMRValues, ?g91 mi hardwareMRValues bufferMRValues a s) \<in> fst (mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (?g91 mi hardwareMRValues bufferMRValues a s))\<rbrakk> \<Longrightarrow> \<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi) - length hardwareMRValues) bufferMRValuesa proof (prove)
goal (3 subgoals):
 1. \<And>mi hardwareMRValues bufferMRValues a. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a; (bufferMRValues, ?g91 mi hardwareMRValues bufferMRValues a s) \<in> fst (mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (?g91 mi hardwareMRValues bufferMRValues a s))\<rbrakk> \<Longrightarrow> \<exists>bufferMRValuesa. (bufferMRValuesa, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues = take (unat (msgLength mi) - length hardwareMRValues) bufferMRValuesa
 2. \<And>mi hardwareMRValues bufferMRValues a x rv. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a; (rv, s) \<in> fst (loadWordUser x s); x \<in> set (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength])\<rbrakk> \<Longrightarrow> (rv, ?g91 mi hardwareMRValues bufferMRValues a s) \<in> fst (loadWordUser x (?g91 mi hardwareMRValues bufferMRValues a s))
 3. \<And>mi hardwareMRValues bufferMRValues a x. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> loadWordUser x \<lbrace>\<lambda>_. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>mi hardwareMRValues bufferMRValues a x rv. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a; (rv, s) \<in> fst (loadWordUser x s); x \<in> set (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength])\<rbrakk> \<Longrightarrow> (rv, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (loadWordUser x (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>))
 2. \<And>mi hardwareMRValues bufferMRValues a x. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> loadWordUser x \<lbrace>\<lambda>_. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>mi hardwareMRValues bufferMRValues a x. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> loadWordUser x \<lbrace>\<lambda>_. (=) s\<rbrace>
 2. \<And>mi hardwareMRValues bufferMRValues a x rv. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a; (rv, s) \<in> fst (loadWordUser x s); x \<in> set (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength])\<rbrakk> \<Longrightarrow> (rv, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (loadWordUser x (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>mi hardwareMRValues bufferMRValues a x rv. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a; (rv, s) \<in> fst (loadWordUser x s); x \<in> set (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength])\<rbrakk> \<Longrightarrow> (rv, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (loadWordUser x (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>mi hardwareMRValues bufferMRValues a rv xa. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a; pointerInUserData (a + xa * word_of_nat wordSize) s; (rv, s) \<in> fst (doMachineOp (loadWord (a + xa * word_of_nat wordSize)) s); 1 + word_of_nat (length TCB_H.msgRegisters) \<le> xa; xa \<le> msgMaxLength\<rbrakk> \<Longrightarrow> pointerInUserData (a + xa * word_of_nat wordSize) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> (rv, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (doMachineOp (loadWord (a + xa * word_of_nat wordSize)) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>mi hardwareMRValues bufferMRValues a rv xa. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a; pointerInUserData (a + xa * word_of_nat wordSize) s; (rv, s) \<in> fst (doMachineOp (loadWord (a + xa * word_of_nat wordSize)) s); 1 + word_of_nat (length TCB_H.msgRegisters) \<le> xa; xa \<le> msgMaxLength\<rbrakk> \<Longrightarrow> pointerInUserData (a + xa * word_of_nat wordSize) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)
 2. \<And>mi hardwareMRValues bufferMRValues a rv xa. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a; pointerInUserData (a + xa * word_of_nat wordSize) s; (rv, s) \<in> fst (doMachineOp (loadWord (a + xa * word_of_nat wordSize)) s); 1 + word_of_nat (length TCB_H.msgRegisters) \<le> xa; xa \<le> msgMaxLength\<rbrakk> \<Longrightarrow> (rv, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (doMachineOp (loadWord (a + xa * word_of_nat wordSize)) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>mi hardwareMRValues bufferMRValues a rv xa. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; cur_tcb' s; valid_ipc_buffer_ptr' a s; args = take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues; buffer = Some a; pointerInUserData (a + xa * word_of_nat wordSize) s; (rv, s) \<in> fst (doMachineOp (loadWord (a + xa * word_of_nat wordSize)) s); 1 + word_of_nat (length TCB_H.msgRegisters) \<le> xa; xa \<le> msgMaxLength\<rbrakk> \<Longrightarrow> (rv, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (doMachineOp (loadWord (a + xa * word_of_nat wordSize)) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal:
No subgoals!