spec: document checked-writes-yields-safe-reads methodology

[erik-3milabs]

Throughout the spec, it is assumed that memory-reads do not have to be range checked (neither value, nor address), based on the assumption that

1. all memory-writes are range checked (both address and value), and
2. if the LogUp will not balance when values are read from out-of-bound addresses / out of range values are read.

This technique does not seem to be documented anywhere in the specification.