fix incorrect mask computation in setting high 128-bit word in write_raw()

There was a latent bug here wherein a call to write_raw() with a handle whose
offset was non-zero and whose aligned width was > 128 bits would trample some
neighbouring bits in the state vector. This bug could not actually be hit
because the maximum aligned handle read is presently 72 bits, but further
extensions would have run into problems here. This issue was only uncovered by a
failure in the write_raw() proof, that is also adjusted in this commit.