theory Ipc_C

lemma replyFromKernel_error_ccorres [corres]:
  "ccorres dc xfdc (valid_pspace' and tcb_at' thread)
     (UNIV \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error
                          (lookup_fault_lift \<acute>current_lookup_fault)
                       = Some err\<rbrace>
           \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs
     (replyFromKernel thread (msgFromSyscallError err))
     (Call replyFromKernel_error_'proc)" apply (cinit lift: thread_') apply clarsimp apply wpc apply (ctac add: lookupIPCBuffer_ccorres) apply simp apply ctac apply (ctac add: setMRs_syscall_error_ccorres[where err=err]) apply ((rule ccorres_Guard_Seq)+)? apply csymbr apply (rule ccorres_abstract_cleanup) apply (rule setMessageInfo_ccorres) apply wp apply (simp add: Collect_const_mem) apply (vcg exspec=setMRs_syscall_error_modifies) apply (wp hoare_case_option_wp) apply (vcg exspec=setRegister_modifies) apply simp apply (wp) apply (simp del: Collect_const) apply (vcg exspec=lookupIPCBuffer_modifies) apply (simp add: msgInfoRegister_def
                   Kernel_C.msgInfoRegister_def Kernel_C.R1_def
                   ARM_H.badgeRegister_def ARM.badgeRegister_def
                   Kernel_C.badgeRegister_def Kernel_C.R0_def
                   message_info_to_H_def valid_pspace_valid_objs') apply (clarsimp simp: msgLengthBits_def msgFromSyscallError_def
                        syscall_error_to_H_def syscall_error_type_defs
                        mask_def option_to_ptr_def
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pspace' and tcb_at' thread) (UNIV \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs (replyFromKernel thread (msgFromSyscallError err)) (Call replyFromKernel_error_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres dc xfdc (?Q217 threada) (?Q'217 threada) (SKIP # hs) (case msgFromSyscallError err of (resultLabel, resultData) \<Rightarrow> do destIPCBuffer <- lookupIPCBuffer True thread;
y <- asUser thread (setRegister Notification_H.badgeRegister 0);
len <- setMRs thread destIPCBuffer resultData;
setMessageInfo thread (Types_H.message_info.MI len 0 0 resultLabel)
od) (\<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,threada);;
(CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0);;
(\<acute>len :== CALL setMRs_syscall_error_'proc(threada,\<acute>ipcBuffer);;
(\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(UCAST(32 \<rightarrow> 32) (type_C \<acute>current_syscall_error),SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,UCAST(32 \<rightarrow> 32) \<acute>len);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long))))))
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> ?Q217 threada s \<and> s' \<in> ?Q'217 threada proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc (?Q217 (tcb_ptr_to_ctcb_ptr thread)) (?Q'217 (tcb_ptr_to_ctcb_ptr thread)) (SKIP # hs) (case msgFromSyscallError err of (resultLabel, resultData) \<Rightarrow> do destIPCBuffer <- lookupIPCBuffer True thread;
y <- asUser thread (setRegister Notification_H.badgeRegister 0);
len <- setMRs thread destIPCBuffer resultData;
setMessageInfo thread (Types_H.message_info.MI len 0 0 resultLabel)
od) (\<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread);;
(CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0);;
(\<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,\<acute>ipcBuffer);;
(\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(type_C \<acute>current_syscall_error,0,0,\<acute>len);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long))))))
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> ?Q217 threada s \<and> s' \<in> ?Q'217 threada proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> ccorres dc xfdc (\<lambda>a. ?R240 (tcb_ptr_to_ctcb_ptr thread) a x1 x2) (?R''241 (tcb_ptr_to_ctcb_ptr thread) x1 x2) (SKIP # hs) (do destIPCBuffer <- lookupIPCBuffer True thread;
y <- asUser thread (setRegister Notification_H.badgeRegister 0);
len <- setMRs thread destIPCBuffer x2;
setMessageInfo thread (Types_H.message_info.MI len 0 0 x1)
od) (\<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread);;
(CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0);;
(\<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,\<acute>ipcBuffer);;
(\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(type_C \<acute>current_syscall_error,0,0,\<acute>len);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long))))))
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> ?R240 threada s x xa) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> ?R''241 threada x xa}}} proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); ((=) \<circ> option_to_ptr) rv ipcBuffer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q246 x1 x2 rv) (?Q'246 x1 x2 rv ipcBuffer) (SKIP # hs) (do y <- asUser thread (setRegister Notification_H.badgeRegister 0);
len <- setMRs thread rv x2;
setMessageInfo thread (Types_H.message_info.MI len 0 0 x1)
od) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0);;
(\<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,ipcBuffer);;
(\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(type_C \<acute>current_syscall_error,0,0,\<acute>len);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long)))))
 2. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>?Q246 x1 x2\<rbrace>
 3. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> ?Q'246 x1 x2 rv (ipcBuffer_' s)}
 4. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q246 x1 x2 rv) (?Q'246 x1 x2 rv ipcBuffer) (SKIP # hs) (do y <- asUser thread (setRegister Notification_H.badgeRegister 0);
len <- setMRs thread rv x2;
setMessageInfo thread (Types_H.message_info.MI len 0 0 x1)
od) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0);;
(\<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,ipcBuffer);;
(\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(type_C \<acute>current_syscall_error,0,0,\<acute>len);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long)))))
 2. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>?Q246 x1 x2\<rbrace>
 3. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> ?Q'246 x1 x2 rv (ipcBuffer_' s)}
 4. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 rv ipcBuffer rva xfdca. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q405 x1 x2 rv ipcBuffer rva) (?Q'405 x1 x2 rv ipcBuffer rva xfdca) (SKIP # hs) (do len <- setMRs thread rv x2;
setMessageInfo thread (Types_H.message_info.MI len 0 0 x1)
od) (\<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,ipcBuffer);;
(\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(type_C \<acute>current_syscall_error,0,0,\<acute>len);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long))))
 2. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<lbrace>?R407 x1 x2 rv\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>?Q405 x1 x2 rv ipcBuffer\<rbrace>
 3. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'405 x1 x2 rv ipcBuffer) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> ?Q'405 x1 x2 rv ipcBuffer rva (xfdc s)}
 4. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?R407 x1 x2 a\<rbrace>
 5. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'405 x1 x2 rv (ipcBuffer_' s)}
 6. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 rv ipcBuffer rva xfdca rvb len. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdca; rvb = len && mask msgLengthBits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q434 x1 x2 rv ipcBuffer rva xfdca rvb) (?Q'434 x1 x2 rv ipcBuffer rva xfdca rvb len) (SKIP # hs) (setMessageInfo thread (Types_H.message_info.MI rvb 0 0 x1)) (\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(type_C \<acute>current_syscall_error,0,0,len);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long)))
 2. \<And>x1 x2 rv ipcBuffer rva xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R436 x1 x2 rv ipcBuffer rva\<rbrace> setMRs thread rv x2 \<lbrace>?Q434 x1 x2 rv ipcBuffer rva xfdc\<rbrace>
 3. \<And>x1 x2 rv ipcBuffer rva xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'434 x1 x2 rv ipcBuffer rva xfdc) \<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,ipcBuffer) {s. \<forall>rvb. rvb = len_' s && mask msgLengthBits \<longrightarrow> s \<in> ?Q'434 x1 x2 rv ipcBuffer rva xfdc rvb (len_' s)}
 4. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<lbrace>?R407 x1 x2 rv\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rva. valid_pspace' and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>_. x2 = snd (msgFromSyscallError err)) and ?R436 x1 x2 rv ipcBuffer rva\<rbrace>
 5. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'405 x1 x2 rv ipcBuffer) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. ipcBuffer) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr rv\<rbrace> \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>} \<inter> ?R'434 x1 x2 rv ipcBuffer rva (xfdc s)}
 6. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?R407 x1 x2 a\<rbrace>
 7. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'405 x1 x2 rv (ipcBuffer_' s)}
 8. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 rv ipcBuffer rva xfdca rvb len. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdca; rvb = len && mask msgLengthBits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q434 x1 x2 rv ipcBuffer rva xfdca rvb) (?Q'434 x1 x2 rv ipcBuffer rva xfdca rvb len) (SKIP # hs) (setMessageInfo thread (Types_H.message_info.MI rvb 0 0 x1)) (\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(type_C \<acute>current_syscall_error,0,0,len);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long)))
 2. \<And>x1 x2 rv ipcBuffer rva xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R436 x1 x2 rv ipcBuffer rva\<rbrace> setMRs thread rv x2 \<lbrace>?Q434 x1 x2 rv ipcBuffer rva xfdc\<rbrace>
 3. \<And>x1 x2 rv ipcBuffer rva xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'434 x1 x2 rv ipcBuffer rva xfdc) \<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,ipcBuffer) {s. \<forall>rvb. rvb = len_' s && mask msgLengthBits \<longrightarrow> s \<in> ?Q'434 x1 x2 rv ipcBuffer rva xfdc rvb (len_' s)}
 4. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<lbrace>?R407 x1 x2 rv\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rva. valid_pspace' and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>_. x2 = snd (msgFromSyscallError err)) and ?R436 x1 x2 rv ipcBuffer rva\<rbrace>
 5. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'405 x1 x2 rv ipcBuffer) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. ipcBuffer) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr rv\<rbrace> \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>} \<inter> ?R'434 x1 x2 rv ipcBuffer rva (xfdc s)}
 6. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?R407 x1 x2 a\<rbrace>
 7. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'405 x1 x2 rv (ipcBuffer_' s)}
 8. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 rv ipcBuffer rva xfdca rvb len ret__struct_seL4_MessageInfo_C. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdca; rvb = len && mask msgLengthBits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q434 x1 x2 rv ipcBuffer rva xfdca rvb) (?G'534 x1 x2 rv ipcBuffer rva xfdca rvb len ret__struct_seL4_MessageInfo_C \<inter> \<lbrace>seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = type_C \<acute>current_syscall_error && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = len && mask 7\<rparr>\<rbrace>) (SKIP # hs) (setMessageInfo thread (Types_H.message_info.MI rvb 0 0 x1)) (\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long))
 2. \<And>x1 x2 rv ipcBuffer rva xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R436 x1 x2 rv ipcBuffer rva\<rbrace> setMRs thread rv x2 \<lbrace>?Q434 x1 x2 rv ipcBuffer rva xfdc\<rbrace>
 3. \<And>x1 x2 rv ipcBuffer rva xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'434 x1 x2 rv ipcBuffer rva xfdc) \<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,ipcBuffer) {s. \<forall>rvb. rvb = len_' s && mask msgLengthBits \<longrightarrow> s \<in> {sa. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 7\<rparr> \<longrightarrow> sa\<lparr>ret__struct_seL4_MessageInfo_C_' := v\<rparr> \<in> ?G'534 x1 x2 rv ipcBuffer rva xfdc rvb (len_' s) v}}
 4. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<lbrace>?R407 x1 x2 rv\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rva. valid_pspace' and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>_. x2 = snd (msgFromSyscallError err)) and ?R436 x1 x2 rv ipcBuffer rva\<rbrace>
 5. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'405 x1 x2 rv ipcBuffer) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. ipcBuffer) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr rv\<rbrace> \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>} \<inter> ?R'434 x1 x2 rv ipcBuffer rva (xfdc s)}
 6. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?R407 x1 x2 a\<rbrace>
 7. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'405 x1 x2 rv (ipcBuffer_' s)}
 8. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 rv ipcBuffer rva xfdca rvb len ret__struct_seL4_MessageInfo_C. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdca; rvb = len && mask msgLengthBits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q434 x1 x2 rv ipcBuffer rva xfdca rvb) (?G'599 x1 x2 rv ipcBuffer rva xfdca rvb len ret__struct_seL4_MessageInfo_C) (SKIP # hs) (setMessageInfo thread (Types_H.message_info.MI rvb 0 0 x1)) (\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long))
 2. \<And>x1 x2 rv ipcBuffer rva xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R436 x1 x2 rv ipcBuffer rva\<rbrace> setMRs thread rv x2 \<lbrace>?Q434 x1 x2 rv ipcBuffer rva xfdc\<rbrace>
 3. \<And>x1 x2 rv ipcBuffer rva xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'434 x1 x2 rv ipcBuffer rva xfdc) \<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,ipcBuffer) {s. \<forall>rvb. rvb = len_' s && mask msgLengthBits \<longrightarrow> s \<in> {sa. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 7\<rparr> \<longrightarrow> sa\<lparr>ret__struct_seL4_MessageInfo_C_' := v\<rparr> \<in> {sa. sa \<in> \<lbrace>seL4_MessageInfo_lift v = \<lparr>label_CL = type_C \<acute>current_syscall_error && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = \<^bsup>s\<^esup>len && mask 7\<rparr>\<rbrace> \<longrightarrow> sa \<in> ?G'599 x1 x2 rv ipcBuffer rva xfdc rvb (len_' s) v}}}
 4. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<lbrace>?R407 x1 x2 rv\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rva. valid_pspace' and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>_. x2 = snd (msgFromSyscallError err)) and ?R436 x1 x2 rv ipcBuffer rva\<rbrace>
 5. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'405 x1 x2 rv ipcBuffer) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. ipcBuffer) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr rv\<rbrace> \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>} \<inter> ?R'434 x1 x2 rv ipcBuffer rva (xfdc s)}
 6. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?R407 x1 x2 a\<rbrace>
 7. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'405 x1 x2 rv (ipcBuffer_' s)}
 8. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (7 subgoals):
 1. \<And>x1 x2 rv ipcBuffer rva xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R436 x1 x2 rv ipcBuffer rva\<rbrace> setMRs thread rv x2 \<lbrace>\<lambda>rvb. tcb_at' thread\<rbrace>
 2. \<And>x1 x2 rv ipcBuffer rva xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'434 x1 x2 rv ipcBuffer rva xfdc) \<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,ipcBuffer) {s. \<forall>rv. rv = len_' s && mask msgLengthBits \<longrightarrow> s \<in> {sa. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 7\<rparr> \<longrightarrow> sa\<lparr>ret__struct_seL4_MessageInfo_C_' := v\<rparr> \<in> {sa. sa \<in> \<lbrace>seL4_MessageInfo_lift v = \<lparr>label_CL = type_C \<acute>current_syscall_error && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = \<^bsup>s\<^esup>len && mask 7\<rparr>\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> \<lbrace>Types_H.message_info.MI rv 0 0 x1 = message_info_to_H v\<rbrace>}}}
 3. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<lbrace>?R407 x1 x2 rv\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rva. valid_pspace' and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>_. x2 = snd (msgFromSyscallError err)) and ?R436 x1 x2 rv ipcBuffer rva\<rbrace>
 4. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'405 x1 x2 rv ipcBuffer) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. ipcBuffer) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr rv\<rbrace> \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>} \<inter> ?R'434 x1 x2 rv ipcBuffer rva (xfdc s)}
 5. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?R407 x1 x2 a\<rbrace>
 6. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'405 x1 x2 rv (ipcBuffer_' s)}
 7. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 rv ipcBuffer rva xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer; dc rva xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'434 x1 x2 rv ipcBuffer rva xfdc) \<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,ipcBuffer) {s. \<forall>rv. rv = len_' s && mask msgLengthBits \<longrightarrow> s \<in> {sa. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. len_' s) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. type_C (current_syscall_error_' (globals sa))) sa)))) && mask 7\<rparr> \<longrightarrow> sa\<lparr>ret__struct_seL4_MessageInfo_C_' := v\<rparr> \<in> {sa. sa \<in> \<lbrace>seL4_MessageInfo_lift v = \<lparr>label_CL = type_C \<acute>current_syscall_error && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = \<^bsup>s\<^esup>len && mask 7\<rparr>\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> \<lbrace>Types_H.message_info.MI rv 0 0 x1 = message_info_to_H v\<rbrace>}}}
 2. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<lbrace>?R407 x1 x2 rv\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rva. valid_pspace' and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>_. x2 = snd (msgFromSyscallError err)) and tcb_at' thread\<rbrace>
 3. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'405 x1 x2 rv ipcBuffer) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. ipcBuffer) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr rv\<rbrace> \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>} \<inter> ?R'434 x1 x2 rv ipcBuffer rva (xfdc s)}
 4. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?R407 x1 x2 a\<rbrace>
 5. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'405 x1 x2 rv (ipcBuffer_' s)}
 6. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 rv ipcBuffer xfdc. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'434 x1 x2 rv ipcBuffer () xfdc) \<acute>len :== CALL setMRs_syscall_error_'proc(tcb_ptr_to_ctcb_ptr thread,ipcBuffer) \<lbrace>\<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = type_C \<acute>current_syscall_error && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = \<acute>len && mask 7\<rparr> \<longrightarrow> Types_H.message_info.MI (\<acute>len && mask msgLengthBits) 0 0 x1 = message_info_to_H v\<rbrace>
 2. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<lbrace>?R407 x1 x2 rv\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rva. valid_pspace' and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>_. x2 = snd (msgFromSyscallError err)) and tcb_at' thread\<rbrace>
 3. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'405 x1 x2 rv ipcBuffer) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. ipcBuffer) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr rv\<rbrace> \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>} \<inter> ?R'434 x1 x2 rv ipcBuffer rva (xfdc s)}
 4. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?R407 x1 x2 a\<rbrace>
 5. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'405 x1 x2 rv (ipcBuffer_' s)}
 6. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<lbrace>?R407 x1 x2 rv\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rva. valid_pspace' and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>_. x2 = snd (msgFromSyscallError err)) and tcb_at' thread\<rbrace>
 2. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'405 x1 x2 rv ipcBuffer) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. ipcBuffer) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr rv\<rbrace> \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>} \<inter> \<lbrace>\<forall>t v. seL4_MessageInfo_lift v = \<lparr>label_CL = type_C \<acute>current_syscall_error && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = \<^bsup>t\<^esup>ret__unsigned_long && mask 7, \<dots> = rva\<rparr> \<longrightarrow> Types_H.message_info.MI (\<^bsup>t\<^esup>ret__unsigned_long && mask msgLengthBits) 0 0 x1 = message_info_to_H v\<rbrace>}
 3. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?R407 x1 x2 a\<rbrace>
 4. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'405 x1 x2 rv (ipcBuffer_' s)}
 5. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 rv ipcBuffer. \<lbrakk>msgFromSyscallError err = (x1, x2); option_to_ptr rv = ipcBuffer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'405 x1 x2 rv ipcBuffer) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,0) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. ipcBuffer) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr rv\<rbrace> \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>} \<inter> \<lbrace>\<forall>t v. seL4_MessageInfo_lift v = \<lparr>label_CL = type_C \<acute>current_syscall_error && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = \<^bsup>t\<^esup>ret__unsigned_long && mask 7, \<dots> = rva\<rparr> \<longrightarrow> Types_H.message_info.MI (\<^bsup>t\<^esup>ret__unsigned_long && mask msgLengthBits) 0 0 x1 = message_info_to_H v\<rbrace>}
 2. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. valid_pspace' s \<and> (case a of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> x2 = snd (msgFromSyscallError err) \<and> tcb_at' thread s)\<rbrace>
 3. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'405 x1 x2 rv (ipcBuffer_' s)}
 4. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. valid_pspace' s \<and> (case a of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> x2 = snd (msgFromSyscallError err) \<and> tcb_at' thread s)\<rbrace>
 2. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> {sa. \<forall>t rva. dc rva (xfdc (sa\<lparr>globals := globals sa\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>)) \<longrightarrow> ipcBuffer_' s = option_to_ptr rv \<and> syscall_error_to_H (current_syscall_error_' (globals sa)) (lookup_fault_lift (current_lookup_fault_' (globals sa))) = Some err \<and> (\<forall>t v. seL4_MessageInfo_lift v = \<lparr>label_CL = type_C (current_syscall_error_' (globals sa)) && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = ret__unsigned_long_' t && mask 7, \<dots> = rva\<rparr> \<longrightarrow> Types_H.message_info.MI (ret__unsigned_long_' t && mask msgLengthBits) 0 0 x1 = message_info_to_H v)}}
 3. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<lbrace>?R253 (tcb_ptr_to_ctcb_ptr thread) x1 x2\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>a aa. valid_pspace' aa \<and> (case a of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) aa \<and> tcb_at' thread aa\<rbrace>
 2. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> {sa. \<forall>t rva. dc rva (xfdc (sa\<lparr>globals := globals sa\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>)) \<longrightarrow> ipcBuffer_' s = option_to_ptr rv \<and> syscall_error_to_H (current_syscall_error_' (globals sa)) (lookup_fault_lift (current_lookup_fault_' (globals sa))) = Some err \<and> (\<forall>t v. seL4_MessageInfo_lift v = \<lparr>label_CL = type_C (current_syscall_error_' (globals sa)) && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = ret__unsigned_long_' t && mask 7, \<dots> = rva\<rparr> \<longrightarrow> Types_H.message_info.MI (ret__unsigned_long_' t && mask msgLengthBits) 0 0 x1 = message_info_to_H v)}}
 3. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and ?R253 threada x xa) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) {s. \<forall>rv. ((=) \<circ> option_to_ptr) rv (ipcBuffer_' s) \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> {sa. \<forall>t rva. dc rva (xfdc (sa\<lparr>globals := globals sa\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>)) \<longrightarrow> ipcBuffer_' s = option_to_ptr rv \<and> syscall_error_to_H (current_syscall_error_' (globals sa)) (lookup_fault_lift (current_lookup_fault_' (globals sa))) = Some err \<and> (\<forall>t v. seL4_MessageInfo_lift v = \<lparr>label_CL = type_C (current_syscall_error_' (globals sa)) && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = ret__unsigned_long_' t && mask 7, \<dots> = rva\<rparr> \<longrightarrow> Types_H.message_info.MI (ret__unsigned_long_' t && mask msgLengthBits) 0 0 x1 = message_info_to_H v)}}
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and (\<lambda>a. valid_pspace' a \<and> valid_objs' a \<and> tcb_at' thread a)) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. msgFromSyscallError err = (x1, x2) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'248 (tcb_ptr_to_ctcb_ptr thread) x1 x2) \<acute>ipcBuffer :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,tcb_ptr_to_ctcb_ptr thread) \<lbrace>(\<exists>rv. option_to_ptr rv = \<acute>ipcBuffer) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister = register_from_H Notification_H.badgeRegister \<and> syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err \<and> (\<forall>t v. seL4_MessageInfo_lift v = \<lparr>label_CL = type_C \<acute>current_syscall_error && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = \<^bsup>t\<^esup>ret__unsigned_long && mask 7\<rparr> \<longrightarrow> Types_H.message_info.MI (\<^bsup>t\<^esup>ret__unsigned_long && mask msgLengthBits) 0 0 x1 = message_info_to_H v)\<rbrace>
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and (\<lambda>a. valid_pspace' a \<and> valid_objs' a \<and> tcb_at' thread a)) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> ?R'248 threada x xa}}} proof (prove)
goal (1 subgoal):
 1. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> \<lbrace>syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x xa. msgFromSyscallError err = (x, xa) \<longrightarrow> (tcb_at' thread and (\<lambda>a. valid_pspace' a \<and> valid_objs' a \<and> tcb_at' thread a)) s) \<and> s' \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. msgFromSyscallError err = (x, xa) \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. threada) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> \<lbrace>\<forall>t. (\<exists>rv. option_to_ptr rv = \<^bsup>t\<^esup>ret__ptr_to_unsigned_long) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister = register_from_H Notification_H.badgeRegister \<and> syscall_error_to_H \<acute>current_syscall_error (lookup_fault_lift \<acute>current_lookup_fault) = Some err \<and> (\<forall>t v. seL4_MessageInfo_lift v = \<lparr>label_CL = type_C \<acute>current_syscall_error && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = \<^bsup>t\<^esup>ret__unsigned_long && mask 7\<rparr> \<longrightarrow> Types_H.message_info.MI (\<^bsup>t\<^esup>ret__unsigned_long && mask msgLengthBits) 0 0 x = message_info_to_H v)\<rbrace>}}} proof (prove)
goal (1 subgoal):
 1. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; valid_pspace' s \<and> tcb_at' thread s; syscall_error_to_H (current_syscall_error_' (globals s')) (lookup_fault_lift (current_lookup_fault_' (globals s'))) = Some err\<rbrakk> \<Longrightarrow> \<forall>x. (\<exists>xa. msgFromSyscallError err = (x, xa)) \<longrightarrow> (\<exists>t rv. option_to_ptr rv = ret__ptr_to_unsigned_long_' t) \<longrightarrow> (\<forall>t. (\<exists>v. seL4_MessageInfo_lift v = \<lparr>label_CL = type_C (current_syscall_error_' (globals s')) && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = ret__unsigned_long_' t && mask 7\<rparr>) \<longrightarrow> ret__unsigned_long_' t && mask msgLengthBits = ret__unsigned_long_' t && mask 7 \<and> x = type_C (current_syscall_error_' (globals s')) && mask 20) proof (prove)
goal:
No subgoals!