As discussed in chat: our smt encoding does not match geth (or even our own concrete semantics) if the index being read from memory is > 2^64. In this situation geth always returns zero (matching the behaviour of readWord on main, but our smt semantics will read data from any index.

The easiest short term fix is probably to constrain BufLength <= 2^64 for all buffers, and update readWord to return 0 for indexes greater than 2^64. longer term we might benefit from encoding bufs as an array with a 64 but address space.

Moving this comment to #401

our smt encoding does not match geth (or even our own concrete semantics) if the index being read from memory is > 2^64. In this situation geth always returns zero

While that's true, geth's behaviour is basically undefined for such large idx. The behaviour mentioned above is guarded by a check that the idx is <2^64. When asked, the geth developers said that it doesn't deal with that large indexes, that's gas-out anyway. So I don't know if we should rely on geth's behaviour here.

This is related to #401 where this is explained in a bit more detail.

This has finally been experimented with and partially fixed, with the fuzzer fix as the last resort. Closing.