theory Ipc_C

lemma doFaultTransfer_ccorres [corres]:
  "ccorres dc xfdc (valid_pspace' and tcb_at' sender and tcb_at' receiver
                    and (case buffer of Some x \<Rightarrow> valid_ipc_buffer_ptr' x | None \<Rightarrow> \<top>)
                    and K (buffer \<noteq> Some 0) and K (receiver \<noteq> 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>receiverIPCBuffer = Ptr (option_to_0 buffer)\<rbrace>
          \<inter> \<lbrace>\<acute>badge = badge\<rbrace>) []
    (doFaultTransfer badge sender receiver buffer)
    (Call doFaultTransfer_'proc)" apply (unfold K_def) apply (intro ccorres_gen_asm) apply (simp add: doFaultTransfer_def) apply (subst makeFaultMessage2) apply (simp only: makeArchFaultMessage2_def) apply (cinit' lift: sender_' receiver_' receiverIPCBuffer_' badge_') apply (rule ccorres_pre_threadGet) apply (rename_tac ft) apply wpc apply (simp del: Collect_const, rule ccorres_fail) apply (simp add: split_def bind_assoc del: Collect_const) apply (simp only: bind_assoc[symmetric, where m="makeFaultMessage ft t" for ft t]) apply (ctac(no_vcg) add: setMRs_fault_ccorres) apply (rule_tac R="obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender"
              and val="case (the ft) of CapFault _ _ _ \<Rightarrow> 1
                  | ArchFault (VMFault _ _) \<Rightarrow> 5 | UnknownSyscallException _ \<Rightarrow> 2
                  | UserException _ _ \<Rightarrow> 3"
              in ccorres_symb_exec_r_known_rv_UNIV
                   [where xf'=ret__unsigned_' and R'=UNIV]) apply (rule conseqPre, vcg, clarsimp) apply (drule(1) obj_at_cslift_tcb) apply (clarsimp simp: typ_heap_simps' ctcb_relation_def
                             cfault_rel_def seL4_Fault_lift_def Let_def
                             seL4_Fault_tag_defs
                      split: if_split_asm) apply ceqv apply csymbr apply (ctac (no_vcg, c_lines 2) add: setMessageInfo_ccorres) apply (ctac add: setRegister_ccorres) apply wp apply (simp add: badgeRegister_def ARM.badgeRegister_def
                      Kernel_C.badgeRegister_def "StrictC'_register_defs") apply (clarsimp simp: message_info_to_H_def guard_is_UNIVI
                          mask_def msgLengthBits_def
                   split: fault.split arch_fault.split) apply wp apply (simp add: setMRs_to_setMR zipWithM_mapM split_def) apply (wp mapM_wp' setMR_tcbFault_obj_at | simp)+ apply (clarsimp simp: obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (receiver \<noteq> 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>receiverIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>) [] (doFaultTransfer badge sender receiver buffer) (Call doFaultTransfer_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>y. buffer \<noteq> Some 0) and (\<lambda>y. receiver \<noteq> 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>receiverIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>) [] (doFaultTransfer badge sender receiver buffer) (Call doFaultTransfer_'proc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (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>receiverIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>) [] (doFaultTransfer badge sender receiver buffer) (Call doFaultTransfer_'proc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (\<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>receiverIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>) [] (do fault <- threadGet tcbFault sender;
f <- case fault of None \<Rightarrow> haskell_fail [] | Some f \<Rightarrow> return f;
(faultLabel, faultMsg) <- makeFaultMessage f sender;
sent <- setMRs receiver buffer faultMsg;
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 faultLabel);
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (Call doFaultTransfer_'proc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (\<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>receiverIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>) [] (do fault <- threadGet tcbFault sender;
f <- case fault of None \<Rightarrow> haskell_fail [] | Some x \<Rightarrow> return x;
(faultLabel, faultMsg) <- do x <- makeFaultMessage f sender;
return (case f of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault x \<Rightarrow> makeArchFaultMessage2 x, snd x)
od;
sent <- setMRs receiver buffer faultMsg;
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 faultLabel);
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (Call doFaultTransfer_'proc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (\<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>receiverIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>) [] (do fault <- threadGet tcbFault sender;
f <- case fault of None \<Rightarrow> haskell_fail [] | Some x \<Rightarrow> return x;
(faultLabel, faultMsg) <- do x <- makeFaultMessage f sender;
return (case f of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5, snd x)
od;
sent <- setMRs receiver buffer faultMsg;
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 faultLabel);
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (Call doFaultTransfer_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q807 badgea receiverIPCBuffer receivera sendera) (?Q'807 badgea receiverIPCBuffer receivera sendera) [SKIP] (do fault <- threadGet tcbFault sender;
f <- case fault of None \<Rightarrow> haskell_fail [] | Some x \<Rightarrow> return x;
x <- makeFaultMessage f sender;
sent <- setMRs receiver buffer (snd x);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (case f of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (\<acute>sent :== CALL setMRs_fault_'proc(sendera,receivera,receiverIPCBuffer);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c sendera} (\<acute>ret__unsigned :== CALL seL4_Fault_get_seL4_FaultType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(sendera\<rightarrow>[''tcbFault_C'']))));;
(\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,UCAST(32 \<rightarrow> 32) \<acute>sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badgea))))))
 2. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q807 badgea receiverIPCBuffer receivera sendera s \<and> s' \<in> ?Q'807 badgea receiverIPCBuffer receivera sendera proof (prove)
goal (2 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera fault. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P813 badgea receiverIPCBuffer receivera sendera fault) (?P'813 badgea receiverIPCBuffer receivera sendera fault) [SKIP] (do f <- case fault of None \<Rightarrow> haskell_fail [] | Some x \<Rightarrow> return x;
x <- makeFaultMessage f sender;
sent <- setMRs receiver buffer (snd x);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (case f of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (\<acute>sent :== CALL setMRs_fault_'proc(sendera,receivera,receiverIPCBuffer);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c sendera} (\<acute>ret__unsigned :== CALL seL4_Fault_get_seL4_FaultType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(sendera\<rightarrow>[''tcbFault_C'']))));;
(\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,UCAST(32 \<rightarrow> 32) \<acute>sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badgea))))))
 2. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> ?P813 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?P'813 badgea receiverIPCBuffer receivera sendera (tcbFault tcb)} proof (prove)
goal (2 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P813 badgea receiverIPCBuffer receivera sendera ft) (?P'813 badgea receiverIPCBuffer receivera sendera ft) [SKIP] (do f <- case ft of None \<Rightarrow> haskell_fail [] | Some x \<Rightarrow> return x;
x <- makeFaultMessage f sender;
sent <- setMRs receiver buffer (snd x);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (case f of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (\<acute>sent :== CALL setMRs_fault_'proc(sendera,receivera,receiverIPCBuffer);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c sendera} (\<acute>ret__unsigned :== CALL seL4_Fault_get_seL4_FaultType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(sendera\<rightarrow>[''tcbFault_C'']))));;
(\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,UCAST(32 \<rightarrow> 32) \<acute>sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badgea))))))
 2. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> ?P813 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?P'813 badgea receiverIPCBuffer receivera sendera (tcbFault tcb)} proof (prove)
goal (3 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = None\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R823 badgea receiverIPCBuffer receivera sendera ft) (?R''825 badgea receiverIPCBuffer receivera sendera ft) [SKIP] (do f <- haskell_fail [];
x <- makeFaultMessage f sender;
sent <- setMRs receiver buffer (snd x);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (case f of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (\<acute>sent :== CALL setMRs_fault_'proc(sendera,receivera,receiverIPCBuffer);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c sendera} (\<acute>ret__unsigned :== CALL seL4_Fault_get_seL4_FaultType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(sendera\<rightarrow>[''tcbFault_C'']))));;
(\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,UCAST(32 \<rightarrow> 32) \<acute>sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badgea))))))
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R824 badgea receiverIPCBuffer receivera sendera ft x2) (?R''826 badgea receiverIPCBuffer receivera sendera ft x2) [SKIP] (do f <- return x2;
x <- makeFaultMessage f sender;
sent <- setMRs receiver buffer (snd x);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (case f of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (\<acute>sent :== CALL setMRs_fault_'proc(sendera,receivera,receiverIPCBuffer);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c sendera} (\<acute>ret__unsigned :== CALL seL4_Fault_get_seL4_FaultType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(sendera\<rightarrow>[''tcbFault_C'']))));;
(\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,UCAST(32 \<rightarrow> 32) \<acute>sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badgea))))))
 3. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> ?R823 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R824 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> ?R''825 badgea receiverIPCBuffer receivera sendera (tcbFault tcb)} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> ?R''826 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x}}} proof (prove)
goal (2 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R824 badgea receiverIPCBuffer receivera sendera ft x2) (?R''826 badgea receiverIPCBuffer receivera sendera ft x2) [SKIP] (do f <- return x2;
x <- makeFaultMessage f sender;
sent <- setMRs receiver buffer (snd x);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (case f of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (\<acute>sent :== CALL setMRs_fault_'proc(sendera,receivera,receiverIPCBuffer);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c sendera} (\<acute>ret__unsigned :== CALL seL4_Fault_get_seL4_FaultType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(sendera\<rightarrow>[''tcbFault_C'']))));;
(\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,UCAST(32 \<rightarrow> 32) \<acute>sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(receivera,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badgea))))))
 2. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R824 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> ?R''826 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x}}} proof (prove)
goal (2 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R824 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2) (?R''826 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2) [SKIP] (do x <- makeFaultMessage x2 sender;
sent <- setMRs receiver buffer (snd x);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (\<acute>sent :== CALL setMRs_fault_'proc(tcb_ptr_to_ctcb_ptr sender,tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_get_seL4_FaultType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,0,0,\<acute>sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badge))))))
 2. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R824 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> ?R''826 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x}}} proof (prove)
goal (2 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R824 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2) (?R''826 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2) [SKIP] (do sent <- do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od;
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (\<acute>sent :== CALL setMRs_fault_'proc(tcb_ptr_to_ctcb_ptr sender,tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_get_seL4_FaultType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,0,0,\<acute>sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badge))))))
 2. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R824 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> ?R''826 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x}}} proof (prove)
goal (3 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q837 badgea receiverIPCBuffer receivera sendera ft x2 rv) (?Q'852 x2 rv sent) [SKIP] (do y <- setMessageInfo receiver (Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_get_seL4_FaultType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,0,0,sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badge)))))
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>?Q837 badgea receiverIPCBuffer receivera sendera ft x2\<rbrace>
 3. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'851 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x t rv}}}}
flex-flex pairs:
\<lambda>x2 t rv. ?Q'852 x2 rv (ret__unsigned_long_' t) \<equiv>\<^sup>? \<lambda>x2. ?Q'851 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2 proof (prove)
goal (6 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent s. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender s \<and> (s, s') \<in> rf_sr}) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_get_seL4_FaultType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])))) ({s'. (s, s') \<in> rf_sr} \<inter> \<lbrace>\<acute>ret__unsigned = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5)\<rbrace>)
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent rv' t t'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv' t t' (\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,0,0,sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badge)))) (?y'1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent rv')
 3. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1054 badgea receiverIPCBuffer receivera sendera ft x2 rv) (?Q1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent) [SKIP] (do y <- setMessageInfo receiver (Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (?y'1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5))
 4. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5)) ret__unsigned_' (\<lambda>rva rv'. ?Q1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent)
 5. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>\<lambda>a. ?P1054 badgea receiverIPCBuffer receivera sendera ft x2 a and obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 6. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (6 subgoals):
 1. \<And>x2 s x. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; obj_at' (\<lambda>tcb. tcbFault tcb = Some x2) sender s; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender \<and> ((\<exists>t. ret__unsigned_' t = seL4_Fault_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])))) \<longrightarrow> seL4_Fault_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))) = (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5))
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent rv' t t'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv' t t' (\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,0,0,sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badge)))) (?y'1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent rv')
 3. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1054 badgea receiverIPCBuffer receivera sendera ft x2 rv) (?Q1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent) [SKIP] (do y <- setMessageInfo receiver (Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (?y'1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5))
 4. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5)) ret__unsigned_' (\<lambda>rva rv'. ?Q1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent)
 5. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>\<lambda>a. ?P1054 badgea receiverIPCBuffer receivera sendera ft x2 a and obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 6. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (6 subgoals):
 1. \<And>x2 s x. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; (s, x) \<in> rf_sr; \<exists>ko ko'. ko_at' ko sender s \<and> tcbFault ko = Some x2 \<and> cslift x (tcb_ptr_to_ctcb_ptr sender) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender \<and> ((\<exists>t. ret__unsigned_' t = seL4_Fault_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])))) \<longrightarrow> seL4_Fault_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))) = (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5))
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent rv' t t'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv' t t' (\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,0,0,sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badge)))) (?y'1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent rv')
 3. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1054 badgea receiverIPCBuffer receivera sendera ft x2 rv) (?Q1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent) [SKIP] (do y <- setMessageInfo receiver (Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (?y'1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5))
 4. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5)) ret__unsigned_' (\<lambda>rva rv'. ?Q1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent)
 5. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>\<lambda>a. ?P1054 badgea receiverIPCBuffer receivera sendera ft x2 a and obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 6. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (5 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent rv' t t'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv' t t' (\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(\<acute>ret__unsigned,0,0,sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badge)))) (?y'1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent rv')
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1054 badgea receiverIPCBuffer receivera sendera ft x2 rv) (?Q1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent) [SKIP] (do y <- setMessageInfo receiver (Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (?y'1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5))
 3. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5)) ret__unsigned_' (\<lambda>rva rv'. ?Q1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent)
 4. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>\<lambda>a. ?P1054 badgea receiverIPCBuffer receivera sendera ft x2 a and obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 5. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (4 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1054 badgea receiverIPCBuffer receivera sendera ft x2 rv) (?Q1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent) [SKIP] (do y <- setMessageInfo receiver (Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (\<acute>msgInfo___struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5,0,0,sent);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badge))))
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5)) ret__unsigned_' (\<lambda>rva rv'. ?Q1050 badgea receiverIPCBuffer receivera sendera ft x2 rv sent)
 3. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>\<lambda>a. ?P1054 badgea receiverIPCBuffer receivera sendera ft x2 a and obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 4. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (4 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits; seL4_MessageInfo_lift msgInfo___struct_seL4_MessageInfo_C = \<lparr>label_CL = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5) && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = sent && mask 7\<rparr>\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1054 badgea receiverIPCBuffer receivera sendera ft x2 rv) (?G'1440 badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C) [SKIP] (do y <- setMessageInfo receiver (Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5));
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) (\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(msgInfo___struct_seL4_MessageInfo_C);;
(CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badge)))
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5)) ret__unsigned_' (\<lambda>rva rv'. {s. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 7\<rparr> \<longrightarrow> s\<lparr>msgInfo___struct_seL4_MessageInfo_C_' := v\<rparr> \<in> ?G'1440 badgea receiverIPCBuffer receivera sendera ft x2 rv sent v})
 3. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>\<lambda>a. ?P1054 badgea receiverIPCBuffer receivera sendera ft x2 a and obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 4. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (6 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C y xfdca. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits; seL4_MessageInfo_lift msgInfo___struct_seL4_MessageInfo_C = \<lparr>label_CL = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5) && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = sent && mask 7\<rparr>; dc y xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1539 badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C y) (?Q'1539 badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C y xfdca) [SKIP] (asUser receiver (setRegister Notification_H.badgeRegister badge)) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,badge))
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits; seL4_MessageInfo_lift msgInfo___struct_seL4_MessageInfo_C = \<lparr>label_CL = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5) && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = sent && mask 7\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R1541 badgea receiverIPCBuffer receivera sendera ft x2 rv\<rbrace> setMessageInfo receiver (Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5)) \<lbrace>?Q1539 badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C\<rbrace>
 3. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C s rva. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits; seL4_MessageInfo_lift msgInfo___struct_seL4_MessageInfo_C = \<lparr>label_CL = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5) && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = sent && mask 7\<rparr>; dc rva (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'1539 badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C rva (xfdc s)
 4. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5)) ret__unsigned_' (\<lambda>rva rv'. {s. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 7\<rparr> \<longrightarrow> s\<lparr>msgInfo___struct_seL4_MessageInfo_C_' := v\<rparr> \<in> UNIV \<inter> \<lbrace>Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5) = message_info_to_H v\<rbrace>})
 5. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>\<lambda>a. tcb_at' receiver and ?R1541 badgea receiverIPCBuffer receivera sendera ft x2 a and obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 6. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (5 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits; seL4_MessageInfo_lift msgInfo___struct_seL4_MessageInfo_C = \<lparr>label_CL = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5) && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = sent && mask 7\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R1541 badgea receiverIPCBuffer receivera sendera ft x2 rv\<rbrace> setMessageInfo receiver (Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5)) \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C s rva. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits; seL4_MessageInfo_lift msgInfo___struct_seL4_MessageInfo_C = \<lparr>label_CL = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5) && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = sent && mask 7\<rparr>; dc rva (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> {s. w_'_update (\<lambda>_. badge) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (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 Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = badge\<rbrace>}
 3. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5)) ret__unsigned_' (\<lambda>rva rv'. {s. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 7\<rparr> \<longrightarrow> s\<lparr>msgInfo___struct_seL4_MessageInfo_C_' := v\<rparr> \<in> UNIV \<inter> \<lbrace>Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5) = message_info_to_H v\<rbrace>})
 4. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>\<lambda>a. tcb_at' receiver and ?R1541 badgea receiverIPCBuffer receivera sendera ft x2 a and obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 5. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (4 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent msgInfo___struct_seL4_MessageInfo_C s rva. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits; seL4_MessageInfo_lift msgInfo___struct_seL4_MessageInfo_C = \<lparr>label_CL = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5) && mask 20, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = sent && mask 7\<rparr>; dc rva (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> {s. w_'_update (\<lambda>_. badge) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (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 Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = badge\<rbrace>}
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5)) ret__unsigned_' (\<lambda>rva rv'. {s. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 7\<rparr> \<longrightarrow> s\<lparr>msgInfo___struct_seL4_MessageInfo_C_' := v\<rparr> \<in> UNIV \<inter> \<lbrace>Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5) = message_info_to_H v\<rbrace>})
 3. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>\<lambda>a. tcb_at' receiver and (\<lambda>a. True) and obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 4. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (3 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2 rv sent. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2; rv = sent && mask msgLengthBits\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5)) ret__unsigned_' (\<lambda>rva rv'. {s. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. sent) (extraCaps_'_update (\<lambda>_. 0) (capsUnwrapped_'_update (\<lambda>_. 0) (label_'_update (\<lambda>_. case the ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault x xa) \<Rightarrow> 5) s)))) && mask 7\<rparr> \<longrightarrow> s\<lparr>msgInfo___struct_seL4_MessageInfo_C_' := v\<rparr> \<in> UNIV \<inter> \<lbrace>Types_H.message_info.MI rv 0 0 (case x2 of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault (ARM_H.VMFault xa xaa) \<Rightarrow> 5) = message_info_to_H v\<rbrace>})
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>\<lambda>a. tcb_at' receiver and (\<lambda>a. True) and obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 3. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (2 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> do x <- makeFaultMessage x2 sender;
setMRs receiver buffer (snd x)
od \<lbrace>\<lambda>a. tcb_at' receiver and (\<lambda>a. True) and obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 2. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (3 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2 x. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?P'1586 badgea receiverIPCBuffer receivera sendera ft x2 x\<rbrace> setMRs receiver buffer (snd x) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. tcbFault tcb = ft) sender\<rbrace>
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> makeFaultMessage x2 sender \<lbrace>\<lambda>x s. tcb_at' receiver s \<and> True \<and> ?P'1586 badgea receiverIPCBuffer receivera sendera ft x2 x s\<rbrace>
 3. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (3 subgoals):
 1. \<And>badgea receiverIPCBuffer receivera sendera ft x2 x. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?P'1586 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2 x\<rbrace> do y <- stateAssert (tcb_at' receiver) [];
ys <- mapM (\<lambda>p. setMR receiver buffer (fst p) (snd p)) (zip [0..<msgMaxLength] (snd x));
return (word_of_nat (if ys = [] then 0 else last ys))
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. tcbFault tcb = Some x2) sender\<rbrace>
 2. \<And>badgea receiverIPCBuffer receivera sendera ft x2. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R846 badge (PTR(32 word) (option_to_0 buffer)) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) (Some x2) x2\<rbrace> makeFaultMessage x2 sender \<lbrace>\<lambda>x s. tcb_at' receiver s \<and> True \<and> ?P'1586 badgea receiverIPCBuffer receivera sendera ft x2 x s\<rbrace>
 3. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and obj_at' (\<lambda>tcba. tcbFault tcba = tcbFault tcb) sender and tcb_at' receiver and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver) and ?R846 badgea receiverIPCBuffer receivera sendera (tcbFault tcb) x) s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. tcbFault tcb = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. tcbFault tcb = Some x \<longrightarrow> s \<in> {s. receiveIPCBuffer_'_update (\<lambda>_. receiverIPCBuffer) (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) s)) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = receiverIPCBuffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t && mask msgLengthBits \<longrightarrow> sent_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}}}} proof (prove)
goal (1 subgoal):
 1. \<And>badgea receiverIPCBuffer receivera sendera s s'. \<lbrakk>receiver \<noteq> sender; buffer \<noteq> Some 0; badgea = badge; receiverIPCBuffer = PTR(32 word) (option_to_0 buffer); receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; valid_pspace' s \<and> tcb_at' sender s \<and> tcb_at' receiver s \<and> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s\<rbrakk> \<Longrightarrow> \<forall>tcb. ko_at' tcb sender s \<longrightarrow> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> obj_at' (\<lambda>tcb. tcbFault tcb = Some x) sender s) proof (prove)
goal:
No subgoals!