MSIZE after access to offset 2^256-1

[ekpyron]

If I see that correctly, then after MSTORE or MLOAD to 2^256-1 (no prior memory writes), μ_i' will be set to max(0,ceil(2^256 - 1 + 32)÷32)), where the addition is specifically excluded from modulo arithmetic. That's 2^251+1.

Now the next MSIZE will return 32μ_i with arithmetic modulo 2^256 - that's 32.

Wouldn't the more reasonable value be 2^256-1?

This is a rather academic corner case, since no client will implement this case, since it will always run out of gas anyways - but we are implementing an EVM interpreter for fuzzing the optimizer of the solidity compiler, which is used to check for execution trace equivalence without considering gas and thereby noticed this oddity (ethereum/solidity#7342). What do you think about changing this in the yellow paper?

[acoglio]

I haven't studied this part of the YP in detail yet, but it looks like perhaps the specifications of MLOAD and MSTORE should use min(µ_s[0] + 32, 2²⁵⁶) instead of (µ_s[0] + 32). That is, if µ_s[0] + 32 exceeds 2²⁵⁶, and the 32 bytes starting at µ_s[0] "wrap around" to memory locations 0 etc., we want to count all 2²⁵⁶ bytes of memory as used: the min operation caps the number of used bytes at 2²⁵⁶. Then we should have the invariant µ_i ≤ 2²⁵¹.

There would still be a bit of a problem with MSIZE when all 2²⁵⁶ memory bytes are used, because in this case µ_i = 2²⁵¹ and 32µ_i = 2²⁵⁶, which doesn't fit into a word. Perhaps returning 2²⁵⁶-1 is the best we can do in this case, but it would have to be a special case. In all other cases, MSIZE returns a multiple of 32.

(MSTORE8 looks unproblematic because, given the expected invariant µ_s[0] < 2²⁵⁶, i.e. that µ_s[0] is a word, we have µ_s[0] + 1 ≤ 2²⁵⁶.)

[ekpyron]

I would actually have been fine with µ_i exceeding 2^251 and consequently have the gas calculation be "as if memory was extended beyond 2^256" instead of just considering all 2^256 bytes used - and then just define MSIZE as "32µi, if µ_i < 2^251 and 2^256-1 otherwise", but maybe you're right and it might be even cleaner to cap µi itself, I'm not entirely sure - I haven't spent too much time looking into it myself.

[acoglio]

Maybe we can wait a few more days to see if anybody else has comments on this issue, and then we can make a decision on how to proceed with editing the YP?

[axic]

Any decision yet? 😉

[acoglio]

Looking at this again, I still stand by my proposal above. @ekpyron what do you think? If you agree, I can make a PR with the proposed change, leave it there for a few days, and eventually merge.

[ekpyron]

@acoglio Yes, your proposal still sounds like a fine solution to me!

[acoglio]

Thanks. I just made the PR -- #775