Two simplifications that will be needed to deal with @zoep's issues regarding initcode equivalence

[msooseth]

Description

One more simplification of readByte. This one works ALSO when CopySlice is not called with a Lit as a srcOffset. So it's more general, but cannot simplify some of the things that the more specific one can. It definitely helps in some cases, as per Zoe's issue

Note that the SMT overflow vs how the EVM actually works is slightly different on CopySlice. We need this rewrite rule, but it means that in some cases, the SMT will differ from the simplification system, when writing to extremely large offsets -- which always leads to over-gas-limit, so it's not a relevant case. However, the rewrite rule actually triggers, in real-world scenarios, and is useful.

NOTE: this is a cherry-pick from Zoe's changeset so it will apply perfectly when this is merged, appearing as less of a changeset for Zoe's PR.

Checklist

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

[blishko]

The simplification is sound, but only if writing to a buffer does not overflow.
In that case we have a conflict between the SMT semantics and EVM semantics.
I guess we have agreed to ignore this weird edge case, right?

[blishko]

Also, there seem to be some test failures on windows:

FAIL
      Exception: Maybe.fromJust: Nothing
      CallStack (from HasCallStack):
        error, called at libraries\base\Data\Maybe.hs:150:21 in base:Data.Maybe
        fromJust, called at test\EVM\Test\Tracing.hs:880:30 in hevm-0.54.2-inplace-test:EVM.Test.Tracing
      Use -p '/calldata-wraparound-1/' to rerun this test only.
    calldata-wraparound-2:                                        Error converting trace! exit code:ExitFailure 127

[msooseth]

The windows build issue is unrelated, unfortunately. It's occurring here too:

https://github.com/ethereum/hevm/actions/runs/13283178489/job/37085893025

which is also unrelated. I'll merge this even if Windows is broken, and I have already asked the Echidna folks to look into the Windows issue. I think it's something small, or at least I'm hoping :) Probably some shell script thing.

But I do wanna make sure the other things are OK :)

[msooseth]

The simplification is sound, but only if writing to a buffer does not overflow. In that case we have a conflict between the SMT semantics and EVM semantics. I guess we have agreed to ignore this weird edge case, right?

Yep, we did :)

[msooseth]

@blishko beware -- I added the same simplification to readWord as well, which I now noticed is missing.

[blishko]

Maybe you should also add a test for the ReadWord simplification?

[msooseth]

Maybe you should also add a test for the ReadWord simplification?

Yes.. sorry. I just added two :)

[blishko]

LGTM!