MSIZE after access to offset ``2^256-1``
ekpyron opened this issue · 7 comments
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?
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, 2256) instead of (µs[0] + 32). That is, if µs[0] + 32 exceeds 2256, and the 32 bytes starting at µs[0] "wrap around" to memory locations 0 etc., we want to count all 2256 bytes of memory as used: the min operation caps the number of used bytes at 2256. Then we should have the invariant µi ≤ 2251.
There would still be a bit of a problem with MSIZE when all 2256 memory bytes are used, because in this case µi = 2251 and 32µi = 2256, which doesn't fit into a word. Perhaps returning 2256-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] < 2256, i.e. that µs[0] is a word, we have µs[0] + 1 ≤ 2256.)
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.
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?
Any decision yet? 😉