Paper "Super-optimization of Smart Contracts" Appx. D may contain an incorrect rewrite rule

[msooseth]

Appendix D of Super-optimization of Smart Contracts, rule 10 says: DIV(x, x) = 1 -- this is actually sadly not true in EVM as far as I understand. When x is zero, that value is actually 0, not 1. It can be checked here. Maybe this rule has a check that x must never be zero, so it may still be correct when applied in the code, but as it is stated in the paper I believe it may be incorrect. Unfortunately I couldn't find where this rule is applied in the code of gasol-opimizer so I couldn't verify how it's actually applied :S Sorry.

I hope the above helps,

Mate

[tutugordillo]

Hi Mate! Thank you for the interest :-)
Yes, it's checked because first it tries to apply DIV(0,X) = 0 or DIV(X,0) = 0 and, after that, it checks DIV(X,X) so in case X =0 it applies always DIV(X,0) rule instead of DIV(X,X).

[msooseth]

Ah, cool! And what if they are both symbolic? So let's say it's some:

DIV((SLOAD a) (SLOAD a))

Then the DIV(0, x) would not apply. Would it apply the DIV(x,x) rule in this case? Because the SLOAD a could be zero here I think? Or maybe it can never encounter this kind of symbolic expression?

[msooseth]

BTW, I stole your other rules 😄 They are very cool, especially the IsZero rules we were definitely missing!

ethereum/hevm#463

[alexcere]

Hi Mate,

Thanks once again for flagging the rule issue! You're right—we missed considering cases where symbolic expressions could represent zero values. In those cases, we shouldn't apply the rewrite rule. We'll fix it.

Glad to hear the rules are proving useful :)