Practical Memory Limit is 32bits ?

[DavePearce]

The main points:

• (Actual) The translation of sequences in Dafny is limited to 32bits (e.g. 2^32) because (presumably) it uses an array under the hood (and Java's arrays are similarly limited). See #2859

• (Enforced) Currently, memory is limited to 256bits through Dafny verification. However, from a verification perspective, such a limit is not even required (see Remove Redundant Memory Checks #250). But, in practice, some of the GeneralStateTests push up to that limit (e.g. vmLogTests/log0).

This means the "verified" EVM can crash at runtime when memory is expanded beyond 32bits.

[DavePearce]

There are some possible options here. We could support an effective array upto 64bits, for example. Or, just impose a limit on usable memory, beyond which its just always zero.

[DavePearce]

Should we file a Dafny bug for this? I couldn't find anything there after a quick look.