From 494eb9241d1417015870420431de6e691c821607 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?=
 <2642849+elopez@users.noreply.github.com>
Date: Tue, 28 Nov 2023 13:46:16 -0300
Subject: [PATCH 01/20] nix: static builds and release workflow (#1133)

* flake.nix: static build support

Adds a "redistributable" flavor of Echidna that is fully static on
Linux, and mostly static on macOS.

* ci: add Nix & release workflow

Replaces previous Nix workflow

* ci: release: add job timeouts

* ci: release: configure Cachix

* README: update echidna-bundle references to echidna-redistributable

* Fix TERMINFO path for Nix release builds on Linux

ncurses in Nix is built with a TERMINFO path that references `/nix`.
This causes the binaries fail when ran on non-nix systems, unless
TERMINFO=/usr/share/terminfo is exported. This patches the binaries
to use a more sensible default TERMINFO path.

See also commit f76a7f4a

* flake.nix: remove redundant stripping
---
 .github/workflows/nix.yml     |  24 --------
 .github/workflows/release.yml | 111 ++++++++++++++++++++++++++++++++++
 README.md                     |   5 +-
 flake.nix                     |  79 +++++++++++++++++++++++-
 4 files changed, 190 insertions(+), 29 deletions(-)
 delete mode 100644 .github/workflows/nix.yml
 create mode 100644 .github/workflows/release.yml

diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
deleted file mode 100644
index 4f15517e2..000000000
--- a/.github/workflows/nix.yml
+++ /dev/null
@@ -1,24 +0,0 @@
-name: Nix
-
-on:
-  push:
-    branches:
-    - master
-  pull_request:
-    branches:
-    - master
-
-jobs:
-  test:
-    runs-on: ${{ matrix.os }}
-    strategy:
-      matrix:
-        os:
-          - ubuntu-latest
-          - macos-latest
-    steps:
-    - uses: actions/checkout@v4
-    - uses: cachix/install-nix-action@v23
-      with:
-        nix_path: nixpkgs=channel:nixos-unstable
-    - run: nix-build
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
new file mode 100644
index 000000000..fad150b10
--- /dev/null
+++ b/.github/workflows/release.yml
@@ -0,0 +1,111 @@
+name: "Nix and release"
+on:
+  push:
+    branches:
+      - master
+    tags:
+      - "v*"
+  pull_request:
+    branches:
+      - master
+
+jobs:
+  nixBuild:
+    name: Build ${{ matrix.name }} binary
+    timeout-minutes: ${{ matrix.timeout || 30 }}
+    runs-on: ${{ matrix.os }}
+    permissions:
+      contents: read
+    outputs:
+      version: ${{ steps.version.outputs.version }}
+    strategy:
+      matrix:
+        include:
+          - os: ubuntu-latest
+            name: Linux (x86_64)
+            tuple: x86_64-linux
+            timeout: 180
+          - os: macos-latest
+            name: macOS (x86_64)
+            tuple: x86_64-macos
+          - os: macos-latest-xlarge
+            name: macOS (aarch64)
+            tuple: aarch64-macos
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install Nix
+        uses: DeterminateSystems/nix-installer-action@v6
+
+      - name: Configure Cachix
+        uses: cachix/cachix-action@v12
+        with:
+          name: trailofbits
+          authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+
+      - name: Configure Nix cache
+        if: runner.arch == 'X64'
+        # Unfortunately the action does not work on ARM runners
+        uses: DeterminateSystems/magic-nix-cache-action@v2
+        with:
+          upstream-cache: https://trailofbits.cachix.org
+
+      - name: Obtain version number
+        id: version
+        run: |
+          if [[ "$GIT_REF" =~ ^refs/tags/v.* ]]; then
+            echo "version=$(echo "$GIT_REF" | sed 's#^refs/tags/v##')" >> "$GITHUB_OUTPUT"
+          else
+            echo "version=HEAD-$(echo "$GIT_SHA" | cut -c1-7)" >> "$GITHUB_OUTPUT"
+          fi
+        env:
+          GIT_REF: ${{ github.ref }}
+          GIT_SHA: ${{ github.sha }}
+
+      - name: Build dynamic echidna
+        run: |
+          nix build .#echidna
+
+      - name: Build redistributable echidna
+        run: |
+          nix build .#echidna-redistributable --out-link redistributable
+          tar -czf "echidna-${{ steps.version.outputs.version }}-${{ matrix.tuple }}.tar.gz" -C ./redistributable/bin/ echidna
+
+      - name: Upload artifact
+        uses: actions/upload-artifact@v3
+        with:
+          name: echidna-redistributable
+          path: echidna-${{ steps.version.outputs.version }}-${{ matrix.tuple }}.tar.gz
+
+  release:
+    name: Create release
+    timeout-minutes: 10
+    needs: [nixBuild]
+    if: startsWith(github.ref, 'refs/tags/')
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+      id-token: write
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Download binaries
+        uses: actions/download-artifact@v3
+        with:
+          name: echidna-redistributable
+
+      - name: Sign binaries
+        uses: sigstore/gh-action-sigstore-python@v2.1.0
+        with:
+          inputs: ./echidna-*.tar.gz
+
+      - name: Create GitHub release and upload binaries
+        uses: softprops/action-gh-release@v0.1.15
+        with:
+          draft: true
+          name: "Echidna ${{ needs.nixBuild.outputs.version }}"
+          files: |
+            ./echidna-*.tar.gz
+            ./echidna-*.tar.gz.sigstore
diff --git a/README.md b/README.md
index 48eed773c..7a747eb13 100644
--- a/README.md
+++ b/README.md
@@ -272,10 +272,11 @@ $ nix run github:crytic/echidna/v2.1.1 # specific ref (tag/branch/commit)
 ```
 
 To build a standalone release for non-Nix macOS systems, the following will
-bundle Echidna and all linked dylibs:
+build Echidna in a mostly static binary. This can also be used on Linux systems
+to produce a fully static binary.
 
 ```sh
-$ nix build .#echidna-bundle
+$ nix build .#echidna-redistributable
 ```
 
 Nix will automatically install all the dependencies required for development
diff --git a/flake.nix b/flake.nix
index 0a740d00b..4206fa77a 100644
--- a/flake.nix
+++ b/flake.nix
@@ -15,7 +15,10 @@
   outputs = { self, nixpkgs, flake-utils, nix-bundle-exe, ... }:
     flake-utils.lib.eachDefaultSystem (system:
       let
-        pkgs = nixpkgs.legacyPackages.${system};
+        systemPkgs = nixpkgs.legacyPackages.${system};
+        # prefer musl on Linux, static glibc + threading does not work properly
+        # TODO: maybe only override it for echidna-redistributable?
+        pkgs = if systemPkgs.stdenv.hostPlatform.isLinux then systemPkgs.pkgsMusl else systemPkgs;
         # this is not perfect for development as it hardcodes solc to 0.5.7, test suite runs fine though
         # would be great to integrate solc-select to be more flexible, improve this in future
         solc = pkgs.stdenv.mkDerivation {
@@ -38,6 +41,12 @@
           '';
         };
 
+        secp256k1-static = pkgs.secp256k1.overrideAttrs (attrs: {
+          configureFlags = attrs.configureFlags ++ [ "--enable-static" ];
+        });
+
+        ncurses-static = pkgs.ncurses.override { enableStatic = true; };
+
         hevm = pkgs.haskell.lib.dontCheck (
           pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
             owner = "elopez";
@@ -55,12 +64,76 @@
             (haskell.lib.compose.addTestToolDepends [ haskellPackages.hpack slither-analyzer solc ])
             (haskell.lib.compose.disableCabalFlag "static")
           ]);
+
+        echidna-static = with pkgs; lib.pipe
+          echidna
+          [
+            (haskell.lib.compose.appendConfigureFlags
+              ([
+                "--extra-lib-dirs=${stripDylib (gmp.override { withStatic = true; })}/lib"
+                "--extra-lib-dirs=${stripDylib secp256k1-static}/lib"
+                "--extra-lib-dirs=${stripDylib (libff.override { enableStatic = true; })}/lib"
+                "--extra-lib-dirs=${zlib.static}/lib"
+                "--extra-lib-dirs=${stripDylib (libffi.overrideAttrs (_: { dontDisableStatic = true; }))}/lib"
+                "--extra-lib-dirs=${stripDylib (ncurses-static)}/lib"
+              ] ++ (if stdenv.hostPlatform.isDarwin then [
+                "--extra-lib-dirs=${stripDylib (libiconv.override { enableStatic = true; })}/lib"
+              ] else [])))
+            (haskell.lib.compose.enableCabalFlag "static")
+          ];
+
+        # "static" binary for distribution
+        # on linux this is actually a real fully static binary
+        # on macos this has everything except libcxx and libsystem
+        # statically linked. we can be confident that these two will always
+        # be provided in a well known location by macos itself.
+        echidnaRedistributable = let
+          grep = "${pkgs.gnugrep}/bin/grep";
+          perl = "${pkgs.perl}/bin/perl";
+          otool = "${pkgs.darwin.binutils.bintools}/bin/otool";
+          install_name_tool = "${pkgs.darwin.binutils.bintools}/bin/install_name_tool";
+          codesign_allocate = "${pkgs.darwin.binutils.bintools}/bin/codesign_allocate";
+          codesign = "${pkgs.darwin.sigtool}/bin/codesign";
+        in if pkgs.stdenv.isLinux
+        then pkgs.runCommand "echidna-stripNixRefs" {} ''
+          mkdir -p $out/bin
+          cp ${pkgs.haskell.lib.dontCheck echidna-static}/bin/echidna $out/bin/
+          # fix TERMINFO path in ncurses
+          ${perl} -i -pe 's#(${ncurses-static}/share/terminfo)#"/usr/share/terminfo" . "\x0" x (length($1) - 19)#e' $out/bin/echidna
+          chmod 555 $out/bin/echidna
+        '' else pkgs.runCommand "echidna-stripNixRefs" {} ''
+          mkdir -p $out/bin
+          cp ${pkgs.haskell.lib.dontCheck echidna-static}/bin/echidna $out/bin/
+          # get the list of dynamic libs from otool and tidy the output
+          libs=$(${otool} -L $out/bin/echidna | tail -n +2 | sed 's/^[[:space:]]*//' | cut -d' ' -f1)
+          # get the path for libcxx
+          cxx=$(echo "$libs" | ${grep} '^/nix/store/.*-libcxx')
+          # rewrite /nix/... library paths to point to /usr/lib
+          chmod 777 $out/bin/echidna
+          ${install_name_tool} -change "$cxx" /usr/lib/libc++.1.dylib $out/bin/echidna
+          # fix TERMINFO path in ncurses
+          ${perl} -i -pe 's#(${ncurses-static}/share/terminfo)#"/usr/share/terminfo" . "\x0" x (length($1) - 19)#e' $out/bin/echidna
+          # re-sign binary
+          CODESIGN_ALLOCATE=${codesign_allocate} ${codesign} -f -s - $out/bin/echidna
+          chmod 555 $out/bin/echidna
+        '';
+
+        # if we pass a library folder to ghc via --extra-lib-dirs that contains
+        # only .a files, then ghc will link that library statically instead of
+        # dynamically (even if --enable-executable-static is not passed to cabal).
+        # we use this trick to force static linking of some libraries on macos.
+        stripDylib = drv : pkgs.runCommand "${drv.name}-strip-dylibs" {} ''
+          mkdir -p $out
+          mkdir -p $out/lib
+          cp -r ${drv}/* $out/
+          rm -rf $out/**/*.dylib
+        '';
+
       in rec {
         packages.echidna = echidna;
         packages.default = echidna;
 
-        packages.echidna-bundle =
-          pkgs.callPackage nix-bundle-exe {} (pkgs.haskell.lib.dontCheck echidna);
+        packages.echidna-redistributable = echidnaRedistributable;
 
         devShell = with pkgs;
           haskellPackages.shellFor {

From d2eac5090cc3b62581b841c4de7a9399e9441b71 Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Tue, 5 Dec 2023 10:48:08 +0100
Subject: [PATCH 02/20] Bump DeterminateSystems/nix-installer-action from 6 to
 8 (#1144)

Bumps [DeterminateSystems/nix-installer-action](https://github.com/determinatesystems/nix-installer-action) from 6 to 8.
- [Release notes](https://github.com/determinatesystems/nix-installer-action/releases)
- [Commits](https://github.com/determinatesystems/nix-installer-action/compare/v6...v8)

---
updated-dependencies:
- dependency-name: DeterminateSystems/nix-installer-action
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
---
 .github/workflows/release.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index fad150b10..c523f1d92 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -36,7 +36,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Install Nix
-        uses: DeterminateSystems/nix-installer-action@v6
+        uses: DeterminateSystems/nix-installer-action@v8
 
       - name: Configure Cachix
         uses: cachix/cachix-action@v12

From 39c4deb324604d2f842ef251df6eb135de8caee2 Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Tue, 5 Dec 2023 10:48:24 +0100
Subject: [PATCH 03/20] Bump cachix/cachix-action from 12 to 13 (#1145)

Bumps [cachix/cachix-action](https://github.com/cachix/cachix-action) from 12 to 13.
- [Release notes](https://github.com/cachix/cachix-action/releases)
- [Commits](https://github.com/cachix/cachix-action/compare/v12...v13)

---
updated-dependencies:
- dependency-name: cachix/cachix-action
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
---
 .github/workflows/release.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index c523f1d92..6fdea65c4 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -39,7 +39,7 @@ jobs:
         uses: DeterminateSystems/nix-installer-action@v8
 
       - name: Configure Cachix
-        uses: cachix/cachix-action@v12
+        uses: cachix/cachix-action@v13
         with:
           name: trailofbits
           authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}

From 25361bdd16b022fc0e967b43f1bce6a6d91740bb Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Tue, 5 Dec 2023 10:48:52 +0100
Subject: [PATCH 04/20] Bump cachix/install-nix-action from 23 to 24 (#1146)

Bumps [cachix/install-nix-action](https://github.com/cachix/install-nix-action) from 23 to 24.
- [Release notes](https://github.com/cachix/install-nix-action/releases)
- [Commits](https://github.com/cachix/install-nix-action/compare/v23...v24)

---
updated-dependencies:
- dependency-name: cachix/install-nix-action
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
---
 .github/workflows/hlint.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/hlint.yml b/.github/workflows/hlint.yml
index 15e46a337..a0b53307f 100644
--- a/.github/workflows/hlint.yml
+++ b/.github/workflows/hlint.yml
@@ -16,7 +16,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Install Nix
-        uses: cachix/install-nix-action@v23
+        uses: cachix/install-nix-action@v24
         with:
           nix_path: nixpkgs=channel:nixos-unstable
 

From 60a68b6886da6ead6a1acaecafbbc2fbf03f866c Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Tue, 26 Dec 2023 23:03:26 +0100
Subject: [PATCH 05/20] Bump sigstore/gh-action-sigstore-python from 2.1.0 to
 2.1.1 (#1149)

Bumps [sigstore/gh-action-sigstore-python](https://github.com/sigstore/gh-action-sigstore-python) from 2.1.0 to 2.1.1.
- [Release notes](https://github.com/sigstore/gh-action-sigstore-python/releases)
- [Commits](https://github.com/sigstore/gh-action-sigstore-python/compare/v2.1.0...v2.1.1)

---
updated-dependencies:
- dependency-name: sigstore/gh-action-sigstore-python
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
---
 .github/workflows/release.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 6fdea65c4..9ced68bec 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -97,7 +97,7 @@ jobs:
           name: echidna-redistributable
 
       - name: Sign binaries
-        uses: sigstore/gh-action-sigstore-python@v2.1.0
+        uses: sigstore/gh-action-sigstore-python@v2.1.1
         with:
           inputs: ./echidna-*.tar.gz
 

From 04c5a79f0be578076a07c08c5562306905a517be Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Tue, 26 Dec 2023 23:03:38 +0100
Subject: [PATCH 06/20] Bump DeterminateSystems/nix-installer-action from 8 to
 9 (#1148)

Bumps [DeterminateSystems/nix-installer-action](https://github.com/determinatesystems/nix-installer-action) from 8 to 9.
- [Release notes](https://github.com/determinatesystems/nix-installer-action/releases)
- [Commits](https://github.com/determinatesystems/nix-installer-action/compare/v8...v9)

---
updated-dependencies:
- dependency-name: DeterminateSystems/nix-installer-action
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
---
 .github/workflows/release.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 9ced68bec..99f5450c0 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -36,7 +36,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Install Nix
-        uses: DeterminateSystems/nix-installer-action@v8
+        uses: DeterminateSystems/nix-installer-action@v9
 
       - name: Configure Cachix
         uses: cachix/cachix-action@v13

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 07/20] 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 08/20] 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

From 0fab478e0b3f9176684b8f567bb497414750d6ba Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Thu, 28 Dec 2023 22:33:08 +0100
Subject: [PATCH 09/20] Bump actions/setup-python from 4 to 5 (#1147)

Bumps [actions/setup-python](https://github.com/actions/setup-python) from 4 to 5.
- [Release notes](https://github.com/actions/setup-python/releases)
- [Commits](https://github.com/actions/setup-python/compare/v4...v5)

---
updated-dependencies:
- dependency-name: actions/setup-python
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
---
 .github/workflows/ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 24455b0ab..c302d84c0 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -207,7 +207,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Setup Python
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: '3.8'
 

From 0d9588545a10478363cc0ec8e211c8d1e02eaf3c Mon Sep 17 00:00:00 2001
From: Artur Cygan <artur.cygan@trailofbits.com>
Date: Thu, 28 Dec 2023 23:23:44 +0100
Subject: [PATCH 10/20] Bump nixpkgs and default back to non-static (#1154)

---
 flake.lock | 18 +++++++++---------
 flake.nix  | 24 ++++++++++++------------
 2 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/flake.lock b/flake.lock
index 1a85b36d2..6f81b13f4 100644
--- a/flake.lock
+++ b/flake.lock
@@ -3,11 +3,11 @@
     "flake-compat": {
       "flake": false,
       "locked": {
-        "lastModified": 1673956053,
-        "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=",
+        "lastModified": 1696426674,
+        "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=",
         "owner": "edolstra",
         "repo": "flake-compat",
-        "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9",
+        "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33",
         "type": "github"
       },
       "original": {
@@ -21,11 +21,11 @@
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1692799911,
-        "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=",
+        "lastModified": 1701680307,
+        "narHash": "sha256-kAuep2h5ajznlPMD9rnQyffWG8EM/C73lejGofXvdM8=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44",
+        "rev": "4022d587cbbfd70fe950c1e2083a02621806a725",
         "type": "github"
       },
       "original": {
@@ -52,11 +52,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1693780807,
-        "narHash": "sha256-diV1X53HjSB3fIcDFieh9tGZkJ3vqJJQhTz89NbYw60=",
+        "lastModified": 1703499205,
+        "narHash": "sha256-lF9rK5mSUfIZJgZxC3ge40tp1gmyyOXZ+lRY3P8bfbg=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "84ef5335abf541d8148433489e0cf79affae3f89",
+        "rev": "e1fa12d4f6c6fe19ccb59cac54b5b3f25e160870",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 5bb59f09a..00f6a1464 100644
--- a/flake.nix
+++ b/flake.nix
@@ -15,10 +15,10 @@
   outputs = { self, nixpkgs, flake-utils, nix-bundle-exe, ... }:
     flake-utils.lib.eachDefaultSystem (system:
       let
-        systemPkgs = nixpkgs.legacyPackages.${system};
+        pkgs = nixpkgs.legacyPackages.${system};
         # prefer musl on Linux, static glibc + threading does not work properly
         # TODO: maybe only override it for echidna-redistributable?
-        pkgs = if systemPkgs.stdenv.hostPlatform.isLinux then systemPkgs.pkgsMusl else systemPkgs;
+        pkgsStatic = if pkgs.stdenv.hostPlatform.isLinux then pkgs.pkgsMusl else pkgs;
         # this is not perfect for development as it hardcodes solc to 0.5.7, test suite runs fine though
         # would be great to integrate solc-select to be more flexible, improve this in future
         solc = pkgs.stdenv.mkDerivation {
@@ -41,13 +41,13 @@
           '';
         };
 
-        secp256k1-static = pkgs.secp256k1.overrideAttrs (attrs: {
+        secp256k1-static = pkgsStatic.secp256k1.overrideAttrs (attrs: {
           configureFlags = attrs.configureFlags ++ [ "--enable-static" ];
         });
 
-        ncurses-static = pkgs.ncurses.override { enableStatic = true; };
+        ncurses-static = pkgsStatic.ncurses.override { enableStatic = true; };
 
-        hevm = pkgs.haskell.lib.dontCheck (
+        hevm = pkgs: pkgs.haskell.lib.dontCheck (
           pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
             owner = "ethereum";
             repo = "hevm";
@@ -57,16 +57,16 @@
 
         # 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.haskell.lib.dontCheck (
+        echidna = pkgs: pkgs.haskell.lib.dontCheck (
           with pkgs; lib.pipe
-          (haskellPackages.callCabal2nix "echidna" ./. { inherit hevm; })
+          (haskellPackages.callCabal2nix "echidna" ./. { inherit (hevm pkgs); })
           [
             (haskell.lib.compose.addTestToolDepends [ haskellPackages.hpack slither-analyzer solc ])
             (haskell.lib.compose.disableCabalFlag "static")
           ]);
 
-        echidna-static = with pkgs; lib.pipe
-          echidna
+        echidna-static = with pkgsStatic; lib.pipe
+          (echidna pkgsStatic)
           [
             (haskell.lib.compose.appendConfigureFlags
               ([
@@ -130,14 +130,14 @@
         '';
 
       in rec {
-        packages.echidna = echidna;
-        packages.default = echidna;
+        packages.echidna = echidna pkgs;
+        packages.default = echidna pkgs;
 
         packages.echidna-redistributable = echidnaRedistributable;
 
         devShell = with pkgs;
           haskellPackages.shellFor {
-            packages = _: [ echidna ];
+            packages = _: [ (echidna pkgs) ];
             shellHook = "hpack";
             buildInputs = [
               solc

From b7f5e79bf1d62ed476a29a36742f9da65a4a2fb7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?=
 <2642849+elopez@users.noreply.github.com>
Date: Wed, 3 Jan 2024 19:27:00 -0300
Subject: [PATCH 11/20] Upgrade actions/upload-artifact and
 actions/download-artifact to v4 (#1155)

---
 .github/workflows/ci.yml      | 6 +++---
 .github/workflows/release.yml | 9 +++++----
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index c302d84c0..a3351446f 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -158,7 +158,7 @@ jobs:
         run: GZIP=-9 tar -czf echidna.tar.gz -C $APPDATA/local/bin/ echidna.exe
 
       - name: Upload artifact
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: echidna-${{ runner.os }}
           path: echidna.tar.gz
@@ -172,7 +172,7 @@ jobs:
 
       - name: Upload testsuite
         if: runner.os != 'macOS'
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: echidna-testsuite-${{ runner.os }}
           path: echidna-testsuite*
@@ -221,7 +221,7 @@ jobs:
           SOLC_VER: ${{ matrix.solc }}
 
       - name: Download testsuite
-        uses: actions/download-artifact@v3
+        uses: actions/download-artifact@v4
         with:
          name: echidna-testsuite-${{ runner.os }}
 
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 99f5450c0..70adf4669 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -73,9 +73,9 @@ jobs:
           tar -czf "echidna-${{ steps.version.outputs.version }}-${{ matrix.tuple }}.tar.gz" -C ./redistributable/bin/ echidna
 
       - name: Upload artifact
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
-          name: echidna-redistributable
+          name: echidna-redistributable-${{ matrix.tuple }}
           path: echidna-${{ steps.version.outputs.version }}-${{ matrix.tuple }}.tar.gz
 
   release:
@@ -92,9 +92,10 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Download binaries
-        uses: actions/download-artifact@v3
+        uses: actions/download-artifact@v4
         with:
-          name: echidna-redistributable
+          pattern: echidna-redistributable-*
+          merge-multiple: true
 
       - name: Sign binaries
         uses: sigstore/gh-action-sigstore-python@v2.1.1

From 0a3480974cb468fb4ffe4d658edb5a44c090958c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?=
 <2642849+elopez@users.noreply.github.com>
Date: Thu, 4 Jan 2024 05:55:08 -0300
Subject: [PATCH 12/20] echidna-redistributable: fix static builds (#1156)

* echidna-redistributable: alert if nix deps remain on binary

* echidna-redistributable: link cxxabi as well on darwin

* echidna-redistributable: use pkgsStatic for haskell operations
---
 flake.nix | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/flake.nix b/flake.nix
index 00f6a1464..9574993b1 100644
--- a/flake.nix
+++ b/flake.nix
@@ -78,6 +78,7 @@
                 "--extra-lib-dirs=${stripDylib (ncurses-static)}/lib"
               ] ++ (if stdenv.hostPlatform.isDarwin then [
                 "--extra-lib-dirs=${stripDylib (libiconv.override { enableStatic = true; })}/lib"
+                "--extra-lib-dirs=${stripDylib (libcxxabi)}/lib"
               ] else [])))
             (haskell.lib.compose.enableCabalFlag "static")
           ];
@@ -97,22 +98,28 @@
         in if pkgs.stdenv.isLinux
         then pkgs.runCommand "echidna-stripNixRefs" {} ''
           mkdir -p $out/bin
-          cp ${pkgs.haskell.lib.dontCheck echidna-static}/bin/echidna $out/bin/
+          cp ${pkgsStatic.haskell.lib.dontCheck echidna-static}/bin/echidna $out/bin/
           # fix TERMINFO path in ncurses
           ${perl} -i -pe 's#(${ncurses-static}/share/terminfo)#"/usr/share/terminfo" . "\x0" x (length($1) - 19)#e' $out/bin/echidna
           chmod 555 $out/bin/echidna
         '' else pkgs.runCommand "echidna-stripNixRefs" {} ''
           mkdir -p $out/bin
-          cp ${pkgs.haskell.lib.dontCheck echidna-static}/bin/echidna $out/bin/
+          cp ${pkgsStatic.haskell.lib.dontCheck echidna-static}/bin/echidna $out/bin/
           # get the list of dynamic libs from otool and tidy the output
           libs=$(${otool} -L $out/bin/echidna | tail -n +2 | sed 's/^[[:space:]]*//' | cut -d' ' -f1)
           # get the path for libcxx
-          cxx=$(echo "$libs" | ${grep} '^/nix/store/.*-libcxx')
+          cxx=$(echo "$libs" | ${grep} '^/nix/store/.*-libcxx-')
           # rewrite /nix/... library paths to point to /usr/lib
           chmod 777 $out/bin/echidna
           ${install_name_tool} -change "$cxx" /usr/lib/libc++.1.dylib $out/bin/echidna
           # fix TERMINFO path in ncurses
           ${perl} -i -pe 's#(${ncurses-static}/share/terminfo)#"/usr/share/terminfo" . "\x0" x (length($1) - 19)#e' $out/bin/echidna
+          # check that no nix deps remain
+          nixdeps=$(${otool} -L $out/bin/echidna | tail -n +2 | { ${grep} /nix/store -c || test $? = 1; })
+          if [ ! "$nixdeps" = "0" ]; then
+            echo "Nix deps remain in redistributable binary!"
+            exit 255
+          fi
           # re-sign binary
           CODESIGN_ALLOCATE=${codesign_allocate} ${codesign} -f -s - $out/bin/echidna
           chmod 555 $out/bin/echidna

From f6e8fbb0167f30c27194df9218b2162caaf08da0 Mon Sep 17 00:00:00 2001
From: Artur Cygan <artur.cygan@trailofbits.com>
Date: Fri, 5 Jan 2024 08:49:01 +0100
Subject: [PATCH 13/20] Use trace printing from hevm (#1157)

---
 lib/Echidna/Campaign.hs    |  5 +--
 lib/Echidna/Output/JSON.hs | 11 ++++---
 lib/Echidna/Shrink.hs      |  3 +-
 lib/Echidna/Test.hs        | 12 +++----
 lib/Echidna/Types/Test.hs  |  5 ++-
 lib/Echidna/UI/Report.hs   | 64 +++++++++++++++++++-------------------
 lib/Echidna/UI/Widgets.hs  | 47 ++++++++++++++++++----------
 package.yaml               |  1 +
 src/test/Tests/Seed.hs     |  5 +--
 stack.yaml                 |  1 +
 10 files changed, 83 insertions(+), 71 deletions(-)

diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs
index 444487cf4..31768d81b 100644
--- a/lib/Echidna/Campaign.hs
+++ b/lib/Echidna/Campaign.hs
@@ -32,7 +32,6 @@ import EVM.Types hiding (Env, Frame(state))
 
 import Echidna.ABI
 import Echidna.Exec
-import Echidna.Events (extractEvents)
 import Echidna.Mutator.Corpus
 import Echidna.Shrink (shrinkTest)
 import Echidna.Symbolic (forceBuf, forceAddr)
@@ -373,14 +372,12 @@ updateTest
   -> EchidnaTest
   -> m (Maybe EchidnaTest)
 updateTest vmForShrink (vm, xs) test = do
-  dappInfo <- asks (.dapp)
   case test.state of
     Open -> do
       (testValue, vm') <- checkETest test vm
       let
-        events = extractEvents False dappInfo vm'
         results = getResultFromVM vm'
-        test' = updateOpenTest test xs (testValue, events, results)
+        test' = updateOpenTest test xs (testValue, vm', results)
       case test'.state of
         Large _ -> do
           pushEvent (TestFalsified test')
diff --git a/lib/Echidna/Output/JSON.hs b/lib/Echidna/Output/JSON.hs
index db0cb13cc..a1abe5a7c 100644
--- a/lib/Echidna/Output/JSON.hs
+++ b/lib/Echidna/Output/JSON.hs
@@ -13,10 +13,11 @@ import Data.Text.Encoding (decodeUtf8)
 import Data.Vector.Unboxed qualified as VU
 import Numeric (showHex)
 
+import EVM.Dapp (DappInfo)
 import EVM.Types (keccak')
 
 import Echidna.ABI (ppAbiValue, GenDict(..))
-import Echidna.Events (Events)
+import Echidna.Events (Events, extractEvents)
 import Echidna.Types (Gas)
 import Echidna.Types.Campaign (WorkerState(..))
 import Echidna.Types.Config (Env(..))
@@ -107,21 +108,21 @@ encodeCampaign env workerStates = do
   pure $ encode Campaign
     { _success = True
     , _error = Nothing
-    , _tests = mapTest <$> tests
+    , _tests = mapTest env.dapp <$> tests
     , seed = worker0.genDict.defSeed
     , coverage = Map.mapKeys (("0x" ++) . (`showHex` "") . keccak') $ VU.toList <$> frozenCov
     , gasInfo = Map.toList $ Map.unionsWith max ((.gasInfo) <$> workerStates)
     }
 
-mapTest :: EchidnaTest -> Test
-mapTest test =
+mapTest :: DappInfo -> EchidnaTest -> Test
+mapTest dappInfo test =
   let (status, transactions, err) = mapTestState test.state test.reproducer
   in Test
     { contract = "" -- TODO add when mapping is available https://github.com/crytic/echidna/issues/415
     , name = "name" -- TODO add a proper name here
     , status = status
     , _error = err
-    , events = test.events
+    , events = maybe [] (extractEvents False dappInfo) test.vm
     , testType = Property
     , transactions = transactions
     }
diff --git a/lib/Echidna/Shrink.hs b/lib/Echidna/Shrink.hs
index 4e070d79e..9e0574722 100644
--- a/lib/Echidna/Shrink.hs
+++ b/lib/Echidna/Shrink.hs
@@ -11,7 +11,6 @@ import Data.List qualified as List
 
 import EVM.Types (VM)
 
-import Echidna.Events (extractEvents)
 import Echidna.Exec
 import Echidna.Transaction
 import Echidna.Types.Solidity (SolConf(..))
@@ -38,7 +37,7 @@ shrinkTest vm test = do
           Just (txs, val, vm') -> do
             Just test { state = Large (i + 1)
                  , reproducer = txs
-                 , events = extractEvents False env.dapp vm'
+                 , vm = Just vm'
                  , result = getResultFromVM vm'
                  , value = val }
           Nothing ->
diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs
index fab706523..bc07d4f91 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -47,7 +47,7 @@ getResultFromVM vm =
     Nothing -> error "getResultFromVM failed"
 
 createTest :: TestType -> EchidnaTest
-createTest m = EchidnaTest Open m v [] Stop []
+createTest m = EchidnaTest Open m v [] Stop Nothing
   where v = case m of
               PropertyTest _ _     -> BoolValue True
               OptimizationTest _ _ -> IntValue minBound
@@ -114,17 +114,17 @@ createTests m td ts r ss = case m of
 updateOpenTest
   :: EchidnaTest
   -> [Tx]
-  -> (TestValue, Events, TxResult)
+  -> (TestValue, VM RealWorld, TxResult)
   -> EchidnaTest
-updateOpenTest test txs (BoolValue False, es, r) =
-  test { Test.state = Large 0, reproducer = txs, events = es, result = r }
+updateOpenTest test txs (BoolValue False, vm, r) =
+  test { Test.state = Large 0, reproducer = txs, vm = Just vm, result = r }
 updateOpenTest test _   (BoolValue True, _, _) =
   test
-updateOpenTest test txs (IntValue v',es,r) =
+updateOpenTest test txs (IntValue v', vm, r) =
   if v' > v then
     test { reproducer = txs
          , value = IntValue v'
-         , events = es
+         , vm = Just vm
          , result = r }
   else
     test
diff --git a/lib/Echidna/Types/Test.hs b/lib/Echidna/Types/Test.hs
index ffc83380c..192e8a00e 100644
--- a/lib/Echidna/Types/Test.hs
+++ b/lib/Echidna/Types/Test.hs
@@ -9,7 +9,6 @@ import Data.Text (Text)
 import EVM.Dapp (DappInfo)
 import EVM.Types (Addr, VM)
 
-import Echidna.Events (Events)
 import Echidna.Types (ExecException)
 import Echidna.Types.Signature (SolSignature)
 import Echidna.Types.Tx (Tx, TxResult)
@@ -85,8 +84,8 @@ data EchidnaTest = EchidnaTest
   , value      :: TestValue
   , reproducer :: [Tx]
   , result     :: TxResult
-  , events     :: Events
-  } deriving (Eq, Show)
+  , vm         :: Maybe (VM RealWorld)
+  } deriving (Show)
 
 isOptimizationTest :: EchidnaTest -> Bool
 isOptimizationTest EchidnaTest{testType = OptimizationTest _ _} = True
diff --git a/lib/Echidna/UI/Report.hs b/lib/Echidna/UI/Report.hs
index 7c4b6420c..eb6956848 100644
--- a/lib/Echidna/UI/Report.hs
+++ b/lib/Echidna/UI/Report.hs
@@ -1,28 +1,29 @@
 module Echidna.UI.Report where
 
 import Control.Monad.Reader (MonadReader, MonadIO (liftIO), asks)
+import Control.Monad.ST (RealWorld)
 import Data.IORef (readIORef)
 import Data.List (intercalate, nub, sortOn)
 import Data.Map (toList)
-import Data.Maybe (catMaybes)
+import Data.Map qualified as Map
+import Data.Maybe (catMaybes, fromJust)
 import Data.Text (Text, unpack)
 import Data.Text qualified as T
 import Data.Time (LocalTime)
 
 import Echidna.ABI (GenDict(..), encodeSig)
-import Echidna.Events (Events)
 import Echidna.Pretty (ppTxCall)
 import Echidna.Types (Gas)
 import Echidna.Types.Campaign
+import Echidna.Types.Config
+import Echidna.Types.Corpus (corpusSize)
 import Echidna.Types.Coverage (scoveragePoints)
 import Echidna.Types.Test (EchidnaTest(..), TestState(..), TestType(..))
 import Echidna.Types.Tx (Tx(..), TxCall(..), TxConf(..))
-import Echidna.Types.Config
-
-import EVM.Types (W256)
-import Echidna.Types.Corpus (corpusSize)
 import Echidna.Utility (timePrefix)
-import qualified Data.Map as Map
+
+import EVM.Format (showTraceTree)
+import EVM.Types (W256, VM)
 
 ppLogLine :: (Int, LocalTime, CampaignEvent) -> String
 ppLogLine (workerId, time, event) =
@@ -96,71 +97,70 @@ ppGasOne (func, (gas, txs)) = do
   pure $ header <> unlines (("    " <>) <$> prettyTxs)
 
 -- | Pretty-print the status of a solved test.
-ppFail :: MonadReader Env m => Maybe (Int, Int) -> Events -> [Tx] -> m String
-ppFail _ _ []  = pure "failed with no transactions made ⁉️  "
-ppFail b es xs = do
+ppFail :: MonadReader Env m => Maybe (Int, Int) -> VM RealWorld -> [Tx] -> m String
+ppFail _ _ []  = pure "failed with no transactions made ⁉️ "
+ppFail b vm xs = do
   let status = case b of
         Nothing    -> ""
         Just (n,m) -> ", shrinking " <> progress n m
   prettyTxs <- mapM (ppTx $ length (nub $ (.src) <$> xs) /= 1) xs
+  dappInfo <- asks (.dapp)
   pure $ "failed!💥  \n  Call sequence" <> status <> ":\n"
          <> unlines (("    " <>) <$> prettyTxs) <> "\n"
-         <> ppEvents es
-
-ppEvents :: Events -> String
-ppEvents es = if null es then "" else unlines $ "Event sequence:" : (T.unpack <$> es)
+         <> "Traces: \n" <> T.unpack (showTraceTree dappInfo vm)
 
 -- | Pretty-print the status of a test.
 
-ppTS :: MonadReader Env m => TestState -> Events -> [Tx] -> m String
+ppTS :: MonadReader Env m => TestState -> VM RealWorld -> [Tx] -> m String
 ppTS (Failed e) _ _  = pure $ "could not evaluate ☣\n  " <> show e
-ppTS Solved     es l = ppFail Nothing es l
+ppTS Solved     vm l = ppFail Nothing vm l
 ppTS Passed     _ _  = pure " passed! 🎉"
 ppTS Open      _ []  = pure "passing"
-ppTS Open      es r  = ppFail Nothing es r
-ppTS (Large n) es l  = do
+ppTS Open      vm r  = ppFail Nothing vm r
+ppTS (Large n) vm l  = do
   m <- asks (.cfg.campaignConf.shrinkLimit)
-  ppFail (if n < m then Just (n, m) else Nothing) es l
+  ppFail (if n < m then Just (n, m) else Nothing) vm l
 
-ppOPT :: MonadReader Env m => TestState -> Events -> [Tx] -> m String
+ppOPT :: MonadReader Env m => TestState -> VM RealWorld -> [Tx] -> m String
 ppOPT (Failed e) _ _  = pure $ "could not evaluate ☣\n  " <> show e
-ppOPT Solved     es l = ppOptimized Nothing es l
+ppOPT Solved     vm l = ppOptimized Nothing vm l
 ppOPT Passed     _ _  = pure " passed! 🎉"
-ppOPT Open      es r  = ppOptimized Nothing es r
-ppOPT (Large n) es l  = do
+ppOPT Open      vm r  = ppOptimized Nothing vm r
+ppOPT (Large n) vm l  = do
   m <- asks (.cfg.campaignConf.shrinkLimit)
-  ppOptimized (if n < m then Just (n, m) else Nothing) es l
+  ppOptimized (if n < m then Just (n, m) else Nothing) vm l
 
 -- | Pretty-print the status of a optimized test.
-ppOptimized :: MonadReader Env m => Maybe (Int, Int) -> Events -> [Tx] -> m String
+ppOptimized :: MonadReader Env m => Maybe (Int, Int) -> VM RealWorld -> [Tx] -> m String
 ppOptimized _ _ []  = pure "Call sequence:\n(no transactions)"
-ppOptimized b es xs = do
+ppOptimized b vm xs = do
   let status = case b of
         Nothing    -> ""
         Just (n,m) -> ", shrinking " <> progress n m
   prettyTxs <- mapM (ppTx $ length (nub $ (.src) <$> xs) /= 1) xs
+  dappInfo <- asks (.dapp)
   pure $ "\n  Call sequence" <> status <> ":\n"
          <> unlines (("    " <>) <$> prettyTxs) <> "\n"
-         <> ppEvents es
+         <> "Traces: \n" <> T.unpack (showTraceTree dappInfo vm)
 
 -- | Pretty-print the status of all 'SolTest's in a 'Campaign'.
-ppTests :: (MonadReader Env m) => [EchidnaTest] -> m String
+ppTests :: MonadReader Env m => [EchidnaTest] -> m String
 ppTests tests = do
   unlines . catMaybes <$> mapM pp tests
   where
   pp t =
     case t.testType of
       PropertyTest n _ -> do
-        status <- ppTS t.state t.events t.reproducer
+        status <- ppTS t.state (fromJust t.vm) t.reproducer
         pure $ Just (T.unpack n <> ": " <> status)
       CallTest n _ -> do
-        status <- ppTS t.state t.events t.reproducer
+        status <- ppTS t.state (fromJust t.vm) t.reproducer
         pure $ Just (T.unpack n <> ": " <> status)
       AssertionTest _ s _ -> do
-        status <- ppTS t.state t.events t.reproducer
+        status <- ppTS t.state (fromJust t.vm) t.reproducer
         pure $ Just (T.unpack (encodeSig s) <> ": " <> status)
       OptimizationTest n _ -> do
-        status <- ppOPT t.state t.events t.reproducer
+        status <- ppOPT t.state (fromJust t.vm) t.reproducer
         pure $ Just (T.unpack n <> ": max value: " <> show t.value <> "\n" <> status)
       Exploration -> pure Nothing
 
diff --git a/lib/Echidna/UI/Widgets.hs b/lib/Echidna/UI/Widgets.hs
index 964b314fe..6bbeec60d 100644
--- a/lib/Echidna/UI/Widgets.hs
+++ b/lib/Echidna/UI/Widgets.hs
@@ -10,12 +10,15 @@ import Brick.Widgets.Border
 import Brick.Widgets.Center
 import Brick.Widgets.Dialog qualified as B
 import Control.Monad.Reader (MonadReader, asks, ask)
+import Control.Monad.ST (RealWorld)
 import Data.List (nub, intersperse, sortBy)
 import Data.Map (Map)
 import Data.Map qualified as Map
-import Data.Maybe (fromMaybe, isJust)
+import Data.Maybe (fromMaybe, isJust, fromJust)
 import Data.Sequence (Seq)
 import Data.Sequence qualified as Seq
+import Data.String.AnsiEscapeCodes.Strip.Text (stripAnsiEscapeCodes)
+import Data.Text (Text)
 import Data.Text qualified as T
 import Data.Time (LocalTime, NominalDiffTime, formatTime, defaultTimeLocale, diffLocalTime)
 import Data.Version (showVersion)
@@ -25,7 +28,6 @@ import Text.Printf (printf)
 import Text.Wrap
 
 import Echidna.ABI
-import Echidna.Events (Events)
 import Echidna.Types.Campaign
 import Echidna.Types.Config
 import Echidna.Types.Test
@@ -33,7 +35,8 @@ import Echidna.Types.Tx (Tx(..), TxResult(..))
 import Echidna.UI.Report
 import Echidna.Utility (timePrefix)
 
-import EVM.Types (Addr, Contract, W256)
+import EVM.Format (showTraceTree)
+import EVM.Types (Addr, Contract, W256, VM(..))
 
 data UIState = UIState
   { status :: UIStateStatus
@@ -276,36 +279,42 @@ tsWidget
   -> EchidnaTest
   -> m (Widget Name, Widget Name)
 tsWidget (Failed e) _ = pure (str "could not evaluate", str $ show e)
-tsWidget Solved     t = failWidget Nothing t.reproducer t.events t.value t.result
+tsWidget Solved     t = failWidget Nothing t.reproducer (fromJust t.vm) t.value t.result
 tsWidget Passed     _ = pure (success $ str "PASSED!", emptyWidget)
 tsWidget Open       _ = pure (success $ str "passing", emptyWidget)
 tsWidget (Large n)  t = do
   m <- asks (.cfg.campaignConf.shrinkLimit)
-  failWidget (if n < m then Just (n,m) else Nothing) t.reproducer t.events t.value t.result
+  failWidget (if n < m then Just (n,m) else Nothing) t.reproducer (fromJust t.vm) t.value t.result
 
 titleWidget :: Widget n
 titleWidget = str "Call sequence" <+> str ":"
 
-eventWidget :: Events -> Widget n
-eventWidget es =
-  if null es then str ""
-  else str "Event sequence" <+> str ":"
-       <=> strBreak (T.unpack $ T.intercalate "\n" es)
+tracesWidget :: MonadReader Env m => VM RealWorld -> m (Widget n)
+tracesWidget vm = do
+  dappInfo <- asks (.dapp)
+  -- TODO: showTraceTree does coloring with ANSI escape codes, we need to strip
+  -- those because they break the Brick TUI. Fix in hevm so we can display
+  -- colors here as well.
+  let traces = stripAnsiEscapeCodes $ showTraceTree dappInfo vm
+  pure $
+    if T.null traces then str ""
+    else str "Traces" <+> str ":" <=> (txtBreak traces)
 
 failWidget
   :: MonadReader Env m
   => Maybe (Int, Int)
   -> [Tx]
-  -> Events
+  -> VM RealWorld
   -> TestValue
   -> TxResult
   -> m (Widget Name, Widget Name)
 failWidget _ [] _  _  _= pure (failureBadge, str "*no transactions made*")
-failWidget b xs es _ r = do
+failWidget b xs vm _ r = do
   s <- seqWidget xs
+  traces <- tracesWidget vm
   pure
     ( failureBadge <+> str (" with " ++ show r)
-    , status <=> titleWidget <=> s <=> eventWidget es
+    , status <=> titleWidget <=> s <=> str " " <=> traces
     )
   where
   status = case b of
@@ -327,21 +336,22 @@ optWidget Open       t =
     "optimizing, max value: " ++ show t.value, emptyWidget)
 optWidget (Large n)  t = do
   m <- asks (.cfg.campaignConf.shrinkLimit)
-  maxWidget (if n < m then Just (n,m) else Nothing) t.reproducer t.events t.value
+  maxWidget (if n < m then Just (n,m) else Nothing) t.reproducer (fromJust t.vm) t.value
 
 maxWidget
   :: MonadReader Env m
   => Maybe (Int, Int)
   -> [Tx]
-  -> Events
+  -> VM RealWorld
   -> TestValue
   -> m (Widget Name, Widget Name)
 maxWidget _ [] _  _ = pure (failureBadge, str "*no transactions made*")
-maxWidget b xs es v = do
+maxWidget b xs vm v = do
   s <- seqWidget xs
+  traces <- tracesWidget vm
   pure
     ( maximumBadge <+> str (" max value: " ++ show v)
-    , status <=> titleWidget <=> s <=> eventWidget es
+    , status <=> titleWidget <=> s <=> str " " <=> traces
     )
   where
   status = case b of
@@ -367,4 +377,7 @@ maximumBadge = withAttr (attrName "maximum") $ str "OPTIMIZED!"
 strBreak :: String -> Widget n
 strBreak = strWrapWith $ defaultWrapSettings { breakLongWords = True }
 
+txtBreak :: Text -> Widget n
+txtBreak = txtWrapWith $ defaultWrapSettings { breakLongWords = True }
+
 #endif
diff --git a/package.yaml b/package.yaml
index 71c4ac15d..da8b29531 100644
--- a/package.yaml
+++ b/package.yaml
@@ -49,6 +49,7 @@ dependencies:
   - http-conduit
   - html-conduit
   - xml-conduit
+  - strip-ansi-escape
 
 language: GHC2021
 
diff --git a/src/test/Tests/Seed.hs b/src/test/Tests/Seed.hs
index 62ddddae2..b1b3e5abc 100644
--- a/src/test/Tests/Seed.hs
+++ b/src/test/Tests/Seed.hs
@@ -7,8 +7,9 @@ import Common (runContract, overrideQuiet)
 import Data.Function ((&))
 import Data.IORef (readIORef)
 import Echidna.Output.Source (CoverageFileType(..))
-import Echidna.Types.Config (Env(..), EConfig(..))
 import Echidna.Types.Campaign
+import Echidna.Types.Config (Env(..), EConfig(..))
+import Echidna.Types.Test
 import Echidna.Mutator.Corpus (defaultMutationConsts)
 import Echidna.Config (defaultConfig)
 
@@ -39,4 +40,4 @@ seedTests =
     gen s = do
       (env, _) <- runContract "basic/flags.sol" Nothing (cfg s)
       readIORef env.testsRef
-    same s t = (==) <$> gen s <*> gen t
+    same s t = (\x y -> ((.reproducer) <$> x) == ((.reproducer) <$> y)) <$> gen s <*> gen t
diff --git a/stack.yaml b/stack.yaml
index 8d199652e..f82e7e23f 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -14,3 +14,4 @@ extra-deps:
 - spool-0.1@sha256:77780cbfc2c0be23ff2ea9e474062f3df97fcd9db946ee0b3508280a923b83e2,1461
 - smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421
 - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162
+- strip-ansi-escape-0.1.0.0@sha256:08f2ed93b16086a837ec46eab7ce8d27cf39d47783caaeb818878ea33c2ff75f,1628

From 937102bcba49ad6c3502403f75cddc943535e5a2 Mon Sep 17 00:00:00 2001
From: Artur Cygan <artur.cygan@trailofbits.com>
Date: Sun, 7 Jan 2024 01:15:01 +0100
Subject: [PATCH 14/20] Simplify saving tx result in coverage (#1158)

---
 lib/Echidna/Exec.hs | 27 ++++++++++++---------------
 1 file changed, 12 insertions(+), 15 deletions(-)

diff --git a/lib/Echidna/Exec.hs b/lib/Echidna/Exec.hs
index c22a2e377..f85301f1f 100644
--- a/lib/Echidna/Exec.hs
+++ b/lib/Echidna/Exec.hs
@@ -35,6 +35,7 @@ import Echidna.Symbolic (forceBuf)
 import Echidna.Transaction
 import Echidna.Types (ExecException(..), Gas, fromEVM, emptyAccount)
 import Echidna.Types.Config (Env(..), EConfig(..), UIConf(..), OperationMode(..), OutputFormat(Text))
+import Echidna.Types.Coverage (CoverageInfo)
 import Echidna.Types.Signature (getBytecodeMetadata, lookupBytecodeMetadata)
 import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Tx (TxCall(..), Tx, TxResult(..), call, dst, initialTimestamp, initialBlockNumber, getResult)
@@ -237,7 +238,7 @@ execTx
 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))
+type CoverageContext = (Bool, Maybe (VMut.IOVector CoverageInfo, Int))
 
 -- | Execute a transaction, logging coverage at every step.
 execTxWithCov
@@ -257,17 +258,13 @@ execTxWithCov tx = do
 
   -- Update the last valid location with the transaction result
   grew' <- liftIO $ case lastLoc of
-    Just (meta, pc) -> do
-      cov <- readIORef covRef
-      case Map.lookup meta cov of
-        Nothing -> pure False -- shouldn't happen
-        Just vec -> do
-          let txResultBit = fromEnum $ getResult $ fst r
-          VMut.read vec pc >>= \case
-            (opIx, depths, txResults) | not (txResults `testBit` txResultBit) -> do
-              VMut.write vec pc (opIx, depths, txResults `setBit` txResultBit)
-              pure True -- we count this as new coverage
-            _ -> pure False
+    Just (vec, pc) -> do
+      let txResultBit = fromEnum $ getResult $ fst r
+      VMut.read vec pc >>= \case
+        (opIx, depths, txResults) | not (txResults `testBit` txResultBit) -> do
+          VMut.write vec pc (opIx, depths, txResults `setBit` txResultBit)
+          pure True -- we count this as new coverage
+        _ -> pure False
     _ -> pure False
 
   pure (r, grew || grew')
@@ -314,7 +311,7 @@ execTxWithCov tx = do
 
               VMut.write vec' pc (opIx, fromIntegral depth, 0 `setBit` fromEnum Stop)
 
-              writeIORef covContextRef (True, Just (meta, pc))
+              writeIORef covContextRef (True, Just (vec', 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
@@ -328,9 +325,9 @@ execTxWithCov tx = do
               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))
+                  writeIORef covContextRef (True, Just (vec, pc))
                 _ ->
-                  modifyIORef' covContextRef $ \(new, _) -> (new, Just (meta, pc))
+                  modifyIORef' covContextRef $ \(new, _) -> (new, Just (vec, pc))
 
       -- | Get the VM's current execution location
       currentCovLoc vm = (vm.state.pc, fromMaybe 0 $ vmOpIx vm, length vm.frames)

From 9d502be26597e26c468f94f7c56a6c5692cd0577 Mon Sep 17 00:00:00 2001
From: Artur Cygan <artur.cygan@trailofbits.com>
Date: Tue, 9 Jan 2024 00:54:28 +0100
Subject: [PATCH 15/20] Make slither optional (#1159)

---
 lib/Echidna.hs                                |  2 +-
 lib/Echidna/Solidity.hs                       | 32 ++++++--
 .../Slither.hs}                               | 80 ++++++++-----------
 3 files changed, 60 insertions(+), 54 deletions(-)
 rename lib/Echidna/{Processor.hs => SourceAnalysis/Slither.hs} (69%)

diff --git a/lib/Echidna.hs b/lib/Echidna.hs
index f36f39b1f..ea207e424 100644
--- a/lib/Echidna.hs
+++ b/lib/Echidna.hs
@@ -18,7 +18,7 @@ import EVM.Types hiding (Env)
 import Echidna.ABI
 import Echidna.Etheno (loadEtheno, extractFromEtheno)
 import Echidna.Output.Corpus
-import Echidna.Processor
+import Echidna.SourceAnalysis.Slither
 import Echidna.Solidity
 import Echidna.Symbolic (forceAddr)
 import Echidna.Test (createTests)
diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs
index 5f3f75f51..1300730e3 100644
--- a/lib/Echidna/Solidity.hs
+++ b/lib/Echidna/Solidity.hs
@@ -12,6 +12,7 @@ import Data.List (find, partition, isSuffixOf, (\\))
 import Data.List.NonEmpty (NonEmpty((:|)))
 import Data.List.NonEmpty qualified as NE
 import Data.List.NonEmpty.Extra qualified as NEE
+import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Maybe (isJust, isNothing, catMaybes, listToMaybe, mapMaybe)
 import Data.Set (Set)
@@ -38,12 +39,12 @@ import Echidna.Deploy (deployContracts, deployBytecodes)
 import Echidna.Etheno (loadEthenoBatch)
 import Echidna.Events (EventMap, extractEvents)
 import Echidna.Exec (execTx, initialVM)
-import Echidna.Processor
+import Echidna.SourceAnalysis.Slither
 import Echidna.Symbolic (forceAddr)
 import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isDapptestMode)
 import Echidna.Types.Config (EConfig(..), Env(..))
 import Echidna.Types.Signature
-  (ContractName, SolSignature, SignatureMap, getBytecodeMetadata)
+  (ContractName, SolSignature, SignatureMap, getBytecodeMetadata, FunctionName)
 import Echidna.Types.Solidity
 import Echidna.Types.Test (EchidnaTest(..))
 import Echidna.Types.Tx
@@ -316,13 +317,28 @@ mkWorld
   -> Maybe ContractName
   -> SlitherInfo
   -> World
-mkWorld SolConf{sender, testMode} em m c si =
+mkWorld SolConf{sender, testMode} eventMap sigMap maybeContract slitherInfo =
   let
-    ps = filterResults c si.payableFunctions
-    as = if isAssertionMode testMode then filterResults c si.asserts else []
-    cs = if isDapptestMode testMode then [] else filterResults c si.constantFunctions \\ as
-    (hm, lm) = prepareHashMaps cs as $ filterFallbacks c si.fallbackDefined si.receiveDefined m
-  in World sender hm lm ps em
+    payableSigs = filterResults maybeContract slitherInfo.payableFunctions
+    as = if isAssertionMode testMode then filterResults maybeContract slitherInfo.asserts else []
+    cs = if isDapptestMode testMode then [] else filterResults maybeContract slitherInfo.constantFunctions \\ as
+    (highSignatureMap, lowSignatureMap) = prepareHashMaps cs as $
+      filterFallbacks maybeContract slitherInfo.fallbackDefined slitherInfo.receiveDefined sigMap
+  in World { senders = sender
+           , highSignatureMap
+           , lowSignatureMap
+           , payableSigs
+           , eventMap
+           }
+
+-- | This function is used to filter the lists of function names according to the supplied
+-- contract name (if any) and returns a list of hashes
+filterResults :: Maybe ContractName -> Map ContractName [FunctionName] -> [FunctionSelector]
+filterResults (Just contractName) rs =
+  case Map.lookup contractName rs of
+    Nothing -> filterResults Nothing rs
+    Just sig -> hashSig <$> sig
+filterResults Nothing rs = hashSig <$> (concat . Map.elems) rs
 
 filterFallbacks
   :: Maybe ContractName
diff --git a/lib/Echidna/Processor.hs b/lib/Echidna/SourceAnalysis/Slither.hs
similarity index 69%
rename from lib/Echidna/Processor.hs
rename to lib/Echidna/SourceAnalysis/Slither.hs
index 9bd48107a..cb60028bb 100644
--- a/lib/Echidna/Processor.hs
+++ b/lib/Echidna/SourceAnalysis/Slither.hs
@@ -1,9 +1,7 @@
 {-# LANGUAGE RecordWildCards #-}
 
-module Echidna.Processor where
+module Echidna.SourceAnalysis.Slither where
 
-import Control.Exception (Exception)
-import Control.Monad.Catch (MonadThrow(..))
 import Data.Aeson ((.:), (.:?), (.!=), eitherDecode, parseJSON, withEmbeddedJSON, withObject)
 import Data.Aeson.Types (FromJSON, Parser, Value(String))
 import Data.ByteString.Base16 qualified as BS16 (decode)
@@ -25,33 +23,13 @@ import System.Process (StdStream(..), readCreateProcessWithExitCode, proc, std_e
 import Text.Read (readMaybe)
 
 import EVM.ABI (AbiValue(..))
-import EVM.Types (Addr(..), FunctionSelector)
+import EVM.Types (Addr(..))
 
-import Echidna.ABI (hashSig, makeNumAbiValues, makeArrayAbiValues)
+import Echidna.ABI (makeNumAbiValues, makeArrayAbiValues)
 import Echidna.Types.Signature (ContractName, FunctionName)
 import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Utility (measureIO)
-
--- | Things that can go wrong trying to run a processor. Read the 'Show'
--- instance for more detailed explanations.
-data ProcException = ProcessorFailure String String
-                   | ProcessorNotFound String String
-
-instance Show ProcException where
-  show = \case
-    ProcessorFailure p e -> "Error running " ++ p ++ ":\n" ++ e
-    ProcessorNotFound p e -> "Cannot find " ++ p ++ " in PATH.\n" ++ e
-
-instance Exception ProcException
-
--- | This function is used to filter the lists of function names according to the supplied
--- contract name (if any) and returns a list of hashes
-filterResults :: Maybe ContractName -> Map ContractName [FunctionName] -> [FunctionSelector]
-filterResults (Just c) rs =
-  case Map.lookup c rs of
-    Nothing -> filterResults Nothing rs
-    Just s -> hashSig <$> s
-filterResults Nothing rs = hashSig <$> (concat . Map.elems) rs
+import System.IO (stderr, hPutStrLn)
 
 enhanceConstants :: SlitherInfo -> Set AbiValue
 enhanceConstants si =
@@ -125,22 +103,34 @@ instance FromJSON SlitherInfo where
 -- Slither processing
 runSlither :: FilePath -> SolConf -> IO SlitherInfo
 runSlither fp solConf = do
-  path <- findExecutable "slither" >>= \case
-    Nothing -> throwM $
-      ProcessorNotFound "slither" "You should install it using 'pip3 install slither-analyzer --user'"
-    Just path -> pure path
-
-  let args = ["--ignore-compile", "--print", "echidna", "--json", "-"]
-             ++ solConf.cryticArgs ++ [fp]
-  (ec, out, err) <- measureIO solConf.quiet ("Running slither on " <> fp) $
-    readCreateProcessWithExitCode (proc path args) {std_err = Inherit} ""
-  case ec of
-    ExitSuccess ->
-      case eitherDecode (BSL.pack out) of
-        Right si -> pure si
-        Left msg -> throwM $
-          ProcessorFailure "slither" ("decoding slither output failed:\n" ++ msg)
-    ExitFailure _ -> throwM $ ProcessorFailure "slither" err
-
-noInfo :: SlitherInfo
-noInfo = SlitherInfo mempty mempty mempty mempty mempty [] [] []
+  findExecutable "slither" >>= \case
+    Nothing -> do
+      hPutStrLn stderr $
+        "WARNING: slither not found. Echidna uses Slither (https://github.com/crytic/slither)"
+        <> " to perform source analysis, which makes fuzzing more effective. You should install it with"
+        <> " 'pip3 install slither-analyzer --user'"
+      pure emptySlitherInfo
+    Just path -> do
+      let args = ["--ignore-compile", "--print", "echidna", "--json", "-"]
+                 ++ solConf.cryticArgs ++ [fp]
+      (exitCode, out, err) <- measureIO solConf.quiet ("Running slither on " <> fp) $
+        readCreateProcessWithExitCode (proc path args) {std_err = Inherit} ""
+      case exitCode of
+        ExitSuccess ->
+          case eitherDecode (BSL.pack out) of
+            Right si -> pure si
+            Left msg -> do
+              hPutStrLn stderr $
+                "WARNING: Decoding slither output failed. Echidna will continue,"
+                <> " however fuzzing will likely be less effective.\n"
+                <> msg
+              pure emptySlitherInfo
+        ExitFailure _ -> do
+          hPutStrLn stderr $
+            "WARNING: Running slither failed. Echidna will continue,"
+            <> " however fuzzing will likely be less effective.\n"
+            <> err
+          pure emptySlitherInfo
+
+emptySlitherInfo :: SlitherInfo
+emptySlitherInfo = SlitherInfo mempty mempty mempty mempty mempty [] [] []

From e0d243a9390f4197b089d2bb2da0f0be774f3093 Mon Sep 17 00:00:00 2001
From: samalws-tob <129795909+samalws-tob@users.noreply.github.com>
Date: Thu, 11 Jan 2024 14:32:33 -0500
Subject: [PATCH 16/20] Index CoverageMap and SignatureMap by codehash (for
 performance) (#1160)

* WIP implementation using codehash map

* compiles and runs; significantly faster than master

* use codehash for signaturemap

* remove metadata cache

* use codeContract rather than contract; use env rather than individual pieces of env

* refactor codehash helper functions

* hlint

* cleanup

* added test (don't know if it works yet)

* Add @arcz 's suggestions

* fallback on bytecode metadata if findSrc doesn't work

* fix tests

* rename Echidna.Types.CodehashMap to Echidna.SignatureMapping
---
 lib/Echidna/Campaign.hs              |  24 ++-----
 lib/Echidna/Exec.hs                  |  69 +++++++-----------
 lib/Echidna/Output/JSON.hs           |   3 +-
 lib/Echidna/Output/Source.hs         |   3 +-
 lib/Echidna/Solidity.hs              |   6 +-
 lib/Echidna/SourceMapping.hs         | 102 +++++++++++++++++++++++++++
 lib/Echidna/Transaction.hs           |  39 +++++-----
 lib/Echidna/Types/Config.hs          |   4 +-
 lib/Echidna/Types/Coverage.hs        |   7 +-
 lib/Echidna/Types/Signature.hs       |  25 +------
 src/Main.hs                          |   4 +-
 src/test/Common.hs                   |   8 +--
 src/test/Tests/Compile.hs            |   4 +-
 src/test/Tests/Integration.hs        |   2 +
 tests/solidity/basic/immutable-2.sol |  15 ++++
 tests/solidity/basic/immutable-3.sol |  11 +++
 16 files changed, 203 insertions(+), 123 deletions(-)
 create mode 100644 lib/Echidna/SourceMapping.hs
 create mode 100644 tests/solidity/basic/immutable-2.sol
 create mode 100644 tests/solidity/basic/immutable-3.sol

diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs
index 31768d81b..9c7c9e144 100644
--- a/lib/Echidna/Campaign.hs
+++ b/lib/Echidna/Campaign.hs
@@ -3,8 +3,6 @@
 
 module Echidna.Campaign where
 
-import Optics.Core hiding ((|>))
-
 import Control.Concurrent (writeChan)
 import Control.DeepSeq (force)
 import Control.Monad (replicateM, when, void, forM_)
@@ -17,16 +15,16 @@ 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.IORef (readIORef, atomicModifyIORef')
 import Data.Map qualified as Map
 import Data.Map (Map, (\\))
-import Data.Maybe (isJust, mapMaybe, fromMaybe, fromJust)
+import Data.Maybe (isJust, mapMaybe, fromMaybe)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text (Text)
 import System.Random (mkStdGen)
 
-import EVM (bytecode, cheatCode)
+import EVM (cheatCode)
 import EVM.ABI (getAbi, AbiType(AbiAddressType), AbiValue(AbiAddress))
 import EVM.Types hiding (Env, Frame(state))
 
@@ -34,7 +32,7 @@ import Echidna.ABI
 import Echidna.Exec
 import Echidna.Mutator.Corpus
 import Echidna.Shrink (shrinkTest)
-import Echidna.Symbolic (forceBuf, forceAddr)
+import Echidna.Symbolic (forceAddr)
 import Echidna.Test
 import Echidna.Transaction
 import Echidna.Types (Gas)
@@ -42,7 +40,7 @@ import Echidna.Types.Campaign
 import Echidna.Types.Corpus (Corpus, corpusSize)
 import Echidna.Types.Coverage (scoveragePoints)
 import Echidna.Types.Config
-import Echidna.Types.Signature (makeBytecodeCache, FunctionName)
+import Echidna.Types.Signature (FunctionName)
 import Echidna.Types.Test
 import Echidna.Types.Test qualified as Test
 import Echidna.Types.Tx (TxCall(..), Tx(..), call)
@@ -86,12 +84,6 @@ runWorker
   -> Int     -- ^ Test limit for this worker
   -> m (WorkerStopReason, WorkerState)
 runWorker callback vm world dict workerId initialCorpus testLimit = do
-  metaCacheRef <- asks (.metadataCache)
-  fetchContractCacheRef <- asks (.fetchContractCache)
-  external <- liftIO $ Map.mapMaybe id <$> readIORef fetchContractCacheRef
-  let concretizeKeys = Map.foldrWithKey (Map.insert . forceAddr) mempty
-  liftIO $ writeIORef metaCacheRef (mkMemo (concretizeKeys vm.env.contracts <> external))
-
   let
     effectiveSeed = dict.defSeed + workerId
     effectiveGenDict = dict { defSeed = effectiveSeed }
@@ -152,8 +144,6 @@ runWorker callback vm world dict workerId initialCorpus testLimit = do
 
   continue = runUpdate (shrinkTest vm) >> lift callback >> run
 
-  mkMemo = makeBytecodeCache . map (forceBuf . fromJust . (^. bytecode)) . Map.elems
-
 -- | Generate a new sequences of transactions, either using the corpus or with
 -- randomly created transactions
 randseq
@@ -163,18 +153,16 @@ randseq
   -> m [Tx]
 randseq deployedContracts world = do
   env <- ask
-  memo <- liftIO $ readIORef env.metadataCache
 
   let
     mutConsts = env.cfg.campaignConf.mutConsts
-    txConf = env.cfg.txConf
     seqLen = env.cfg.campaignConf.seqLen
 
   -- TODO: include reproducer when optimizing
   --let rs = filter (not . null) $ map (.testReproducer) $ ca._tests
 
   -- Generate new random transactions
-  randTxs <- replicateM seqLen (genTx memo world txConf deployedContracts)
+  randTxs <- replicateM seqLen (genTx world deployedContracts)
   -- Generate a random mutator
   cmut <- if seqLen == 1 then seqMutatorsStateless (fromConsts mutConsts)
                          else seqMutatorsStateful (fromConsts mutConsts)
diff --git a/lib/Echidna/Exec.hs b/lib/Echidna/Exec.hs
index f85301f1f..c7495f904 100644
--- a/lib/Echidna/Exec.hs
+++ b/lib/Echidna/Exec.hs
@@ -10,11 +10,11 @@ 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', execStateT)
-import Control.Monad.Reader (MonadReader, asks)
+import Control.Monad.Reader (MonadReader, ask, 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')
+import Data.IORef (readIORef, atomicWriteIORef, newIORef, writeIORef, modifyIORef')
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, fromJust)
 import Data.Text qualified as T
@@ -31,12 +31,12 @@ import EVM.Types hiding (Env)
 
 import Echidna.Events (emptyEvents)
 import Echidna.RPC (safeFetchContractFrom, safeFetchSlotFrom)
+import Echidna.SourceMapping (lookupUsingCodehashOrInsert)
 import Echidna.Symbolic (forceBuf)
 import Echidna.Transaction
 import Echidna.Types (ExecException(..), Gas, fromEVM, emptyAccount)
 import Echidna.Types.Config (Env(..), EConfig(..), UIConf(..), OperationMode(..), OutputFormat(Text))
 import Echidna.Types.Coverage (CoverageInfo)
-import Echidna.Types.Signature (getBytecodeMetadata, lookupBytecodeMetadata)
 import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Tx (TxCall(..), Tx, TxResult(..), call, dst, initialTimestamp, initialBlockNumber, getResult)
 import Echidna.Utility (getTimestamp, timePrefix)
@@ -121,11 +121,6 @@ execTxWith executeTx tx = do
                 case ret of
                   -- TODO: fix hevm to not return an empty contract in case of an error
                   Just contract | contract.code /= RuntimeCode (ConcreteRuntimeCode "") -> do
-                    metaCacheRef <- asks (.metadataCache)
-                    metaCache <- liftIO $ readIORef metaCacheRef
-                    let bc = forceBuf $ fromJust (contract ^. bytecode)
-                    liftIO $ atomicWriteIORef metaCacheRef $ Map.insert bc (getBytecodeMetadata bc) metaCache
-
                     fromEVM (continuation contract)
                     liftIO $ atomicWriteIORef cacheRef $ Map.insert addr (Just contract) cache
                   _ -> do
@@ -246,13 +241,11 @@ execTxWithCov
   => Tx
   -> m ((VMResult RealWorld, Gas), Bool)
 execTxWithCov tx = do
-  covRef <- asks (.coverageRef)
-  metaCacheRef <- asks (.metadataCache)
-  cache <- liftIO $ readIORef metaCacheRef
+  env <- ask
 
   covContextRef <- liftIO $ newIORef (False, Nothing)
 
-  r <- execTxWith (execCov covRef covContextRef cache) tx
+  r <- execTxWith (execCov env covContextRef) tx
 
   (grew, lastLoc) <- liftIO $ readIORef covContextRef
 
@@ -270,7 +263,7 @@ execTxWithCov tx = do
   pure (r, grew || grew')
   where
     -- the same as EVM.exec but collects coverage, will stop on a query
-    execCov covRef covContextRef cache = do
+    execCov env covContextRef = do
       vm <- get
       (r, vm') <- liftIO $ loop vm
       put vm'
@@ -292,35 +285,25 @@ execTxWithCov tx = do
       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 . fromJust . view bytecode . fromJust $
-                  Map.lookup vm.state.contract vm.env.contracts
-            if size > 0 then do
-              vec <- VMut.new size
-              -- We use -1 for opIx to indicate that the location was not covered
-              forM_ [0..size-1] $ \i -> VMut.write vec i (-1, 0, 0)
-
-              vec' <- atomicModifyIORef' covRef $ \cm ->
-                -- this should reduce races
-                case Map.lookup meta cm of
-                  Nothing -> (Map.insert meta vec cm, vec)
-                  Just vec' -> (cm, vec')
-
-              VMut.write vec' pc (opIx, fromIntegral depth, 0 `setBit` fromEnum Stop)
-
-              writeIORef covContextRef (True, Just (vec', 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 ()
-          Just vec ->
+            contract = currentContract vm
+
+        maybeCovVec <- lookupUsingCodehashOrInsert env.codehashMap contract env.dapp env.coverageRef $ do
+          let size = BS.length . forceBuf . fromJust . view bytecode $ contract
+          if size == 0 then pure Nothing else do
+            -- IO for making a new vec
+            vec <- VMut.new size
+            -- We use -1 for opIx to indicate that the location was not covered
+            forM_ [0..size-1] $ \i -> VMut.write vec i (-1, 0, 0)
+            pure $ Just vec
+
+        case maybeCovVec of
+          Nothing -> pure ()
+          Just vec -> do
             -- 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.
+            -- ... this should be fixed now, since we use `codeContract` instead
+            -- of `contract` for everything; it may be safe to remove this check.
             when (pc < VMut.length vec) $
               VMut.read vec pc >>= \case
                 (_, depths, results) | depth < 64 && not (depths `testBit` depth) -> do
@@ -332,11 +315,9 @@ execTxWithCov tx = do
       -- | Get the VM's current execution location
       currentCovLoc vm = (vm.state.pc, fromMaybe 0 $ vmOpIx vm, length vm.frames)
 
-      -- | 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 $ fromJust buffer
-        pure $ lookupBytecodeMetadata cache bc
+      -- | Get the current contract being executed
+      currentContract vm = fromMaybe (error "no contract information on coverage") $
+        vm ^? #env % #contracts % at vm.state.codeContract % _Just
 
 initialVM :: Bool -> ST s (VM s)
 initialVM ffi = do
diff --git a/lib/Echidna/Output/JSON.hs b/lib/Echidna/Output/JSON.hs
index a1abe5a7c..ebacc8183 100644
--- a/lib/Echidna/Output/JSON.hs
+++ b/lib/Echidna/Output/JSON.hs
@@ -14,7 +14,6 @@ import Data.Vector.Unboxed qualified as VU
 import Numeric (showHex)
 
 import EVM.Dapp (DappInfo)
-import EVM.Types (keccak')
 
 import Echidna.ABI (ppAbiValue, GenDict(..))
 import Echidna.Events (Events, extractEvents)
@@ -110,7 +109,7 @@ encodeCampaign env workerStates = do
     , _error = Nothing
     , _tests = mapTest env.dapp <$> tests
     , seed = worker0.genDict.defSeed
-    , coverage = Map.mapKeys (("0x" ++) . (`showHex` "") . keccak') $ VU.toList <$> frozenCov
+    , coverage = Map.mapKeys (("0x" ++) . (`showHex` "")) $ VU.toList <$> frozenCov
     , gasInfo = Map.toList $ Map.unionsWith max ((.gasInfo) <$> workerStates)
     }
 
diff --git a/lib/Echidna/Output/Source.hs b/lib/Echidna/Output/Source.hs
index 6be9f0096..6e8075fe0 100644
--- a/lib/Echidna/Output/Source.hs
+++ b/lib/Echidna/Output/Source.hs
@@ -29,7 +29,6 @@ import EVM.Solidity (SourceCache(..), SrcMap, SolcContract(..))
 
 import Echidna.Types.Coverage (OpIx, unpackTxResults, CoverageMap)
 import Echidna.Types.Tx (TxResult(..))
-import Echidna.Types.Signature (getBytecodeMetadata)
 
 saveCoverages
   :: [CoverageFileType]
@@ -163,7 +162,7 @@ srcMapCov sc covMap contracts = do
   where
   linesCovered :: SolcContract -> IO (Map FilePath (Map Int [TxResult]))
   linesCovered c =
-    case Map.lookup (getBytecodeMetadata c.runtimeCode) covMap of
+    case Map.lookup c.runtimeCodehash covMap of
       Just vec -> VU.foldl' (\acc covInfo -> case covInfo of
         (-1, _, _) -> acc -- not covered
         (opIx, _stackDepths, txResults) ->
diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs
index 1300730e3..7f2547333 100644
--- a/lib/Echidna/Solidity.hs
+++ b/lib/Echidna/Solidity.hs
@@ -44,7 +44,7 @@ import Echidna.Symbolic (forceAddr)
 import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isDapptestMode)
 import Echidna.Types.Config (EConfig(..), Env(..))
 import Echidna.Types.Signature
-  (ContractName, SolSignature, SignatureMap, getBytecodeMetadata, FunctionName)
+  (ContractName, SolSignature, SignatureMap, FunctionName)
 import Echidna.Types.Solidity
 import Echidna.Types.Test (EchidnaTest(..))
 import Echidna.Types.Tx
@@ -219,11 +219,11 @@ loadSpecified env name cs = do
             let filtered = filterMethods contract.contractName
                                          solConf.methodFilter
                                          (abiOf solConf.prefix contract)
-            in (getBytecodeMetadata contract.runtimeCode,) <$> NE.nonEmpty filtered)
+            in (contract.runtimeCodehash,) <$> NE.nonEmpty filtered)
           cs
       else
         case NE.nonEmpty fabiOfc of
-          Just ne -> Map.singleton (getBytecodeMetadata mainContract.runtimeCode) ne
+          Just ne -> Map.singleton mainContract.runtimeCodehash ne
           Nothing -> mempty
 
   -- Set up initial VM, either with chosen contract or Etheno initialization file
diff --git a/lib/Echidna/SourceMapping.hs b/lib/Echidna/SourceMapping.hs
new file mode 100644
index 000000000..e0c476d85
--- /dev/null
+++ b/lib/Echidna/SourceMapping.hs
@@ -0,0 +1,102 @@
+module Echidna.SourceMapping where
+
+import Control.Applicative ((<|>))
+import Data.ByteString (ByteString)
+import Data.ByteString qualified as BS
+import Data.IORef (IORef, readIORef, atomicModifyIORef')
+import Data.List (find)
+import Data.Map.Strict qualified as Map
+import Data.Map.Strict (Map)
+import Data.Maybe (mapMaybe)
+import Data.Vector qualified as V
+import Echidna.Symbolic (forceWord)
+import EVM.Dapp (DappInfo(..), findSrc)
+import EVM.Solidity (SolcContract(..))
+import EVM.Types (Contract(..), ContractCode(..), RuntimeCode(..), W256, maybeLitByte)
+
+-- | Map from contracts' codehashes to their compile-time codehash.
+-- This is relevant when the immutables solidity feature is used;
+-- when this feature is not used, the map will just end up being an identity map.
+-- `CodehashMap` is used in signature map and coverage map lookups.
+type CodehashMap = IORef (Map W256 W256)
+
+-- | Lookup a codehash in the `CodehashMap`.
+-- In the case that it's not found, find the compile-time codehash and add it to the map.
+-- This is done using hevm's `findSrc` function.
+lookupCodehash :: CodehashMap -> W256 -> Contract -> DappInfo -> IO W256
+lookupCodehash chmap codehash contr dapp = do
+  chmapVal <- readIORef chmap
+  case Map.lookup codehash chmapVal of
+    Just val -> pure val
+    Nothing -> do
+      -- hevm's `findSrc` doesn't always work, since `SolcContract.immutableReferences` isn't always populated
+      let solcContract = findSrc contr dapp <|> findSrcByMetadata contr dapp
+          originalCodehash = maybe codehash (.runtimeCodehash) solcContract
+      atomicModifyIORef' chmap $ (, ()) . Map.insert codehash originalCodehash
+      pure originalCodehash
+
+-- | Given a map from codehash to some values of type `a`, lookup a contract in the map using its codehash.
+-- In current use, the `Map W256 a` will be either a `SignatureMap` or a `CoverageMap`.
+-- Returns the compile-time codehash, and the map entry if it is found.
+lookupUsingCodehash :: CodehashMap -> Contract -> DappInfo -> Map W256 a -> IO (W256, Maybe a)
+lookupUsingCodehash chmap contr dapp mapVal =
+  ifNotFound codehash $ do
+    codehash' <- lookupCodehash chmap codehash contr dapp
+    ifNotFound codehash' $
+      pure (codehash', Nothing)
+  where
+    codehash = forceWord contr.codehash
+    ifNotFound key notFoundCase = case Map.lookup key mapVal of
+      Nothing -> notFoundCase
+      Just val -> pure (key, Just val)
+
+-- | Same as `lookupUsingCodehash`, except we add to the map if we don't find anything.
+-- The `make` argument is the IO to generate a new element;
+-- it is only run if nothing is found in the map.
+-- In the case that `make` returns `Nothing`, the map will be unchanged.
+-- Returns the map entry, if it is found or generated.
+lookupUsingCodehashOrInsert :: CodehashMap -> Contract -> DappInfo -> IORef (Map W256 a) -> IO (Maybe a) -> IO (Maybe a)
+lookupUsingCodehashOrInsert chmap contr dapp mapRef make = do
+  mapVal <- readIORef mapRef
+  (key, valFound) <- lookupUsingCodehash chmap contr dapp mapVal
+  case valFound of
+    Just val -> pure (Just val)
+    Nothing -> applyModification key =<< make
+  where
+    applyModification _ Nothing = pure Nothing
+    applyModification key (Just val) = atomicModifyIORef' mapRef $ modifyFn key val
+
+    -- Take care of multithreaded edge case
+    modifyFn key val oldMap = case Map.lookup key oldMap of
+      Just val' -> (oldMap, Just val')
+      Nothing -> (Map.insert key val oldMap, Just val)
+
+-- | Try to find a SolcContract with a matching bytecode metadata
+findSrcByMetadata :: Contract -> DappInfo -> Maybe SolcContract
+findSrcByMetadata contr dapp = find compareMetadata (snd <$> Map.elems dapp.solcByHash) where
+  compareMetadata solc = contrMeta == Just (getBytecodeMetadata solc.runtimeCode)
+  contrMeta = getBytecodeMetadata <$> contrCode
+  contrCode = case contr.code of
+    (UnknownCode _) -> Nothing
+    (InitCode c _) -> Just c
+    (RuntimeCode (ConcreteRuntimeCode c)) -> Just c
+    (RuntimeCode (SymbolicRuntimeCode c)) -> Just $ BS.pack $ mapMaybe maybeLitByte $ V.toList c
+
+getBytecodeMetadata :: ByteString -> ByteString
+getBytecodeMetadata bs =
+  let stripCandidates = flip BS.breakSubstring bs <$> knownBzzrPrefixes in
+    case find ((/= mempty) . snd) stripCandidates of
+      Nothing     -> bs -- if no metadata is found, return the complete bytecode
+      Just (_, m) -> m
+
+knownBzzrPrefixes :: [ByteString]
+knownBzzrPrefixes =
+  -- a1 65 "bzzr0" 0x58 0x20 (solc <= 0.5.8)
+  [ BS.pack [0xa1, 0x65, 98, 122, 122, 114, 48, 0x58, 0x20]
+  -- a2 65 "bzzr0" 0x58 0x20 (solc >= 0.5.9)
+  , BS.pack [0xa2, 0x65, 98, 122, 122, 114, 48, 0x58, 0x20]
+  -- a2 65 "bzzr1" 0x58 0x20 (solc >= 0.5.11)
+  , BS.pack [0xa2, 0x65, 98, 122, 122, 114, 49, 0x58, 0x20]
+  -- a2 64 "ipfs" 0x58 0x22 (solc >= 0.6.0)
+  , BS.pack [0xa2, 0x64, 0x69, 0x70, 0x66, 0x73, 0x58, 0x22]
+  ]
diff --git a/lib/Echidna/Transaction.hs b/lib/Echidna/Transaction.hs
index f78b43da2..3a5dc528e 100644
--- a/lib/Echidna/Transaction.hs
+++ b/lib/Echidna/Transaction.hs
@@ -7,27 +7,30 @@ import Optics.Core
 import Optics.State.Operators
 
 import Control.Monad (join)
-import Control.Monad.Random.Strict (MonadRandom, getRandomR, uniform, MonadIO)
+import Control.Monad.IO.Class (MonadIO, liftIO)
+import Control.Monad.Random.Strict (MonadRandom, getRandomR, uniform)
+import Control.Monad.Reader (MonadReader, ask)
 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, fromJust)
+import Data.Maybe (catMaybes)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Vector qualified as V
 
-import EVM (initialContract, loadContract, bytecode, resetState)
+import EVM (initialContract, loadContract, resetState)
 import EVM.ABI (abiValueType)
-import EVM.Types hiding (VMOpts(timestamp, gasprice))
+import EVM.Types hiding (Env, VMOpts(timestamp, gasprice))
 
 import Echidna.ABI
 import Echidna.Orphans.JSON ()
-import Echidna.Symbolic (forceBuf, forceWord, forceAddr)
+import Echidna.SourceMapping (lookupUsingCodehash)
+import Echidna.Symbolic (forceWord, forceAddr)
 import Echidna.Types (fromEVM)
+import Echidna.Types.Config (Env(..), EConfig(..))
 import Echidna.Types.Random
 import Echidna.Types.Signature
-  (SignatureMap, SolCall, ContractA, MetadataCache, lookupBytecodeMetadata)
+  (SignatureMap, SolCall, ContractA)
 import Echidna.Types.Tx
 import Echidna.Types.World (World(..))
 import Echidna.Types.Campaign
@@ -53,18 +56,18 @@ getSignatures hmm (Just lmm) =
 
 -- | Generate a random 'Transaction' with either synthesis or mutation of dictionary entries.
 genTx
-  :: (MonadRandom m, MonadState WorkerState m)
-  => MetadataCache
-  -> World
-  -> TxConf
+  :: (MonadIO m, MonadRandom m, MonadState WorkerState m, MonadReader Env m)
+  => World
   -> Map (Expr EAddr) Contract
   -> m Tx
-genTx memo world txConf deployedContracts = do
+genTx world deployedContracts = do
+  env <- ask
+  let txConf = env.cfg.txConf
   genDict <- gets (.genDict)
   sigMap <- getSignatures world.highSignatureMap world.lowSignatureMap
   sender <- rElem' world.senders
-  (dstAddr, dstAbis) <- rElem' $ Set.fromList $
-    mapMaybe (toContractA sigMap) (toList deployedContracts)
+  contractAList <- liftIO $ mapM (toContractA env sigMap) (toList deployedContracts)
+  (dstAddr, dstAbis) <- rElem' $ Set.fromList $ catMaybes contractAList
   solCall <- genInteractionsM genDict dstAbis
   value <- genValue txConf.maxValue genDict.dictValues world.payableSigs solCall
   ts <- (,) <$> genDelay txConf.maxTimeDelay genDict.dictValues
@@ -78,11 +81,9 @@ genTx memo world txConf deployedContracts = do
             , delay = level ts
             }
   where
-    toContractA :: SignatureMap -> (Expr EAddr, Contract) -> Maybe ContractA
-    toContractA sigMap (addr, c) =
-      let bc = forceBuf $ fromJust $ view bytecode c
-          metadata = lookupBytecodeMetadata memo bc
-      in (forceAddr addr,) <$> Map.lookup metadata sigMap
+    toContractA :: Env -> SignatureMap -> (Expr EAddr, Contract) -> IO (Maybe ContractA)
+    toContractA env sigMap (addr, c) =
+      fmap (forceAddr addr,) . snd <$> lookupUsingCodehash env.codehashMap c env.dapp sigMap
 
 genDelay :: MonadRandom m => W256 -> Set W256 -> m W256
 genDelay mv ds = do
diff --git a/lib/Echidna/Types/Config.hs b/lib/Echidna/Types/Config.hs
index 0098bbce7..0f2dc39d5 100644
--- a/lib/Echidna/Types/Config.hs
+++ b/lib/Echidna/Types/Config.hs
@@ -12,10 +12,10 @@ import Data.Word (Word64)
 import EVM.Dapp (DappInfo)
 import EVM.Types (Addr, Contract, W256)
 
+import Echidna.SourceMapping (CodehashMap)
 import Echidna.Types.Campaign (CampaignConf, CampaignEvent)
 import Echidna.Types.Corpus (Corpus)
 import Echidna.Types.Coverage (CoverageMap)
-import Echidna.Types.Signature (MetadataCache)
 import Echidna.Types.Solidity (SolConf)
 import Echidna.Types.Test (TestConf, EchidnaTest)
 import Echidna.Types.Tx (TxConf)
@@ -71,7 +71,7 @@ data Env = Env
   , coverageRef :: IORef CoverageMap
   , corpusRef :: IORef Corpus
 
-  , metadataCache :: IORef MetadataCache
+  , codehashMap :: CodehashMap
   , fetchContractCache :: IORef (Map Addr (Maybe Contract))
   , fetchSlotCache :: IORef (Map Addr (Map W256 (Maybe W256)))
   , chainId :: Maybe W256
diff --git a/lib/Echidna/Types/Coverage.hs b/lib/Echidna/Types/Coverage.hs
index f793abf5a..36075b7bd 100644
--- a/lib/Echidna/Types/Coverage.hs
+++ b/lib/Echidna/Types/Coverage.hs
@@ -1,18 +1,19 @@
 module Echidna.Types.Coverage where
 
 import Data.Bits (testBit)
-import Data.ByteString (ByteString)
 import Data.List (foldl')
 import Data.Map qualified as Map
 import Data.Map.Strict (Map)
 import Data.Vector.Unboxed.Mutable (IOVector)
 import Data.Vector.Unboxed.Mutable qualified as V
 import Data.Word (Word64)
+import EVM.Types (W256)
 
 import Echidna.Types.Tx (TxResult)
 
--- | Map with the coverage information needed for fuzzing and source code printing
-type CoverageMap = Map ByteString (IOVector CoverageInfo)
+-- | Map with the coverage information needed for fuzzing and source code printing.
+-- Indexed by contracts' compile-time codehash; see `CodehashMap`.
+type CoverageMap = Map W256 (IOVector CoverageInfo)
 
 -- | Basic coverage information
 type CoverageInfo = (OpIx, StackDepths, TxResults)
diff --git a/lib/Echidna/Types/Signature.hs b/lib/Echidna/Types/Signature.hs
index 6a420b678..b2638f478 100644
--- a/lib/Echidna/Types/Signature.hs
+++ b/lib/Echidna/Types/Signature.hs
@@ -4,14 +4,11 @@ module Echidna.Types.Signature where
 
 import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
-import Data.Foldable (find)
 import Data.List.NonEmpty (NonEmpty)
-import Data.Map.Strict qualified as M
-import Data.Maybe (fromMaybe)
 import Data.Text (Text)
 
 import EVM.ABI (AbiType, AbiValue)
-import EVM.Types (Addr)
+import EVM.Types (Addr, W256)
 import Data.Map (Map)
 
 -- | Name of the contract
@@ -31,24 +28,8 @@ type SolCall = (FunctionName, [AbiValue])
 -- | A contract is just an address with an ABI (for our purposes).
 type ContractA = (Addr, NonEmpty SolSignature)
 
--- | Used to memoize results of getBytecodeMetadata
-type MetadataCache = Map ByteString ByteString
-
-type SignatureMap = Map ByteString (NonEmpty SolSignature)
-
-getBytecodeMetadata :: ByteString -> ByteString
-getBytecodeMetadata bs =
-  let stripCandidates = flip BS.breakSubstring bs <$> knownBzzrPrefixes in
-    case find ((/= mempty) . snd) stripCandidates of
-      Nothing     -> bs -- if no metadata is found, return the complete bytecode
-      Just (_, m) -> m
-
-lookupBytecodeMetadata :: MetadataCache -> ByteString -> ByteString
-lookupBytecodeMetadata memo bs = fromMaybe (getBytecodeMetadata bs) (memo M.!? bs)
-
--- | Precalculate getBytecodeMetadata for all contracts in a list
-makeBytecodeCache :: [ByteString] -> MetadataCache
-makeBytecodeCache bss = M.fromList $ bss `zip` (getBytecodeMetadata <$> bss)
+-- | Indexed by contracts' compile-time codehash; see `CodehashMap`.
+type SignatureMap = Map W256 (NonEmpty SolSignature)
 
 knownBzzrPrefixes :: [ByteString]
 knownBzzrPrefixes =
diff --git a/src/Main.hs b/src/Main.hs
index 7645ec055..f79d28aa7 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -89,7 +89,7 @@ main = withUtf8 $ withCP65001 $ do
   buildOutputs <- compileContracts cfg.solConf cliFilePath
   cacheContractsRef <- newIORef $ fromMaybe mempty loadedContractsCache
   cacheSlotsRef <- newIORef $ fromMaybe mempty loadedSlotsCache
-  cacheMetaRef <- newIORef mempty
+  codehashMap <- newIORef mempty
   chainId <- RPC.fetchChainId cfg.rpcUrl
   eventQueue <- newChan
   coverageRef <- newIORef mempty
@@ -102,7 +102,7 @@ main = withUtf8 $ withCP65001 $ do
     env = Env { cfg
                 -- TODO put in real path
               , dapp = dappInfo "/" buildOutput
-              , metadataCache = cacheMetaRef
+              , codehashMap = codehashMap
               , fetchContractCache = cacheContractsRef
               , fetchSlotCache = cacheSlotsRef
               , chainId = chainId
diff --git a/src/test/Common.hs b/src/test/Common.hs
index 6b3a022f8..17a1918f6 100644
--- a/src/test/Common.hs
+++ b/src/test/Common.hs
@@ -97,7 +97,7 @@ runContract f selectedContract cfg = do
     buildOutput = selectBuildOutput selectedContract buildOutputs
     contracts = Map.elems . Map.unions $ (\(BuildOutput (Contracts c) _) -> c) <$> buildOutputs
 
-  metadataCache <- newIORef mempty
+  codehashMap <- newIORef mempty
   fetchContractCache <- newIORef mempty
   fetchSlotCache <- newIORef mempty
   coverageRef <- newIORef mempty
@@ -106,7 +106,7 @@ runContract f selectedContract cfg = do
   testsRef <- newIORef mempty
   let env = Env { cfg = cfg
                 , dapp = dappInfo "/" buildOutput
-                , metadataCache
+                , codehashMap
                 , fetchContractCache
                 , fetchSlotCache
                 , coverageRef
@@ -161,7 +161,7 @@ testContract' fp n v configPath s expectations = testCase fp $ withSolcVersion v
 
 checkConstructorConditions :: FilePath -> String -> TestTree
 checkConstructorConditions fp as = testCase fp $ do
-  cacheMeta <- newIORef mempty
+  codehashMap <- newIORef mempty
   cacheContracts <- newIORef mempty
   cacheSlots <- newIORef mempty
   coverageRef <- newIORef mempty
@@ -170,7 +170,7 @@ checkConstructorConditions fp as = testCase fp $ do
   eventQueue <- newChan
   let env = Env { cfg = testConfig
                 , dapp = emptyDapp
-                , metadataCache = cacheMeta
+                , codehashMap
                 , fetchContractCache = cacheContracts
                 , fetchSlotCache = cacheSlots
                 , coverageRef
diff --git a/src/test/Tests/Compile.hs b/src/test/Tests/Compile.hs
index 54a9afa19..54415f265 100644
--- a/src/test/Tests/Compile.hs
+++ b/src/test/Tests/Compile.hs
@@ -42,7 +42,7 @@ compilationTests = testGroup "Compilation and loading tests"
 loadFails :: FilePath -> Maybe Text -> String -> (SolException -> Bool) -> TestTree
 loadFails fp c e p = testCase fp . catch tryLoad $ assertBool e . p where
   tryLoad = do
-    cacheMeta <- newIORef mempty
+    codehashMap <- newIORef mempty
     cacheContracts <- newIORef mempty
     cacheSlots <- newIORef mempty
     eventQueue <- newChan
@@ -51,7 +51,7 @@ loadFails fp c e p = testCase fp . catch tryLoad $ assertBool e . p where
     testsRef <- newIORef mempty
     let env = Env { cfg = testConfig
                   , dapp = emptyDapp
-                  , metadataCache = cacheMeta
+                  , codehashMap
                   , fetchContractCache = cacheContracts
                   , fetchSlotCache = cacheSlots
                   , chainId = Nothing
diff --git a/src/test/Tests/Integration.hs b/src/test/Tests/Integration.hs
index bb0303609..287c17170 100644
--- a/src/test/Tests/Integration.hs
+++ b/src/test/Tests/Integration.hs
@@ -70,6 +70,8 @@ integrationTests = testGroup "Solidity Integration Testing"
       , ("echidna_timestamp passed",               solved    "echidna_timestamp") ]
   , testContractV "basic/immutable.sol"    (Just (>= solcV (0,6,0))) Nothing
       [ ("echidna_test passed",                    solved      "echidna_test") ]
+  , testContractV "basic/immutable-2.sol"    (Just (>= solcV (0,6,0))) Nothing
+      [ ("echidna_test passed",                    solved      "echidna_test") ]
   , testContract "basic/construct.sol"    Nothing
       [ ("echidna_construct passed",               solved      "echidna_construct") ]
   , testContract "basic/gasprice.sol"     (Just "basic/gasprice.yaml")
diff --git a/tests/solidity/basic/immutable-2.sol b/tests/solidity/basic/immutable-2.sol
new file mode 100644
index 000000000..88f16fe2e
--- /dev/null
+++ b/tests/solidity/basic/immutable-2.sol
@@ -0,0 +1,15 @@
+import "./immutable-3.sol";
+
+contract C {
+  D d;
+  constructor() public {
+    d = new D(0);
+  }
+  function set(uint256 n) external {
+    d = new D(n);
+    d.set();
+  }
+  function echidna_test() external returns (bool) {
+    return d.state();
+  }
+}
diff --git a/tests/solidity/basic/immutable-3.sol b/tests/solidity/basic/immutable-3.sol
new file mode 100644
index 000000000..5a61c26ff
--- /dev/null
+++ b/tests/solidity/basic/immutable-3.sol
@@ -0,0 +1,11 @@
+contract D {
+  uint256 public immutable n;
+  bool public state = true;
+  constructor(uint256 _n) public {
+    n = _n;
+  }
+  function set() external {
+    if (n != 1) revert();
+    state = false;
+  }
+}

From 988bda7c70eba8290aafa1ec4f3b9de8707a86c6 Mon Sep 17 00:00:00 2001
From: Gustavo Grieco <31542053+ggrieco-tob@users.noreply.github.com>
Date: Fri, 12 Jan 2024 14:14:19 +0100
Subject: [PATCH 17/20] Deliver status information using server-sent events
 (#1131)

* POC of delivering status information using server-sent events

* deliver only events instead of status lines

* Stream JSON events

* Hide event server behind config

---------

Co-authored-by: Artur Cygan <artur.cygan@trailofbits.com>
---
 lib/Echidna/Campaign.hs           |  2 +-
 lib/Echidna/Config.hs             |  1 +
 lib/Echidna/Server.hs             | 54 +++++++++++++++++++++++++++++++
 lib/Echidna/Types/Campaign.hs     | 15 ++++++++-
 lib/Echidna/Types/Test.hs         | 30 +++++++++++++++--
 lib/Echidna/UI.hs                 | 23 +++++++++----
 package.yaml                      |  2 ++
 src/Main.hs                       |  7 +++-
 src/test/Tests/Seed.hs            |  1 +
 tests/solidity/basic/default.yaml |  2 ++
 10 files changed, 125 insertions(+), 12 deletions(-)
 create mode 100644 lib/Echidna/Server.hs

diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs
index 9c7c9e144..565b6e698 100644
--- a/lib/Echidna/Campaign.hs
+++ b/lib/Echidna/Campaign.hs
@@ -73,7 +73,7 @@ replayCorpus vm txSeqs =
 -- optional dictionary to generate calls with. Return the 'Campaign' state once
 -- we can't solve or shrink anything.
 runWorker
-  :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m)
+  :: (MonadIO m, MonadThrow m, MonadReader Env m)
   => StateT WorkerState m ()
   -- ^ Callback to run after each state update (for instrumentation)
   -> VM RealWorld -- ^ Initial VM state
diff --git a/lib/Echidna/Config.hs b/lib/Echidna/Config.hs
index 575b1a1b4..9503f3e94 100644
--- a/lib/Echidna/Config.hs
+++ b/lib/Echidna/Config.hs
@@ -96,6 +96,7 @@ instance FromJSON EConfigWithUsage where
         <*> v ..:? "mutConsts" ..!= defaultMutationConsts
         <*> v ..:? "coverageFormats" ..!= [Txt,Html,Lcov]
         <*> v ..:? "workers"
+        <*> v ..:? "server"
 
       solConfParser = SolConf
         <$> v ..:? "contractAddr"    ..!= defaultContractAddr
diff --git a/lib/Echidna/Server.hs b/lib/Echidna/Server.hs
new file mode 100644
index 000000000..b9e0f851c
--- /dev/null
+++ b/lib/Echidna/Server.hs
@@ -0,0 +1,54 @@
+module Echidna.Server where
+
+import Control.Concurrent
+import Control.Monad (when, void)
+import Data.Aeson
+import Data.Binary.Builder (fromLazyByteString)
+import Data.IORef
+import Data.Time (LocalTime)
+import Data.Word (Word16)
+import Network.Wai.EventSource (ServerEvent(..), eventSourceAppIO)
+import Network.Wai.Handler.Warp (run)
+
+import Echidna.Types.Campaign (CampaignEvent (..))
+import Echidna.Types.Config (Env(..))
+
+newtype SSE = SSE (Int, LocalTime, CampaignEvent)
+
+instance ToJSON SSE where
+  toJSON (SSE (workerId, time, event)) =
+    object [ "worker" .= workerId
+           , "timestamp" .= time
+           , "data" .= event
+           ]
+
+runSSEServer :: MVar () -> Env -> Word16 -> Int -> IO ()
+runSSEServer serverStopVar env port nworkers = do
+  aliveRef <- newIORef nworkers
+  sseChan <- dupChan env.eventQueue
+
+  let sseListener = do
+        aliveNow <- readIORef aliveRef
+        if aliveNow == 0 then
+          pure CloseEvent
+        else do
+          event@(_, _, campaignEvent) <- readChan sseChan
+          let eventName = \case
+                TestFalsified _ -> "test_falsified"
+                TestOptimized _ -> "test_optimized"
+                NewCoverage {} -> "new_coverage"
+                TxSequenceReplayed _ _ -> "tx_sequence_replayed"
+                WorkerStopped _ -> "worker_stopped"
+          case campaignEvent of
+            WorkerStopped _ -> do
+              aliveAfter <- atomicModifyIORef' aliveRef (\n -> (n-1, n-1))
+              when (aliveAfter == 0) $ putMVar serverStopVar ()
+            _ -> pure ()
+          pure $ ServerEvent
+            { eventName = Just (eventName campaignEvent)
+            , eventId = Nothing
+            , eventData = [ fromLazyByteString $ encode (SSE event) ]
+            }
+
+  void . forkIO $ do
+    run (fromIntegral port) $ eventSourceAppIO sseListener
diff --git a/lib/Echidna/Types/Campaign.hs b/lib/Echidna/Types/Campaign.hs
index 85f0ca478..c29f2b48f 100644
--- a/lib/Echidna/Types/Campaign.hs
+++ b/lib/Echidna/Types/Campaign.hs
@@ -1,9 +1,10 @@
 module Echidna.Types.Campaign where
 
+import Data.Aeson
 import Data.Map (Map)
 import Data.Text (Text)
 import Data.Text qualified as T
-import Data.Word (Word8)
+import Data.Word (Word8, Word16)
 
 import Echidna.ABI (GenDict, emptyDict, encodeSig)
 import Echidna.Output.Source (CoverageFileType)
@@ -39,6 +40,9 @@ data CampaignConf = CampaignConf
   , coverageFormats :: [CoverageFileType]
     -- ^ List of file formats to save coverage reports
   , workers         :: Maybe Word8
+    -- ^ Number of fuzzing workers
+  , serverPort      :: Maybe Word16
+    -- ^ Server-Sent Events HTTP port number, if missing server is not ran
   }
 
 data CampaignEvent
@@ -51,6 +55,15 @@ data CampaignEvent
   -- this one
   deriving Show
 
+instance ToJSON CampaignEvent where
+  toJSON = \case
+    TestFalsified test -> toJSON test
+    TestOptimized test -> toJSON test
+    NewCoverage coverage numContracts corpusSize ->
+      object [ "coverage" .= coverage, "contracts" .= numContracts, "corpus_size" .= corpusSize]
+    TxSequenceReplayed current total -> object [ "current" .= current, "total" .= total ]
+    WorkerStopped reason -> object [ "reason" .= show reason ]
+
 data WorkerStopReason
   = TestLimitReached
   | TimeLimitReached
diff --git a/lib/Echidna/Types/Test.hs b/lib/Echidna/Types/Test.hs
index 192e8a00e..7b2b58391 100644
--- a/lib/Echidna/Types/Test.hs
+++ b/lib/Echidna/Types/Test.hs
@@ -1,7 +1,10 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE RecordWildCards #-}
+
 module Echidna.Types.Test where
 
 import Control.Monad.ST (RealWorld)
-import Data.Aeson (ToJSON(..), object)
+import Data.Aeson
 import Data.DoubleWord (Int256)
 import Data.Maybe (maybeToList)
 import Data.Text (Text)
@@ -12,6 +15,7 @@ import EVM.Types (Addr, VM)
 import Echidna.Types (ExecException)
 import Echidna.Types.Signature (SolSignature)
 import Echidna.Types.Tx (Tx, TxResult)
+import GHC.Generics (Generic)
 
 -- | Test mode is parsed from a string
 type TestMode = String
@@ -40,7 +44,7 @@ data TestValue
   = BoolValue Bool
   | IntValue Int256
   | NoValue
-  deriving (Eq, Ord)
+  deriving (Eq, Ord, Generic, ToJSON)
 
 instance Show TestValue where
   show (BoolValue x) = show x
@@ -70,6 +74,19 @@ instance Show TestType where
     CallTest t _         -> show t
     Exploration          -> "Exploration"
 
+instance ToJSON TestType where
+  toJSON = \case
+    PropertyTest name addr ->
+      object [ "type" .= ("property_test" :: String), "name" .= name, "addr" .= addr ]
+    OptimizationTest name addr ->
+      object [ "type" .= ("optimization_test" :: String), "name" .= name, "addr" .= addr ]
+    AssertionTest _ sig addr ->
+      object [ "type" .= ("assertion_test" :: String), "signature" .= sig, "addr" .= addr ]
+    CallTest name _ ->
+      object [ "type" .= ("call_test" :: String), "name" .= name ]
+    Exploration ->
+      object [ "type" .= ("exploration_test" :: String) ]
+
 instance Eq TestState where
   Open    == Open    = True
   Large i == Large j = i == j
@@ -87,6 +104,15 @@ data EchidnaTest = EchidnaTest
   , vm         :: Maybe (VM RealWorld)
   } deriving (Show)
 
+instance ToJSON EchidnaTest where
+  toJSON EchidnaTest{..} = object
+    [ "state" .= state
+    , "type" .= testType
+    , "value" .= value
+    , "reproducer" .= reproducer
+    , "result" .= result
+    ]
+
 isOptimizationTest :: EchidnaTest -> Bool
 isOptimizationTest EchidnaTest{testType = OptimizationTest _ _} = True
 isOptimizationTest _ = False
diff --git a/lib/Echidna/UI.hs b/lib/Echidna/UI.hs
index 9d68dfd76..4c2bfec5b 100644
--- a/lib/Echidna/UI.hs
+++ b/lib/Echidna/UI.hs
@@ -18,19 +18,17 @@ import Control.Concurrent (killThread, threadDelay)
 import Control.Exception (AsyncException)
 import Control.Monad
 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.Binary.Builder
 import Data.ByteString.Lazy qualified as BS
 import Data.List.Split (chunksOf)
 import Data.Map (Map)
 import Data.Maybe (fromMaybe, isJust)
 import Data.Time
 import UnliftIO
-  ( MonadUnliftIO, newIORef, readIORef, atomicWriteIORef, hFlush, stdout
-  , writeIORef, atomicModifyIORef', timeout
-  )
+  ( MonadUnliftIO, newIORef, readIORef, hFlush, stdout , writeIORef, timeout)
 import UnliftIO.Concurrent hiding (killThread, threadDelay)
 
 import EVM.Types (Addr, Contract, VM, W256)
@@ -38,11 +36,12 @@ import EVM.Types (Addr, Contract, VM, W256)
 import Echidna.ABI
 import Echidna.Campaign (runWorker)
 import Echidna.Output.JSON qualified
+import Echidna.Server (runSSEServer)
 import Echidna.Types.Campaign
 import Echidna.Types.Config
 import Echidna.Types.Corpus (corpusSize)
 import Echidna.Types.Coverage (scoveragePoints)
-import Echidna.Types.Test (EchidnaTest(..), didFail, isOptimizationTest, TestType, TestState(..))
+import Echidna.Types.Test (EchidnaTest(..), didFail, isOptimizationTest)
 import Echidna.Types.Tx (Tx)
 import Echidna.Types.World (World)
 import Echidna.UI.Report
@@ -57,7 +56,7 @@ data UIEvent =
 -- | Set up and run an Echidna 'Campaign' and display interactive UI or
 -- print non-interactive output in desired format at the end
 ui
-  :: (MonadCatch m, MonadRandom m, MonadReader Env m, MonadUnliftIO m)
+  :: (MonadCatch m, MonadReader Env m, MonadUnliftIO m)
   => VM RealWorld -- ^ Initial VM state
   -> World   -- ^ Initial world state
   -> GenDict
@@ -159,10 +158,11 @@ ui vm world dict initialCorpus = do
 #endif
 
     NonInteractive outputFormat -> do
+      serverStopVar <- newEmptyMVar
 #ifdef INTERACTIVE_UI
       -- Handles ctrl-c, TODO: this doesn't work on Windows
       liftIO $ forM_ [sigINT, sigTERM] $ \sig ->
-        installHandler sig (Catch $ stopWorkers workers) Nothing
+        installHandler sig (Catch $ stopWorkers workers >> putMVar serverStopVar ()) Nothing
 #endif
       let forwardEvent = putStrLn . ppLogLine
       liftIO $ spawnListener env forwardEvent nworkers listenerStopVar
@@ -174,6 +174,10 @@ ui vm world dict initialCorpus = do
             putStrLn $ time <> "[status] " <> line
             hFlush stdout
 
+      case conf.campaignConf.serverPort of
+        Just port -> liftIO $ runSSEServer serverStopVar env port nworkers
+        Nothing -> pure ()
+
       ticker <- liftIO . forkIO . forever $ do
         threadDelay 3_000_000 -- 3 seconds
         printStatus
@@ -186,6 +190,11 @@ ui vm world dict initialCorpus = do
       -- print final status regardless the last scheduled update
       liftIO printStatus
 
+      when (isJust conf.campaignConf.serverPort) $ do
+        -- wait until we send all SSE events
+        liftIO $ putStrLn "Waiting until all SSE are received..."
+        readMVar serverStopVar
+
       states <- liftIO $ workerStates workers
 
       case outputFormat of
diff --git a/package.yaml b/package.yaml
index da8b29531..b7577f30b 100644
--- a/package.yaml
+++ b/package.yaml
@@ -48,6 +48,8 @@ dependencies:
   - yaml
   - http-conduit
   - html-conduit
+  - warp
+  - wai-extra
   - xml-conduit
   - strip-ansi-escape
 
diff --git a/src/Main.hs b/src/Main.hs
index f79d28aa7..ed45883f3 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -24,7 +24,7 @@ import Data.Text (Text)
 import Data.Time.Clock.System (getSystemTime, systemSeconds)
 import Data.Vector qualified as Vector
 import Data.Version (showVersion)
-import Data.Word (Word8)
+import Data.Word (Word8, Word16)
 import Main.Utf8 (withUtf8)
 import Options.Applicative
 import Paths_echidna (version)
@@ -225,6 +225,7 @@ readFileIfExists path = do
 data Options = Options
   { cliFilePath         :: NE.NonEmpty FilePath
   , cliWorkers          :: Maybe Word8
+  , cliServerPort       :: Maybe Word16
   , cliSelectedContract :: Maybe Text
   , cliConfigFilepath   :: Maybe FilePath
   , cliOutputFormat     :: Maybe OutputFormat
@@ -255,6 +256,9 @@ options = Options
   <*> optional (option auto $ long "workers"
     <> metavar "N"
     <> help "Number of workers to run")
+  <*> optional (option auto $ long "server"
+    <> metavar "PORT"
+    <> help "Run events server on the given port")
   <*> optional (option str $ long "contract"
     <> metavar "CONTRACT"
     <> help "Contract to analyze")
@@ -339,6 +343,7 @@ overrideConfig config Options{..} = do
       , seqLen = fromMaybe campaignConf.seqLen cliSeqLen
       , seed = cliSeed <|> campaignConf.seed
       , workers = cliWorkers <|> campaignConf.workers
+      , serverPort = cliServerPort <|> campaignConf.serverPort
       }
 
     overrideSolConf solConf = solConf
diff --git a/src/test/Tests/Seed.hs b/src/test/Tests/Seed.hs
index b1b3e5abc..5c8c46e99 100644
--- a/src/test/Tests/Seed.hs
+++ b/src/test/Tests/Seed.hs
@@ -34,6 +34,7 @@ seedTests =
         , mutConsts = defaultMutationConsts
         , coverageFormats = [Txt,Html,Lcov]
         , workers = Nothing
+        , serverPort = Nothing
         }
       }
       & overrideQuiet
diff --git a/tests/solidity/basic/default.yaml b/tests/solidity/basic/default.yaml
index 9b2c6f71a..f07593d0a 100644
--- a/tests/solidity/basic/default.yaml
+++ b/tests/solidity/basic/default.yaml
@@ -89,3 +89,5 @@ rpcUrl: null
 rpcBlock: null
 # number of workers
 workers: 1
+# events server port
+server: null

From fb42ab4b5a1041ba1877a764aada50782a3907cd Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Tue, 16 Jan 2024 12:23:10 +0100
Subject: [PATCH 18/20] Bump cachix/cachix-action from 13 to 14 (#1162)

Bumps [cachix/cachix-action](https://github.com/cachix/cachix-action) from 13 to 14.
- [Release notes](https://github.com/cachix/cachix-action/releases)
- [Commits](https://github.com/cachix/cachix-action/compare/v13...v14)

---
updated-dependencies:
- dependency-name: cachix/cachix-action
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
---
 .github/workflows/release.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 70adf4669..993aa4d51 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -39,7 +39,7 @@ jobs:
         uses: DeterminateSystems/nix-installer-action@v9
 
       - name: Configure Cachix
-        uses: cachix/cachix-action@v13
+        uses: cachix/cachix-action@v14
         with:
           name: trailofbits
           authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}

From e604b300ae0e6cfb21c4c2db4ee9f44612ad7850 Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Tue, 16 Jan 2024 12:23:30 +0100
Subject: [PATCH 19/20] Bump cachix/install-nix-action from 24 to 25 (#1163)

Bumps [cachix/install-nix-action](https://github.com/cachix/install-nix-action) from 24 to 25.
- [Release notes](https://github.com/cachix/install-nix-action/releases)
- [Commits](https://github.com/cachix/install-nix-action/compare/v24...v25)

---
updated-dependencies:
- dependency-name: cachix/install-nix-action
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
---
 .github/workflows/hlint.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/hlint.yml b/.github/workflows/hlint.yml
index a0b53307f..65e005133 100644
--- a/.github/workflows/hlint.yml
+++ b/.github/workflows/hlint.yml
@@ -16,7 +16,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Install Nix
-        uses: cachix/install-nix-action@v24
+        uses: cachix/install-nix-action@v25
         with:
           nix_path: nixpkgs=channel:nixos-unstable
 

From 24cd9729a08af6148921377e264c05e54b32e869 Mon Sep 17 00:00:00 2001
From: Feist Josselin <josselin.feist@gmail.com>
Date: Wed, 17 Jan 2024 17:32:09 +0100
Subject: [PATCH 20/20] Add list of security reviews (#1165)

---
 README.md | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/README.md b/README.md
index 7a747eb13..db62cddc9 100644
--- a/README.md
+++ b/README.md
@@ -310,6 +310,40 @@ This is a partial list of smart contracts projects that use Echidna for testing:
 * [Tokencard](https://github.com/tokencard/contracts/tree/master/tools/echidna)
 * [Minimalist USD Stablecoin](https://github.com/usmfum/USM/pull/41)
 
+### Security reviews
+
+The following shows public security reviews that used Echidna to uncover vulnerabilities
+
+- [Advanced Blockchain](https://github.com/trailofbits/publications/blob/master/reviews/AdvancedBlockchain.pdf)
+- [Amp](https://github.com/trailofbits/publications/blob/master/reviews/amp.pdf)
+- [Ampleforth](https://github.com/trailofbits/publications/blob/master/reviews/ampleforth.pdf)
+- [Atlendis](https://github.com/trailofbits/publications/blob/master/reviews/2023-03-atlendis-atlendissmartcontracts-securityreview.pdf)
+- [Balancer](https://github.com/trailofbits/publications/blob/master/reviews/2021-04-balancer-balancerv2-securityreview.pdf)
+- [Basis](https://github.com/trailofbits/publications/blob/master/reviews/basis.pdf)
+- [Dai](https://github.com/trailofbits/publications/blob/master/reviews/mc-dai.pdf)
+- [Frax](https://github.com/trailofbits/publications/blob/master/reviews/FraxQ22022.pdf)
+- [Liquity](https://github.com/trailofbits/publications/blob/master/reviews/LiquityProtocolandStabilityPoolFinalReport.pdf)
+- [LooksRare](https://github.com/trailofbits/publications/blob/master/reviews/LooksRare.pdf)
+- [Maple](https://github.com/trailofbits/publications/blob/master/reviews/2022-03-maplefinance-securityreview.pdf)
+- [Optimism](https://github.com/trailofbits/publications/blob/master/reviews/2022-11-optimism-securityreview.pdf)
+- [Opyn](https://github.com/trailofbits/publications/blob/master/reviews/Opyn.pdf)
+- [Origin Dollar](https://github.com/trailofbits/publications/blob/master/reviews/OriginDollar.pdf)
+- [Origin](https://github.com/trailofbits/publications/blob/master/reviews/origin.pdf)
+- [Paxos](https://github.com/trailofbits/publications/blob/master/reviews/paxos.pdf)
+- [Primitive](https://github.com/trailofbits/publications/blob/master/reviews/Primitive.pdf)
+- [RocketPool](https://github.com/trailofbits/publications/blob/master/reviews/RocketPool.pdf)
+- [Seaport](https://github.com/trailofbits/publications/blob/master/reviews/SeaportProtocol.pdf)
+- [Set Protocol](https://github.com/trailofbits/publications/blob/master/reviews/setprotocol.pdf)
+- [Shell protocol](https://github.com/trailofbits/publications/blob/master/reviews/ShellProtocolv2.pdf)
+- [Sherlock](https://github.com/trailofbits/publications/blob/master/reviews/Sherlockv2.pdf)
+- [Pegasys Pantheon](https://github.com/trailofbits/publications/blob/master/reviews/pantheon.pdf)
+- [TokenCard](https://github.com/trailofbits/publications/blob/master/reviews/TokenCard.pdf)
+- [Uniswap](https://github.com/trailofbits/publications/blob/master/reviews/UniswapV3Core.pdf)
+- [Yearn](https://github.com/trailofbits/publications/blob/master/reviews/YearnV2Vaults.pdf)
+- [Yield](https://github.com/trailofbits/publications/blob/master/reviews/YieldProtocol.pdf)
+- [88mph](https://github.com/trailofbits/publications/blob/master/reviews/88mph.pdf)
+- [0x](https://github.com/trailofbits/publications/blob/master/reviews/0x-protocol.pdf)
+
 ### Trophies
 
 The following security vulnerabilities were found by Echidna. If you found a security vulnerability using our tool, please submit a PR with the relevant information.