theory TcbAcc_R

lemma getMRs_corres:
  "corres (=) (tcb_at t)
              (tcb_at' t and case_option \<top> valid_ipc_buffer_ptr' buf)
              (get_mrs t buf mi) (getMRs t buf (message_info_map mi))" proof - have S: "get = gets id" by (simp add: gets_def) have T: "corres (\<lambda>con regs. regs = map con msg_registers) (tcb_at t) (tcb_at' t)
     (thread_get (arch_tcb_get_registers o tcb_arch) t) (asUser t (mapM getRegister ARM_H.msgRegisters))" unfolding arch_tcb_get_registers_def apply (subst thread_get_as_user) apply (rule asUser_corres') apply (subst mapM_gets) apply (simp add: getRegister_def) apply (simp add: S ARM_H.msgRegisters_def msg_registers_def) done show ?thesis apply (case_tac mi, simp add: get_mrs_def getMRs_def split del: if_split) apply (case_tac buf) apply (rule corres_guard_imp) apply (rule corres_split [where R = "\<lambda>_. \<top>" and R' =  "\<lambda>_. \<top>", OF T]) apply simp apply wp+ apply simp apply simp apply (rule corres_guard_imp) apply (rule corres_split[OF T]) apply (simp only: option.simps return_bind fun_app_def
                        load_word_offs_def doMachineOp_mapM ef_loadWord) apply (rule corres_split_eqr) apply (simp only: mapM_map_simp msgMaxLength_def msgLengthBits_def
                           msg_max_length_def o_def upto_enum_word) apply (rule corres_mapM [where r'="(=)" and S="{a. fst a = snd a \<and> fst a < unat max_ipc_words}"]) apply simp apply simp apply (simp add: word_size wordSize_def wordBits_def) apply (rule loadWordUser_corres) apply simp apply wp+ apply simp apply (unfold msgRegisters_unfold)[1] apply simp apply (clarsimp simp: set_zip) apply (simp add: msgRegisters_unfold max_ipc_words nth_append) apply (rule corres_trivial, simp) apply (wp hoare_vcg_all_lift | simp add: valid_ipc_buffer_ptr'_def)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (get_mrs t buf mi) (getMRs t buf (message_info_map mi)) proof (state)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (get_mrs t buf mi) (getMRs t buf (message_info_map mi)) proof (prove)
goal (1 subgoal):
 1. get = gets id proof (state)
this:
get = gets id

goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (get_mrs t buf mi) (getMRs t buf (message_info_map mi)) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>con regs. regs = map con msg_registers) (tcb_at t) (tcb_at' t) (thread_get (arch_tcb_get_registers \<circ> tcb_arch) t) (asUser t (mapM getRegister TCB_H.msgRegisters)) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>con regs. regs = map con msg_registers) (tcb_at t) (tcb_at' t) (thread_get (arch_tcb_context_get \<circ> tcb_arch) t) (asUser t (mapM getRegister TCB_H.msgRegisters)) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>con regs. regs = map con msg_registers) (tcb_at t) (tcb_at' t) (as_user t get) (asUser t (mapM getRegister TCB_H.msgRegisters)) proof (prove)
goal (1 subgoal):
 1. corres_underlying Id False True (\<lambda>con regs. regs = map con msg_registers) (\<lambda>_. True) (\<lambda>_. True) get (mapM getRegister TCB_H.msgRegisters) proof (prove)
goal (2 subgoals):
 1. \<And>x. getRegister x = gets (?f2 x)
 2. corres_underlying Id False True (\<lambda>con regs. regs = map con msg_registers) (\<lambda>_. True) (\<lambda>_. True) get (gets (\<lambda>s. map (\<lambda>x. ?f2 x s) TCB_H.msgRegisters)) proof (prove)
goal (1 subgoal):
 1. corres_underlying Id False True (\<lambda>con regs. regs = map con msg_registers) (\<lambda>_. True) (\<lambda>_. True) get (gets (\<lambda>s. map s TCB_H.msgRegisters)) proof (prove)
goal:
No subgoals! proof (state)
this:
corres (\<lambda>con regs. regs = map con msg_registers) (tcb_at t) (tcb_at' t) (thread_get (arch_tcb_get_registers \<circ> tcb_arch) t) (asUser t (mapM getRegister TCB_H.msgRegisters))

goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (get_mrs t buf mi) (getMRs t buf (message_info_map mi)) proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (get_mrs t buf mi) (getMRs t buf (message_info_map mi)) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. mi = Structures_A.message_info.MI x1 x2 x3 x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) t;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do hardwareMRValues <- asUser t (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) hardwareMRValues @ take (unat x1 - length hardwareMRValues) bufferMRValues)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) t;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do hardwareMRValues <- asUser t (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) hardwareMRValues @ take (unat x1 - length hardwareMRValues) bufferMRValues)
od)
 2. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) t;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do hardwareMRValues <- asUser t (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) hardwareMRValues @ take (unat x1 - length hardwareMRValues) bufferMRValues)
od) proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 x3 x4. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None\<rbrakk> \<Longrightarrow> corres (=) (?Q5 x1 x2 x3 x4) (?Q'5 x1 x2 x3 x4) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) t;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do hardwareMRValues <- asUser t (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) hardwareMRValues @ take (unat x1 - length hardwareMRValues) bufferMRValues)
od)
 2. \<And>x1 x2 x3 x4 s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None; tcb_at t s\<rbrakk> \<Longrightarrow> ?Q5 x1 x2 x3 x4 s
 3. \<And>x1 x2 x3 x4 s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> ?Q'5 x1 x2 x3 x4 s
 4. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) t;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do hardwareMRValues <- asUser t (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) hardwareMRValues @ take (unat x1 - length hardwareMRValues) bufferMRValues)
od) proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 x3 x4 context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>_. True) (do buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) rv' @ take (unat x1 - length rv') bufferMRValues)
od)
 2. \<And>x1 x2 x3 x4. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 x1 x2 x3 x4\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x1 x2 x3 x4. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'9 x1 x2 x3 x4\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>x1 x2 x3 x4 s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q9 x1 x2 x3 x4) s
 5. \<And>x1 x2 x3 x4 s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'9 x1 x2 x3 x4) s
 6. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) t;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do hardwareMRValues <- asUser t (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) hardwareMRValues @ take (unat x1 - length hardwareMRValues) bufferMRValues)
od) proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 x3 x4. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 x1 x2 x3 x4\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>x1 x2 x3 x4. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'9 x1 x2 x3 x4\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x1 x2 x3 x4 s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q9 x1 x2 x3 x4) s
 4. \<And>x1 x2 x3 x4 s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'9 x1 x2 x3 x4) s
 5. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) t;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do hardwareMRValues <- asUser t (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) hardwareMRValues @ take (unat x1 - length hardwareMRValues) bufferMRValues)
od) proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 x3 x4 s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and (\<lambda>_. True)) s
 2. \<And>x1 x2 x3 x4 s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>s. True)) s
 3. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) t;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do hardwareMRValues <- asUser t (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) hardwareMRValues @ take (unat x1 - length hardwareMRValues) bufferMRValues)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = None; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>s. True)) s
 2. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) t;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do hardwareMRValues <- asUser t (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) hardwareMRValues @ take (unat x1 - length hardwareMRValues) bufferMRValues)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) t;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do hardwareMRValues <- asUser t (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) hardwareMRValues @ take (unat x1 - length hardwareMRValues) bufferMRValues)
od) proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> corres (=) (?Q21 x1 x2 x3 x4 a) (?Q'21 x1 x2 x3 x4 a) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) t;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do hardwareMRValues <- asUser t (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) hardwareMRValues @ take (unat x1 - length hardwareMRValues) bufferMRValues)
od)
 2. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> ?Q21 x1 x2 x3 x4 a s
 3. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> ?Q'21 x1 x2 x3 x4 a s proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R25 x1 x2 x3 x4 a context) (?R'25 x1 x2 x3 x4 a rv') (do buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do bufferMRValues <- case buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> mapM loadWordUser (map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) rv' @ take (unat x1 - length rv') bufferMRValues)
od)
 2. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>?R25 x1 x2 x3 x4 a\<rbrace>
 3. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>?R'25 x1 x2 x3 x4 a\<rbrace>
 4. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
 5. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'25 x1 x2 x3 x4 a) s proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R25 x1 x2 x3 x4 a context) (?R'25 x1 x2 x3 x4 a (map context msg_registers)) (do buf_mrs <- mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) buf_mrs)
od) (do bufferMRValues <- mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) bufferMRValues)
od)
 2. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>?R25 x1 x2 x3 x4 a\<rbrace>
 3. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>?R'25 x1 x2 x3 x4 a\<rbrace>
 4. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
 5. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'25 x1 x2 x3 x4 a) s proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?P44 x1 x2 x3 x4 a context) (?P'39 x1 x2 x3 x4 a (map context msg_registers)) (mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else [])) (mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))
 2. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 3. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 4. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 5. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. ?P44 x1 x2 x3 x4 a b and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 6. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. ?P'39 x1 x2 x3 x4 a b and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
 7. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
 8. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'25 x1 x2 x3 x4 a) s proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?P44 x1 x2 x3 x4 a context) (?P'39 x1 x2 x3 x4 a (map context msg_registers)) (mapM (load_word_offs a) (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else [])) (mapM (\<lambda>x. loadWordUser (a + word_of_nat x * word_of_nat wordSize)) [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)])
 2. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 3. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 4. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 5. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. ?P44 x1 x2 x3 x4 a b and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 6. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. ?P'39 x1 x2 x3 x4 a b and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
 7. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
 8. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'25 x1 x2 x3 x4 a) s proof (prove)
goal (14 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x1 x2 x3 x4 a context rv' x xs y ys. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; xs = ys; x = y\<rbrakk> \<Longrightarrow> x # xs = y # ys
 3. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> corres (=) (?P44 x1 x2 x3 x4 a context) (?P'39 x1 x2 x3 x4 a (map context msg_registers)) (load_word_offs a x) (loadWordUser (a + word_of_nat y * word_of_nat wordSize))
 4. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P44 x1 x2 x3 x4 a context\<rbrace> load_word_offs a x \<lbrace>\<lambda>rv. ?P44 x1 x2 x3 x4 a context\<rbrace>
 5. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P'39 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> loadWordUser (a + word_of_nat y * word_of_nat wordSize) \<lbrace>\<lambda>rv. ?P'39 x1 x2 x3 x4 a (map context msg_registers)\<rbrace>
 6. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> length (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) = length [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]
 7. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> set (zip (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]) \<subseteq> {a. fst a = snd a \<and> fst a < unat max_ipc_words}
 8. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 9. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 10. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv' x xs y ys. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; xs = ys; x = y\<rbrakk> \<Longrightarrow> x # xs = y # ys
 2. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> corres (=) (?P44 x1 x2 x3 x4 a context) (?P'39 x1 x2 x3 x4 a (map context msg_registers)) (load_word_offs a x) (loadWordUser (a + word_of_nat y * word_of_nat wordSize))
 3. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P44 x1 x2 x3 x4 a context\<rbrace> load_word_offs a x \<lbrace>\<lambda>rv. ?P44 x1 x2 x3 x4 a context\<rbrace>
 4. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P'39 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> loadWordUser (a + word_of_nat y * word_of_nat wordSize) \<lbrace>\<lambda>rv. ?P'39 x1 x2 x3 x4 a (map context msg_registers)\<rbrace>
 5. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> length (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) = length [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]
 6. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> set (zip (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]) \<subseteq> {a. fst a = snd a \<and> fst a < unat max_ipc_words}
 7. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 8. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 9. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 10. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. ?P44 x1 x2 x3 x4 a b and ?Q42 x1 x2 x3 x4 a b\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> corres (=) (?P44 x1 x2 x3 x4 a context) (?P'39 x1 x2 x3 x4 a (map context msg_registers)) (load_word_offs a x) (loadWordUser (a + word_of_nat y * word_of_nat wordSize))
 2. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P44 x1 x2 x3 x4 a context\<rbrace> load_word_offs a x \<lbrace>\<lambda>rv. ?P44 x1 x2 x3 x4 a context\<rbrace>
 3. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P'39 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> loadWordUser (a + word_of_nat y * word_of_nat wordSize) \<lbrace>\<lambda>rv. ?P'39 x1 x2 x3 x4 a (map context msg_registers)\<rbrace>
 4. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> length (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) = length [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]
 5. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> set (zip (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]) \<subseteq> {a. fst a = snd a \<and> fst a < unat max_ipc_words}
 6. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 7. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 8. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 9. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. ?P44 x1 x2 x3 x4 a b and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 10. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. ?P'39 x1 x2 x3 x4 a b and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv' x. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> corres (=) (?P44 x1 x2 x3 x4 a context) (?P'39 x1 x2 x3 x4 a (map context msg_registers)) (load_word_offs a x) (loadWordUser (a + word_of_nat x * 4))
 2. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P44 x1 x2 x3 x4 a context\<rbrace> load_word_offs a x \<lbrace>\<lambda>rv. ?P44 x1 x2 x3 x4 a context\<rbrace>
 3. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>?P'39 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> loadWordUser (a + word_of_nat y * word_of_nat wordSize) \<lbrace>\<lambda>rv. ?P'39 x1 x2 x3 x4 a (map context msg_registers)\<rbrace>
 4. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> length (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) = length [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]
 5. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> set (zip (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]) \<subseteq> {a. fst a = snd a \<and> fst a < unat max_ipc_words}
 6. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 7. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 8. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 9. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. ?P44 x1 x2 x3 x4 a b and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 10. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. ?P'39 x1 x2 x3 x4 a b and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv' x. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; x < unat max_ipc_words\<rbrakk> \<Longrightarrow> x < unat max_ipc_words
 2. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> load_word_offs a x \<lbrace>\<lambda>rv a. True\<rbrace>
 3. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>valid_ipc_buffer_ptr' a\<rbrace> loadWordUser (a + word_of_nat y * word_of_nat wordSize) \<lbrace>\<lambda>rv. valid_ipc_buffer_ptr' a\<rbrace>
 4. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> length (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) = length [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]
 5. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> set (zip (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]) \<subseteq> {a. fst a = snd a \<and> fst a < unat max_ipc_words}
 6. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 7. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 8. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 9. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. (\<lambda>a. True) and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 10. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. valid_ipc_buffer_ptr' a and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> load_word_offs a x \<lbrace>\<lambda>rv a. True\<rbrace>
 2. \<And>x1 x2 x3 x4 a context rv' x y. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers; (x, y) \<in> {a. fst a = snd a \<and> fst a < unat max_ipc_words}\<rbrakk> \<Longrightarrow> \<lbrace>valid_ipc_buffer_ptr' a\<rbrace> loadWordUser (a + word_of_nat y * word_of_nat wordSize) \<lbrace>\<lambda>rv. valid_ipc_buffer_ptr' a\<rbrace>
 3. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> length (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) = length [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]
 4. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> set (zip (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]) \<subseteq> {a. fst a = snd a \<and> fst a < unat max_ipc_words}
 5. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 6. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 7. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 8. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. (\<lambda>a. True) and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 9. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. valid_ipc_buffer_ptr' a and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
 10. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> length (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) = length [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]
 2. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> set (zip (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]) \<subseteq> {a. fst a = snd a \<and> fst a < unat max_ipc_words}
 3. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 4. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 5. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 6. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. (\<lambda>a. True) and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 7. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. valid_ipc_buffer_ptr' a and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
 8. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
 9. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'25 x1 x2 x3 x4 a) s proof (prove)
goal (9 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> (length msg_registers \<le> 119 \<longrightarrow> Suc (119 - length msg_registers) = 121 - unat (1 + word_of_nat (length TCB_H.msgRegisters))) \<and> (\<not> length msg_registers \<le> 119 \<longrightarrow> 121 \<le> unat (1 + word_of_nat (length TCB_H.msgRegisters)))
 2. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> set (zip (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]) \<subseteq> {a. fst a = snd a \<and> fst a < unat max_ipc_words}
 3. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 4. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 5. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 6. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. (\<lambda>a. True) and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 7. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. valid_ipc_buffer_ptr' a and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
 8. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
 9. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'25 x1 x2 x3 x4 a) s proof (prove)
goal (9 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context [R2, R3, R4, R5]\<rbrakk> \<Longrightarrow> (length [R2, R3, R4, R5] \<le> 119 \<longrightarrow> Suc (119 - length [R2, R3, R4, R5]) = 121 - unat (1 + word_of_nat (length (map Register [R2, R3, R4, R5])))) \<and> (\<not> length [R2, R3, R4, R5] \<le> 119 \<longrightarrow> 121 \<le> unat (1 + word_of_nat (length (map Register [R2, R3, R4, R5]))))
 2. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> set (zip (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]) \<subseteq> {a. fst a = snd a \<and> fst a < unat max_ipc_words}
 3. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 4. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 5. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 6. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. (\<lambda>a. True) and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 7. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. valid_ipc_buffer_ptr' a and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
 8. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
 9. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'25 x1 x2 x3 x4 a) s proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> set (zip (if Suc (length msg_registers) \<le> 120 then [Suc (length msg_registers)..<120] @ [120] else []) [unat (1 + word_of_nat (length TCB_H.msgRegisters))..<Suc (unat 0x78)]) \<subseteq> {a. fst a = snd a \<and> fst a < unat max_ipc_words}
 2. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 3. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 4. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 5. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. (\<lambda>a. True) and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 6. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. valid_ipc_buffer_ptr' a and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
 7. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
 8. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'25 x1 x2 x3 x4 a) s proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 x3 x4 a i. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; length msg_registers \<le> 119; i < Suc (119 - length msg_registers); i < 121 - unat (1 + word_of_nat (length TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> ([Suc (length msg_registers)..<120] @ [120]) ! i = unat (1 + word_of_nat (length TCB_H.msgRegisters)) + i \<and> ([Suc (length msg_registers)..<120] @ [120]) ! i < unat max_ipc_words
 2. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 3. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 4. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 5. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. (\<lambda>a. True) and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 6. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. valid_ipc_buffer_ptr' a and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
 7. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
 8. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'25 x1 x2 x3 x4 a) s proof (prove)
goal (7 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv' rv. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> corres (=) (?R29 x1 x2 x3 x4 a context rv' rv) (?R'29 x1 x2 x3 x4 a context rv' rv) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length msg_registers) rv)) (return (take (unat x1) (map context msg_registers) @ take (unat x1 - length (map context msg_registers)) rv))
 2. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>?R29 x1 x2 x3 x4 a context rv'\<rbrace>
 3. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>?R'29 x1 x2 x3 x4 a context rv'\<rbrace>
 4. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. (\<lambda>a. True) and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 5. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. valid_ipc_buffer_ptr' a and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
 6. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
 7. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'25 x1 x2 x3 x4 a) s proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 x1 x2 x3 x4 a context\<rbrace> mapM (load_word_offs a) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>x1 x2 x3 x4 a context rv'. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; rv' = map context msg_registers\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 x1 x2 x3 x4 a (map context msg_registers)\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 x1 x2 x3 x4 a\<rbrace> thread_get (arch_tcb_get_registers \<circ> tcb_arch) t \<lbrace>\<lambda>b. (\<lambda>a. True) and ?Q42 x1 x2 x3 x4 a b\<rbrace>
 4. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x1 x2 x3 x4 a\<rbrace> asUser t (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>b. valid_ipc_buffer_ptr' a and ?Q'37 x1 x2 x3 x4 a b\<rbrace>
 5. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q25 x1 x2 x3 x4 a) s
 6. \<And>x1 x2 x3 x4 a s. \<lbrakk>mi = Structures_A.message_info.MI x1 x2 x3 x4; buf = Some a; (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'25 x1 x2 x3 x4 a) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres (=) (tcb_at t) (tcb_at' t and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (get_mrs t buf mi) (getMRs t buf (message_info_map mi))

goal:
No subgoals!