Update hevm to 0.53.0

flake.nix

@@ -51,15 +51,15 @@
           pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
             owner = "ethereum";
             repo = "hevm";
-            rev = "release/0.52.0";
-            sha256 = "sha256-LCv3m6AbLr9mV7pHj7r08dzsg1UVpQDn0zyJXbzRS2Q=";
+            rev = "release/0.53.0";
+            sha256 = "sha256-/B+McCJBcIxYCmYMcJ5FiwMqPeSCL97WbNusabTUb34=";
         }) { secp256k1 = pkgs.secp256k1; });
 
         # FIXME: figure out solc situation, it conflicts with the one from
         # solc-select that is installed with slither, disable tests in the meantime
         echidna = pkgs: pkgs.haskell.lib.dontCheck (
           with pkgs; lib.pipe
-          (haskellPackages.callCabal2nix "echidna" ./. { inherit (hevm pkgs); })
+          (haskellPackages.callCabal2nix "echidna" ./. { hevm = hevm pkgs; })
           [
             (haskell.lib.compose.addTestToolDepends [ haskellPackages.hpack slither-analyzer solc ])
             (haskell.lib.compose.disableCabalFlag "static")

lib/Echidna.hs

@@ -49,7 +49,7 @@ prepareContract
   -> NonEmpty FilePath
   -> Maybe ContractName
   -> Seed
-  -> IO (VM RealWorld, World, GenDict)
+  -> IO (VM Concrete RealWorld, World, GenDict)
 prepareContract env solFiles specifiedContract seed = do
   let solConf = env.cfg.solConf
       contracts = Map.elems env.dapp.solcByName

lib/Echidna/Campaign.hs

@@ -28,7 +28,7 @@ import System.Random (mkStdGen)
 
 import EVM (cheatCode)
 import EVM.ABI (getAbi, AbiType(AbiAddressType), AbiValue(AbiAddress))
-import EVM.Types hiding (Env, Frame(state))
+import EVM.Types hiding (Env, Frame(state), Gas)
 
 import Echidna.ABI
 import Echidna.Exec
@@ -63,7 +63,7 @@ isSuccessful =
 -- contain minized corpus without sequences that didn't increase the coverage.
 replayCorpus
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m)
-  => VM RealWorld -- ^ VM to start replaying from
+  => VM Concrete RealWorld -- ^ VM to start replaying from
   -> [(FilePath, [Tx])] -- ^ corpus to replay
   -> m ()
 replayCorpus vm txSeqs =
@@ -85,7 +85,7 @@ runWorker
   :: (MonadIO m, MonadThrow m, MonadReader Env m)
   => StateT WorkerState m ()
   -- ^ Callback to run after each state update (for instrumentation)
-  -> VM RealWorld -- ^ Initial VM state
+  -> VM Concrete RealWorld -- ^ Initial VM state
   -> World   -- ^ Initial world state
   -> GenDict -- ^ Generation dictionary
   -> Int     -- ^ Worker id starting from 0
@@ -187,9 +187,9 @@ randseq deployedContracts world = do
 -- minimized. Stores any useful data in the campaign state if coverage increased.
 callseq
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m)
-  => VM RealWorld
+  => VM Concrete RealWorld
   -> [Tx]
-  -> m (VM RealWorld)
+  -> m (VM Concrete RealWorld)
 callseq vm txSeq = do
   env <- ask
   -- First, we figure out whether we need to execute with or without coverage
@@ -261,7 +261,7 @@ callseq vm txSeq = do
   -- know the return type for each function called. If yes, tries to parse the
   -- return value as a value of that type. Returns a 'GenDict' style Map.
   returnValues
-    :: [(Tx, VMResult RealWorld)]
+    :: [(Tx, VMResult Concrete RealWorld)]
     -> (FunctionName -> Maybe AbiType)
     -> Map AbiType (Set AbiValue)
   returnValues txResults returnTypeOf =
@@ -280,7 +280,7 @@ callseq vm txSeq = do
         _ -> Nothing
 
   -- | Add transactions to the corpus discarding reverted ones
-  addToCorpus :: Int -> [(Tx, (VMResult RealWorld, Gas))] -> Corpus -> Corpus
+  addToCorpus :: Int -> [(Tx, (VMResult Concrete RealWorld, Gas))] -> Corpus -> Corpus
   addToCorpus n res corpus =
     if null rtxs then corpus else Set.insert (n, rtxs) corpus
     where rtxs = fst <$> res
@@ -289,8 +289,8 @@ callseq vm txSeq = do
 -- executed, saving the transaction if it finds new coverage.
 execTxOptC
   :: (MonadIO m, MonadReader Env m, MonadState WorkerState m, MonadThrow m)
-  => VM RealWorld -> Tx
-  -> m ((VMResult RealWorld, Gas), VM RealWorld)
+  => VM Concrete RealWorld -> Tx
+  -> m ((VMResult Concrete RealWorld, Gas), VM Concrete RealWorld)
 execTxOptC vm tx = do
   ((res, grew), vm') <- runStateT (execTxWithCov tx) vm
   when grew $ do
@@ -305,7 +305,7 @@ execTxOptC vm tx = do
 -- | Given current `gasInfo` and a sequence of executed transactions, updates
 -- information on highest gas usage for each call
 updateGasInfo
-  :: [(Tx, (VMResult RealWorld, Gas))]
+  :: [(Tx, (VMResult Concrete RealWorld, Gas))]
   -> [Tx]
   -> Map Text (Gas, [Tx])
   -> Map Text (Gas, [Tx])
@@ -326,10 +326,10 @@ updateGasInfo ((t, _):ts) tseq gi = updateGasInfo ts (t:tseq) gi
 -- known solves.
 evalSeq
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m)
-  => VM RealWorld -- ^ Initial VM
-  -> (VM RealWorld -> Tx -> m (result, VM RealWorld))
+  => VM Concrete RealWorld -- ^ Initial VM
+  -> (VM Concrete RealWorld -> Tx -> m (result, VM Concrete RealWorld))
   -> [Tx]
-  -> m ([(Tx, result)], VM RealWorld)
+  -> m ([(Tx, result)], VM Concrete RealWorld)
 evalSeq vm0 execFunc = go vm0 [] where
   go vm executedSoFar toExecute = do
     -- NOTE: we do reverse here because we build up this list by prepending,
@@ -369,8 +369,8 @@ runUpdate f = do
 -- Then update accordingly, keeping track of how many times we've tried to solve or shrink.
 updateTest
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m)
-  => VM RealWorld
-  -> (VM RealWorld, [Tx])
+  => VM Concrete RealWorld
+  -> (VM Concrete RealWorld, [Tx])
   -> EchidnaTest
   -> m (Maybe EchidnaTest)
 updateTest vmForShrink (vm, xs) test = do

lib/Echidna/Deploy.hs

@@ -25,16 +25,16 @@ deployContracts
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
   => [(Addr, SolcContract)]
   -> Addr
-  -> VM RealWorld
-  -> m (VM RealWorld)
+  -> VM Concrete RealWorld
+  -> m (VM Concrete RealWorld)
 deployContracts cs = deployBytecodes' $ map (\(a, c) -> (a, c.creationCode)) cs
 
 deployBytecodes
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
   => [(Addr, Text)]
   -> Addr
-  -> VM RealWorld
-  -> m (VM RealWorld)
+  -> VM Concrete RealWorld
+  -> m (VM Concrete RealWorld)
 deployBytecodes cs = deployBytecodes' $
   (\(a, bc) ->
     (a, fromRight (error ("invalid b16 decoding of: " ++ show bc)) $ BS16.decode $ encodeUtf8 bc)
@@ -45,8 +45,8 @@ deployBytecodes'
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
   => [(Addr, ByteString)]
   -> Addr
-  -> VM RealWorld
-  -> m (VM RealWorld)
+  -> VM Concrete RealWorld
+  -> m (VM Concrete RealWorld)
 deployBytecodes' cs src initialVM = foldM deployOne initialVM cs
   where
   deployOne vm (dst, bytecode) = do

lib/Echidna/Etheno.hs

@@ -121,7 +121,7 @@ matchSignatureAndCreateTx _ _ = []
 
 -- | Main function: takes a filepath where the initialization sequence lives and returns
 -- | the initialized VM along with a list of Addr's to put in GenConf
-loadEthenoBatch :: Bool -> FilePath -> IO (VM RealWorld)
+loadEthenoBatch :: Bool -> FilePath -> IO (VM Concrete RealWorld)
 loadEthenoBatch ffi fp = do
   bs <- eitherDecodeFileStrict fp
   case bs of
@@ -132,7 +132,7 @@ loadEthenoBatch ffi fp = do
       vm <- stToIO $ initialVM ffi
       execStateT initVM vm
 
-initAddress :: MonadState (VM s) m => Addr -> m ()
+initAddress :: MonadState (VM Concrete s) m => Addr -> m ()
 initAddress addr = do
   cs <- gets (.env.contracts)
   if LitAddr addr `member` cs then pure ()
@@ -144,8 +144,8 @@ initAddress addr = do
         & set #balance (Lit 100000000000000000000) -- default balance for EOAs in etheno
 
 crashWithQueryError
-  :: (MonadState (VM s) m, MonadFail m, MonadThrow m)
-  => Query s
+  :: (MonadState (VM Concrete s) m, MonadFail m, MonadThrow m)
+  => Query Concrete s
   -> Etheno
   -> m ()
 crashWithQueryError q et =
@@ -166,7 +166,7 @@ crashWithQueryError q et =
 
 -- | Takes a list of Etheno transactions and loads them into the VM, returning the
 -- | address containing echidna tests
-execEthenoTxs :: (MonadIO m, MonadState (VM RealWorld) m, MonadFail m, MonadThrow m) => Etheno -> m ()
+execEthenoTxs :: (MonadIO m, MonadState (VM Concrete RealWorld) m, MonadFail m, MonadThrow m) => Etheno -> m ()
 execEthenoTxs et = do
   setupEthenoTx et
   vm <- get
@@ -177,12 +177,6 @@ execEthenoTxs et = do
     case (res, et) of
       (_        , AccountCreated _)  -> pure ()
       (Reversion,   _)               -> void $ put vm
-      (HandleEffect (Query (PleaseAskSMT (Lit c) _ continue)), _) -> do
-        -- NOTE: this is not a real SMT query, we know it is concrete and can
-        -- resume right away. It is done this way to support iterations counting
-        -- in hevm.
-        fromEVM (continue (Case (c > 0)))
-        runFully vm
       (HandleEffect (Query q), _)    -> crashWithQueryError q et
       (VMFailure x, _)               -> vmExcept x >> M.fail "impossible"
       (VMSuccess (ConcreteBuf bc),
@@ -194,7 +188,7 @@ execEthenoTxs et = do
       _ -> pure ()
 
 -- | For an etheno txn, set up VM to execute txn
-setupEthenoTx :: (MonadIO m, MonadState (VM RealWorld) m) => Etheno -> m ()
+setupEthenoTx :: (MonadIO m, MonadState (VM Concrete RealWorld) m) => Etheno -> m ()
 setupEthenoTx (AccountCreated f) =
   initAddress f -- TODO: improve etheno to include initial balance
 setupEthenoTx (ContractCreated f c _ _ d v) =

lib/Echidna/Events.hs

@@ -29,7 +29,7 @@ type Events = [Text]
 emptyEvents :: TreePos Empty a
 emptyEvents = fromForest []
 
-extractEvents :: Bool -> DappInfo -> VM s -> Events
+extractEvents :: Bool -> DappInfo -> VM Concrete s -> Events
 extractEvents decodeErrors dappInfo vm =
   let forest = traceForest vm
   in maybeToList (decodeRevert decodeErrors vm)
@@ -76,7 +76,7 @@ maybeContractNameFromCodeHash info codeHash = contractToName <$> maybeContract
   where maybeContract = snd <$> Map.lookup codeHash info.solcByHash
         contractToName c = contractNamePart c.contractName
 
-decodeRevert :: Bool -> VM s -> Maybe Text
+decodeRevert :: Bool -> VM Concrete s -> Maybe Text
 decodeRevert decodeErrors vm =
   case vm.result of
     Just (VMFailure (Revert (ConcreteBuf bs))) -> decodeRevertMsg decodeErrors bs

lib/Echidna/Exec.hs

@@ -27,7 +27,7 @@ import EVM.ABI
 import EVM.Exec (exec, vmForEthrunCreation)
 import EVM.Fetch qualified
 import EVM.Format (hexText)
-import EVM.Types hiding (Env)
+import EVM.Types hiding (Env, Gas)
 
 import Echidna.Events (emptyEvents)
 import Echidna.Onchain (safeFetchContractFrom, safeFetchSlotFrom)
@@ -57,16 +57,16 @@ classifyError = \case
   _                    -> UnknownE
 
 -- | Extracts the 'Query' if there is one.
-getQuery :: VMResult s -> Maybe (Query s)
+getQuery :: VMResult Concrete s -> Maybe (Query Concrete s)
 getQuery (HandleEffect (Query q)) = Just q
 getQuery _ = Nothing
 
 -- | Matches execution errors that just cause a reversion.
-pattern Reversion :: VMResult s
+pattern Reversion :: VMResult Concrete s
 pattern Reversion <- VMFailure (classifyError -> RevertE)
 
 -- | Matches execution errors caused by illegal behavior.
-pattern Illegal :: VMResult s
+pattern Illegal :: VMResult Concrete s
 pattern Illegal <- VMFailure (classifyError -> IllegalE)
 
 -- | Given an execution error, throw the appropriate exception.
@@ -75,10 +75,10 @@ vmExcept e = throwM $
   case VMFailure e of {Illegal -> IllegalExec e; _ -> UnknownFailure e}
 
 execTxWith
-  :: (MonadIO m, MonadState (VM RealWorld) m, MonadReader Env m, MonadThrow m)
-  => m (VMResult RealWorld)
+  :: (MonadIO m, MonadState (VM Concrete RealWorld) m, MonadReader Env m, MonadThrow m)
+  => m (VMResult Concrete RealWorld)
   -> Tx
-  -> m (VMResult RealWorld, Gas)
+  -> m (VMResult Concrete RealWorld, Gas)
 execTxWith executeTx tx = do
   vm <- get
   if hasSelfdestructed vm tx.dst then
@@ -180,16 +180,6 @@ execTxWith executeTx tx = do
         fromEVM (continuation encodedResponse)
         runFully
 
-      Just (PleaseAskSMT (Lit c) _ continue) -> do
-        -- NOTE: this is not a real SMT query, we know it is concrete and can
-        -- resume right away. It is done this way to support iterations counting
-        -- in hevm.
-        fromEVM (continue (Case (c > 0)))
-        runFully
-
-      Just q@(PleaseAskSMT {}) ->
-        error $ "Unexpected SMT query: " <> show q
-
       -- No queries to answer, the tx is fully executed and the result is final
       _ -> pure vmResult
 
@@ -230,19 +220,19 @@ logMsg msg = do
 -- | Execute a transaction "as normal".
 execTx
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
-  => VM RealWorld
+  => VM Concrete RealWorld
   -> Tx
-  -> m ((VMResult RealWorld, Gas), VM RealWorld)
+  -> m ((VMResult Concrete RealWorld, Gas), VM Concrete RealWorld)
 execTx vm tx = runStateT (execTxWith (fromEVM exec) tx) vm
 
 -- | A type alias for the context we carry while executing instructions
 type CoverageContext = (Bool, Maybe (VMut.IOVector CoverageInfo, Int))
 
 -- | Execute a transaction, logging coverage at every step.
 execTxWithCov
-  :: (MonadIO m, MonadState (VM RealWorld) m, MonadReader Env m, MonadThrow m)
+  :: (MonadIO m, MonadState (VM Concrete RealWorld) m, MonadReader Env m, MonadThrow m)
   => Tx
-  -> m ((VMResult RealWorld, Gas), Bool)
+  -> m ((VMResult Concrete RealWorld, Gas), Bool)
 execTxWithCov tx = do
   env <- ask
 
@@ -273,19 +263,19 @@ execTxWithCov tx = do
       pure r
       where
       -- | Repeatedly exec a step and add coverage until we have an end result
-      loop :: VM RealWorld -> IO (VMResult RealWorld, VM RealWorld)
+      loop :: VM Concrete RealWorld -> IO (VMResult Concrete RealWorld, VM Concrete RealWorld)
       loop !vm = case vm.result of
         Nothing -> do
           addCoverage vm
           stepVM vm >>= loop
         Just r -> pure (r, vm)
 
       -- | Execute one instruction on the EVM
-      stepVM :: VM RealWorld -> IO (VM RealWorld)
+      stepVM :: VM Concrete RealWorld -> IO (VM Concrete RealWorld)
       stepVM = stToIO . execStateT exec1
 
       -- | Add current location to the CoverageMap
-      addCoverage :: VM RealWorld -> IO ()
+      addCoverage :: VM Concrete RealWorld -> IO ()
       addCoverage !vm = do
         let (pc, opIx, depth) = currentCovLoc vm
             contract = currentContract vm
@@ -322,7 +312,7 @@ execTxWithCov tx = do
       currentContract vm = fromMaybe (error "no contract information on coverage") $
         vm ^? #env % #contracts % at vm.state.codeContract % _Just
 
-initialVM :: Bool -> ST s (VM s)
+initialVM :: Bool -> ST s (VM Concrete s)
 initialVM ffi = do
   vm <- vmForEthrunCreation mempty
   pure $ vm & #block % #timestamp .~ Lit initialTimestamp

lib/Echidna/Shrink.hs

@@ -9,7 +9,7 @@ import Control.Monad.ST (RealWorld)
 import Data.Set qualified as Set
 import Data.List qualified as List
 
-import EVM.Types (VM)
+import EVM.Types (VM, VMType(Concrete))
 
 import Echidna.Exec
 import Echidna.Transaction
@@ -22,7 +22,7 @@ import Echidna.Test (getResultFromVM, checkETest)
 
 shrinkTest
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m)
-  => VM RealWorld
+  => VM Concrete RealWorld
   -> EchidnaTest
   -> m (Maybe EchidnaTest)
 shrinkTest vm test = do
@@ -53,11 +53,11 @@ shrinkTest vm test = do
 -- generate a smaller one that still solves that test.
 shrinkSeq
   :: (MonadIO m, MonadRandom m, MonadReader Env m, MonadThrow m)
-  => VM RealWorld
-  -> (VM RealWorld -> m (TestValue, VM RealWorld))
+  => VM Concrete RealWorld
+  -> (VM Concrete RealWorld -> m (TestValue, VM Concrete RealWorld))
   -> TestValue
   -> [Tx]
-  -> m (Maybe ([Tx], TestValue, VM RealWorld))
+  -> m (Maybe ([Tx], TestValue, VM Concrete RealWorld))
 shrinkSeq vm f v txs = do
   txs' <- uniform =<< sequence [shorten, shrunk]
   (value, vm') <- check txs' vm