hevm equivalence reports no discrepancies on two bytecodes that compute different values

[konnov]

Hi! Perhaps I am expecting too much of hevm. I feed it two bytecodes: One computes a value via SAR, and another one computes a value via SDIV. They do compute slightly different values, but hevm reports no discrepancies.

$ cat bytecode1
7fe7f7981242e0f50016a573e27a65b63c8fd75305b4b504a70fd5c21f7d9ea4fd60161d
$ cat bytecode2
7fe7f7981242e0f50016a573e27a65b63c8fd75305b4b504a70fd5c21f7d9ea4fd7f00000000000000000000000000000000000000000000000000000000004000009005
$ hevm equivalence --code-a `cat bytecode1` --code-b `cat bytecode2`
Found 1 total pairs of endstates
Asking the SMT solver for 1 pairs
Reuse of previous queries was Useful in 0 cases
No discrepancies found

When I run the two bytecodes on evm.codes, they compute two different values. This behavior seems to be consistent with bitwise_sar and sdiv of EELS.

[msooseth]

Thanks! Definitely reproducible on main. However:

cabal run exe:hevm equivalence -- --code-a "7f" --code-b "7fe7"

Also reports equivalent. But:

cabal run exe:hevm equivalence -- --code-a "600060015260406000f3" --code-b "600a60015260406000f3"

Reports fail. There reason for this is that we compare what would happen when the contract is called. The contract you put forth doesn't return a value.

If I add an MSTORE&RETURN to your bytecodes, we get:

cabal run exe:hevm equivalence -- --code-a "7fe7f7981242e0f50016a573e27a65b63c8fd75305b4b504a70fd5c21f7d9ea4fd60161d60205260406000f3" --code-b "7fe7f7981242e0f50016a573e27a65b63c8fd75305b4b504a70fd5c21f7d9ea4fd7f0000000000000000000000000000000000000000000000000000000000400000900560205260406000f3"
[...]
Asking the SMT solver for 1 pairs
   [FAIL] Contracts do not behave equivalently

Not equivalent. The following inputs result in differing behaviours:
-----
Calldata:
  Empty

The two bytecodes are now:

PUSH32 0xe7f7981242e0f50016a573e27a65b63c8fd75305b4b504a70fd5c21f7d9ea4fd
PUSH1 0x16
SAR
PUSH1 0x20
MSTORE
PUSH1 0x40
PUSH1 0x00
RETURN

And

PUSH32 0xe7f7981242e0f50016a573e27a65b63c8fd75305b4b504a70fd5c21f7d9ea4fd
PUSH32 0x0000000000000000000000000000000000000000000000000000000000400000
SWAP1
SDIV
PUSH1 0x20
MSTORE
PUSH1 0x40
PUSH1 0x00
RETURN

Where all I did was add:

PUSH1 0x20
MSTORE
PUSH1 0x40
PUSH1 0x00
RETURN

to both.

Note that we also distinguish when the return is empty but there is a difference in success/fail:

cabal run exe:hevm equivalence -- --code-a "60006000f3" --code-b "60006000fd"

Where these are respectively:

PUSH1 0x00
PUSH1 0x00
RETURN

And:

PUSH1 0x00
PUSH1 0x00
REVERT

To be honest, we probably should explain this better in our documentation at hevm.dev. Let me know if the above explains the rationale why we consider the two equivalent. And let me keep this issue open so (1) you can respond, I'm curious what you think, and (2) so I can improve our documentation.

[konnov]

@msooseth your explanation definitely makes sense to me! Having read it, I am not sure what kind of equivalence I had in mind. It would definitely be great to see an explanation of what it means for two contracts to be equivalent. In addition to the return value or revert cause, I would probably expect equal storage contents on successful return, but it's probably not so easy to verify.

[msooseth]

Actually, storage is also checked, sorry, that's good point I forgot! I'll add that to the docs, too. Sorry about that.

[msooseth]

I am closing, and following through #690 -- I would be very grateful if you could take a peek at that PR and give me your opinion! I wanna make this tool more accessible :)