theory Ipc_C

lemma doIPCTransfer_ccorres [corres]:
  "ccorres dc xfdc
    (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver
                   and K (receiver \<noteq> sender \<and> endpoint \<noteq> Some 0))
    (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>canGrant = to_bool \<acute>grant\<rbrace>
          \<inter> \<lbrace>\<acute>badge = badge\<rbrace>
          \<inter> \<lbrace>\<acute>endpoint = option_to_ptr endpoint\<rbrace>)  []
    (doIPCTransfer sender endpoint badge canGrant receiver)
    (Call doIPCTransfer_'proc)" apply (cinit lift: sender_' receiver_' grant_' badge_' endpoint_') apply (rule_tac xf'="\<lambda>s. ret__ptr_to_unsigned_long_' s"
                in ccorres_split_nothrow_call_novcg) apply (rule lookupIPCBuffer_ccorres) apply simp_all[3] apply ceqv apply (rule ccorres_pre_threadGet) apply csymbr apply (rename_tac fault) apply (rule ccorres_move_c_guard_tcb) apply (rule_tac val="case_option (scast seL4_Fault_NullFault) fault_to_fault_tag fault"
                and xf'=ret__unsigned_'
                and R="\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = fault"
                 in ccorres_symb_exec_r_known_rv_UNIV [where R'=UNIV]) apply (vcg, clarsimp) apply (erule(1) cmap_relation_ko_atE [OF cmap_relation_tcb]) apply (fastforce simp: ctcb_relation_def typ_heap_simps
                             cfault_rel_def seL4_Fault_lift_def Let_def
                      split: if_split_asm option.split) apply ceqv apply wpc apply (clarsimp simp: seL4_Fault_NullFault_def ccorres_cond_univ_iff) apply (rule ccorres_rhs_assoc) apply (rule_tac xf'="ret__ptr_to_unsigned_long_'"
                   in ccorres_split_nothrow_call_novcg) apply (rule lookupIPCBuffer_ccorres) apply simp_all[3] apply ceqv apply csymbr apply ctac apply (wp lookupIPCBuffer_not_Some_0 lookupIPCBuffer_aligned) apply (clarsimp simp: seL4_Fault_NullFault_def ccorres_cond_iffs
                           fault_to_fault_tag_nonzero) apply ctac apply (clarsimp simp: guard_is_UNIV_def option_to_ptr_def split: option.splits) apply (rule_tac Q="\<lambda>rv. valid_pspace' and cur_tcb' and tcb_at' sender
                       and tcb_at' receiver and K (rv \<noteq> Some 0)
                       and (case_option \<top> valid_ipc_buffer_ptr' rv)
                       and K (receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)"
                in hoare_post_imp) apply (auto simp: valid_ipc_buffer_ptr'_def option_to_0_def
                   split: option.splits)[1] apply (wp lookupIPCBuffer_not_Some_0 lookupIPCBuffer_aligned) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and K (receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) (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>canGrant = to_bool \<acute>grant\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>endpoint = option_to_ptr endpoint\<rbrace>) [] (doIPCTransfer sender endpoint badge canGrant receiver) (Call doIPCTransfer_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1035 endpointa badgea grant receivera sendera) (?Q'1035 endpointa badgea grant receivera sendera) [SKIP] (do receiveBuffer <- lookupIPCBuffer True receiver;
fault <- threadGet tcbFault sender;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver receiveBuffer
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver receiveBuffer
od) (\<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) true,receivera);;
(\<acute>receiveBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
(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'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
FI)))
 2. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1035 endpointa badgea grant receivera sendera s \<and> s' \<in> ?Q'1035 endpointa badgea grant receivera sendera proof (prove)
goal (8 subgoals):
 1. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ccorres (?r'1041 endpointa badgea grant receivera sendera) (?xf''1041 endpointa badgea grant receivera sendera) (?P1041 endpointa badgea grant receivera sendera) (?P'1041 endpointa badgea grant receivera sendera) [] (lookupIPCBuffer True receiver) (Call lookupIPCBuffer_'proc)
 2. \<And>endpointa badgea grant receivera sendera x y s. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> globals (s\<lparr>ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' y\<rparr>) = globals s
 3. \<And>endpointa badgea grant receivera sendera a s t. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ret__ptr_to_unsigned_long_' (s\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr>) = ?xf''1041 endpointa badgea grant receivera sendera t
 4. \<And>endpointa badgea grant receivera sendera s. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> globals (thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s)) = globals s
 5. \<And>endpointa badgea grant receivera sendera rv' t t'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__ptr_to_unsigned_long_' rv' t t' (\<acute>receiveBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
(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'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
FI)) (?d'1041 endpointa badgea grant receivera sendera rv')
 6. \<And>endpointa badgea grant receivera sendera rv rv'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ?r'1041 endpointa badgea grant receivera sendera rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1041 endpointa badgea grant receivera sendera rv) (?Q'1041 endpointa badgea grant receivera sendera rv rv') [SKIP] (do fault <- threadGet tcbFault sender;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv
od) (?d'1041 endpointa badgea grant receivera sendera rv')
 7. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>?Q1041 endpointa badgea grant receivera sendera\<rbrace>
 8. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P1041 endpointa badgea grant receivera sendera and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> ?P'1041 endpointa badgea grant receivera sendera} \<inter> {s'. \<forall>t rv. ?r'1041 endpointa badgea grant receivera sendera rv (?xf''1041 endpointa badgea grant receivera sendera t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> ?Q'1041 endpointa badgea grant receivera sendera rv (?xf''1041 endpointa badgea grant receivera sendera t)} proof (prove)
goal (7 subgoals):
 1. \<And>endpointa badgea grant receivera sendera x y s. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> globals (s\<lparr>ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' y\<rparr>) = globals s
 2. \<And>endpointa badgea grant receivera sendera a s t. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ret__ptr_to_unsigned_long_' (s\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr>) = ret__ptr_to_unsigned_long_' t
 3. \<And>endpointa badgea grant receivera sendera s. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> globals (thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s)) = globals s
 4. \<And>endpointa badgea grant receivera sendera rv' t t'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__ptr_to_unsigned_long_' rv' t t' (\<acute>receiveBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
(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'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
FI)) (?d'1041 endpointa badgea grant receivera sendera rv')
 5. \<And>endpointa badgea grant receivera sendera rv rv'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1041 endpointa badgea grant receivera sendera rv) (?Q'1041 endpointa badgea grant receivera sendera rv rv') [SKIP] (do fault <- threadGet tcbFault sender;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv
od) (?d'1041 endpointa badgea grant receivera sendera rv')
 6. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>?Q1041 endpointa badgea grant receivera sendera\<rbrace>
 7. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> ?Q'1041 endpointa badgea grant receivera sendera rv (ret__ptr_to_unsigned_long_' t)} proof (prove)
goal (4 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv' t t'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__ptr_to_unsigned_long_' rv' t t' (\<acute>receiveBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
(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'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
FI)) (?d'1041 endpointa badgea grant receivera sendera rv')
 2. \<And>endpointa badgea grant receivera sendera rv rv'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1041 endpointa badgea grant receivera sendera rv) (?Q'1041 endpointa badgea grant receivera sendera rv rv') [SKIP] (do fault <- threadGet tcbFault sender;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv
od) (?d'1041 endpointa badgea grant receivera sendera rv')
 3. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>?Q1041 endpointa badgea grant receivera sendera\<rbrace>
 4. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> ?Q'1041 endpointa badgea grant receivera sendera rv (ret__ptr_to_unsigned_long_' t)} proof (prove)
goal (3 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv rv'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1041 endpointa badgea grant receivera sendera rv) (?Q'1041 endpointa badgea grant receivera sendera rv rv') [SKIP] (do fault <- threadGet tcbFault sender;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv
od) (\<acute>receiveBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) rv';;
(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'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
FI))
 2. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>?Q1041 endpointa badgea grant receivera sendera\<rbrace>
 3. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> ?Q'1041 endpointa badgea grant receivera sendera rv (ret__ptr_to_unsigned_long_' t)} proof (prove)
goal (3 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1175 endpointa badgea grant receivera sendera rv fault) (?P'1173 endpointa badgea grant receivera sendera rv rv' fault) [SKIP] (case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv) (\<acute>receiveBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) rv';;
(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'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>receiveBuffer___ptr_to_void)
FI))
 2. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ?P1175 endpointa badgea grant receivera sendera a (tcbFault tcb) b\<rbrace>
 3. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?P'1173 endpointa badgea grant receivera sendera rv (ret__ptr_to_unsigned_long_' t) (tcbFault tcb)}} proof (prove)
goal (3 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1175 endpointa badgea grant receivera sendera rv fault) (?G'1179 endpointa badgea grant receivera sendera rv rv' fault) [SKIP] (case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv) (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'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 2. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ?P1175 endpointa badgea grant receivera sendera a (tcbFault tcb) b\<rbrace>
 3. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> ?G'1179 endpointa badgea grant receivera sendera rv (ret__ptr_to_unsigned_long_' t) (tcbFault tcb)}}} proof (prove)
goal (3 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1175 endpointa badgea grant receivera sendera rv fault) (?G'1179 endpointa badgea grant receivera sendera rv rv' fault) [SKIP] (case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv) (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'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 2. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ?P1175 endpointa badgea grant receivera sendera a (tcbFault tcb) b\<rbrace>
 3. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> ?G'1179 endpointa badgea grant receivera sendera rv (ret__ptr_to_unsigned_long_' t) (tcbFault tcb)}}} proof (prove)
goal (3 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A1322 endpointa badgea grant receivera sendera rv fault) (?C'1321 endpointa badgea grant receivera sendera rv rv' fault) [SKIP] (case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv) (\<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''])));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 2. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> (?A1322 endpointa badgea grant receivera sendera a (tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 3. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> ?C'1321 endpointa badgea grant receivera sendera rv (ret__ptr_to_unsigned_long_' t) (tcbFault tcb) \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (6 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv rv' fault s. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. (\<exists>t. ko_at' t sender s \<and> tcbFault t = fault) \<and> (s, s') \<in> rf_sr}) \<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'']))) ({s'. (s, s') \<in> rf_sr} \<inter> \<lbrace>\<acute>ret__unsigned = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)\<rbrace>)
 2. \<And>endpointa badgea grant receivera sendera rv rv' fault rv'a t t'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv'a t t' (IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI) (?y'1325 endpointa badgea grant receivera sendera rv rv' fault rv'a)
 3. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1327 endpointa badgea grant receivera sendera rv fault) (?Q1325 endpointa badgea grant receivera sendera rv rv' fault) [SKIP] (case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv) (?y'1325 endpointa badgea grant receivera sendera rv rv' fault (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x))
 4. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. ?Q1325 endpointa badgea grant receivera sendera rv rv' fault)
 5. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> (?P1327 endpointa badgea grant receivera sendera a (tcbFault tcb) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 6. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (6 subgoals):
 1. \<And>s x t. \<lbrakk>(s, x) \<in> rf_sr; ko_at' t sender s\<rbrakk> \<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 tcbFault t of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)
 2. \<And>endpointa badgea grant receivera sendera rv rv' fault rv'a t t'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv'a t t' (IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI) (?y'1325 endpointa badgea grant receivera sendera rv rv' fault rv'a)
 3. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1327 endpointa badgea grant receivera sendera rv fault) (?Q1325 endpointa badgea grant receivera sendera rv rv' fault) [SKIP] (case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv) (?y'1325 endpointa badgea grant receivera sendera rv rv' fault (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x))
 4. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. ?Q1325 endpointa badgea grant receivera sendera rv rv' fault)
 5. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> (?P1327 endpointa badgea grant receivera sendera a (tcbFault tcb) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 6. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (6 subgoals):
 1. \<And>s x t ko'. \<lbrakk>ko_at' t sender s; cslift x (tcb_ptr_to_ctcb_ptr sender) = Some ko'; ctcb_relation t ko'\<rbrakk> \<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 tcbFault t of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)
 2. \<And>endpointa badgea grant receivera sendera rv rv' fault rv'a t t'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv'a t t' (IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI) (?y'1325 endpointa badgea grant receivera sendera rv rv' fault rv'a)
 3. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1327 endpointa badgea grant receivera sendera rv fault) (?Q1325 endpointa badgea grant receivera sendera rv rv' fault) [SKIP] (case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv) (?y'1325 endpointa badgea grant receivera sendera rv rv' fault (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x))
 4. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. ?Q1325 endpointa badgea grant receivera sendera rv rv' fault)
 5. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> (?P1327 endpointa badgea grant receivera sendera a (tcbFault tcb) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 6. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (5 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv rv' fault rv'a t t'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv'a t t' (IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI) (?y'1325 endpointa badgea grant receivera sendera rv rv' fault rv'a)
 2. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1327 endpointa badgea grant receivera sendera rv fault) (?Q1325 endpointa badgea grant receivera sendera rv rv' fault) [SKIP] (case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv) (?y'1325 endpointa badgea grant receivera sendera rv rv' fault (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x))
 3. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. ?Q1325 endpointa badgea grant receivera sendera rv rv' fault)
 4. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> (?P1327 endpointa badgea grant receivera sendera a (tcbFault tcb) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 5. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (4 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1327 endpointa badgea grant receivera sendera rv fault) (?Q1325 endpointa badgea grant receivera sendera rv rv' fault) [SKIP] (case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver rv) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 2. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. ?Q1325 endpointa badgea grant receivera sendera rv rv' fault)
 3. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> (?P1327 endpointa badgea grant receivera sendera a (tcbFault tcb) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 4. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (5 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'; fault = None\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1791 endpointa badgea grant receivera sendera rv fault) (?R''1793 endpointa badgea grant receivera sendera rv rv' fault) [SKIP] (do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge canGrant receiver rv
od) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 2. \<And>endpointa badgea grant receivera sendera rv rv' fault x2. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'; fault = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1792 endpointa badgea grant receivera sendera rv fault x2) (?R''1794 endpointa badgea grant receivera sendera rv rv' fault x2) [SKIP] (doFaultTransfer badge sender receiver rv) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 3. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> ?R''1793 endpointa badgea grant receivera sendera rv rv' fault} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> ?R''1794 endpointa badgea grant receivera sendera rv rv' fault x}})
 4. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> ?R1791 endpointa badgea grant receivera sendera a (tcbFault tcb) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R1792 endpointa badgea grant receivera sendera a (tcbFault tcb) x s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 5. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (5 subgoals):
 1. \<And>grant rv. canGrant = to_bool grant \<Longrightarrow> ccorres dc xfdc (?R1791 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv None) (?R''1793 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv (option_to_ptr rv) None) [SKIP] (do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge (to_bool grant) receiver rv
od) (\<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,tcb_ptr_to_ctcb_ptr sender);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(tcb_ptr_to_ctcb_ptr sender,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,option_to_ptr endpoint,badge,grant,tcb_ptr_to_ctcb_ptr receiver,option_to_ptr rv))
 2. \<And>endpointa badgea grant receivera sendera rv rv' fault x2. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'; fault = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1792 endpointa badgea grant receivera sendera rv fault x2) (?R''1794 endpointa badgea grant receivera sendera rv rv' fault x2) [SKIP] (doFaultTransfer badge sender receiver rv) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 3. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> ?R''1793 endpointa badgea grant receivera sendera rv rv' fault} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> ?R''1794 endpointa badgea grant receivera sendera rv rv' fault x}})
 4. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> ?R1791 endpointa badgea grant receivera sendera a (tcbFault tcb) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R1792 endpointa badgea grant receivera sendera a (tcbFault tcb) x s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 5. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (5 subgoals):
 1. \<And>grant rv. canGrant = to_bool grant \<Longrightarrow> ccorres dc xfdc (?R1791 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv None) (?R''1793 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv (option_to_ptr rv) None) [SKIP] (do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge (to_bool grant) receiver rv
od) (\<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,tcb_ptr_to_ctcb_ptr sender);;
(\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(tcb_ptr_to_ctcb_ptr sender,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,option_to_ptr endpoint,badge,grant,tcb_ptr_to_ctcb_ptr receiver,option_to_ptr rv)))
 2. \<And>endpointa badgea grant receivera sendera rv rv' fault x2. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'; fault = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1792 endpointa badgea grant receivera sendera rv fault x2) (?R''1794 endpointa badgea grant receivera sendera rv rv' fault x2) [SKIP] (doFaultTransfer badge sender receiver rv) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 3. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> ?R''1793 endpointa badgea grant receivera sendera rv rv' fault} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> ?R''1794 endpointa badgea grant receivera sendera rv rv' fault x}})
 4. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> ?R1791 endpointa badgea grant receivera sendera a (tcbFault tcb) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R1792 endpointa badgea grant receivera sendera a (tcbFault tcb) x s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 5. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (11 subgoals):
 1. \<And>grant rv. canGrant = to_bool grant \<Longrightarrow> ccorres (?r'1815 grant rv) (?xf''1815 grant rv) (?P1825 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv None) (?P'1823 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv (option_to_ptr rv) None) [] (lookupIPCBuffer False sender) (Call lookupIPCBuffer_'proc)
 2. \<And>grant rv x y s. canGrant = to_bool grant \<Longrightarrow> globals (s\<lparr>ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' y\<rparr>) = globals s
 3. \<And>grant rv a s t. canGrant = to_bool grant \<Longrightarrow> ret__ptr_to_unsigned_long_' (s\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr>) = ?xf''1815 grant rv t
 4. \<And>grant rv s. canGrant = to_bool grant \<Longrightarrow> globals (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s)) = globals s
 5. \<And>grant rv rv' t t'. canGrant = to_bool grant \<Longrightarrow> ceqv \<Gamma> ret__ptr_to_unsigned_long_' rv' t t' (\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(tcb_ptr_to_ctcb_ptr sender,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,option_to_ptr endpoint,badge,grant,tcb_ptr_to_ctcb_ptr receiver,option_to_ptr rv)) (?d'1815 grant rv rv')
 6. \<And>grant rv rva rv'. \<lbrakk>canGrant = to_bool grant; ?r'1815 grant rv rva rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1815 grant rv rva) (?Q'1815 grant rv rva rv') [SKIP] (doNormalTransfer sender rva endpoint badge (to_bool grant) receiver rv) (?d'1815 grant rv rv')
 7. \<And>grant rv. canGrant = to_bool grant \<Longrightarrow> \<lbrace>?R1824 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv None\<rbrace> lookupIPCBuffer False sender \<lbrace>?Q1815 grant rv\<rbrace>
 8. \<And>endpointa badgea grant receivera sendera rv rv' fault x2. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'; fault = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1792 endpointa badgea grant receivera sendera rv fault x2) (?R''1794 endpointa badgea grant receivera sendera rv rv' fault x2) [SKIP] (doFaultTransfer badge sender receiver rv) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 9. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. sendera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s) \<in> ?P'1823 endpointa badgea grant receivera sendera rv rv' fault} \<inter> {s'. \<forall>t rva. ?r'1822 endpointa badgea grant receivera sendera rv rv' fault t rva \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> ?Q'1821 endpointa badgea grant receivera sendera rv rv' fault t rva}} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> ?R''1794 endpointa badgea grant receivera sendera rv rv' fault x}})
 10. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> (?P1825 endpointa badgea grant receivera sendera a (tcbFault tcb) and ?R1824 endpointa badgea grant receivera sendera a (tcbFault tcb)) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R1792 endpointa badgea grant receivera sendera a (tcbFault tcb) x s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
A total of 11 subgoals...
flex-flex pairs:
\<lambda>grant rv. ?r'1822 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv (option_to_ptr rv) None \<equiv>\<^sup>? \<lambda>grant rv t rva. ?r'1815 grant rv rva (?xf''1815 grant rv t)
\<lambda>grant rv. ?Q'1821 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv (option_to_ptr rv) None \<equiv>\<^sup>? \<lambda>grant rv t rva. ?Q'1815 grant rv rva (?xf''1815 grant rv t) proof (prove)
goal (10 subgoals):
 1. \<And>grant rv x y s. canGrant = to_bool grant \<Longrightarrow> globals (s\<lparr>ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' y\<rparr>) = globals s
 2. \<And>grant rv a s t. canGrant = to_bool grant \<Longrightarrow> ret__ptr_to_unsigned_long_' (s\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr>) = ret__ptr_to_unsigned_long_' t
 3. \<And>grant rv s. canGrant = to_bool grant \<Longrightarrow> globals (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s)) = globals s
 4. \<And>grant rv rv' t t'. canGrant = to_bool grant \<Longrightarrow> ceqv \<Gamma> ret__ptr_to_unsigned_long_' rv' t t' (\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(tcb_ptr_to_ctcb_ptr sender,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,option_to_ptr endpoint,badge,grant,tcb_ptr_to_ctcb_ptr receiver,option_to_ptr rv)) (?d'1815 grant rv rv')
 5. \<And>grant rv rva rv'. \<lbrakk>canGrant = to_bool grant; ((=) \<circ> option_to_ptr) rva rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1815 grant rv rva) (?Q'1815 grant rv rva rv') [SKIP] (doNormalTransfer sender rva endpoint badge (to_bool grant) receiver rv) (?d'1815 grant rv rv')
 6. \<And>grant rv. canGrant = to_bool grant \<Longrightarrow> \<lbrace>?R1824 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv None\<rbrace> lookupIPCBuffer False sender \<lbrace>?Q1815 grant rv\<rbrace>
 7. \<And>endpointa badgea grant receivera sendera rv rv' fault x2. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'; fault = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1792 endpointa badgea grant receivera sendera rv fault x2) (?R''1794 endpointa badgea grant receivera sendera rv rv' fault x2) [SKIP] (doFaultTransfer badge sender receiver rv) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 8. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. sendera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = sendera\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool False\<rbrace>} \<inter> {s'. \<forall>t rva. ((=) \<circ> option_to_ptr) rva (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> ?Q'1821 endpointa badgea grant receivera sendera rv rv' fault t rva}} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> ?R''1794 endpointa badgea grant receivera sendera rv rv' fault x}})
 9. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> (tcb_at' sender and ?R1824 endpointa badgea grant receivera sendera a (tcbFault tcb)) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R1792 endpointa badgea grant receivera sendera a (tcbFault tcb) x s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 10. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}}
flex-flex pairs:
\<lambda>grant rv. ?Q'1821 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv (option_to_ptr rv) None \<equiv>\<^sup>? \<lambda>grant rv t rva. ?Q'1815 grant rv rva (ret__ptr_to_unsigned_long_' t) proof (prove)
goal (7 subgoals):
 1. \<And>grant rv rv' t t'. canGrant = to_bool grant \<Longrightarrow> ceqv \<Gamma> ret__ptr_to_unsigned_long_' rv' t t' (\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(tcb_ptr_to_ctcb_ptr sender,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,option_to_ptr endpoint,badge,grant,tcb_ptr_to_ctcb_ptr receiver,option_to_ptr rv)) (?d'1815 grant rv rv')
 2. \<And>grant rv rva rv'. \<lbrakk>canGrant = to_bool grant; ((=) \<circ> option_to_ptr) rva rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1815 grant rv rva) (?Q'1815 grant rv rva rv') [SKIP] (doNormalTransfer sender rva endpoint badge (to_bool grant) receiver rv) (?d'1815 grant rv rv')
 3. \<And>grant rv. canGrant = to_bool grant \<Longrightarrow> \<lbrace>?R1824 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv None\<rbrace> lookupIPCBuffer False sender \<lbrace>?Q1815 grant rv\<rbrace>
 4. \<And>endpointa badgea grant receivera sendera rv rv' fault x2. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'; fault = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1792 endpointa badgea grant receivera sendera rv fault x2) (?R''1794 endpointa badgea grant receivera sendera rv rv' fault x2) [SKIP] (doFaultTransfer badge sender receiver rv) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 5. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. sendera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = sendera\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool False\<rbrace>} \<inter> {s'. \<forall>t rva. ((=) \<circ> option_to_ptr) rva (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> ?Q'1821 endpointa badgea grant receivera sendera rv rv' fault t rva}} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> ?R''1794 endpointa badgea grant receivera sendera rv rv' fault x}})
 6. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> (tcb_at' sender and ?R1824 endpointa badgea grant receivera sendera a (tcbFault tcb)) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R1792 endpointa badgea grant receivera sendera a (tcbFault tcb) x s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 7. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}}
flex-flex pairs:
\<lambda>grant rv. ?Q'1821 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv (option_to_ptr rv) None \<equiv>\<^sup>? \<lambda>grant rv t rva. ?Q'1815 grant rv rva (ret__ptr_to_unsigned_long_' t) proof (prove)
goal (6 subgoals):
 1. \<And>grant rv rva rv'. \<lbrakk>canGrant = to_bool grant; ((=) \<circ> option_to_ptr) rva rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1815 grant rv rva) (?Q'1815 grant rv rva rv') [SKIP] (doNormalTransfer sender rva endpoint badge (to_bool grant) receiver rv) (\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) rv';;
CALL doNormalTransfer_'proc(tcb_ptr_to_ctcb_ptr sender,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,option_to_ptr endpoint,badge,grant,tcb_ptr_to_ctcb_ptr receiver,option_to_ptr rv))
 2. \<And>grant rv. canGrant = to_bool grant \<Longrightarrow> \<lbrace>?R1824 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv None\<rbrace> lookupIPCBuffer False sender \<lbrace>?Q1815 grant rv\<rbrace>
 3. \<And>endpointa badgea grant receivera sendera rv rv' fault x2. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'; fault = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1792 endpointa badgea grant receivera sendera rv fault x2) (?R''1794 endpointa badgea grant receivera sendera rv rv' fault x2) [SKIP] (doFaultTransfer badge sender receiver rv) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 4. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. sendera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = sendera\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool False\<rbrace>} \<inter> {s'. \<forall>t rva. ((=) \<circ> option_to_ptr) rva (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> ?Q'1821 endpointa badgea grant receivera sendera rv rv' fault t rva}} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> ?R''1794 endpointa badgea grant receivera sendera rv rv' fault x}})
 5. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> (tcb_at' sender and ?R1824 endpointa badgea grant receivera sendera a (tcbFault tcb)) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R1792 endpointa badgea grant receivera sendera a (tcbFault tcb) x s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 6. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}}
flex-flex pairs:
\<lambda>grant rv. ?Q'1821 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv (option_to_ptr rv) None \<equiv>\<^sup>? \<lambda>grant rv t rva. ?Q'1815 grant rv rva (ret__ptr_to_unsigned_long_' t) proof (prove)
goal (6 subgoals):
 1. \<And>grant rv rva rv'. \<lbrakk>canGrant = to_bool grant; ((=) \<circ> option_to_ptr) rva rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1815 grant rv rva) (?G'1880 grant rv rva rv') [SKIP] (doNormalTransfer sender rva endpoint badge (to_bool grant) receiver rv) (CALL doNormalTransfer_'proc(tcb_ptr_to_ctcb_ptr sender,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'),option_to_ptr endpoint,badge,grant,tcb_ptr_to_ctcb_ptr receiver,option_to_ptr rv))
 2. \<And>grant rv. canGrant = to_bool grant \<Longrightarrow> \<lbrace>?R1824 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv None\<rbrace> lookupIPCBuffer False sender \<lbrace>?Q1815 grant rv\<rbrace>
 3. \<And>endpointa badgea grant receivera sendera rv rv' fault x2. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'; fault = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1792 endpointa badgea grant receivera sendera rv fault x2) (?R''1794 endpointa badgea grant receivera sendera rv rv' fault x2) [SKIP] (doFaultTransfer badge sender receiver rv) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 4. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. sendera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = sendera\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool False\<rbrace>} \<inter> {s'. \<forall>t rva. ((=) \<circ> option_to_ptr) rva (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s. s\<lparr>sendBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> ?G'1884 endpointa badgea grant receivera sendera rv rv' fault t rva}}} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> ?R''1794 endpointa badgea grant receivera sendera rv rv' fault x}})
 5. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> (tcb_at' sender and ?R1824 endpointa badgea grant receivera sendera a (tcbFault tcb)) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R1792 endpointa badgea grant receivera sendera a (tcbFault tcb) x s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 6. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}}
flex-flex pairs:
\<lambda>grant rv. ?G'1884 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv (option_to_ptr rv) None \<equiv>\<^sup>? \<lambda>grant rv t rva. ?G'1880 grant rv rva (ret__ptr_to_unsigned_long_' t) proof (prove)
goal (5 subgoals):
 1. \<And>grant rv. canGrant = to_bool grant \<Longrightarrow> \<lbrace>?R1824 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv None\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>a. valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and K (endpoint \<noteq> Some 0) and (case a of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (case rv of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a)\<rbrace>
 2. \<And>endpointa badgea grant receivera sendera rv rv' fault x2. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'; fault = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1792 endpointa badgea grant receivera sendera rv fault x2) (?R''1794 endpointa badgea grant receivera sendera rv rv' fault x2) [SKIP] (doFaultTransfer badge sender receiver rv) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 3. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. sendera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = sendera\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool False\<rbrace>} \<inter> {s'. \<forall>t rva. ((=) \<circ> option_to_ptr) rva (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s. s\<lparr>sendBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> {s. receiveBuffer_'_update (\<lambda>_. rv') (receiver_'_update (\<lambda>_. receivera) (canGrant_'_update (\<lambda>_. grant) (badge_'_update (\<lambda>_. badgea) (endpoint_'_update (\<lambda>_. endpointa) (sendBuffer_'_update (\<lambda>_. PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t))) (sender_'_update (\<lambda>_. sendera) s)))))) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>sendBuffer = PTR(32 word) (option_to_0 rva)\<rbrace> \<inter> \<lbrace>\<acute>receiveBuffer = PTR(32 word) (option_to_0 rv)\<rbrace> \<inter> \<lbrace>to_bool grant = to_bool \<acute>canGrant\<rbrace> \<inter> \<lbrace>\<acute>badge = badgea\<rbrace> \<inter> \<lbrace>\<acute>endpoint = endpointa\<rbrace>}}}} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> ?R''1794 endpointa badgea grant receivera sendera rv rv' fault x}})
 4. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a b. \<forall>tcb. ko_at' tcb sender b \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> (tcb_at' sender and ?R1824 endpointa badgea grant receivera sendera a (tcbFault tcb)) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R1792 endpointa badgea grant receivera sendera a (tcbFault tcb) x s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) b\<rbrace>
 5. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (4 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv rv' fault x2. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'; fault = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R1792 endpointa badgea grant receivera sendera rv fault x2) (?R''1794 endpointa badgea grant receivera sendera rv rv' fault x2) [SKIP] (doFaultTransfer badge sender receiver rv) (IF (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault THEN
  \<acute>ret__ptr_to_unsigned_long :== CALL lookupIPCBuffer_'proc(SCAST(32 signed \<rightarrow> 32) false,sendera);;
\<acute>sendBuffer___ptr_to_void :== PTR_COERCE(32 word \<rightarrow> unit) \<acute>ret__ptr_to_unsigned_long;;
CALL doNormalTransfer_'proc(sendera,PTR_COERCE(unit \<rightarrow> 32 word) \<acute>sendBuffer___ptr_to_void,endpointa,badgea,grant,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
ELSE
  CALL doFaultTransfer_'proc(badgea,sendera,receivera,PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) rv'))
FI)
 2. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. sendera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = sendera\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool False\<rbrace>} \<inter> {s'. \<forall>t rva. ((=) \<circ> option_to_ptr) rva (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s. s\<lparr>sendBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> {s. receiveBuffer_'_update (\<lambda>_. rv') (receiver_'_update (\<lambda>_. receivera) (canGrant_'_update (\<lambda>_. grant) (badge_'_update (\<lambda>_. badgea) (endpoint_'_update (\<lambda>_. endpointa) (sendBuffer_'_update (\<lambda>_. PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t))) (sender_'_update (\<lambda>_. sendera) s)))))) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>sendBuffer = PTR(32 word) (option_to_0 rva)\<rbrace> \<inter> \<lbrace>\<acute>receiveBuffer = PTR(32 word) (option_to_0 rv)\<rbrace> \<inter> \<lbrace>to_bool grant = to_bool \<acute>canGrant\<rbrace> \<inter> \<lbrace>\<acute>badge = badgea\<rbrace> \<inter> \<lbrace>\<acute>endpoint = endpointa\<rbrace>}}}} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> ?R''1794 endpointa badgea grant receivera sendera rv rv' fault x}})
 3. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a aa. \<forall>tcb. ko_at' tcb sender aa \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> (tcb_at' sender and (\<lambda>aa. (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and K (endpoint \<noteq> Some 0)) aa \<and> valid_objs' aa \<and> (case a of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa)) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R1792 endpointa badgea grant receivera sendera a (tcbFault tcb) x s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) aa\<rbrace>
 4. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (4 subgoals):
 1. \<And>grant rv x2. canGrant = to_bool grant \<Longrightarrow> ccorres dc xfdc (?R1792 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv (Some x2) x2) (?R''1794 (option_to_ptr endpoint) badge grant (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) rv (option_to_ptr rv) (Some x2) x2) [SKIP] (doFaultTransfer badge sender receiver rv) (CALL doFaultTransfer_'proc(badge,tcb_ptr_to_ctcb_ptr sender,tcb_ptr_to_ctcb_ptr receiver,option_to_ptr rv))
 2. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. sendera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = sendera\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool False\<rbrace>} \<inter> {s'. \<forall>t rva. ((=) \<circ> option_to_ptr) rva (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s. s\<lparr>sendBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> {s. receiveBuffer_'_update (\<lambda>_. rv') (receiver_'_update (\<lambda>_. receivera) (canGrant_'_update (\<lambda>_. grant) (badge_'_update (\<lambda>_. badgea) (endpoint_'_update (\<lambda>_. endpointa) (sendBuffer_'_update (\<lambda>_. PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t))) (sender_'_update (\<lambda>_. sendera) s)))))) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>sendBuffer = PTR(32 word) (option_to_0 rva)\<rbrace> \<inter> \<lbrace>\<acute>receiveBuffer = PTR(32 word) (option_to_0 rv)\<rbrace> \<inter> \<lbrace>to_bool grant = to_bool \<acute>canGrant\<rbrace> \<inter> \<lbrace>\<acute>badge = badgea\<rbrace> \<inter> \<lbrace>\<acute>endpoint = endpointa\<rbrace>}}}} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> ?R''1794 endpointa badgea grant receivera sendera rv rv' fault x}})
 3. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a aa. \<forall>tcb. ko_at' tcb sender aa \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> (tcb_at' sender and (\<lambda>aa. (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and K (endpoint \<noteq> Some 0)) aa \<and> valid_objs' aa \<and> (case a of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa)) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> ?R1792 endpointa badgea grant receivera sendera a (tcbFault tcb) x s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) aa\<rbrace>
 4. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (3 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv rv' fault. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ((=) \<circ> option_to_ptr) rv rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = (case fault of None \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault | Some x \<Rightarrow> fault_to_fault_tag x)) ret__unsigned_' (\<lambda>rva rv'a. {s. fault = None \<longrightarrow> s \<in> {s. thread_'_update (\<lambda>_. sendera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = sendera\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool False\<rbrace>} \<inter> {s'. \<forall>t rva. ((=) \<circ> option_to_ptr) rva (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s. s\<lparr>sendBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> {s. receiveBuffer_'_update (\<lambda>_. rv') (receiver_'_update (\<lambda>_. receivera) (canGrant_'_update (\<lambda>_. grant) (badge_'_update (\<lambda>_. badgea) (endpoint_'_update (\<lambda>_. endpointa) (sendBuffer_'_update (\<lambda>_. PTR_COERCE(unit \<rightarrow> 32 word) (PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t))) (sender_'_update (\<lambda>_. sendera) s)))))) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>sendBuffer = PTR(32 word) (option_to_0 rva)\<rbrace> \<inter> \<lbrace>\<acute>receiveBuffer = PTR(32 word) (option_to_0 rv)\<rbrace> \<inter> \<lbrace>to_bool grant = to_bool \<acute>canGrant\<rbrace> \<inter> \<lbrace>\<acute>badge = badgea\<rbrace> \<inter> \<lbrace>\<acute>endpoint = endpointa\<rbrace>}}}} \<inter> {s. \<forall>x. s \<in> {s. fault = Some x \<longrightarrow> s \<in> {s. receiverIPCBuffer_'_update (\<lambda>_. rv') (receiver_'_update (\<lambda>_. receivera) (sender_'_update (\<lambda>_. sendera) (badge_'_update (\<lambda>_. badgea) s))) \<in> UNIV \<inter> \<lbrace>\<acute>sender = sendera\<rbrace> \<inter> \<lbrace>\<acute>receiver = receivera\<rbrace> \<inter> \<lbrace>\<acute>receiverIPCBuffer = PTR(32 word) (option_to_0 rv)\<rbrace> \<inter> \<lbrace>\<acute>badge = badgea\<rbrace>}}})
 2. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a aa. \<forall>tcb. ko_at' tcb sender aa \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> (tcb_at' sender and (\<lambda>aa. (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and K (endpoint \<noteq> Some 0)) aa \<and> valid_objs' aa \<and> (case a of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa)) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case a of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (a \<noteq> Some 0) and K (receiver \<noteq> sender)) s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) aa\<rbrace>
 3. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (2 subgoals):
 1. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>a aa. \<forall>tcb. ko_at' tcb sender aa \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> (tcb_at' sender and (\<lambda>aa. (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and K (endpoint \<noteq> Some 0)) aa \<and> valid_objs' aa \<and> (case a of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa)) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case a of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (a \<noteq> Some 0) and K (receiver \<noteq> sender)) s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) aa\<rbrace>
 2. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (3 subgoals):
 1. \<And>endpointa badgea grant receivera sendera rv s. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and K (rv \<noteq> Some 0) and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s\<rbrakk> \<Longrightarrow> \<forall>tcb. ko_at' tcb sender s \<longrightarrow> ((\<lambda>s. (tcbFault tcb = None \<longrightarrow> (tcb_at' sender and (\<lambda>a. (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and K (endpoint \<noteq> Some 0)) a \<and> valid_objs' a \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) a)) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> (valid_pspace' and tcb_at' sender and tcb_at' receiver and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (rv \<noteq> Some 0) and K (receiver \<noteq> sender)) s)) and (\<lambda>s. \<exists>t. ko_at' t sender s \<and> tcbFault t = tcbFault tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr sendera)) s
 2. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>rv. valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and K (rv \<noteq> Some 0) and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)\<rbrace>
 3. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (2 subgoals):
 1. \<And>endpointa badgea grant receivera sendera. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> \<lbrace>?R1041 endpointa badgea grant receivera sendera\<rbrace> lookupIPCBuffer True receiver \<lbrace>\<lambda>rv. valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and K (rv \<noteq> Some 0) and (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)\<rbrace>
 2. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and ?R1041 endpointa badgea grant receivera sendera) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal (1 subgoal):
 1. \<And>endpointa badgea grant receivera sendera s s'. \<lbrakk>endpointa = option_to_ptr endpoint; badgea = badge; canGrant = to_bool grant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. receiver \<noteq> sender \<and> endpoint \<noteq> Some 0)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' receiver and (\<lambda>s. (valid_pspace' and cur_tcb' and tcb_at' sender and tcb_at' receiver) s \<and> True \<and> valid_objs' s \<and> K (receiver \<noteq> sender \<and> endpoint \<noteq> Some 0) s)) s \<and> s' \<in> {s. thread_'_update (\<lambda>_. receivera) (isReceiver_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>isReceiver = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> option_to_ptr) rv (ret__ptr_to_unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__ptr_to_unsigned_long_' := ret__ptr_to_unsigned_long_' t\<rparr> \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s. s\<lparr>receiveBuffer___ptr_to_void_' := PTR_COERCE(32 word \<rightarrow> unit) (ret__ptr_to_unsigned_long_' t)\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}}} proof (prove)
goal:
No subgoals!