writeAtMost allows for more static bounds check merging using rules,
at the risk of wasting some buffer space.