From 7ca2cf744727e970fe9160e459eb200ec85fe35b Mon Sep 17 00:00:00 2001
From: Artur Cygan <artur.cygan@trailofbits.com>
Date: Wed, 1 Nov 2023 20:14:40 +0100
Subject: [PATCH 1/2] Small cleanup in execTxWith

---
 lib/Echidna/Exec.hs | 117 +++++++++++++++++++++-----------------------
 1 file changed, 57 insertions(+), 60 deletions(-)

diff --git a/lib/Echidna/Exec.hs b/lib/Echidna/Exec.hs
index 4c51e676e..9083f75e7 100644
--- a/lib/Echidna/Exec.hs
+++ b/lib/Echidna/Exec.hs
@@ -5,16 +5,15 @@
 module Echidna.Exec where
 
 import Optics.Core
-import Optics.State
 import Optics.State.Operators
 
 import Control.Monad (when, forM_)
 import Control.Monad.Catch (MonadThrow(..))
-import Control.Monad.State.Strict (MonadState(get, put), execState, runStateT, MonadIO(liftIO))
+import Control.Monad.State.Strict (MonadState(get, put), execState, runStateT, MonadIO(liftIO), gets, modify')
 import Control.Monad.Reader (MonadReader, asks)
 import Data.Bits
 import Data.ByteString qualified as BS
-import Data.IORef (readIORef, atomicWriteIORef, atomicModifyIORef')
+import Data.IORef (readIORef, atomicWriteIORef, atomicModifyIORef', newIORef, writeIORef, modifyIORef')
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, fromJust)
 import Data.Text qualified as T
@@ -73,26 +72,22 @@ vmExcept :: MonadThrow m => EvmError -> m ()
 vmExcept e = throwM $
   case VMFailure e of {Illegal -> IllegalExec e; _ -> UnknownFailure e}
 
--- | Given an error handler `onErr`, an execution strategy `executeTx`, and a transaction `tx`,
--- execute that transaction using the given execution strategy, calling `onErr` on errors.
 execTxWith
-  :: (MonadIO m, MonadState s m, MonadReader Env m)
-  => Lens' s VM
-  -> (EvmError -> m ())
-  -> m VMResult
+  :: (MonadIO m, MonadState VM m, MonadReader Env m, MonadThrow m)
+  => m VMResult
   -> Tx
   -> m (VMResult, Gas)
-execTxWith l onErr executeTx tx = do
-  vm <- use l
+execTxWith executeTx tx = do
+  vm <- get
   if hasSelfdestructed vm tx.dst then
     pure (VMFailure (Revert (ConcreteBuf "")), 0)
   else do
-    l % #traces .= emptyEvents
-    vmBeforeTx <- use l
-    l %= execState (setupTx tx)
-    gasLeftBeforeTx <- use $ l % #state % #gas
+    #traces .= emptyEvents
+    vmBeforeTx <- get
+    setupTx tx
+    gasLeftBeforeTx <- gets (.state.gas)
     vmResult <- runFully
-    gasLeftAfterTx <- use $ l % #state % #gas
+    gasLeftAfterTx <- gets (.state.gas)
     handleErrorsAndConstruction vmResult vmBeforeTx
     pure (vmResult, gasLeftBeforeTx - gasLeftAfterTx)
   where
@@ -111,9 +106,9 @@ execTxWith l onErr executeTx tx = do
         cacheRef <- asks (.fetchContractCache)
         cache <- liftIO $ readIORef cacheRef
         case Map.lookup addr cache of
-          Just (Just contract) -> l %= execState (continuation contract)
+          Just (Just contract) -> modify' $ execState (continuation contract)
           Just Nothing ->
-            l %= execState (continuation emptyAccount)
+            modify' $ execState (continuation emptyAccount)
           Nothing -> do
             logMsg $ "INFO: Performing RPC: " <> show q
             case config.rpcUrl of
@@ -127,7 +122,7 @@ execTxWith l onErr executeTx tx = do
                     let bc = forceBuf (contract ^. bytecode)
                     liftIO $ atomicWriteIORef metaCacheRef $ Map.insert bc (getBytecodeMetadata bc) metaCache
 
-                    l %= execState (continuation contract)
+                    modify' $ execState (continuation contract)
                     liftIO $ atomicWriteIORef cacheRef $ Map.insert addr (Just contract) cache
                   _ -> do
                     -- TODO: better error reporting in HEVM, when intermmittent
@@ -136,13 +131,13 @@ execTxWith l onErr executeTx tx = do
                     logMsg $ "ERROR: Failed to fetch contract: " <> show q
                     -- TODO: How should we fail here? It could be a network error,
                     -- RPC server returning junk etc.
-                    l %= execState (continuation emptyAccount)
+                    modify' $ execState (continuation emptyAccount)
               Nothing -> do
                 liftIO $ atomicWriteIORef cacheRef $ Map.insert addr Nothing cache
                 logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q
                 -- TODO: How should we fail here? RPC is not configured but VM
                 -- wants to fetch
-                l %= execState (continuation emptyAccount)
+                modify' $ execState (continuation emptyAccount)
         runFully -- resume execution
 
       -- A previously unknown slot is required
@@ -150,8 +145,8 @@ execTxWith l onErr executeTx tx = do
         cacheRef <- asks (.fetchSlotCache)
         cache <- liftIO $ readIORef cacheRef
         case Map.lookup addr cache >>= Map.lookup slot of
-          Just (Just value) -> l %= execState (continuation value)
-          Just Nothing -> l %= execState (continuation 0)
+          Just (Just value) -> modify' $ execState (continuation value)
+          Just Nothing -> modify' $ execState (continuation 0)
           Nothing -> do
             logMsg $ "INFO: Performing RPC: " <> show q
             case config.rpcUrl of
@@ -159,7 +154,7 @@ execTxWith l onErr executeTx tx = do
                 ret <- liftIO $ safeFetchSlotFrom rpcBlock rpcUrl addr slot
                 case ret of
                   Just value -> do
-                    l %= execState (continuation value)
+                    modify' $ execState (continuation value)
                     liftIO $ atomicWriteIORef cacheRef $
                       Map.insertWith Map.union addr (Map.singleton slot (Just value)) cache
                   Nothing -> do
@@ -168,11 +163,11 @@ execTxWith l onErr executeTx tx = do
                     logMsg $ "ERROR: Failed to fetch slot: " <> show q
                     liftIO $ atomicWriteIORef cacheRef $
                       Map.insertWith Map.union addr (Map.singleton slot Nothing) cache
-                    l %= execState (continuation 0)
+                    modify' $ execState (continuation 0)
               Nothing -> do
                 logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q
                 -- Use the zero slot
-                l %= execState (continuation 0)
+                modify' $ execState (continuation 0)
         runFully -- resume execution
 
       -- Execute a FFI call
@@ -180,14 +175,14 @@ execTxWith l onErr executeTx tx = do
         (_, stdout, _) <- liftIO $ readProcessWithExitCode cmd args ""
         let encodedResponse = encodeAbiValue $
               AbiTuple (V.fromList [AbiBytesDynamic . hexText . T.pack $ stdout])
-        l %= execState (continuation encodedResponse)
+        modify' $ execState (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.
-        l %= execState (continue (Case (c > 0)))
+        modify' $ execState (continue (Case (c > 0)))
         runFully
 
       Just q@(PleaseAskSMT {}) ->
@@ -200,24 +195,24 @@ execTxWith l onErr executeTx tx = do
   -- (`vmResult`) of executing transaction `tx`.
   handleErrorsAndConstruction vmResult vmBeforeTx = case (vmResult, tx.call) of
     (Reversion, _) -> do
-      tracesBeforeVMReset <- use $ l % #traces
-      codeContractBeforeVMReset <- use $ l % #state % #codeContract
-      calldataBeforeVMReset <- use $ l % #state % #calldata
-      callvalueBeforeVMReset <- use $ l % #state % #callvalue
+      tracesBeforeVMReset <- gets (.traces)
+      codeContractBeforeVMReset <- gets (.state.codeContract)
+      calldataBeforeVMReset <- gets (.state.calldata)
+      callvalueBeforeVMReset <- gets (.state.callvalue)
       -- If a transaction reverts reset VM to state before the transaction.
-      l .= vmBeforeTx
+      put vmBeforeTx
       -- Undo reset of some of the VM state.
       -- Otherwise we'd loose all information about the reverted transaction like
       -- contract address, calldata, result and traces.
-      l % #result ?= vmResult
-      l % #state % #calldata .= calldataBeforeVMReset
-      l % #state % #callvalue .= callvalueBeforeVMReset
-      l % #traces .= tracesBeforeVMReset
-      l % #state % #codeContract .= codeContractBeforeVMReset
-    (VMFailure x, _) -> onErr x
+      #result ?= vmResult
+      #state % #calldata .= calldataBeforeVMReset
+      #state % #callvalue .= callvalueBeforeVMReset
+      #traces .= tracesBeforeVMReset
+      #state % #codeContract .= codeContractBeforeVMReset
+    (VMFailure x, _) -> vmExcept x
     (VMSuccess (ConcreteBuf bytecode'), SolCreate _) ->
       -- Handle contract creation.
-      l %= execState (do
+      modify' $ execState (do
         #env % #contracts % at tx.dst % _Just % #contractcode .= InitCode mempty mempty
         replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode bytecode'))
         loadContract tx.dst)
@@ -238,7 +233,7 @@ execTx
   => VM
   -> Tx
   -> m ((VMResult, Gas), VM)
-execTx vm tx = runStateT (execTxWith equality' vmExcept (fromEVM exec) tx) vm
+execTx vm tx = runStateT (execTxWith (fromEVM exec) tx) vm
 
 -- | A type alias for the context we carry while executing instructions
 type CoverageContext = (Bool, Maybe (BS.ByteString, Int))
@@ -250,12 +245,14 @@ execTxWithCov
   -> m ((VMResult, Gas), Bool)
 execTxWithCov tx = do
   covRef <- asks (.coverageRef)
-  vm <- get
   metaCacheRef <- asks (.metadataCache)
   cache <- liftIO $ readIORef metaCacheRef
-  (r, (vm', (grew, lastLoc))) <-
-    runStateT (execTxWith _1 vmExcept (execCov covRef cache) tx) (vm, (False, Nothing))
-  put vm'
+
+  covContextRef <- liftIO $ newIORef (False, Nothing)
+
+  r <- execTxWith (execCov covRef covContextRef cache) tx
+
+  (grew, lastLoc) <- liftIO $ readIORef covContextRef
 
   -- Update the last valid location with the transaction result
   grew' <- liftIO $ case lastLoc of
@@ -275,25 +272,25 @@ execTxWithCov tx = do
   pure (r, grew || grew')
   where
     -- the same as EVM.exec but collects coverage, will stop on a query
-    execCov covRef cache = do
-      (vm, cm) <- get
-      (r, vm', cm') <- liftIO $ loop vm cm
-      put (vm', cm')
+    execCov covRef covContextRef cache = do
+      vm <- get
+      (r, vm') <- liftIO $ loop vm
+      put vm'
       pure r
       where
       -- | Repeatedly exec a step and add coverage until we have an end result
-      loop :: VM -> CoverageContext -> IO (VMResult, VM, CoverageContext)
-      loop !vm !cc = case vm.result of
-        Nothing -> addCoverage vm cc >>= loop (stepVM vm)
-        Just r -> pure (r, vm, cc)
+      loop :: VM -> IO (VMResult, VM)
+      loop !vm = case vm.result of
+        Nothing -> addCoverage vm >> loop (stepVM vm)
+        Just r -> pure (r, vm)
 
       -- | Execute one instruction on the EVM
       stepVM :: VM -> VM
       stepVM = execState exec1
 
       -- | Add current location to the CoverageMap
-      addCoverage :: VM -> CoverageContext -> IO CoverageContext
-      addCoverage !vm (new, lastLoc) = do
+      addCoverage :: VM -> IO ()
+      addCoverage !vm = do
         let (pc, opIx, depth) = currentCovLoc vm
             meta = currentMeta vm
         cov <- readIORef covRef
@@ -314,25 +311,25 @@ execTxWithCov tx = do
 
               VMut.write vec' pc (opIx, fromIntegral depth, 0 `setBit` fromEnum Stop)
 
-              pure (True, Just (meta, pc))
+              writeIORef covContextRef (True, Just (meta, pc))
             else do
               -- TODO: should we collect the coverage here? Even if there is no
               -- bytecode for external contract, we could have a "virtual" location
               -- that PC landed at and record that.
-              pure (new, lastLoc)
+              pure ()
           Just vec ->
             if pc < VMut.length vec then
               VMut.read vec pc >>= \case
                 (_, depths, results) | depth < 64 && not (depths `testBit` depth) -> do
                   VMut.write vec pc (opIx, depths `setBit` depth, results `setBit` fromEnum Stop)
-                  pure (True, Just (meta, pc))
+                  writeIORef covContextRef (True, Just (meta, pc))
                 _ ->
-                  pure (new, Just (meta, pc))
+                  modifyIORef' covContextRef $ \(new, _) -> (new, Just (meta, pc))
             else
               -- TODO: no-op: pc is out-of-bounds. This shouldn't happen but we
               -- observed this in some real-world scenarios. This is likely a bug
               -- in another place, investigate.
-              pure (new, lastLoc)
+              pure ()
 
       -- | Get the VM's current execution location
       currentCovLoc vm = (vm.state.pc, fromMaybe 0 $ vmOpIx vm, length vm.frames)

From ce70a8e95848ad9915fea65d5bbf83f44743a074 Mon Sep 17 00:00:00 2001
From: Artur Cygan <artur.cygan@trailofbits.com>
Date: Thu, 2 Nov 2023 11:08:59 +0100
Subject: [PATCH 2/2] hevm: update to 0.52.0

---
 flake.nix                    |   7 ++-
 lib/Echidna.hs               |  10 ++--
 lib/Echidna/Campaign.hs      |  45 ++++++++-------
 lib/Echidna/Deploy.hs        |  13 +++--
 lib/Echidna/Etheno.hs        |  36 ++++++------
 lib/Echidna/Events.hs        |  14 ++---
 lib/Echidna/Exec.hs          | 108 ++++++++++++++++++-----------------
 lib/Echidna/Output/Source.hs |   2 +-
 lib/Echidna/RPC.hs           |   9 +--
 lib/Echidna/Shrink.hs        |   9 +--
 lib/Echidna/Solidity.hs      |  29 +++++-----
 lib/Echidna/Symbolic.hs      |  23 ++++++++
 lib/Echidna/Test.hs          |  53 ++++++++---------
 lib/Echidna/Transaction.hs   |  56 +++++++++---------
 lib/Echidna/Types.hs         |   9 +--
 lib/Echidna/Types/Buffer.hs  |  16 ------
 lib/Echidna/Types/Test.hs    |   5 +-
 lib/Echidna/Types/Tx.hs      |   6 +-
 lib/Echidna/UI.hs            |   3 +-
 src/Main.hs                  |   7 +--
 stack.yaml                   |   4 +-
 21 files changed, 246 insertions(+), 218 deletions(-)
 create mode 100644 lib/Echidna/Symbolic.hs
 delete mode 100644 lib/Echidna/Types/Buffer.hs

diff --git a/flake.nix b/flake.nix
index 4206fa77a..5bb59f09a 100644
--- a/flake.nix
+++ b/flake.nix
@@ -49,10 +49,10 @@
 
         hevm = pkgs.haskell.lib.dontCheck (
           pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
-            owner = "elopez";
+            owner = "ethereum";
             repo = "hevm";
-            rev = "release/0.51.3-plus-ghc-9.4-support";
-            sha256 = "sha256-gJMFYfsPqf5XZyyPDGJLqr9q9RpXkemGeUQUvFT6V0E";
+            rev = "release/0.52.0";
+            sha256 = "sha256-LCv3m6AbLr9mV7pHj7r08dzsg1UVpQDn0zyJXbzRS2Q=";
         }) { secp256k1 = pkgs.secp256k1; });
 
         # FIXME: figure out solc situation, it conflicts with the one from
@@ -141,6 +141,7 @@
             shellHook = "hpack";
             buildInputs = [
               solc
+              slither-analyzer
               haskellPackages.hlint
               haskellPackages.cabal-install
               haskellPackages.haskell-language-server
diff --git a/lib/Echidna.hs b/lib/Echidna.hs
index 4c79102c7..f36f39b1f 100644
--- a/lib/Echidna.hs
+++ b/lib/Echidna.hs
@@ -1,6 +1,7 @@
 module Echidna where
 
 import Control.Monad.Catch (MonadThrow(..))
+import Control.Monad.ST (RealWorld)
 import Data.IORef (writeIORef)
 import Data.List (find)
 import Data.List.NonEmpty (NonEmpty)
@@ -19,6 +20,7 @@ import Echidna.Etheno (loadEtheno, extractFromEtheno)
 import Echidna.Output.Corpus
 import Echidna.Processor
 import Echidna.Solidity
+import Echidna.Symbolic (forceAddr)
 import Echidna.Test (createTests)
 import Echidna.Types.Campaign
 import Echidna.Types.Config
@@ -45,7 +47,7 @@ prepareContract
   -> NonEmpty FilePath
   -> Maybe ContractName
   -> Seed
-  -> IO (VM, World, GenDict)
+  -> IO (VM RealWorld, World, GenDict)
 prepareContract env contracts solFiles specifiedContract seed = do
   let solConf = env.cfg.solConf
 
@@ -64,13 +66,13 @@ prepareContract env contracts solFiles specifiedContract seed = do
     echidnaTests = createTests solConf.testMode
                                solConf.testDestruction
                                testNames
-                               vm.state.contract
+                               (forceAddr vm.state.contract)
                                funs
 
     eventMap = Map.unions $ map (.eventMap) contracts
     world = mkWorld solConf eventMap signatureMap specifiedContract slitherInfo
 
-    deployedAddresses = Set.fromList $ AbiAddress <$> Map.keys vm.env.contracts
+    deployedAddresses = Set.fromList $ AbiAddress . forceAddr <$> Map.keys vm.env.contracts
     constants = enhanceConstants slitherInfo
                 <> timeConstants
                 <> extremeConstants
@@ -79,7 +81,7 @@ prepareContract env contracts solFiles specifiedContract seed = do
 
     dict = mkGenDict env.cfg.campaignConf.dictFreq
                      -- make sure we don't use cheat codes to form fuzzing call sequences
-                     (Set.delete (AbiAddress cheatCode) constants)
+                     (Set.delete (AbiAddress $ forceAddr cheatCode) constants)
                      Set.empty
                      seed
                      (returnTypes contracts)
diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs
index 3e8638c49..444487cf4 100644
--- a/lib/Echidna/Campaign.hs
+++ b/lib/Echidna/Campaign.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
 
 module Echidna.Campaign where
 
@@ -12,13 +13,14 @@ import Control.Monad.Random.Strict (MonadRandom, RandT, evalRandT)
 import Control.Monad.Reader (MonadReader, asks, liftIO, ask)
 import Control.Monad.State.Strict
   (MonadState(..), StateT(..), gets, MonadIO, modify')
+import Control.Monad.ST (RealWorld)
 import Control.Monad.Trans (lift)
 import Data.Binary.Get (runGetOrFail)
 import Data.ByteString.Lazy qualified as LBS
 import Data.IORef (readIORef, writeIORef, atomicModifyIORef')
 import Data.Map qualified as Map
 import Data.Map (Map, (\\))
-import Data.Maybe (isJust, mapMaybe, fromMaybe)
+import Data.Maybe (isJust, mapMaybe, fromMaybe, fromJust)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text (Text)
@@ -33,10 +35,10 @@ import Echidna.Exec
 import Echidna.Events (extractEvents)
 import Echidna.Mutator.Corpus
 import Echidna.Shrink (shrinkTest)
+import Echidna.Symbolic (forceBuf, forceAddr)
 import Echidna.Test
 import Echidna.Transaction
 import Echidna.Types (Gas)
-import Echidna.Types.Buffer (forceBuf)
 import Echidna.Types.Campaign
 import Echidna.Types.Corpus (Corpus, corpusSize)
 import Echidna.Types.Coverage (scoveragePoints)
@@ -62,7 +64,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     -- ^ VM to start replaying from
+  => VM RealWorld -- ^ VM to start replaying from
   -> [[Tx]] -- ^ corpus to replay
   -> m ()
 replayCorpus vm txSeqs =
@@ -77,7 +79,7 @@ runWorker
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m)
   => StateT WorkerState m ()
   -- ^ Callback to run after each state update (for instrumentation)
-  -> VM      -- ^ Initial VM state
+  -> VM RealWorld -- ^ Initial VM state
   -> World   -- ^ Initial world state
   -> GenDict -- ^ Generation dictionary
   -> Int     -- ^ Worker id starting from 0
@@ -88,7 +90,8 @@ runWorker callback vm world dict workerId initialCorpus testLimit = do
   metaCacheRef <- asks (.metadataCache)
   fetchContractCacheRef <- asks (.fetchContractCache)
   external <- liftIO $ Map.mapMaybe id <$> readIORef fetchContractCacheRef
-  liftIO $ writeIORef metaCacheRef (mkMemo (vm.env.contracts <> external))
+  let concretizeKeys = Map.foldrWithKey (Map.insert . forceAddr) mempty
+  liftIO $ writeIORef metaCacheRef (mkMemo (concretizeKeys vm.env.contracts <> external))
 
   let
     effectiveSeed = dict.defSeed + workerId
@@ -150,13 +153,13 @@ runWorker callback vm world dict workerId initialCorpus testLimit = do
 
   continue = runUpdate (shrinkTest vm) >> lift callback >> run
 
-  mkMemo = makeBytecodeCache . map (forceBuf . (^. bytecode)) . Map.elems
+  mkMemo = makeBytecodeCache . map (forceBuf . fromJust . (^. bytecode)) . Map.elems
 
 -- | Generate a new sequences of transactions, either using the corpus or with
 -- randomly created transactions
 randseq
   :: (MonadRandom m, MonadReader Env m, MonadState WorkerState m, MonadIO m)
-  => Map Addr Contract
+  => Map (Expr 'EAddr) Contract
   -> World
   -> m [Tx]
 randseq deployedContracts world = do
@@ -187,9 +190,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
+  => VM RealWorld
   -> [Tx]
-  -> m VM
+  -> m (VM RealWorld)
 callseq vm txSeq = do
   env <- ask
   -- First, we figure out whether we need to execute with or without coverage
@@ -224,7 +227,7 @@ callseq vm txSeq = do
       -- compute the addresses not present in the old VM via set difference
       newAddrs = Map.keys $ vm'.env.contracts \\ vm.env.contracts
       -- and construct a set to union to the constants table
-      diffs = Map.fromList [(AbiAddressType, Set.fromList $ AbiAddress <$> newAddrs)]
+      diffs = Map.fromList [(AbiAddressType, Set.fromList $ AbiAddress . forceAddr <$> newAddrs)]
       -- Now we try to parse the return values as solidity constants, and add them to 'GenDict'
       resultMap = returnValues (map (\(t, (vr, _)) -> (t, vr)) results) workerState.genDict.rTypes
       -- union the return results with the new addresses
@@ -257,7 +260,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)]
+    :: [(Tx, VMResult RealWorld)]
     -> (FunctionName -> Maybe AbiType)
     -> Map AbiType (Set AbiValue)
   returnValues txResults returnTypeOf =
@@ -270,13 +273,13 @@ callseq vm txSeq = do
           type' <- returnTypeOf fname
           case runGetOrFail (getAbi type') (LBS.fromStrict buf) of
             -- make sure we don't use cheat codes to form fuzzing call sequences
-            Right (_, _, abiValue) | abiValue /= AbiAddress cheatCode ->
+            Right (_, _, abiValue) | abiValue /= AbiAddress (forceAddr cheatCode) ->
               Just (type', Set.singleton abiValue)
             _ -> Nothing
         _ -> Nothing
 
   -- | Add transactions to the corpus discarding reverted ones
-  addToCorpus :: Int -> [(Tx, (VMResult, Gas))] -> Corpus -> Corpus
+  addToCorpus :: Int -> [(Tx, (VMResult RealWorld, Gas))] -> Corpus -> Corpus
   addToCorpus n res corpus =
     if null rtxs then corpus else Set.insert (n, rtxs) corpus
     where rtxs = fst <$> res
@@ -285,8 +288,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 -> Tx
-  -> m ((VMResult, Gas), VM)
+  => VM RealWorld -> Tx
+  -> m ((VMResult RealWorld, Gas), VM RealWorld)
 execTxOptC vm tx = do
   ((res, grew), vm') <- runStateT (execTxWithCov tx) vm
   when grew $ do
@@ -301,7 +304,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, Gas))]
+  :: [(Tx, (VMResult RealWorld, Gas))]
   -> [Tx]
   -> Map Text (Gas, [Tx])
   -> Map Text (Gas, [Tx])
@@ -322,10 +325,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 -- ^ Initial VM
-  -> (VM -> Tx -> m (result, VM))
+  => VM RealWorld -- ^ Initial VM
+  -> (VM RealWorld -> Tx -> m (result, VM RealWorld))
   -> [Tx]
-  -> m ([(Tx, result)], VM)
+  -> m ([(Tx, result)], VM 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,
@@ -365,8 +368,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
-  -> (VM, [Tx])
+  => VM RealWorld
+  -> (VM RealWorld, [Tx])
   -> EchidnaTest
   -> m (Maybe EchidnaTest)
 updateTest vmForShrink (vm, xs) test = do
diff --git a/lib/Echidna/Deploy.hs b/lib/Echidna/Deploy.hs
index 6e078d968..f2b4574a9 100644
--- a/lib/Echidna/Deploy.hs
+++ b/lib/Echidna/Deploy.hs
@@ -19,21 +19,22 @@ import Echidna.Events (extractEvents)
 import Echidna.Types.Config (Env(..))
 import Echidna.Types.Solidity (SolException(..))
 import Echidna.Types.Tx (createTx, unlimitedGasPerBlock)
+import Control.Monad.ST (RealWorld)
 
 deployContracts
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
   => [(Addr, SolcContract)]
   -> Addr
-  -> VM
-  -> m VM
+  -> VM RealWorld
+  -> m (VM RealWorld)
 deployContracts cs = deployBytecodes' $ map (\(a, c) -> (a, c.creationCode)) cs
 
 deployBytecodes
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
   => [(Addr, Text)]
   -> Addr
-  -> VM
-  -> m VM
+  -> VM RealWorld
+  -> m (VM RealWorld)
 deployBytecodes cs = deployBytecodes' $
   (\(a, bc) ->
     (a, fromRight (error ("invalid b16 decoding of: " ++ show bc)) $ BS16.decode $ encodeUtf8 bc)
@@ -44,8 +45,8 @@ deployBytecodes'
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
   => [(Addr, ByteString)]
   -> Addr
-  -> VM
-  -> m VM
+  -> VM RealWorld
+  -> m (VM RealWorld)
 deployBytecodes' cs src initialVM = foldM deployOne initialVM cs
   where
   deployOne vm (dst, bytecode) = do
diff --git a/lib/Echidna/Etheno.hs b/lib/Echidna/Etheno.hs
index f43611a92..967cc6848 100644
--- a/lib/Echidna/Etheno.hs
+++ b/lib/Echidna/Etheno.hs
@@ -11,7 +11,7 @@ import Control.Exception (Exception)
 import Control.Monad (void)
 import Control.Monad.Catch (MonadThrow, throwM)
 import Control.Monad.Fail qualified as M (MonadFail(..))
-import Control.Monad.State.Strict (MonadState, get, put, execStateT, gets, modify', execState)
+import Control.Monad.State.Strict (MonadIO, MonadState, get, gets, put, execState, execStateT)
 import Data.Aeson (FromJSON(..), (.:), withObject, eitherDecodeFileStrict)
 import Data.ByteString.Base16 qualified as BS16 (decode)
 import Data.ByteString.Char8 (ByteString)
@@ -35,6 +35,7 @@ import Echidna.ABI (encodeSig)
 import Echidna.Types (fromEVM)
 import Echidna.Types.Tx (TxCall(..), Tx(..), makeSingleTx, createTxWithValue, unlimitedGasPerBlock)
 import Data.Set (Set)
+import Control.Monad.ST (RealWorld, stToIO)
 
 -- | During initialization we can either call a function or create an account or contract
 data Etheno
@@ -120,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
+loadEthenoBatch :: Bool -> FilePath -> IO (VM RealWorld)
 loadEthenoBatch ffi fp = do
   bs <- eitherDecodeFileStrict fp
   case bs of
@@ -128,30 +129,31 @@ loadEthenoBatch ffi fp = do
     Right (ethenoInit :: [Etheno]) -> do
       -- Execute contract creations and initial transactions,
       let initVM = mapM execEthenoTxs ethenoInit
-      execStateT initVM (initialVM ffi)
+      vm <- stToIO $ initialVM ffi
+      execStateT initVM vm
 
-initAddress :: MonadState VM m => Addr -> m ()
+initAddress :: MonadState (VM s) m => Addr -> m ()
 initAddress addr = do
   cs <- gets (.env.contracts)
-  if addr `member` cs then pure ()
-  else #env % #contracts % at addr .= Just account
+  if LitAddr addr `member` cs then pure ()
+  else #env % #contracts % at (LitAddr addr) .= Just account
   where
     account =
       initialContract (RuntimeCode (ConcreteRuntimeCode mempty))
-        & set #nonce 0
-        & set #balance 100000000000000000000 -- default balance for EOAs in etheno
+        & set #nonce (Just 0)
+        & set #balance (Lit 100000000000000000000) -- default balance for EOAs in etheno
 
 crashWithQueryError
-  :: (MonadState VM m, MonadFail m, MonadThrow m)
-  => Query
+  :: (MonadState (VM s) m, MonadFail m, MonadThrow m)
+  => Query s
   -> Etheno
   -> m ()
 crashWithQueryError q et =
   case (q, et) of
-    (PleaseFetchContract addr _, FunctionCall f t _ _ _ _) ->
+    (PleaseFetchContract addr _ _, FunctionCall f t _ _ _ _) ->
       error $ "Address " ++ show addr ++ " was used during function call from "
                 ++ show f ++ " to " ++ show t ++ " but it was never defined as EOA or deployed as a contract"
-    (PleaseFetchContract addr _, ContractCreated f t _ _ _ _) ->
+    (PleaseFetchContract addr _ _, ContractCreated f t _ _ _ _) ->
       error $ "Address " ++ show addr ++ " was used during the contract creation of "
                 ++ show t ++ " from " ++ show f ++ " but it was never defined as EOA or deployed as a contract"
     (PleaseFetchSlot slot _ _, FunctionCall f t _ _ _ _) ->
@@ -164,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 :: (MonadState VM m, MonadFail m, MonadThrow m) => Etheno -> m ()
+execEthenoTxs :: (MonadIO m, MonadState (VM RealWorld) m, MonadFail m, MonadThrow m) => Etheno -> m ()
 execEthenoTxs et = do
   setupEthenoTx et
   vm <- get
@@ -179,20 +181,20 @@ execEthenoTxs et = 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.
-        modify' $ execState (continue (Case (c > 0)))
+        fromEVM (continue (Case (c > 0)))
         runFully vm
       (HandleEffect (Query q), _)    -> crashWithQueryError q et
       (VMFailure x, _)               -> vmExcept x >> M.fail "impossible"
       (VMSuccess (ConcreteBuf bc),
        ContractCreated _ ca _ _ _ _) -> do
-        #env % #contracts % at ca % _Just % #contractcode .= InitCode mempty mempty
+        #env % #contracts % at (LitAddr ca) % _Just % #code .= InitCode mempty mempty
         fromEVM $ do
           replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode bc))
-          loadContract ca
+          get <&> execState (loadContract (LitAddr ca)) >>= put
       _ -> pure ()
 
 -- | For an etheno txn, set up VM to execute txn
-setupEthenoTx :: MonadState VM m => Etheno -> m ()
+setupEthenoTx :: (MonadIO m, MonadState (VM RealWorld) m) => Etheno -> m ()
 setupEthenoTx (AccountCreated f) =
   initAddress f -- TODO: improve etheno to include initial balance
 setupEthenoTx (ContractCreated f c _ _ d v) =
diff --git a/lib/Echidna/Events.hs b/lib/Echidna/Events.hs
index ff1427459..75f4bf9a9 100644
--- a/lib/Echidna/Events.hs
+++ b/lib/Echidna/Events.hs
@@ -3,6 +3,7 @@
 
 module Echidna.Events where
 
+import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
 import Data.ByteString.Lazy (fromStrict)
 import Data.Map (Map)
@@ -20,8 +21,7 @@ import EVM.Format (showValues, showError, contractNamePart)
 import EVM.Solidity (SolcContract(..))
 import EVM.Types
 
-import Echidna.Types.Buffer (forceLit, forceBuf)
-import Data.ByteString (ByteString)
+import Echidna.Symbolic (forceWord, forceBuf)
 
 type EventMap = Map W256 Event
 type Events = [Text]
@@ -29,7 +29,7 @@ type Events = [Text]
 emptyEvents :: TreePos Empty a
 emptyEvents = fromForest []
 
-extractEvents :: Bool -> DappInfo -> VM -> Events
+extractEvents :: Bool -> DappInfo -> VM s -> Events
 extractEvents decodeErrors dappInfo vm =
   let forest = traceForest vm
   in maybeToList (decodeRevert decodeErrors vm)
@@ -41,7 +41,7 @@ extractEvents decodeErrors dappInfo vm =
         maybeContractName = maybeContractNameFromCodeHash dappInfo codehash'
     in case trace.tracedata of
       EventTrace addr bytes (topic:_) ->
-        case Map.lookup (forceLit topic) dappInfo.eventMap of
+        case Map.lookup (forceWord topic) dappInfo.eventMap of
           Just (Event name _ types) ->
             -- TODO this is where indexed types are filtered out
             -- they are filtered out for a reason as they only contain
@@ -51,8 +51,8 @@ extractEvents decodeErrors dappInfo vm =
               <> showValues [t | (_, t, NotIndexed) <- types] bytes
               <> " from: "
               <> maybe mempty (<> "@") maybeContractName
-              <> pack (show $ forceLit addr)
-          Nothing -> Just $ pack $ show (forceLit topic)
+              <> pack (show $ forceWord addr)
+          Nothing -> Just $ pack $ show (forceWord topic)
       ErrorTrace e ->
         case e of
           Revert out ->
@@ -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 -> Maybe Text
+decodeRevert :: Bool -> VM s -> Maybe Text
 decodeRevert decodeErrors vm =
   case vm.result of
     Just (VMFailure (Revert (ConcreteBuf bs))) -> decodeRevertMsg decodeErrors bs
diff --git a/lib/Echidna/Exec.hs b/lib/Echidna/Exec.hs
index 9083f75e7..c22a2e377 100644
--- a/lib/Echidna/Exec.hs
+++ b/lib/Echidna/Exec.hs
@@ -9,8 +9,9 @@ import Optics.State.Operators
 
 import Control.Monad (when, forM_)
 import Control.Monad.Catch (MonadThrow(..))
-import Control.Monad.State.Strict (MonadState(get, put), execState, runStateT, MonadIO(liftIO), gets, modify')
+import Control.Monad.State.Strict (MonadState(get, put), execState, runStateT, MonadIO(liftIO), gets, modify', execStateT)
 import Control.Monad.Reader (MonadReader, asks)
+import Control.Monad.ST (ST, stToIO, RealWorld)
 import Data.Bits
 import Data.ByteString qualified as BS
 import Data.IORef (readIORef, atomicWriteIORef, atomicModifyIORef', newIORef, writeIORef, modifyIORef')
@@ -30,9 +31,9 @@ import EVM.Types hiding (Env)
 
 import Echidna.Events (emptyEvents)
 import Echidna.RPC (safeFetchContractFrom, safeFetchSlotFrom)
+import Echidna.Symbolic (forceBuf)
 import Echidna.Transaction
 import Echidna.Types (ExecException(..), Gas, fromEVM, emptyAccount)
-import Echidna.Types.Buffer (forceBuf)
 import Echidna.Types.Config (Env(..), EConfig(..), UIConf(..), OperationMode(..), OutputFormat(Text))
 import Echidna.Types.Signature (getBytecodeMetadata, lookupBytecodeMetadata)
 import Echidna.Types.Solidity (SolConf(..))
@@ -55,16 +56,16 @@ classifyError = \case
   _                    -> UnknownE
 
 -- | Extracts the 'Query' if there is one.
-getQuery :: VMResult -> Maybe Query
+getQuery :: VMResult s -> Maybe (Query s)
 getQuery (HandleEffect (Query q)) = Just q
 getQuery _ = Nothing
 
 -- | Matches execution errors that just cause a reversion.
-pattern Reversion :: VMResult
+pattern Reversion :: VMResult s
 pattern Reversion <- VMFailure (classifyError -> RevertE)
 
 -- | Matches execution errors caused by illegal behavior.
-pattern Illegal :: VMResult
+pattern Illegal :: VMResult s
 pattern Illegal <- VMFailure (classifyError -> IllegalE)
 
 -- | Given an execution error, throw the appropriate exception.
@@ -73,10 +74,10 @@ vmExcept e = throwM $
   case VMFailure e of {Illegal -> IllegalExec e; _ -> UnknownFailure e}
 
 execTxWith
-  :: (MonadIO m, MonadState VM m, MonadReader Env m, MonadThrow m)
-  => m VMResult
+  :: (MonadIO m, MonadState (VM RealWorld) m, MonadReader Env m, MonadThrow m)
+  => m (VMResult RealWorld)
   -> Tx
-  -> m (VMResult, Gas)
+  -> m (VMResult RealWorld, Gas)
 execTxWith executeTx tx = do
   vm <- get
   if hasSelfdestructed vm tx.dst then
@@ -102,13 +103,15 @@ execTxWith executeTx tx = do
     -- the execution by recursively calling `runFully`.
     case getQuery vmResult of
       -- A previously unknown contract is required
-      Just q@(PleaseFetchContract addr continuation) -> do
+      Just q@(PleaseFetchContract addr _ continuation) -> do
         cacheRef <- asks (.fetchContractCache)
         cache <- liftIO $ readIORef cacheRef
         case Map.lookup addr cache of
-          Just (Just contract) -> modify' $ execState (continuation contract)
-          Just Nothing ->
-            modify' $ execState (continuation emptyAccount)
+          Just (Just contract) -> fromEVM (continuation contract)
+          Just Nothing -> do
+            v <- get
+            v' <- liftIO $ stToIO $ execStateT (continuation emptyAccount) v
+            put v'
           Nothing -> do
             logMsg $ "INFO: Performing RPC: " <> show q
             case config.rpcUrl of
@@ -116,13 +119,13 @@ execTxWith executeTx tx = do
                 ret <- liftIO $ safeFetchContractFrom rpcBlock rpcUrl addr
                 case ret of
                   -- TODO: fix hevm to not return an empty contract in case of an error
-                  Just contract | contract.contractcode /= RuntimeCode (ConcreteRuntimeCode "") -> do
+                  Just contract | contract.code /= RuntimeCode (ConcreteRuntimeCode "") -> do
                     metaCacheRef <- asks (.metadataCache)
                     metaCache <- liftIO $ readIORef metaCacheRef
-                    let bc = forceBuf (contract ^. bytecode)
+                    let bc = forceBuf $ fromJust (contract ^. bytecode)
                     liftIO $ atomicWriteIORef metaCacheRef $ Map.insert bc (getBytecodeMetadata bc) metaCache
 
-                    modify' $ execState (continuation contract)
+                    fromEVM (continuation contract)
                     liftIO $ atomicWriteIORef cacheRef $ Map.insert addr (Just contract) cache
                   _ -> do
                     -- TODO: better error reporting in HEVM, when intermmittent
@@ -131,13 +134,13 @@ execTxWith executeTx tx = do
                     logMsg $ "ERROR: Failed to fetch contract: " <> show q
                     -- TODO: How should we fail here? It could be a network error,
                     -- RPC server returning junk etc.
-                    modify' $ execState (continuation emptyAccount)
+                    fromEVM (continuation emptyAccount)
               Nothing -> do
                 liftIO $ atomicWriteIORef cacheRef $ Map.insert addr Nothing cache
                 logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q
                 -- TODO: How should we fail here? RPC is not configured but VM
                 -- wants to fetch
-                modify' $ execState (continuation emptyAccount)
+                fromEVM (continuation emptyAccount)
         runFully -- resume execution
 
       -- A previously unknown slot is required
@@ -145,8 +148,8 @@ execTxWith executeTx tx = do
         cacheRef <- asks (.fetchSlotCache)
         cache <- liftIO $ readIORef cacheRef
         case Map.lookup addr cache >>= Map.lookup slot of
-          Just (Just value) -> modify' $ execState (continuation value)
-          Just Nothing -> modify' $ execState (continuation 0)
+          Just (Just value) -> fromEVM (continuation value)
+          Just Nothing -> fromEVM (continuation 0)
           Nothing -> do
             logMsg $ "INFO: Performing RPC: " <> show q
             case config.rpcUrl of
@@ -154,7 +157,7 @@ execTxWith executeTx tx = do
                 ret <- liftIO $ safeFetchSlotFrom rpcBlock rpcUrl addr slot
                 case ret of
                   Just value -> do
-                    modify' $ execState (continuation value)
+                    fromEVM (continuation value)
                     liftIO $ atomicWriteIORef cacheRef $
                       Map.insertWith Map.union addr (Map.singleton slot (Just value)) cache
                   Nothing -> do
@@ -163,11 +166,11 @@ execTxWith executeTx tx = do
                     logMsg $ "ERROR: Failed to fetch slot: " <> show q
                     liftIO $ atomicWriteIORef cacheRef $
                       Map.insertWith Map.union addr (Map.singleton slot Nothing) cache
-                    modify' $ execState (continuation 0)
+                    fromEVM (continuation 0)
               Nothing -> do
                 logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q
                 -- Use the zero slot
-                modify' $ execState (continuation 0)
+                fromEVM (continuation 0)
         runFully -- resume execution
 
       -- Execute a FFI call
@@ -175,14 +178,14 @@ execTxWith executeTx tx = do
         (_, stdout, _) <- liftIO $ readProcessWithExitCode cmd args ""
         let encodedResponse = encodeAbiValue $
               AbiTuple (V.fromList [AbiBytesDynamic . hexText . T.pack $ stdout])
-        modify' $ execState (continuation encodedResponse)
+        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.
-        modify' $ execState (continue (Case (c > 0)))
+        fromEVM (continue (Case (c > 0)))
         runFully
 
       Just q@(PleaseAskSMT {}) ->
@@ -210,15 +213,13 @@ execTxWith executeTx tx = do
       #traces .= tracesBeforeVMReset
       #state % #codeContract .= codeContractBeforeVMReset
     (VMFailure x, _) -> vmExcept x
-    (VMSuccess (ConcreteBuf bytecode'), SolCreate _) ->
+    (VMSuccess (ConcreteBuf bytecode'), SolCreate _) -> do
       -- Handle contract creation.
-      modify' $ execState (do
-        #env % #contracts % at tx.dst % _Just % #contractcode .= InitCode mempty mempty
-        replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode bytecode'))
-        loadContract tx.dst)
+      #env % #contracts % at (LitAddr tx.dst) % _Just % #code .= InitCode mempty mempty
+      fromEVM $ replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode bytecode'))
+      modify' $ execState $ loadContract (LitAddr tx.dst)
     _ -> pure ()
 
-
 logMsg :: (MonadIO m, MonadReader Env m) => String -> m ()
 logMsg msg = do
   cfg <- asks (.cfg)
@@ -230,9 +231,9 @@ logMsg msg = do
 -- | Execute a transaction "as normal".
 execTx
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
-  => VM
+  => VM RealWorld
   -> Tx
-  -> m ((VMResult, Gas), VM)
+  -> m ((VMResult RealWorld, Gas), VM RealWorld)
 execTx vm tx = runStateT (execTxWith (fromEVM exec) tx) vm
 
 -- | A type alias for the context we carry while executing instructions
@@ -240,9 +241,9 @@ type CoverageContext = (Bool, Maybe (BS.ByteString, Int))
 
 -- | Execute a transaction, logging coverage at every step.
 execTxWithCov
-  :: (MonadIO m, MonadState VM m, MonadReader Env m, MonadThrow m)
+  :: (MonadIO m, MonadState (VM RealWorld) m, MonadReader Env m, MonadThrow m)
   => Tx
-  -> m ((VMResult, Gas), Bool)
+  -> m ((VMResult RealWorld, Gas), Bool)
 execTxWithCov tx = do
   covRef <- asks (.coverageRef)
   metaCacheRef <- asks (.metadataCache)
@@ -279,24 +280,26 @@ execTxWithCov tx = do
       pure r
       where
       -- | Repeatedly exec a step and add coverage until we have an end result
-      loop :: VM -> IO (VMResult, VM)
+      loop :: VM RealWorld -> IO (VMResult RealWorld, VM RealWorld)
       loop !vm = case vm.result of
-        Nothing -> addCoverage vm >> loop (stepVM vm)
+        Nothing -> do
+          addCoverage vm
+          stepVM vm >>= loop
         Just r -> pure (r, vm)
 
       -- | Execute one instruction on the EVM
-      stepVM :: VM -> VM
-      stepVM = execState exec1
+      stepVM :: VM RealWorld -> IO (VM RealWorld)
+      stepVM = stToIO . execStateT exec1
 
       -- | Add current location to the CoverageMap
-      addCoverage :: VM -> IO ()
+      addCoverage :: VM RealWorld -> IO ()
       addCoverage !vm = do
         let (pc, opIx, depth) = currentCovLoc vm
             meta = currentMeta vm
         cov <- readIORef covRef
         case Map.lookup meta cov of
           Nothing -> do
-            let size = BS.length . forceBuf . view bytecode . fromJust $
+            let size = BS.length . forceBuf . fromJust . view bytecode . fromJust $
                   Map.lookup vm.state.contract vm.env.contracts
             if size > 0 then do
               vec <- VMut.new size
@@ -318,18 +321,16 @@ execTxWithCov tx = do
               -- that PC landed at and record that.
               pure ()
           Just vec ->
-            if pc < VMut.length vec then
+            -- TODO: no-op when pc is out-of-bounds. This shouldn't happen but
+            -- we observed this in some real-world scenarios. This is likely a
+            -- bug in another place, investigate.
+            when (pc < VMut.length vec) $
               VMut.read vec pc >>= \case
                 (_, depths, results) | depth < 64 && not (depths `testBit` depth) -> do
                   VMut.write vec pc (opIx, depths `setBit` depth, results `setBit` fromEnum Stop)
                   writeIORef covContextRef (True, Just (meta, pc))
                 _ ->
                   modifyIORef' covContextRef $ \(new, _) -> (new, Just (meta, pc))
-            else
-              -- TODO: no-op: pc is out-of-bounds. This shouldn't happen but we
-              -- observed this in some real-world scenarios. This is likely a bug
-              -- in another place, investigate.
-              pure ()
 
       -- | Get the VM's current execution location
       currentCovLoc vm = (vm.state.pc, fromMaybe 0 $ vmOpIx vm, length vm.frames)
@@ -337,12 +338,13 @@ execTxWithCov tx = do
       -- | Get the current contract's bytecode metadata
       currentMeta vm = fromMaybe (error "no contract information on coverage") $ do
         buffer <- vm ^? #env % #contracts % at vm.state.codeContract % _Just % bytecode
-        let bc = forceBuf buffer
+        let bc = forceBuf $ fromJust buffer
         pure $ lookupBytecodeMetadata cache bc
 
-initialVM :: Bool -> VM
-initialVM ffi = vmForEthrunCreation mempty
-  & #block % #timestamp .~ Lit initialTimestamp
-  & #block % #number .~ initialBlockNumber
-  & #env % #contracts .~ mempty -- fixes weird nonce issues
-  & #allowFFI .~ ffi
+initialVM :: Bool -> ST s (VM s)
+initialVM ffi = do
+  vm <- vmForEthrunCreation mempty
+  pure $ vm & #block % #timestamp .~ Lit initialTimestamp
+            & #block % #number .~ initialBlockNumber
+            & #env % #contracts .~ mempty -- fixes weird nonce issues
+            & #config % #allowFFI .~ ffi
diff --git a/lib/Echidna/Output/Source.hs b/lib/Echidna/Output/Source.hs
index 668087f97..6be9f0096 100644
--- a/lib/Echidna/Output/Source.hs
+++ b/lib/Echidna/Output/Source.hs
@@ -24,7 +24,7 @@ import System.Directory (createDirectoryIfMissing)
 import System.FilePath ((</>))
 import Text.Printf (printf)
 
-import EVM.Debug (srcMapCodePos)
+import EVM.Dapp (srcMapCodePos)
 import EVM.Solidity (SourceCache(..), SrcMap, SolcContract(..))
 
 import Echidna.Types.Coverage (OpIx, unpackTxResults, CoverageMap)
diff --git a/lib/Echidna/RPC.hs b/lib/Echidna/RPC.hs
index 1759b7a84..e4ba36c0b 100644
--- a/lib/Echidna/RPC.hs
+++ b/lib/Echidna/RPC.hs
@@ -19,6 +19,7 @@ import EVM.Fetch qualified
 import EVM.Types
 
 import Echidna.Orphans.JSON ()
+import Echidna.Symbolic (forceWord)
 import Echidna.Types (emptyAccount)
 
 rpcUrlEnv :: IO (Maybe Text)
@@ -51,7 +52,7 @@ fetchChainId Nothing = pure Nothing
 
 data FetchedContractData = FetchedContractData
   { runtimeCode :: ByteString
-  , nonce :: W256
+  , nonce :: Maybe W64
   , balance :: W256
   }
   deriving (Generic, ToJSON, FromJSON, Show)
@@ -63,17 +64,17 @@ fromFetchedContractData :: FetchedContractData -> Contract
 fromFetchedContractData contractData =
   (initialContract (RuntimeCode (ConcreteRuntimeCode contractData.runtimeCode)))
     { nonce = contractData.nonce
-    , balance = contractData.balance
+    , balance = Lit contractData.balance
     , external = True
     }
 
 toFetchedContractData :: Contract -> FetchedContractData
 toFetchedContractData contract =
-  let code = case contract.contractcode of
+  let code = case contract.code of
                RuntimeCode (ConcreteRuntimeCode c) -> c
                _ -> error "unexpected code"
   in FetchedContractData
     { runtimeCode = code
     , nonce = contract.nonce
-    , balance = contract.balance
+    , balance = forceWord contract.balance
     }
diff --git a/lib/Echidna/Shrink.hs b/lib/Echidna/Shrink.hs
index cf76c9e54..4e070d79e 100644
--- a/lib/Echidna/Shrink.hs
+++ b/lib/Echidna/Shrink.hs
@@ -5,6 +5,7 @@ import Control.Monad.Catch (MonadThrow)
 import Control.Monad.Random.Strict (MonadRandom, getRandomR, uniform)
 import Control.Monad.Reader.Class (MonadReader (ask), asks)
 import Control.Monad.State.Strict (MonadIO)
+import Control.Monad.ST (RealWorld)
 import Data.Set qualified as Set
 import Data.List qualified as List
 
@@ -22,7 +23,7 @@ import Echidna.Test (getResultFromVM, checkETest)
 
 shrinkTest
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m)
-  => VM
+  => VM RealWorld
   -> EchidnaTest
   -> m (Maybe EchidnaTest)
 shrinkTest vm test = do
@@ -53,11 +54,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
-  -> (VM -> m (TestValue, VM))
+  => VM RealWorld
+  -> (VM RealWorld -> m (TestValue, VM RealWorld))
   -> TestValue
   -> [Tx]
-  -> m (Maybe ([Tx], TestValue, VM))
+  -> m (Maybe ([Tx], TestValue, VM RealWorld))
 shrinkSeq vm f v txs = do
   txs' <- uniform =<< sequence [shorten, shrunk]
   (value, vm') <- check txs' vm
diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs
index 1d3f70361..5f3f75f51 100644
--- a/lib/Echidna/Solidity.hs
+++ b/lib/Echidna/Solidity.hs
@@ -6,6 +6,7 @@ import Control.Monad (when, unless, forM_)
 import Control.Monad.Catch (MonadThrow(..))
 import Control.Monad.Extra (whenM)
 import Control.Monad.Reader (ReaderT(runReaderT))
+import Control.Monad.ST (stToIO, RealWorld)
 import Data.Foldable (toList)
 import Data.List (find, partition, isSuffixOf, (\\))
 import Data.List.NonEmpty (NonEmpty((:|)))
@@ -38,6 +39,7 @@ import Echidna.Etheno (loadEthenoBatch)
 import Echidna.Events (EventMap, extractEvents)
 import Echidna.Exec (execTx, initialVM)
 import Echidna.Processor
+import Echidna.Symbolic (forceAddr)
 import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isDapptestMode)
 import Echidna.Types.Config (EConfig(..), Env(..))
 import Echidna.Types.Signature
@@ -132,18 +134,19 @@ staticAddresses SolConf{contractAddr, deployer, sender} =
   Set.map AbiAddress $
     Set.union sender (Set.fromList [contractAddr, deployer, 0x0])
 
-populateAddresses :: Set Addr -> Integer -> VM -> VM
+populateAddresses :: Set Addr -> Integer -> VM s -> VM s
 populateAddresses addrs b vm =
   Set.foldl' (\vm' addr ->
     if deployed addr
        then vm'
-       else vm' & set (#env % #contracts % at addr) (Just account)
+       else vm' & set (#env % #contracts % at (LitAddr addr)) (Just account)
   ) vm addrs
   where
     account =
-      (initialContract (RuntimeCode (ConcreteRuntimeCode mempty)))
-        { nonce = 0, balance = fromInteger b }
-    deployed addr = addr `Map.member` vm.env.contracts
+      initialContract (RuntimeCode (ConcreteRuntimeCode mempty))
+        & set #nonce (Just 0)
+        & set #balance (Lit $ fromInteger b)
+    deployed addr = LitAddr addr `Map.member` vm.env.contracts
 
 -- | Address to load the first library
 addrLibrary :: Addr
@@ -185,7 +188,7 @@ loadSpecified
   :: Env
   -> Maybe Text
   -> [SolcContract]
-  -> IO (VM, [SolSignature], [Text], SignatureMap)
+  -> IO (VM RealWorld, [SolSignature], [Text], SignatureMap)
 loadSpecified env name cs = do
   let solConf = env.cfg.solConf
 
@@ -222,11 +225,11 @@ loadSpecified env name cs = do
           Just ne -> Map.singleton (getBytecodeMetadata mainContract.runtimeCode) ne
           Nothing -> mempty
 
-    -- Set up initial VM, either with chosen contract or Etheno initialization file
-    -- need to use snd to add to ABI dict
-    vm = initialVM solConf.allowFFI
-           & #block % #gaslimit .~ unlimitedGasPerBlock
-           & #block % #maxCodeSize .~ fromIntegral solConf.codeSize
+  -- Set up initial VM, either with chosen contract or Etheno initialization file
+  -- need to use snd to add to ABI dict
+  initVM <- stToIO $ initialVM solConf.allowFFI
+  let vm = initVM & #block % #gaslimit .~ unlimitedGasPerBlock
+                  & #block % #maxCodeSize .~ fromIntegral solConf.codeSize
 
   blank' <- maybe (pure vm) (loadEthenoBatch solConf.allowFFI) solConf.initialize
   let blank = populateAddresses (Set.insert solConf.deployer solConf.sender)
@@ -362,7 +365,7 @@ loadSolTests
   :: Env
   -> NonEmpty FilePath
   -> Maybe Text
-  -> IO (VM, World, [EchidnaTest])
+  -> IO (VM RealWorld, World, [EchidnaTest])
 loadSolTests env fp name = do
   let solConf = env.cfg.solConf
   buildOutputs <- compileContracts solConf fp
@@ -371,7 +374,7 @@ loadSolTests env fp name = do
   let
     eventMap = Map.unions $ map (.eventMap) contracts
     world = World solConf.sender mempty Nothing [] eventMap
-    echidnaTests = createTests solConf.testMode True testNames vm.state.contract funs
+    echidnaTests = createTests solConf.testMode True testNames (forceAddr vm.state.contract) funs
   pure (vm, world, echidnaTests)
 
 mkLargeAbiInt :: Int -> AbiValue
diff --git a/lib/Echidna/Symbolic.hs b/lib/Echidna/Symbolic.hs
new file mode 100644
index 000000000..2f9625b14
--- /dev/null
+++ b/lib/Echidna/Symbolic.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+
+module Echidna.Symbolic where
+
+import Data.ByteString (ByteString)
+import EVM.Types (Expr(..), EType(..), W256, Addr)
+
+forceBuf :: Expr Buf -> ByteString
+forceBuf b = case b of
+  ConcreteBuf b' -> b'
+  _ -> error $ "expected ConcreteBuf: " <> show b
+
+forceWord :: Expr EWord -> W256
+forceWord x = case x of
+  Lit x' -> x'
+  WAddr x' -> fromIntegral $ forceAddr x'
+  _ -> error $ "expected Lit: " <> show x
+
+forceAddr :: Expr EAddr -> Addr
+forceAddr x = case x of
+  LitAddr x' -> x'
+  _ -> error $ "expected LitAddr: " <> show x
diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs
index d5a11b5e2..fab706523 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -7,6 +7,7 @@ import Prelude hiding (Word)
 import Control.Monad.Catch (MonadThrow)
 import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.Reader.Class (MonadReader, asks)
+import Control.Monad.ST (RealWorld)
 import Data.ByteString qualified as BS
 import Data.ByteString.Lazy qualified as LBS
 import Data.Text (Text)
@@ -19,7 +20,7 @@ import EVM.Types hiding (Env)
 import Echidna.ABI
 import Echidna.Events (Events, extractEvents)
 import Echidna.Exec
-import Echidna.Types.Buffer (forceBuf)
+import Echidna.Symbolic (forceBuf)
 import Echidna.Types.Config
 import Echidna.Types.Signature (SolSignature)
 import Echidna.Types.Test
@@ -31,7 +32,7 @@ data CallRes = ResFalse | ResTrue | ResRevert | ResOther
   deriving (Eq, Show)
 
 --- | Given a 'VMResult', classify it assuming it was the result of a call to an Echidna test.
-classifyRes :: VMResult -> CallRes
+classifyRes :: VMResult s -> CallRes
 classifyRes (VMSuccess b)
   | forceBuf b == encodeAbiValue (AbiBool True)  = ResTrue
   | forceBuf b == encodeAbiValue (AbiBool False) = ResFalse
@@ -39,7 +40,7 @@ classifyRes (VMSuccess b)
 classifyRes Reversion = ResRevert
 classifyRes _         = ResOther
 
-getResultFromVM :: VM -> TxResult
+getResultFromVM :: VM s -> TxResult
 getResultFromVM vm =
   case vm.result of
     Just r -> getResult r
@@ -137,8 +138,8 @@ updateOpenTest _ _ _ = error "Invalid type of test"
 checkETest
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
   => EchidnaTest
-  -> VM
-  -> m (TestValue, VM)
+  -> VM RealWorld
+  -> m (TestValue, VM RealWorld)
 checkETest test vm = case test.testType of
   Exploration -> pure (BoolValue True, vm) -- These values are never used
   PropertyTest n a -> checkProperty vm n a
@@ -150,10 +151,10 @@ checkETest test vm = case test.testType of
 -- | Given a property test, evaluate it and see if it currently passes.
 checkProperty
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
-  => VM
+  => VM RealWorld
   -> Text
   -> Addr
-  -> m (TestValue, VM)
+  -> m (TestValue, VM RealWorld)
 checkProperty vm f a = do
   case vm.result of
     Just (VMSuccess _) -> do
@@ -164,11 +165,11 @@ checkProperty vm f a = do
 
 runTx
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
-  => VM
+  => VM RealWorld
   -> Text
   -> (Addr -> Addr)
   -> Addr
-  -> m VM
+  -> m (VM RealWorld)
 runTx vm f s a = do
   -- Our test is a regular user-defined test, we exec it and check the result
   g <- asks (.cfg.txConf.propGas)
@@ -176,7 +177,7 @@ runTx vm f s a = do
   pure vm'
 
 --- | Extract a test value from an execution.
-getIntFromResult :: Maybe VMResult -> TestValue
+getIntFromResult :: Maybe (VMResult RealWorld) -> TestValue
 getIntFromResult (Just (VMSuccess b)) =
   let bs = forceBuf b
   in case decodeAbiValue (AbiIntType 256) $ LBS.fromStrict bs of
@@ -187,10 +188,10 @@ getIntFromResult _ = IntValue minBound
 -- | Given a property test, evaluate it and see if it currently passes.
 checkOptimization
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
-  => VM
+  => VM RealWorld
   -> Text
   -> Addr
-  -> m (TestValue, VM)
+  -> m (TestValue, VM RealWorld)
 checkOptimization vm f a = do
   TestConf _ s <- asks (.cfg.testConf)
   vm' <- runTx vm f s a
@@ -198,10 +199,10 @@ checkOptimization vm f a = do
 
 checkStatefulAssertion
   :: (MonadReader Env m, MonadThrow m)
-  => VM
+  => VM RealWorld
   -> SolSignature
   -> Addr
-  -> m (TestValue, VM)
+  -> m (TestValue, VM RealWorld)
 checkStatefulAssertion vm sig addr = do
   dappInfo <- asks (.dapp)
   let
@@ -210,7 +211,7 @@ checkStatefulAssertion vm sig addr = do
       BS.isPrefixOf (BS.take 4 (abiCalldata (encodeSig sig) mempty))
                     (forceBuf vm.state.calldata)
     -- Whether the last transaction executed a function on the contract `addr`.
-    isCorrectAddr = addr == vm.state.codeContract
+    isCorrectAddr = LitAddr addr == vm.state.codeContract
     isCorrectTarget = isCorrectFn && isCorrectAddr
     -- Whether the last transaction executed opcode 0xfe, meaning an assertion failure.
     isAssertionFailure = case vm.result of
@@ -228,10 +229,10 @@ assumeMagicReturnCode = "FOUNDRY::ASSUME\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0"
 
 checkDapptestAssertion
   :: (MonadReader Env m, MonadThrow m)
-  => VM
+  => VM RealWorld
   -> SolSignature
   -> Addr
-  -> m (TestValue, VM)
+  -> m (TestValue, VM RealWorld)
 checkDapptestAssertion vm sig addr = do
   let
     -- Whether the last transaction has any value
@@ -245,21 +246,21 @@ checkDapptestAssertion vm sig addr = do
         not $ BS.isSuffixOf assumeMagicReturnCode bs
       Just (VMFailure _) -> True
       _ -> False
-    isCorrectAddr = addr == vm.state.codeContract
+    isCorrectAddr = LitAddr addr == vm.state.codeContract
     isCorrectTarget = isCorrectFn && isCorrectAddr
     isFailure = not hasValue && (isCorrectTarget && isAssertionFailure)
   pure (BoolValue (not isFailure), vm)
 
 checkCall
   :: (MonadReader Env m, MonadThrow m)
-  => VM
-  -> (DappInfo -> VM -> TestValue)
-  -> m (TestValue, VM)
+  => VM RealWorld
+  -> (DappInfo -> VM RealWorld -> TestValue)
+  -> m (TestValue, VM RealWorld)
 checkCall vm f = do
   dappInfo <- asks (.dapp)
   pure (f dappInfo vm, vm)
 
-checkAssertionTest :: DappInfo -> VM -> TestValue
+checkAssertionTest :: DappInfo -> VM RealWorld -> TestValue
 checkAssertionTest dappInfo vm =
   let events = extractEvents False dappInfo vm
   in BoolValue $ null events || not (checkAssertionEvent events)
@@ -267,19 +268,19 @@ checkAssertionTest dappInfo vm =
 checkAssertionEvent :: Events -> Bool
 checkAssertionEvent = any (T.isPrefixOf "AssertionFailed(")
 
-checkSelfDestructedTarget :: Addr -> DappInfo -> VM -> TestValue
+checkSelfDestructedTarget :: Addr -> DappInfo -> VM RealWorld -> TestValue
 checkSelfDestructedTarget addr _ vm =
   let selfdestructs' = vm.tx.substate.selfdestructs
-  in BoolValue $ addr `notElem` selfdestructs'
+  in BoolValue $ LitAddr addr `notElem` selfdestructs'
 
-checkAnySelfDestructed :: DappInfo -> VM -> TestValue
+checkAnySelfDestructed :: DappInfo -> VM RealWorld -> TestValue
 checkAnySelfDestructed _ vm =
   BoolValue $ null vm.tx.substate.selfdestructs
 
 checkPanicEvent :: T.Text -> Events -> Bool
 checkPanicEvent n = any (T.isPrefixOf ("Panic(" <> n <> ")"))
 
-checkOverflowTest :: DappInfo -> VM -> TestValue
+checkOverflowTest :: DappInfo -> VM RealWorld-> TestValue
 checkOverflowTest dappInfo vm =
   let es = extractEvents False dappInfo vm
   in BoolValue $ null es || not (checkPanicEvent "17" es)
diff --git a/lib/Echidna/Transaction.hs b/lib/Echidna/Transaction.hs
index 05ad3505d..f78b43da2 100644
--- a/lib/Echidna/Transaction.hs
+++ b/lib/Echidna/Transaction.hs
@@ -7,32 +7,33 @@ import Optics.Core
 import Optics.State.Operators
 
 import Control.Monad (join)
-import Control.Monad.Random.Strict (MonadRandom, getRandomR, uniform)
-import Control.Monad.State.Strict (MonadState, gets, modify')
+import Control.Monad.Random.Strict (MonadRandom, getRandomR, uniform, MonadIO)
+import Control.Monad.State.Strict (MonadState, gets, modify', execState)
+import Control.Monad.ST (RealWorld)
 import Data.Map (Map, toList)
 import Data.Map qualified as Map
-import Data.Maybe (mapMaybe)
+import Data.Maybe (mapMaybe, fromJust)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Vector qualified as V
 
-import EVM (initialContract, loadContract, bytecode)
+import EVM (initialContract, loadContract, bytecode, resetState)
 import EVM.ABI (abiValueType)
 import EVM.Types hiding (VMOpts(timestamp, gasprice))
 
 import Echidna.ABI
-import Echidna.Types.Random
 import Echidna.Orphans.JSON ()
+import Echidna.Symbolic (forceBuf, forceWord, forceAddr)
 import Echidna.Types (fromEVM)
-import Echidna.Types.Buffer (forceBuf, forceLit)
+import Echidna.Types.Random
 import Echidna.Types.Signature
   (SignatureMap, SolCall, ContractA, MetadataCache, lookupBytecodeMetadata)
 import Echidna.Types.Tx
 import Echidna.Types.World (World(..))
 import Echidna.Types.Campaign
 
-hasSelfdestructed :: VM -> Addr -> Bool
-hasSelfdestructed vm addr = addr `elem` vm.tx.substate.selfdestructs
+hasSelfdestructed :: VM s -> Addr -> Bool
+hasSelfdestructed vm addr = LitAddr addr `elem` vm.tx.substate.selfdestructs
 
 -- | If half a tuple is zero, make both halves zero. Useful for generating
 -- delays, since block number only goes up with timestamp
@@ -56,7 +57,7 @@ genTx
   => MetadataCache
   -> World
   -> TxConf
-  -> Map Addr Contract
+  -> Map (Expr EAddr) Contract
   -> m Tx
 genTx memo world txConf deployedContracts = do
   genDict <- gets (.genDict)
@@ -77,11 +78,11 @@ genTx memo world txConf deployedContracts = do
             , delay = level ts
             }
   where
-    toContractA :: SignatureMap -> (Addr, Contract) -> Maybe ContractA
+    toContractA :: SignatureMap -> (Expr EAddr, Contract) -> Maybe ContractA
     toContractA sigMap (addr, c) =
-      let bc = forceBuf $ view bytecode c
+      let bc = forceBuf $ fromJust $ view bytecode c
           metadata = lookupBytecodeMetadata memo bc
-      in (addr,) <$> Map.lookup metadata sigMap
+      in (forceAddr addr,) <$> Map.lookup metadata sigMap
 
 genDelay :: MonadRandom m => W256 -> Set W256 -> m W256
 genDelay mv ds = do
@@ -152,47 +153,46 @@ mutateTx tx = pure tx
 
 -- | Given a 'Transaction', set up some 'VM' so it can be executed. Effectively, this just brings
 -- 'Transaction's \"on-chain\".
-setupTx :: MonadState VM m => Tx -> m ()
+setupTx :: (MonadIO m, MonadState (VM RealWorld) m) => Tx -> m ()
 setupTx tx@Tx{call = NoCall} = fromEVM $ do
+  resetState
   modify' $ \vm -> vm
-    { state = resetState vm.state
+    { state = vm.state
     , block = advanceBlock vm.block tx.delay
     }
-  loadContract tx.dst
+  modify' $ execState $ loadContract (LitAddr tx.dst)
 
 setupTx tx@Tx{call} = fromEVM $ do
+  resetState
   modify' $ \vm -> vm
     { result = Nothing
-    , state = (resetState vm.state)
+    , state = vm.state
                  { gas = tx.gas
-                 , caller = Lit (fromIntegral tx.src)
+                 , caller = LitAddr (fromIntegral tx.src)
                  , callvalue = Lit tx.value
                  }
     , block = advanceBlock vm.block tx.delay
-    , tx = vm.tx { gasprice = tx.gasprice, origin = tx.src }
+    , tx = vm.tx { gasprice = tx.gasprice, origin = LitAddr tx.src }
     }
   case call of
     SolCreate bc -> do
-      #env % #contracts % at tx.dst .=
-        Just (initialContract (InitCode bc mempty) & set #balance tx.value)
-      loadContract tx.dst
+      #env % #contracts % at (LitAddr tx.dst) .=
+        Just (initialContract (InitCode bc mempty) & set #balance (Lit tx.value))
+      modify' $ execState $ loadContract (LitAddr tx.dst)
       #state % #code .= RuntimeCode (ConcreteRuntimeCode bc)
     SolCall cd -> do
       incrementBalance
-      loadContract tx.dst
+      modify' $ execState $ loadContract (LitAddr tx.dst)
       #state % #calldata .= ConcreteBuf (encode cd)
     SolCalldata cd -> do
       incrementBalance
-      loadContract tx.dst
+      modify' $ execState $ loadContract (LitAddr tx.dst)
       #state % #calldata .= ConcreteBuf cd
   where
-    incrementBalance = #env % #contracts % ix tx.dst % #balance %= (+ tx.value)
+    incrementBalance = #env % #contracts % ix (LitAddr tx.dst) % #balance %= (\v -> Lit $ forceWord v + tx.value)
     encode (n, vs) = abiCalldata (encodeSig (n, abiValueType <$> vs)) $ V.fromList vs
 
-resetState :: FrameState -> FrameState
-resetState s = s { pc = 0, stack = mempty, memory = mempty }
-
 advanceBlock :: Block -> (W256, W256) -> Block
 advanceBlock blk (t,b) =
-  blk { timestamp = Lit (forceLit blk.timestamp + t)
+  blk { timestamp = Lit (forceWord blk.timestamp + t)
       , number = blk.number + b }
diff --git a/lib/Echidna/Types.hs b/lib/Echidna/Types.hs
index b3b53a8fc..1fbdd829e 100644
--- a/lib/Echidna/Types.hs
+++ b/lib/Echidna/Types.hs
@@ -1,7 +1,8 @@
 module Echidna.Types where
 
 import Control.Exception (Exception)
-import Control.Monad.State.Strict (MonadState, runState, get, put)
+import Control.Monad.State.Strict (MonadState, get, put, MonadIO(liftIO), runStateT)
+import Control.Monad.ST (RealWorld, stToIO)
 import Data.Word (Word64)
 import EVM (initialContract)
 import EVM.Types
@@ -21,12 +22,12 @@ type Gas = Word64
 type MutationConsts a = (a, a, a, a)
 
 -- | Transform an EVM action from HEVM to our MonadState VM
-fromEVM :: MonadState VM m => EVM a -> m a
+fromEVM :: (MonadIO m, MonadState (VM RealWorld) m) => EVM RealWorld r -> m r
 fromEVM evmAction = do
   vm <- get
-  let (r, vm') = runState evmAction vm
+  (result, vm') <- liftIO $ stToIO $ runStateT evmAction vm
   put vm'
-  pure r
+  pure result
 
 emptyAccount :: Contract
 emptyAccount = initialContract (RuntimeCode (ConcreteRuntimeCode mempty))
diff --git a/lib/Echidna/Types/Buffer.hs b/lib/Echidna/Types/Buffer.hs
deleted file mode 100644
index 9ff648128..000000000
--- a/lib/Echidna/Types/Buffer.hs
+++ /dev/null
@@ -1,16 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-
-module Echidna.Types.Buffer where
-
-import Data.ByteString (ByteString)
-import EVM.Types (Expr(ConcreteBuf, Lit), EType(Buf, EWord), W256)
-
-forceBuf :: Expr 'Buf -> ByteString
-forceBuf (ConcreteBuf b) = b
-forceBuf _ = error "expected ConcreteBuf"
-
-forceLit :: Expr 'EWord -> W256
-forceLit x = case x of
-  Lit x' -> x'
-  _ -> error "expected Lit"
diff --git a/lib/Echidna/Types/Test.hs b/lib/Echidna/Types/Test.hs
index 9e8958387..ffc83380c 100644
--- a/lib/Echidna/Types/Test.hs
+++ b/lib/Echidna/Types/Test.hs
@@ -1,5 +1,6 @@
 module Echidna.Types.Test where
 
+import Control.Monad.ST (RealWorld)
 import Data.Aeson (ToJSON(..), object)
 import Data.DoubleWord (Int256)
 import Data.Maybe (maybeToList)
@@ -18,7 +19,7 @@ type TestMode = String
 
 -- | Configuration for the creation of Echidna tests.
 data TestConf = TestConf
-  { classifier :: Text -> VM -> Bool
+  { classifier :: Text -> VM RealWorld -> Bool
     -- ^ Given a VM state and test name, check if a test just passed (typically
     -- examining '_result'.)
   , testSender :: Addr -> Addr
@@ -51,7 +52,7 @@ data TestType
   = PropertyTest Text Addr
   | OptimizationTest Text Addr
   | AssertionTest Bool SolSignature Addr
-  | CallTest Text (DappInfo -> VM -> TestValue)
+  | CallTest Text (DappInfo -> VM RealWorld -> TestValue)
   | Exploration
 
 instance Eq TestType where
diff --git a/lib/Echidna/Types/Tx.hs b/lib/Echidna/Types/Tx.hs
index fc9a8fd96..ba39bf6e6 100644
--- a/lib/Echidna/Types/Tx.hs
+++ b/lib/Echidna/Types/Tx.hs
@@ -20,7 +20,7 @@ import EVM.ABI (encodeAbiValue, AbiValue(..), AbiType)
 import EVM.Types
 
 import Echidna.Orphans.JSON ()
-import Echidna.Types.Buffer (forceBuf)
+import Echidna.Symbolic (forceBuf)
 import Echidna.Types.Signature (SolCall)
 import Control.DeepSeq (NFData)
 import GHC.Generics (Generic)
@@ -176,6 +176,7 @@ data TxResult
   | ErrorMaxIterationsReached
   | ErrorPrecompileFailure
   | ErrorUnexpectedSymbolic
+  | ErrorJumpIntoSymbolicCode
   | ErrorDeadPath
   | ErrorChoose -- not entirely sure what this is
   | ErrorWhiffNotUnique
@@ -202,7 +203,7 @@ data TxConf = TxConf
   }
 
 -- | Transform a VMResult into a more hash friendly sum type
-getResult :: VMResult -> TxResult
+getResult :: VMResult s -> TxResult
 getResult = \case
   VMSuccess b | forceBuf b == encodeAbiValue (AbiBool True)  -> ReturnTrue
               | forceBuf b == encodeAbiValue (AbiBool False) -> ReturnFalse
@@ -213,6 +214,7 @@ getResult = \case
 
   Unfinished (UnexpectedSymbolicArg{})    -> ErrorUnexpectedSymbolic
   Unfinished (MaxIterationsReached _ _)   -> ErrorMaxIterationsReached
+  Unfinished (JumpIntoSymbolicCode _ _)   -> ErrorJumpIntoSymbolicCode
 
   VMFailure (BalanceTooLow _ _)           -> ErrorBalanceTooLow
   VMFailure (UnrecognizedOpcode _)        -> ErrorUnrecognizedOpcode
diff --git a/lib/Echidna/UI.hs b/lib/Echidna/UI.hs
index 559e22769..9d68dfd76 100644
--- a/lib/Echidna/UI.hs
+++ b/lib/Echidna/UI.hs
@@ -21,6 +21,7 @@ import Control.Monad.Catch
 import Control.Monad.Random.Strict (MonadRandom)
 import Control.Monad.Reader
 import Control.Monad.State.Strict hiding (state)
+import Control.Monad.ST (RealWorld)
 import Data.ByteString.Lazy qualified as BS
 import Data.List.Split (chunksOf)
 import Data.Map (Map)
@@ -57,7 +58,7 @@ data UIEvent =
 -- print non-interactive output in desired format at the end
 ui
   :: (MonadCatch m, MonadRandom m, MonadReader Env m, MonadUnliftIO m)
-  => VM      -- ^ Initial VM state
+  => VM RealWorld -- ^ Initial VM state
   -> World   -- ^ Initial world state
   -> GenDict
   -> [[Tx]]
diff --git a/src/Main.hs b/src/Main.hs
index 9eef594c8..7645ec055 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -18,7 +18,7 @@ import Data.IORef (newIORef, readIORef)
 import Data.List.NonEmpty qualified as NE
 import Data.Map (Map)
 import Data.Map qualified as Map
-import Data.Maybe (fromMaybe, isJust)
+import Data.Maybe (fromMaybe, isJust, fromJust)
 import Data.Set qualified as Set
 import Data.Text (Text)
 import Data.Time.Clock.System (getSystemTime, systemSeconds)
@@ -41,7 +41,7 @@ import EVM.Types (Addr, Contract(..), keccak', W256)
 
 import Echidna
 import Echidna.Config
-import Echidna.Types.Buffer (forceBuf)
+import Echidna.Symbolic (forceBuf)
 import Echidna.Types.Campaign
 import Echidna.Types.Config
 import Echidna.Types.Solidity
@@ -183,7 +183,7 @@ main = withUtf8 $ withCP65001 $ do
   -- code fetched from the outside
   externalSolcContract :: Addr -> Contract -> IO (Maybe (SourceCache, SolcContract))
   externalSolcContract addr c = do
-    let runtimeCode = forceBuf $ view bytecode c
+    let runtimeCode = forceBuf $ fromJust $ view bytecode c
     putStr $ "Fetching Solidity source for contract at address " <> show addr <> "... "
     srcRet <- Etherscan.fetchContractSource addr
     putStrLn $ if isJust srcRet then "Success!" else "Error!"
@@ -350,4 +350,3 @@ overrideConfig config Options{..} = do
       , testMode = maybe solConf.testMode validateTestMode cliTestMode
       , allContracts = cliAllContracts || solConf.allContracts
       }
-
diff --git a/stack.yaml b/stack.yaml
index cb19c1775..8d199652e 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -4,8 +4,8 @@ packages:
 - '.'
 
 extra-deps:
-- git: https://github.com/elopez/hevm.git
-  commit: 6ffb685574b556ef148c884b412a92c6909c2b4f
+- git: https://github.com/ethereum/hevm.git
+  commit: 91d906b6593f2ba74748fff9a7d34eadf1980ceb
 
 - restless-git-0.7@sha256:346a5775a586f07ecb291036a8d3016c3484ccdc188b574bcdec0a82c12db293,968
 - s-cargot-0.1.4.0@sha256:61ea1833fbb4c80d93577144870e449d2007d311c34d74252850bb48aa8c31fb,3525