Avoid reading out of buffer limits in readWordFromBytes

[zoep]

Description

It adds a check that avoids trying to read a word from a concrete buffer that goes beyond its address space.

Closes #401.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[d-xo]

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.

[msooseth]

Moving this comment to #401

[msooseth]

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.