Atomic writes to a buffer

A value Write n io denotes the write of n bytes to a buffer. The
actual write is executed by calling io with a pointer pf to the first
free byte that the write should start with. Note that the caller of io pf
must ensure that n bytes are free starting from pf.

Writes are atomic. This means that the written data cannot be wrapped
over buffer boundaries as it can be done for builders. For writes it holds
that either the buffer has enough free space and the write can proceed or a
new buffer with a size larger or equal to the number of bytes to write has
to be allocated.

Moreover, for a Write, the size of the data to be written must be known
before the data can be written. Hence, if this size is data-dependent, the
control flow becomes complicated: first, all data must be forced and stored,
then the size check happens, and only afterwards the stored data can be
written. Therefore, because of cache misses, composing writes with
data-dependent size computations may actually be slower than combining the
resulting builders. Use benchmarking to make informed decisions.