Equivalence fixes

CHANGELOG.md

@@ -39,6 +39,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   so we don't get too large buffers as counterexamples
 - More symbolic overapproximation for Balance and ExtCodeHash opcodes, fixing
   CodeHash SMT representation
+- Add deployment code flag to the `equivalenceCheck` function
 - PNeg + PGT/PGEq/PLeq/PLT simplification rules
 - We no longer dispatch Props to SMT that can be solved by a simplification
 
@@ -57,6 +58,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - CopySlice rewrite rule is now less strict while still being sound
 - Assumptions about reading from buffer after its size are now the same in all cases.
   Previously, they were too weak in case of reading 32 bytes.
+- The equivalence checker now is able to prove that an empty store is
+  equivalent to a store with all slots initialized to 0.
+- Equivalence checking was incorrectly assuming that overapproximated values
+  were sequentially equivalent. We now distinguish these symbolic values with
+  `A-` and `B-`
 
 ## Changed
 - Warnings now lead printing FAIL. This way, users don't accidentally think that

cli/cli.hs

@@ -134,6 +134,7 @@ data Command w
       , maxBranch     :: w ::: Int              <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
       , maxBufSize    :: w ::: Int              <!> "64" <?> "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)"
       , promiseNoReent:: w ::: Bool             <!> "Promise no reentrancy is possible into the contract(s) being examined"
+      , create        :: w ::: Bool             <?> "Tx: creation"
       }
   | Exec -- Execute a given program with specified env & calldata
       { code        :: w ::: Maybe ByteString  <?> "Program bytecode"
@@ -312,7 +313,7 @@ equivalence cmd = do
   cores <- liftIO $ unsafeInto <$> getNumProcessors
   let solverCount = fromMaybe cores cmd.numSolvers
   withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \s -> do
-    (res, e) <- equivalenceCheck s (fromJust bytecodeA) (fromJust bytecodeB) veriOpts calldata
+    (res, e) <- equivalenceCheck s (fromJust bytecodeA) (fromJust bytecodeB) veriOpts calldata cmd.create
     liftIO $ case (any isCex res, any Expr.isPartial e || any isUnknown res) of
       (False, False) -> putStrLn "   \x1b[32m[PASS]\x1b[0m Contracts behave equivalently"
       (True, _)      -> putStrLn "   \x1b[31m[FAIL]\x1b[0m Contracts do not behave equivalently"

src/EVM.hs

@@ -1601,9 +1601,9 @@ freshBufFallback xs = do
   freshVar <- use #freshVar
   assign #freshVar (freshVar + 1)
   let opName = pack $ show $ getOp ?op
-  let freshVarExpr = Var (opName <> "-result-stack-" <> (pack . show) freshVar)
+  let freshVarExpr = Var (opName <> "-result-stack-fresh-" <> (pack . show) freshVar)
   modifying #constraints ((:) (PLEq freshVarExpr (Lit 1) ))
-  let freshReturndataExpr = AbstractBuf (opName <> "-result-data-" <> (pack . show) freshVar)
+  let freshReturndataExpr = AbstractBuf (opName <> "-result-data-fresh-" <> (pack . show) freshVar)
   modifying #constraints ((:) (PLEq (bufLength freshReturndataExpr) (Lit (2 ^ ?conf.maxBufSize))))
   assign (#state % #returndata) freshReturndataExpr
   next >> assign (#state % #stack) (freshVarExpr:xs)
@@ -1617,7 +1617,7 @@ freshVarFallback xs _ = do
   freshVar <- use #freshVar
   assign #freshVar (freshVar + 1)
   let opName = pack $ show $ getOp ?op
-  let freshVarExpr = Var (opName <> "-result-stack-" <> (pack . show) freshVar)
+  let freshVarExpr = Var (opName <> "-result-stack-fresh-" <> (pack . show) freshVar)
   next >> assign (#state % #stack) (freshVarExpr:xs)
 
 forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()
@@ -2962,7 +2962,7 @@ instance VMOps Symbolic where
   pushGas = do
     modifying (#env % #freshGasVals) (+ 1)
     n <- use (#env % #freshGasVals)
-    pushSym $ Expr.Gas n
+    pushSym $ Expr.Gas "" n
   enoughGas _ _ = True
   subGas _ _ = ()
   toGas _ = ()

src/EVM/Format.hs

@@ -29,7 +29,6 @@ module EVM.Format
   , strip0x'
   , hexByteString
   , hexText
-  , bsToHex
   , showVal
   ) where
 
@@ -859,9 +858,6 @@ hexText t =
     Right x -> x
     _ -> internalError $ "invalid hex bytestring " ++ show t
 
-bsToHex :: ByteString -> String
-bsToHex bs = concatMap (paddedShowHex 2) (BS.unpack bs)
-
 showVal :: AbiValue -> Text
 showVal (AbiBytes _ bs) = formatBytes bs
 showVal (AbiAddress addr) = T.pack  . show $ addr

src/EVM/SMT.hs

@@ -82,7 +82,10 @@ instance Monoid CexVars where
 data BufModel
   = Comp CompressedBuf
   | Flat ByteString
-  deriving (Eq, Show)
+  deriving (Eq)
+instance Show BufModel where
+  show (Comp c) = "Comp " <> show c
+  show (Flat b) = "Flat 0x" <> bsToHex b
 
 -- | This representation lets us store buffers of arbitrary length without
 -- exhausting the available memory, it closely matches the format used by
@@ -322,10 +325,10 @@ referencedFrameContext expr = nubOrd $ foldTerm go [] expr
   where
     go :: Expr a -> [(Builder, [Prop])]
     go = \case
-      TxValue -> [(fromString "txvalue", [])]
-      v@(Balance a) -> [(fromString "balance_" <> formatEAddr a, [PLT v (Lit $ 2 ^ (96 :: Int))])]
-      Gas freshVar -> [(fromString ("gas_" <> show freshVar), [])]
-      CodeHash a@(LitAddr _) -> [(fromString "codehash_" <> formatEAddr a, [])]
+      o@TxValue -> [(fromRight' $ exprToSMT o, [])]
+      o@(Balance _) -> [(fromRight' $ exprToSMT o, [PLT o (Lit $ 2 ^ (96 :: Int))])]
+      o@(Gas _ _) -> [(fromRight' $ exprToSMT o, [])]
+      o@(CodeHash (LitAddr _)) -> [(fromRight' $ exprToSMT o, [])]
       _ -> []
 
 referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])]
@@ -443,20 +446,26 @@ declareConstrainAddrs names = SMT2 (["; concrete and symbolic addresses"] <> fma
     assume n = "(assert (bvugt " <> n <> " (_ bv9 160)))"
     cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names }
 
+-- The gas is a tuple of (prefix, index). Within each prefix, the gas is strictly decreasing as the
+-- index increases. This function gets a map of Prefix -> [Int], and for each prefix,
+-- enforces the order
 enforceGasOrder :: [Prop] -> SMT2
-enforceGasOrder ps = SMT2 (["; gas ordering"] <> order indices) mempty mempty
+enforceGasOrder ps = SMT2 (["; gas ordering"] <> (concatMap (uncurry order) indices)) mempty mempty
   where
-    order :: [Int] -> [Builder]
-    order n = consecutivePairs n >>= \(x, y)->
+    order :: TS.Text -> [Int] -> [Builder]
+    order prefix n = consecutivePairs (nubInt n) >>= \(x, y)->
       -- The GAS instruction itself costs gas, so it's strictly decreasing
-      ["(assert (bvugt gas_" <> (fromString . show $ x) <> " gas_" <> (fromString . show $ y) <> "))"]
+      ["(assert (bvugt " <> fromRight' (exprToSMT (Gas prefix x)) <> " " <>
+        fromRight' ((exprToSMT (Gas prefix y))) <> "))"]
     consecutivePairs :: [Int] -> [(Int, Int)]
     consecutivePairs [] = []
     consecutivePairs l = zip l (tail l)
-    indices :: [Int] = nubInt $ concatMap (foldProp go mempty) ps
-    go :: Expr a -> [Int]
+    indices = Map.toList $ toMapOfLists $ concatMap (foldProp go mempty) ps
+    toMapOfLists :: [(TS.Text, Int)] -> Map.Map TS.Text [Int]
+    toMapOfLists = foldr (\(k, v) acc -> Map.insertWith (++) k [v] acc) Map.empty
+    go :: Expr a -> [(TS.Text, Int)]
     go e = case e of
-      Gas freshVar -> [freshVar]
+      Gas prefix v -> [(prefix, v)]
       _ -> []
 
 declareFrameContext :: [(Builder, [Prop])] -> Err SMT2
@@ -872,8 +881,8 @@ exprToSMT = \case
     pure $ "(store" `sp` encPrev `sp` encIdx `sp` encVal <> ")"
   SLoad idx store -> op2 "select" store idx
   LitAddr n -> pure $ fromLazyText $ "(_ bv" <> T.pack (show (into n :: Integer)) <> " 160)"
-  Gas freshVar -> pure $ fromLazyText $ "gas_"  <> (T.pack $ show freshVar)
   CodeHash a@(LitAddr _) -> pure $ fromLazyText "codehash_" <> formatEAddr a
+  Gas prefix var -> pure $ fromLazyText $ "gas_" <> T.pack (TS.unpack prefix) <> T.pack (show var)
 
   a -> internalError $ "TODO: implement: " <> show a
   where
@@ -1060,14 +1069,12 @@ parseBlockCtx "prevrandao" = PrevRandao
 parseBlockCtx "gaslimit" = GasLimit
 parseBlockCtx "chainid" = ChainId
 parseBlockCtx "basefee" = BaseFee
-parseBlockCtx gas | TS.isPrefixOf (TS.pack "gas_") gas = Gas (textToInt $ TS.drop 4 gas)
 parseBlockCtx val = internalError $ "cannot parse '" <> (TS.unpack val) <> "' into an Expr"
 
 parseTxCtx :: TS.Text -> Expr EWord
 parseTxCtx name
   | name == "txvalue" = TxValue
   | Just a <- TS.stripPrefix "balance_" name = Balance (parseEAddr a)
-  | Just a <- TS.stripPrefix "gas_" name = Gas (textToInt a)
   | Just a <- TS.stripPrefix "codehash_" name = CodeHash (parseEAddr a)
   | otherwise = internalError $ "cannot parse " <> (TS.unpack name) <> " into an Expr"
 

src/EVM/Solidity.hs

@@ -50,7 +50,7 @@
 import Control.Applicative
 import Control.Monad
 import Control.Monad.IO.Unlift
 import Data.Aeson hiding (json)
 import Data.Aeson.Types
 import Data.Aeson.Optics
 import Data.Aeson.Key qualified as Key
@@ -394,6 +394,7 @@
       Just (Contracts sol, _, _) -> pure $ Map.lookup ("hevm.sol:" <> contract) sol <&> (.runtimeCode)
       Nothing -> internalError $ "unable to parse solidity output:\n" <> (T.unpack json)
 
+
 functionAbi :: Text -> IO Method
 functionAbi f = do
   json <- solc Solidity ("contract ABI { function " <> f <> " public {}}")

src/EVM/Solvers.hs

@@ -107,7 +107,7 @@ checkMulti (SolverGroup taskQueue) smt2 multiSol = do
     -- collect result
     readChan resChan
 
-checkSatWithProps :: App m => SolverGroup -> [Prop] ->m (CheckSatResult, Err SMT2)
+checkSatWithProps :: App m => SolverGroup -> [Prop] -> m (CheckSatResult, Err SMT2)
 checkSatWithProps (SolverGroup taskQueue) props = do
   conf <- readConfig
   let psSimp = simplifyProps props