theory Ipc_C

lemma copyMRsFault_ccorres_exception:
  "ccorres dc xfdc
           (valid_pspace'
             and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) ARM_H.exceptionMessage = msg) sender
             and K (length msg = 3)
             and K (recvBuffer \<noteq> Some 0)
             and K (sender \<noteq> receiver))
           (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace>
                 \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace>
                 \<inter> \<lbrace>\<acute>receiveIPCBuffer = Ptr (option_to_0 recvBuffer)\<rbrace>
                 \<inter> \<lbrace> \<acute>length___unsigned_long = 3 \<rbrace>
                 \<inter> \<lbrace> \<acute>id___anonymous_enum = MessageID_Exception \<rbrace>)
           hs
           (mapM_x (\<lambda>(x, y). setMR receiver recvBuffer x y) (zip [0..<120] msg))
           (Call copyMRsFault_'proc)" apply (unfold K_def) apply (intro ccorres_gen_asm) apply (cinit' lift: sender_' receiver_' receiveIPCBuffer_'
                     length___unsigned_long_' id___anonymous_enum_'
                simp: whileAnno_def) apply (simp only: mapM_x_append[where xs="take (unat n_msgRegisters) (zip as bs)"
                                         and ys="drop (unat n_msgRegisters) (zip as bs)"
                                         for as bs, simplified] bind_assoc) apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg) apply (rule_tac F="K $ obj_at' (\<lambda>tcb. map ((atcbContext o tcbArch) tcb) ARM_H.exceptionMessage = msg) sender"
                     in ccorres_mapM_x_while) apply (clarsimp simp: n_msgRegisters_def) apply (rule ccorres_guard_imp2) apply (rule_tac t=sender and r="ARM_H.exceptionMessage ! n"
                            in ccorres_add_getRegister) apply (ctac(no_vcg)) apply (rule_tac P="\<lambda>s. rv = msg ! n" in ccorres_cross_over_guard) apply (simp add: setMR_def length_msgRegisters n_msgRegisters_def
                                    liftM_def[symmetric]) apply ctac apply (wp user_getreg_rv) apply (clarsimp simp: msgRegisters_ccorres n_msgRegisters_def
                                 syscallMessage_ccorres n_syscallMessage_def
                                 obj_at'_def projectKOs
                                 atcbContextGet_def unat_of_nat32[unfolded word_bits_def]) apply (clarsimp simp: exceptionMessage_ccorres[simplified,symmetric,OF exceptionMessage_length_aux]) apply (clarsimp simp: word_of_nat_less MessageID_Exception_def) apply (clarsimp simp: n_msgRegisters_def foo) apply (rule allI, rule conseqPre, vcg exspec=setRegister_modifies exspec=getRegister_modifies) apply simp apply (simp add: setMR_def) apply (rule hoare_pre) apply (wp asUser_obj_at_elsewhere | wpc)+ apply simp apply (simp add: word_bits_def) apply ceqv apply (rule ccorres_Cond_rhs) apply (simp del: Collect_const) apply (simp add: n_msgRegisters_def mapM_x_Nil) apply (subst ccorres_expand_while_iff[symmetric]) apply (rule ccorres_cond_false) apply (rule ccorres_return_Skip') apply (simp add: n_msgRegisters_def mapM_x_Nil) apply (rule ccorres_return_Skip') apply wp apply (simp add: guard_is_UNIV_def) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender and K (length msg = 3) and K (recvBuffer \<noteq> Some 0) and K (sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer)\<rbrace> \<inter> \<lbrace>\<acute>length___unsigned_long = 3\<rbrace> \<inter> \<lbrace>\<acute>id___anonymous_enum = MessageID_Exception\<rbrace>) hs (mapM_x (\<lambda>(x, y). setMR receiver recvBuffer x y) (zip [0..<120] msg)) (Call copyMRsFault_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender and (\<lambda>y. length msg = 3) and (\<lambda>y. recvBuffer \<noteq> Some 0) and (\<lambda>y. sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer)\<rbrace> \<inter> \<lbrace>\<acute>length___unsigned_long = 3\<rbrace> \<inter> \<lbrace>\<acute>id___anonymous_enum = MessageID_Exception\<rbrace>) hs (mapM_x (\<lambda>(x, y). setMR receiver recvBuffer x y) (zip [0..<120] msg)) (Call copyMRsFault_'proc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3\<rbrakk> \<Longrightarrow> ccorres dc xfdc (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer)\<rbrace> \<inter> \<lbrace>\<acute>length___unsigned_long = 3\<rbrace> \<inter> \<lbrace>\<acute>id___anonymous_enum = MessageID_Exception\<rbrace>) hs (mapM_x (\<lambda>(x, y). setMR receiver recvBuffer x y) (zip [0..<120] msg)) (Call copyMRsFault_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1369 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) (?Q'1369 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) (SKIP # hs) (mapM_x (\<lambda>(x, y). setMR receiver recvBuffer x y) (zip [0..<120] msg)) (\<acute>i :== 0;;
(While \<lbrace>\<acute>i < (if length___unsigned_long < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then length___unsigned_long else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>id___anonymous_enum <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s id___anonymous_enum\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(sendera,kernel_all_global_addresses.fault_messages.[unat id___anonymous_enum].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(receivera,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long));;
\<acute>i :== \<acute>i + 1);;
IF receiveIPCBuffer \<noteq> NULL THEN
  While \<lbrace>\<acute>i < length___unsigned_long\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>id___anonymous_enum <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s id___anonymous_enum\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(sendera,kernel_all_global_addresses.fault_messages.[unat id___anonymous_enum].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion receiveIPCBuffer (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (receiveIPCBuffer +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion receiveIPCBuffer (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (receiveIPCBuffer +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI))
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1369 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s \<and> s' \<in> ?Q'1369 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera proof (prove)
goal (2 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1369 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)) (?Q'1369 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)) (SKIP # hs) (do y <- mapM_x (\<lambda>(x, y). setMR receiver recvBuffer x y) (take (unat n_msgRegisters) (zip [0..<120] msg));
mapM_x (\<lambda>(x, y). setMR receiver recvBuffer x y) (drop (unat n_msgRegisters) (zip [0..<120] msg))
od) (\<acute>i :== 0;;
(While \<lbrace>\<acute>i < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long));;
\<acute>i :== \<acute>i + 1);;
IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI))
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1369 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s \<and> s' \<in> ?Q'1369 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera proof (prove)
goal (6 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ccorres (?r'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) (?xf'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) (?P1385 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)) (?Q'1369 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)) [] (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg))) (\<acute>i :== 0;;
While \<lbrace>\<acute>i < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long));;
\<acute>i :== \<acute>i + 1))
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ?r'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (?r'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) (?xf'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P1385 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> ?Q'1369 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera proof (prove)
goal (10 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>n<length (take (unat n_msgRegisters) (zip [0..<120] msg)). ccorres dc xfdc ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n) \<lbrace>\<acute>i = word_of_nat n\<rbrace> [] (case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)))
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 10. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (10 subgoals):
 1. \<And>n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3\<rbrakk> \<Longrightarrow> ccorres dc xfdc (obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) \<lbrace>\<acute>i = word_of_nat n\<rbrace> [] (setMR receiver recvBuffer n (msg ! n)) (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds (if MessageID_Exception <s 2 then UNIV else {}) (Guard ArrayBounds (if 0 \<le>s MessageID_Exception then UNIV else {}) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)))
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 10. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (11 subgoals):
 1. \<And>n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1403 n) (?Q'1403 n) [] (setMR receiver recvBuffer n (msg ! n)) (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds (if MessageID_Exception <s 2 then UNIV else {}) (Guard ArrayBounds (if 0 \<le>s MessageID_Exception then UNIV else {}) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)))
 2. \<And>n s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3; (s, s') \<in> rf_sr; obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ?Q1403 n s \<and> s' \<in> ?Q'1403 n
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 10. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1406 n) (?Q'1403 n) [] (do _ <- asUser sender (getRegister (FaultHandler_H.exceptionMessage ! n));
setMR receiver recvBuffer n (msg ! n)
od) (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds (if MessageID_Exception <s 2 then UNIV else {}) (Guard ArrayBounds (if 0 \<le>s MessageID_Exception then UNIV else {}) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)))
 2. \<And>n s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3; (s, s') \<in> rf_sr; obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> (?P1406 n and tcb_at' sender) s \<and> s' \<in> ?Q'1403 n
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 10. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>n rv ret__unsigned_long. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3; rv = ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1412 n rv) (?Q'1412 n rv ret__unsigned_long) [] (setMR receiver recvBuffer n (msg ! n)) (Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],ret__unsigned_long)))
 2. \<And>n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3\<rbrakk> \<Longrightarrow> \<lbrace>?R1412 n\<rbrace> asUser sender (getRegister (FaultHandler_H.exceptionMessage ! n)) \<lbrace>?Q1412 n\<rbrace>
 3. \<And>n s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3; (s, s') \<in> rf_sr; obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R1412 n and tcb_at' sender) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (FaultHandler_H.exceptionMessage ! n)\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'1412 n rv (ret__unsigned_long_' t)} \<inter> (if 0 \<le>s MessageID_Exception then UNIV else {}) \<inter> (if MessageID_Exception <s 2 then UNIV else {}) \<inter> \<lbrace>\<acute>i < 0xC\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 10. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>n rv ret__unsigned_long. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3; rv = ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P'1457 n rv) (?Q1455 n rv ret__unsigned_long) [] (setMR receiver recvBuffer n (msg ! n)) (Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],ret__unsigned_long)))
 2. \<And>n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3\<rbrakk> \<Longrightarrow> \<lbrace>?R1412 n\<rbrace> asUser sender (getRegister (FaultHandler_H.exceptionMessage ! n)) \<lbrace>\<lambda>rv. (\<lambda>s. rv = msg ! n) and ?P'1457 n rv\<rbrace>
 3. \<And>n s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3; (s, s') \<in> rf_sr; obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R1412 n and tcb_at' sender) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (FaultHandler_H.exceptionMessage ! n)\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> rv = msg ! n \<longrightarrow> s' \<in> ?Q1455 n rv (ret__unsigned_long_' t)}} \<inter> (if 0 \<le>s MessageID_Exception then UNIV else {}) \<inter> (if MessageID_Exception <s 2 then UNIV else {}) \<inter> \<lbrace>\<acute>i < 0xC\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 10. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>n rv ret__unsigned_long. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3; rv = ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P'1457 n ret__unsigned_long) (?Q1455 n ret__unsigned_long ret__unsigned_long) [] (asUser receiver (setRegister (TCB_H.msgRegisters ! n) (msg ! n))) (Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],ret__unsigned_long)))
 2. \<And>n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3\<rbrakk> \<Longrightarrow> \<lbrace>?R1412 n\<rbrace> asUser sender (getRegister (FaultHandler_H.exceptionMessage ! n)) \<lbrace>\<lambda>rv. (\<lambda>s. rv = msg ! n) and ?P'1457 n rv\<rbrace>
 3. \<And>n s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3; (s, s') \<in> rf_sr; obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R1412 n and tcb_at' sender) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (FaultHandler_H.exceptionMessage ! n)\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> rv = msg ! n \<longrightarrow> s' \<in> ?Q1455 n rv (ret__unsigned_long_' t)}} \<inter> (if 0 \<le>s MessageID_Exception then UNIV else {}) \<inter> (if MessageID_Exception <s 2 then UNIV else {}) \<inter> \<lbrace>\<acute>i < 0xC\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 10. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3\<rbrakk> \<Longrightarrow> \<lbrace>?R1412 n\<rbrace> asUser sender (getRegister (FaultHandler_H.exceptionMessage ! n)) \<lbrace>\<lambda>rv. (\<lambda>s. rv = msg ! n) and (\<lambda>a. True)\<rbrace>
 2. \<And>n s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3; (s, s') \<in> rf_sr; obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R1412 n and tcb_at' sender) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (FaultHandler_H.exceptionMessage ! n)\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> rv = msg ! n \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. ret__unsigned_long_' t) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! n)\<rbrace> \<inter> \<lbrace>\<acute>w = msg ! n\<rbrace>} \<inter> \<lbrace>\<acute>i < 4\<rbrace>}} \<inter> (if 0 \<le>s MessageID_Exception then UNIV else {}) \<inter> (if MessageID_Exception <s 2 then UNIV else {}) \<inter> \<lbrace>\<acute>i < 0xC\<rbrace>
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 10. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>n s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; n < 3; (s, s') \<in> rf_sr; obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and obj_at' (\<lambda>tcb. (atcbContextGet \<circ> tcbArch) tcb (FaultHandler_H.exceptionMessage ! n) = msg ! n \<and> True) sender and tcb_at' sender) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (FaultHandler_H.exceptionMessage ! n)\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> rv = msg ! n \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. ret__unsigned_long_' t) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! n)\<rbrace> \<inter> \<lbrace>\<acute>w = msg ! n\<rbrace>} \<inter> \<lbrace>\<acute>i < 4\<rbrace>}} \<inter> (if 0 \<le>s MessageID_Exception then UNIV else {}) \<inter> (if MessageID_Exception <s 2 then UNIV else {}) \<inter> \<lbrace>\<acute>i < 0xC\<rbrace>
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 10. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (10 subgoals):
 1. \<And>n s s' obj. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length FaultHandler_H.exceptionMessage = 3; n < 3; (s, s') \<in> rf_sr; i_' s' = word_of_nat n; ksPSpace s sender = Some (KOTCB obj); is_aligned sender (objBitsKO (KOTCB obj)); ps_clear sender (objBitsKO (KOTCB obj)) s; msg = map (atcbContext (tcbArch obj)) FaultHandler_H.exceptionMessage\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[n] = register_from_H (FaultHandler_H.exceptionMessage ! n) \<and> ((\<exists>t. (\<exists>s. (s, s'\<lparr>globals := globals t\<rparr>) \<in> rf_sr) \<and> ret__unsigned_long_' t = atcbContext (tcbArch obj) (FaultHandler_H.exceptionMessage ! n)) \<longrightarrow> word_of_nat n < 4) \<and> s' \<in> (if 0 \<le>s MessageID_Exception then UNIV else {}) \<and> s' \<in> (if MessageID_Exception <s 2 then UNIV else {}) \<and> word_of_nat n < 0xC
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 10. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (10 subgoals):
 1. \<And>n s s' obj. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length FaultHandler_H.exceptionMessage = 3; n < 3; (s, s') \<in> rf_sr; i_' s' = word_of_nat n; ksPSpace s sender = Some (KOTCB obj); is_aligned sender (objBitsKO (KOTCB obj)); ps_clear sender (objBitsKO (KOTCB obj)) s; msg = map (atcbContext (tcbArch obj)) FaultHandler_H.exceptionMessage\<rbrakk> \<Longrightarrow> ((\<exists>t. (\<exists>s. (s, s'\<lparr>globals := globals t\<rparr>) \<in> rf_sr) \<and> ret__unsigned_long_' t = atcbContext (tcbArch obj) (FaultHandler_H.exceptionMessage ! n)) \<longrightarrow> word_of_nat n < 4) \<and> s' \<in> (if 0 \<le>s MessageID_Exception then UNIV else {}) \<and> s' \<in> (if MessageID_Exception <s 2 then UNIV else {}) \<and> word_of_nat n < 0xC
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 10. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (9 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> (n < (if 3 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters then 3 else SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = (n < word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))))
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 9. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> {s} \<subseteq> \<lbrace>\<acute>i < 0xC \<longrightarrow> MessageID_Exception <s 2 \<longrightarrow> 0 \<le>s MessageID_Exception \<longrightarrow> \<acute>i < 4 \<longrightarrow> \<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; Suc n < length (take (unat n_msgRegisters) (zip [0..<120] msg))\<rbrakk> \<Longrightarrow> \<lbrace>(K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) n\<rbrace> case take (unat n_msgRegisters) (zip [0..<120] msg) ! n of (a, b) \<Rightarrow> setMR receiver recvBuffer a b \<lbrace>\<lambda>_. (K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) (Suc n)\<rbrace>
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; n < 2 \<and> Suc n < unat n_msgRegisters\<rbrakk> \<Longrightarrow> \<lbrace>obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender\<rbrace> if n < length TCB_H.msgRegisters then do asUser receiver (setRegister (TCB_H.msgRegisters ! n) (msg ! n));
return (n + 1)
od else case recvBuffer of None \<Rightarrow> return (length TCB_H.msgRegisters) | Some buf \<Rightarrow> do storeWordUser (buf + word_of_nat (n + 1) * word_size) (msg ! n);
return (n + 1)
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender\<rbrace>
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; n < 2 \<and> Suc n < unat n_msgRegisters\<rbrakk> \<Longrightarrow> \<lbrace>?Q1574 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n\<rbrace> if n < length TCB_H.msgRegisters then do asUser receiver (setRegister (TCB_H.msgRegisters ! n) (msg ! n));
return (n + 1)
od else case recvBuffer of None \<Rightarrow> return (length TCB_H.msgRegisters) | Some buf \<Rightarrow> do storeWordUser (buf + word_of_nat (n + 1) * word_size) (msg ! n);
return (n + 1)
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender\<rbrace>
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n s. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; n < 2 \<and> Suc n < unat n_msgRegisters; obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender s\<rbrakk> \<Longrightarrow> ?Q1574 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n s
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 8. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera n s. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; n < 2 \<and> Suc n < unat n_msgRegisters; obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender s\<rbrakk> \<Longrightarrow> (n < length TCB_H.msgRegisters \<longrightarrow> (obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender and (\<lambda>_. receiver \<noteq> sender)) s) \<and> (\<not> n < length TCB_H.msgRegisters \<longrightarrow> (recvBuffer = None \<longrightarrow> obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender s) \<and> (\<forall>x. recvBuffer = Some x \<longrightarrow> obj_at' (\<lambda>a. map (atcbContext (tcbArch a)) FaultHandler_H.exceptionMessage = msg) sender s))
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 7. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> length (take (unat n_msgRegisters) (zip [0..<120] msg)) < 2 ^ word_bits
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 6. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv' t t'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> i_' rv' t t' (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (?d'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv')
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (IF PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL THEN
  While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI)
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>?Q1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera\<rbrace>
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (?Q'1379 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera)
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))); PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1732 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?S1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (i_' s + 1))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer) +\<^sub>p uint (\<acute>i + 1)) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1))
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))); \<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) SKIP
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>\<lambda>rv s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?Q1732 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s)\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (\<lambda>rv rv'. {s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?S1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv')})
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (min 3 (unat n_msgRegisters)); option_to_0 recvBuffer \<noteq> 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1732 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) ()) (?S1730 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () (word_of_nat (min 3 (unat n_msgRegisters)))) (SKIP # hs) (mapM_x (\<lambda>(x, y). setMR receiver recvBuffer x y) (drop (unat n_msgRegisters) (zip [0..<120] msg))) (While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds \<lbrace>MessageID_Exception <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s MessageID_Exception\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c PTR(32 word) (option_to_0 recvBuffer + (i_' s * 4 + 4))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer + (\<acute>i * 4 + 4))) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1))
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))); \<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) SKIP
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>\<lambda>rv s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?Q1732 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s)\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (\<lambda>rv rv'. {s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?S1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv')})
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = 3; option_to_0 recvBuffer \<noteq> 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1732 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) ()) (?S1730 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () 3) (SKIP # hs) (return ()) (While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds (if MessageID_Exception <s 2 then UNIV else {}) (Guard ArrayBounds (if 0 \<le>s MessageID_Exception then UNIV else {}) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c PTR(32 word) (option_to_0 recvBuffer + (i_' s * 4 + 4))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer + (\<acute>i * 4 + 4))) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1))
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))); \<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) SKIP
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>\<lambda>rv s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?Q1732 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s)\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (\<lambda>rv rv'. {s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?S1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv')})
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = 3; option_to_0 recvBuffer \<noteq> 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1747 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) ()) (?S1748 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () 3) (SKIP # hs) (return ()) (IF \<acute>i < 3 THEN
  Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds (if MessageID_Exception <s 2 then UNIV else {}) (Guard ArrayBounds (if 0 \<le>s MessageID_Exception then UNIV else {}) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c PTR(32 word) (option_to_0 recvBuffer + (i_' s * 4 + 4))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer + (\<acute>i * 4 + 4))) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1;;
While \<lbrace>\<acute>i < 3\<rbrace> (Guard ArrayBounds \<lbrace>\<acute>i < 0xC\<rbrace> (Guard ArrayBounds (if MessageID_Exception <s 2 then UNIV else {}) (Guard ArrayBounds (if 0 \<le>s MessageID_Exception then UNIV else {}) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[unat \<acute>i]))));;
Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (unat (\<acute>i + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c PTR(32 word) (option_to_0 recvBuffer + (i_' s * 4 + 4))} (Guard MemorySafety \<lbrace>\<acute>i + 1 = 0 \<or> array_assertion (PTR(32 word) (option_to_0 recvBuffer)) (Suc (unat (\<acute>i + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (option_to_0 recvBuffer + (\<acute>i * 4 + 4))) \<acute>ret__unsigned_long)))));;
\<acute>i :== \<acute>i + 1)
FI)
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))); \<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) SKIP
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>\<lambda>rv s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?Q1732 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s)\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (\<lambda>rv rv'. {s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?S1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv')})
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV
flex-flex pairs:
?S1748 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () 3 \<equiv>\<^sup>? ?S1730 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () 3
?Q1747 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () \<equiv>\<^sup>? ?Q1732 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () proof (prove)
goal (5 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = 3; option_to_0 recvBuffer \<noteq> 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1747 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) ()) (?R'1751 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () 3) (SKIP # hs) (return ()) SKIP
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))); \<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) SKIP
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>\<lambda>rv s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?Q1732 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s)\<rbrace>
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (\<lambda>rv rv'. {s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?R'1752 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv' \<inter> - \<lbrace>\<acute>i < rv'\<rbrace>) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv')})
 5. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV
flex-flex pairs:
?R'1752 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () 3 \<equiv>\<^sup>? ?R'1751 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () 3
?Q1747 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () \<equiv>\<^sup>? ?Q1732 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () proof (prove)
goal (4 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg))); \<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv) (?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv') (SKIP # hs) (mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (drop (unat n_msgRegisters) (zip [0..<120] msg))) SKIP
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>\<lambda>rv s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> True) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s)\<rbrace>
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (\<lambda>rv rv'. {s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)} \<inter> - \<lbrace>\<acute>i < rv'\<rbrace>) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv')})
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = NULL; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; rv' = 3; option_to_0 recvBuffer = 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1734 MessageID_Exception 3 NULL (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) ()) (?T1730 MessageID_Exception 3 NULL (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) () 3) (SKIP # hs) (return ()) SKIP
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>\<lambda>rv s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> True) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> ?R1734 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv s)\<rbrace>
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (\<lambda>rv rv'. {s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)} \<inter> - \<lbrace>\<acute>i < rv'\<rbrace>) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> ?T1730 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera rv rv')})
 4. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (3 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1383 MessageID_Exception 3 (PTR(32 word) (option_to_0 recvBuffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> mapM_x (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver recvBuffer a b) (take (unat n_msgRegisters) (zip [0..<120] msg)) \<lbrace>\<lambda>rv s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> True) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> True)\<rbrace>
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (\<lambda>rv rv'. {s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)} \<inter> - \<lbrace>\<acute>i < rv'\<rbrace>) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)})})
 3. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and ?R1383 id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera) s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = word_of_nat (length (take (unat n_msgRegisters) (zip [0..<120] msg)))) i_' (\<lambda>rv rv'. {s. (PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)} \<inter> - \<lbrace>\<acute>i < rv'\<rbrace>) \<and> (\<not> PTR(32 word) (option_to_0 recvBuffer) \<noteq> NULL \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)})})
 2. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and (\<lambda>a. (receiveIPCBuffer \<noteq> NULL \<longrightarrow> True) \<and> (\<not> receiveIPCBuffer \<noteq> NULL \<longrightarrow> True))) s \<and> s' \<in> UNIV proof (prove)
goal (1 subgoal):
 1. \<And>id___anonymous_enum length___unsigned_long receiveIPCBuffer receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; recvBuffer \<noteq> Some 0; length msg = 3; id___anonymous_enum = MessageID_Exception; length___unsigned_long = 3; receiveIPCBuffer = PTR(32 word) (option_to_0 recvBuffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and obj_at' (\<lambda>tcb. map (atcbContext (tcbArch tcb)) FaultHandler_H.exceptionMessage = msg) sender) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((K $ obj_at' (\<lambda>tcb. map ((atcbContext \<circ> tcbArch) tcb) FaultHandler_H.exceptionMessage = msg) sender) 0 and (\<lambda>a. (receiveIPCBuffer \<noteq> NULL \<longrightarrow> True) \<and> (\<not> receiveIPCBuffer \<noteq> NULL \<longrightarrow> True))) s \<and> s' \<in> UNIV proof (prove)
goal:
No subgoals!