Inter-process buffers in separation logic with rely-guarantee