Expr: sound disjointness rule for readWord/WriteWord with bounded offset

[msooseth]

Summary

Adds a new readWord clause that elides a WriteWord whose offset is of the form Add (Lit c) X, when X has a derivable static upper bound and the write region is provably disjoint from the read in EVM (mod 2^256) arithmetic.

• New helper upperBound :: Expr EWord -> Maybe W256 — conservative static upper bound handling Lit, And-with-Lit, Mod-by-Lit, Div-by-Lit, Mul/Add with one Lit operand, and SHR by a Lit shift.
• New helper writeDisjointFromReadWord :: W256 -> Expr EWord -> Bool — uses Integer arithmetic to detect wrap on both the read and write byte ranges before concluding the write can be skipped, so the rule does not assume non-wrapping addition.
• Hook in readWord at the WriteWord case.

Split out from #1063 so the disjointness rule is reviewable on its own; #1063 will be rebased on top of this.

Tests

5 new unit tests in test/EVM/Expr/ExprTests.hs:

• positive: WriteWord at Add(Lit, And-bounded) skipped
• positive: WriteWord at Add(Lit, Mul-And-bounded) skipped
• negative: unbounded X — not skipped
• negative: wrap-risk near maxBound — not skipped
• negative: read region overlaps write min offset — not skipped

Checklist

• tested locally
• added automated tests
• updated the docs — N/A, internal simplifier rule
• updated the changelog

🤖 Generated with Claude Code

[blishko]

Looks good!

I am suggesting one small change that I think makes the condition more readable.

[blishko]

Suggested change

	&& (cI >= iI + 32 || writeMaxI < iI)
	&& (cI > readMaxI || writeMaxI < iI)

[msooseth]

Wait, doesn't that modify the code?

readMaxI  = iI + 31

But you also changed >= to > ?

[blishko]

Yes.
readMaxI = iI + 31 means you can rewrite cI > readMaxI as cI > iL + 31and that's equivalent to cI >= iL + 32, which is you original expression, no?