hevm equivalence does not check log equivalence

[charles-cooper]

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]

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]

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.