Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Equivalence checking does not treat empty store as equal to a store initialized to zero #647

Open
zoep opened this issue Feb 7, 2025 · 2 comments · May be fixed by #650
Open

Equivalence checking does not treat empty store as equal to a store initialized to zero #647

zoep opened this issue Feb 7, 2025 · 2 comments · May be fixed by #650

Comments

@zoep
Copy link
Collaborator

zoep commented Feb 7, 2025

By convention, an empty store is a store whose all values are initialized to zero. However, this is not implemented in the equivalence checker, resulting in the counterexamples shown below.

This snippet creates two endstates, one with an empty store and one with a store with slot 0 set to value 0. According to the semantics of Expr these to should be equivalent. However, running the equivalence checker returns a counterexample.

{-# LANGUAGE OverloadedStrings, RecordWildCards #-}

import EVM.Types
import EVM.Expr
import EVM.Solvers
import EVM.SymExec
import EVM.Effects hiding (Env)

import Data.Map as M

-- helper for runnning equivalenceCheck' from the repl
testEquiv :: [Expr End] -> [Expr End] -> IO ()
testEquiv end1 end2 = do
  res <- runEnv defaultEnv $ withSolvers Z3 1 1 Nothing $ \solvers -> equivalenceCheck' solvers end1 end2
  putStrLn (show res)

exp1 :: Expr Storage
exp1 = (ConcreteStore $ M.fromList [])

exp2 :: Expr Storage
exp2 = (ConcreteStore $ M.fromList [(0x0,0x0)])

code :: ContractCode
code = (RuntimeCode (ConcreteRuntimeCode ""))

trace :: TraceContext
trace = TraceContext { traces = [], contracts = M.empty, labels = M.empty }

c1 :: Expr EContract
c1 = (C code exp1 (ConcreteStore (M.fromList [])) (Lit 0) Nothing)

c2 :: Expr EContract
c2 = (C code exp2 (ConcreteStore (M.fromList [])) (Lit 0) Nothing)

endState1 :: Expr End
endState1 = Success [] trace (ConcreteBuf "") (M.fromList [(SymAddr "entry", c1)])

endState2 :: Expr End
endState2 = Success [] trace (ConcreteBuf "") (M.fromList [(SymAddr "entry", c2)])

Then in the repl, we can show that endState1 and endState2 are not equivalent (though they should be)

> cabal repl test
ghci> :load test
[1 of 2] Compiling Main             ( test.hs, interpreted )
ghci> testEquiv [endState1] [endState2]
Found 1 total pairs of endstates

Asking the SMT solver for 1 pairs
Reuse of previous queries was Useful in 0 cases
[Cex (SMTCex {vars = fromList [(TxValue,0x0)], addrs = fromList [], buffers = fromList [], store = fromList [], blockContext = fromList [], txContext = fromList []})]

That does not allow us to prove the following two contracts equivalent:

contract C {
  uint x;
  // constructor is implicit
 }
contract C {
  uint x;
  constructor() {
    x = 0;
  }
}

I have a branch in which I have pushed a fix for the first code snippet. I have added the second example to the test suite and I have modified equivalenceCheck to be able to run on deployment code as well as runtime code. However, I'm running into a weird error (Exception: Internal Error: cannot analyze symbolic code:). Any help will be appreciated!
@zoep zoep changed the title Equivalence checking does not treat emptystore as equal to a store initialized to zero Equivalence checking does not treat empty store as equal to a store initialized to zero Feb 7, 2025
@msooseth
Copy link
Collaborator

msooseth commented Feb 7, 2025

Oh wow, thanks, I'll have a look at this first thing on Monday!

@zoep zoep linked a pull request Feb 10, 2025 that will close this issue
Open
4 tasks
@msooseth
Copy link
Collaborator

BTW, I actually made progress on this. It needs to be completed, if you wanna take a peek, it's at equiv-fix-mate, The props from the init need to be used as preconditions for the deployed bytecode. They show up as warnings in that branch.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix in equivalence checking ethereum/hevm
2 participants
@zoep @msooseth