theory Ipc_C

lemma handleArchFaultReply_corres:
  "ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_'
           (valid_pspace' and tcb_at' sender
                          and tcb_at' receiver
                          and K (f = ArchFault af)
                          and K (sender \<noteq> receiver))
           (UNIV \<inter> \<lbrace> \<acute>faultType = fault_to_fault_tag f \<rbrace>
           \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace>
           \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace>)
           hs
           (handleArchFaultReply' af sender receiver msg)
           (Call Arch_handleFaultReply_'proc)" apply (unfold K_def) apply (rule ccorres_gen_asm)+ apply (cinit lift: faultType_' sender_' receiver_') apply (clarsimp simp: bind_assoc seL4_Fault_tag_defs ccorres_cond_iffs
                   split del: if_split split: arch_fault.split) apply (rule ccorres_symb_exec_l) apply (rule ccorres_stateAssert) apply wpc apply (clarsimp simp: ccorres_cond_iffs) apply (rule ccorres_return_C) apply simp+ apply (rule ccorres_symb_exec_l) apply (ctac add: ccorres_return_C) apply (wp mapM_wp' empty_fail_loadWordUser | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (valid_pspace' and tcb_at' sender and tcb_at' receiver and K (f = Fault_H.fault.ArchFault af) and K (sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag f\<rbrace> \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace>) hs (handleArchFaultReply' af sender receiver msg) (Call Arch_handleFaultReply_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (valid_pspace' and tcb_at' sender and tcb_at' receiver and (\<lambda>y. f = Fault_H.fault.ArchFault af) and (\<lambda>y. sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag f\<rbrace> \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace>) hs (handleArchFaultReply' af sender receiver msg) (Call Arch_handleFaultReply_'proc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (valid_pspace' and tcb_at' sender and tcb_at' receiver) (UNIV \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag f\<rbrace> \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace>) hs (handleArchFaultReply' af sender receiver msg) (Call Arch_handleFaultReply_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>receivera sendera faultType. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; faultType = arch_fault_to_fault_tag af\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?Q198 receivera sendera faultType) (?Q'198 receivera sendera faultType) (SKIP # hs) (case af of ARM_H.VMFault x xa \<Rightarrow> do sendBuf <- lookupIPCBuffer False sender;
stateAssert (tcb_at' sender) [];
case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> do mapM loadWordUser (map (\<lambda>i. bufferPtr + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]);
return ()
od;
return True
od) (IF faultType = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)
ELSE
  Guard DontReach {} SKIP
FI)
 2. \<And>receivera sendera faultType s s'. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; faultType = arch_fault_to_fault_tag af; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q198 receivera sendera faultType s \<and> s' \<in> ?Q'198 receivera sendera faultType proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?Q198 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5) (?Q'198 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5) (SKIP # hs) (do sendBuf <- lookupIPCBuffer False sender;
a <- stateAssert (tcb_at' sender) [];
a <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> do mapM loadWordUser (map (\<lambda>i. bufferPtr + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]);
return ()
od;
return True
od) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>receivera sendera faultType s s'. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; faultType = arch_fault_to_fault_tag af; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q198 receivera sendera faultType s \<and> s' \<in> ?Q'198 receivera sendera faultType proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 sendBuf. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?Q232 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf) (?Q'230 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf) (SKIP # hs) (do a <- stateAssert (tcb_at' sender) [];
a <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> do mapM loadWordUser (map (\<lambda>i. bufferPtr + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]);
return ()
od;
return True
od) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>x1 x2 s. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q198 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5\<rbrace> lookupIPCBuffer False sender \<lbrace>?Q232 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5\<rbrace>
 4. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> empty_fail (lookupIPCBuffer False sender)
 5. \<And>receivera sendera faultType s s'. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; faultType = arch_fault_to_fault_tag af; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q198 receivera sendera faultType s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q232 receivera sendera faultType rv s \<longrightarrow> s' \<in> ?Q'230 receivera sendera faultType rv} proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 sendBuf. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?P239 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf) (?Q'230 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf) (SKIP # hs) (do a <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> do mapM loadWordUser (map (\<lambda>i. bufferPtr + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]);
return ()
od;
return True
od) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>x1 x2 s. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q198 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>a b. tcb_at' sender b \<longrightarrow> ?P239 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 a b\<rbrace>
 4. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> empty_fail (lookupIPCBuffer False sender)
 5. \<And>receivera sendera faultType s s'. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; faultType = arch_fault_to_fault_tag af; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q198 receivera sendera faultType s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (tcb_at' sender s \<longrightarrow> ?P239 receivera sendera faultType rv s) \<longrightarrow> s' \<in> ?Q'230 receivera sendera faultType rv} proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 sendBuf. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = None\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?R256 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf) (?R''259 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf) (SKIP # hs) (do a <- return ();
return True
od) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>x1 x2 sendBuf x2a. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = Some x2a\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>a. ?R255 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf a x2a) (?R''257 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf x2a) (SKIP # hs) (do a <- do mapM loadWordUser (map (\<lambda>i. x2a + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]);
return ()
od;
return True
od) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 3. \<And>x1 x2 s. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q198 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>a b. tcb_at' sender b \<longrightarrow> (a = None \<longrightarrow> ?R256 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R255 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 a b x)\<rbrace>
 5. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> empty_fail (lookupIPCBuffer False sender)
 6. \<And>receivera sendera faultType s s'. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; faultType = arch_fault_to_fault_tag af; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q198 receivera sendera faultType s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (tcb_at' sender s \<longrightarrow> (rv = None \<longrightarrow> ?R256 receivera sendera faultType rv s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R255 receivera sendera faultType rv s x)) \<longrightarrow> s' \<in> {s. rv = None \<longrightarrow> s \<in> ?R''259 receivera sendera faultType rv} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''257 receivera sendera faultType rv x}}} proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?R256 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 None) (?R''259 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 None) (SKIP # hs) (return True) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>x1 x2 sendBuf x2a. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = Some x2a\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>a. ?R255 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf a x2a) (?R''257 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf x2a) (SKIP # hs) (do a <- do mapM loadWordUser (map (\<lambda>i. x2a + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]);
return ()
od;
return True
od) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 3. \<And>x1 x2 s. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q198 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>a b. tcb_at' sender b \<longrightarrow> (a = None \<longrightarrow> ?R256 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R255 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 a b x)\<rbrace>
 5. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> empty_fail (lookupIPCBuffer False sender)
 6. \<And>receivera sendera faultType s s'. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; faultType = arch_fault_to_fault_tag af; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q198 receivera sendera faultType s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (tcb_at' sender s \<longrightarrow> (rv = None \<longrightarrow> ?R256 receivera sendera faultType rv s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R255 receivera sendera faultType rv s x)) \<longrightarrow> s' \<in> {s. rv = None \<longrightarrow> s \<in> ?R''259 receivera sendera faultType rv} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''257 receivera sendera faultType rv x}}} proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 s fa. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> ret__unsigned_long_' (global_exn_var_'_update fa (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) true\<rparr>)) = SCAST(32 signed \<rightarrow> 32) true
 2. \<And>x1 x2 s fa. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> globals (ret__unsigned_long_'_update fa s) = globals s
 3. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> wfhandlers (SKIP # hs)
 4. \<And>x1 x2 sendBuf x2a. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = Some x2a\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>a. ?R255 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf a x2a) (?R''257 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 sendBuf x2a) (SKIP # hs) (do a <- do mapM loadWordUser (map (\<lambda>i. x2a + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]);
return ()
od;
return True
od) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 5. \<And>x1 x2 s. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q198 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>a b. tcb_at' sender b \<longrightarrow> (a = None \<longrightarrow> True) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R255 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 a b x)\<rbrace>
 7. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> empty_fail (lookupIPCBuffer False sender)
 8. \<And>receivera sendera faultType s s'. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; faultType = arch_fault_to_fault_tag af; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q198 receivera sendera faultType s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (tcb_at' sender s \<longrightarrow> (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R255 receivera sendera faultType rv s x)) \<longrightarrow> s' \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''257 receivera sendera faultType rv x}}} proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 sendBuf x2a. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = Some x2a\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>a. ?R255 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 (Some x2a) a x2a) (?R''257 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 (Some x2a) x2a) (SKIP # hs) (do y <- mapM loadWordUser (map (\<lambda>i. x2a + i * 4) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]);
return True
od) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>x1 x2 s. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q198 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>a b. tcb_at' sender b \<longrightarrow> (a = None \<longrightarrow> True) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R255 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 a b x)\<rbrace>
 4. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> empty_fail (lookupIPCBuffer False sender)
 5. \<And>receivera sendera faultType s s'. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; faultType = arch_fault_to_fault_tag af; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q198 receivera sendera faultType s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (tcb_at' sender s \<longrightarrow> (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R255 receivera sendera faultType rv s x)) \<longrightarrow> s' \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''257 receivera sendera faultType rv x}}} proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 sendBuf x2a rv. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = Some x2a\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?Q280 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 (Some x2a) x2a rv) (?Q'278 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 (Some x2a) x2a rv) (SKIP # hs) (return True) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>x1 x2 sendBuf x2a s. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = Some x2a\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> mapM loadWordUser (map (\<lambda>i. x2a + i * 4) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>x1 x2 sendBuf x2a. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = Some x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R277 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 (Some x2a) x2a\<rbrace> mapM loadWordUser (map (\<lambda>i. x2a + i * 4) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]) \<lbrace>?Q280 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 (Some x2a) x2a\<rbrace>
 4. \<And>x1 x2 sendBuf x2a. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = Some x2a\<rbrakk> \<Longrightarrow> empty_fail (mapM loadWordUser (map (\<lambda>i. x2a + i * 4) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]))
 5. \<And>x1 x2 s. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q198 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>a b. tcb_at' sender b \<longrightarrow> (a = None \<longrightarrow> True) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R277 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 a x b)\<rbrace>
 7. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> empty_fail (lookupIPCBuffer False sender)
 8. \<And>receivera sendera faultType s s'. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; faultType = arch_fault_to_fault_tag af; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q198 receivera sendera faultType s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (tcb_at' sender s \<longrightarrow> (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R277 receivera sendera faultType rv x s)) \<longrightarrow> s' \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> ?Q280 receivera sendera faultType rv x rva s \<longrightarrow> s' \<in> ?Q'278 receivera sendera faultType rv x rva}}}} proof (prove)
goal (7 subgoals):
 1. \<And>x1 x2 sendBuf x2a s. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = Some x2a\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> mapM loadWordUser (map (\<lambda>i. x2a + i * 4) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>x1 x2 sendBuf x2a. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = Some x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R277 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 (Some x2a) x2a\<rbrace> mapM loadWordUser (map (\<lambda>i. x2a + i * 4) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>x1 x2 sendBuf x2a. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2; sendBuf = Some x2a\<rbrakk> \<Longrightarrow> empty_fail (mapM loadWordUser (map (\<lambda>i. x2a + i * 4) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. msgMaxLength]))
 4. \<And>x1 x2 s. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q198 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>a b. tcb_at' sender b \<longrightarrow> (a = None \<longrightarrow> True) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R277 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) 5 a x b)\<rbrace>
 6. \<And>x1 x2. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault (ARM_H.VMFault x1 x2); af = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> empty_fail (lookupIPCBuffer False sender)
 7. \<And>receivera sendera faultType s s'. \<lbrakk>sender \<noteq> receiver; f = Fault_H.fault.ArchFault af; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; faultType = arch_fault_to_fault_tag af; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' sender and tcb_at' receiver) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q198 receivera sendera faultType s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (tcb_at' sender s \<longrightarrow> (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R277 receivera sendera faultType rv x s)) \<longrightarrow> s' \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> True \<longrightarrow> s' \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace>}}}} proof (prove)
goal:
No subgoals!