ethereum / hevm

symbolic EVM evaluator
https://hevm.dev
GNU Affero General Public License v3.0
235 stars 48 forks source link

`hevm equivalence` does not check log equivalence #586

Open charles-cooper opened 1 month ago

charles-cooper commented 1 month ago

per title. an example

diff --git a/examples/tokens/ERC20.vy b/examples/tokens/ERC20.vy
index 2d70fd670..73065bcb4 100644
--- a/examples/tokens/ERC20.vy
+++ b/examples/tokens/ERC20.vy
@@ -120,7 +120,7 @@ def _burn(_to: address, _value: uint256):
     assert _to != empty(address)
     self.totalSupply -= _value
     self.balanceOf[_to] -= _value
-    log IERC20.Transfer(_to, empty(address), _value)
+    log IERC20.Transfer(empty(address), _to, _value)

(pulled from https://github.com/vyperlang/vyper/blob/c02d2d8c5ed8c904c31b7f3f937ab01781fc9891/examples/tokens/ERC20.vy)

results in hevm equivalence reporting

Found 3969 total pairs of endstates
Asking the SMT solver for 1120 pairs
Reuse of previous queries was Useful in 0 cases
No discrepancies found
msooseth commented 1 month ago

We are "fixing" this via #590 -- defining what it means to be "equivalent". Logs are explicitly excluded. However, maybe they should be included.... I'll keep this open, so we can discuss whether they should be included, instead.

charles-cooper commented 4 weeks ago

i think it makes sense to add logs to the definition of equivalence (bandwidth permitting). they affect the state root (iirc), and applications depend on them for semantics. a non-equivalent log (like in the example) might not affect the smart contract semantics directly, but it can affect the behavior of downstream applications.