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