Solc 0.8.18: Added optimization rule and(shl(X, Y), shl(X, Z)) => shl(X, and(Y, Z))

[barakman]

This is either a documentation issue or a real bug.

I have not verified this is a bug, only read it in the release notes of solc 0.8.18.

So it is possibly just a documentation issue (either incorrect documentation or my incorrect understanding of it).

Yet, I wanted to point that to your immediate attention:

A quick check reveals that for X = 1, Y = 0, Z = 1:

• The LHS and(shl(X, Y), shl(X, Z)) evaluates to 0
• The RHS shl(X, and(Y, Z)) evaluates to 1

[ekpyron]

with X = 1, Y = 0, Z = 1, it holds that

and(shl(X, Y), shl(X, Z)) =
and(shl(1, 0), shl(1, 1)) =
and(0, 2) = 0

shl(X, and(Y, Z)) =
shl(1, and(0, 1)) =
shl(1, 0) = 0

Note that the argument order for shifts is (not our fault, it's like that on the EVM level) shl(shiftAmount, value).

We do have SMT-based formal proofs about the correctness of these rules, so they're not likely to be incorrect. But to me this doesn't look like a bug in the documentation/changelog either, but rather a misunderstanding about the arguments of the opcodes.

Hence I'm closing this issue, but feel free to reopen, if you think this is an issue after all!