From a16d3c084cbf25c974cba3c92c8611df9dbd2519 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Thu, 24 Oct 2024 15:12:25 +0200
Subject: [PATCH 01/27] Making assert... into reverts, as per std-forge

---
 CHANGELOG.md        |   2 +
 src/EVM.hs          | 101 ++++++++++++++++++++++++++++++++++++++++++++
 src/EVM/UnitTest.hs |  26 +++++-------
 3 files changed, 114 insertions(+), 15 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ccfdf87a1..38e30de38 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,6 +10,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - More complete and precise array/mapping slot rewrite, along with a copySlice improvement
 - Use a let expression in copySlice to decrease expression size
 - The `--debug` flag now dumps the internal expressions as well
+- hevm now uses the std-forge library's way of detecting failures, i.e. through
+  reverting with a specific error code
 
 ## Added
 - More POr and PAnd rules
diff --git a/src/EVM.hs b/src/EVM.hs
index a5a83930c..a85426e9b 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -32,6 +32,7 @@ import Data.Bits (FiniteBits, countLeadingZeros, finiteBitSize)
 import Data.ByteArray qualified as BA
 import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
+import Data.ByteString.Char8 qualified as BS8
 import Data.ByteString.Base16 qualified as BS16
 import Data.ByteString.Lazy (fromStrict)
 import Data.ByteString.Lazy qualified as LS
@@ -1903,6 +1904,57 @@ cheatActions = Map.fromList
   , $(envReadMultipleCheat "envBytes32(string,string)" $ AbiBytesType 32) stringToBytes32
   , $(envReadMultipleCheat "envString(string,string)" AbiStringType) stringToByteString
   , $(envReadMultipleCheat "envBytes(bytes,bytes)" AbiBytesDynamicType) stringHexToByteString
+  , action "asserTrue(bool)" $ \sig input ->
+      case decodeBuf [AbiBoolType] input of
+        CAbi [AbiBool True] -> doStop
+        CAbi [AbiBool False] -> frameRevert "assertion failed"
+        _ -> vmError $ BadCheatCode ("assertTrue(bool) parameter decoding failed") sig
+  , action "asserFalse(bool)" $ \sig input ->
+      case decodeBuf [AbiBoolType] input of
+        CAbi [AbiBool False] -> doStop
+        CAbi [AbiBool True] -> frameRevert "assertion failed"
+        _ -> vmError $ BadCheatCode ("assertFalse(bool) parameter decoding failed") sig
+  , action "assertEq(bool,bool)"       $ assertEq AbiBoolType
+  , action "assertEq(uint256,uint256)" $ assertEq (AbiUIntType 256)
+  , action "assertEq(int256,int256)"   $ assertEq (AbiIntType 256)
+  , action "assertEq(address,address)" $ assertEq AbiAddressType
+  , action "assertEq(bytes32,bytes32)" $ assertEq (AbiBytesType 32)
+  , action "assertEq(string,string)"   $ assertEq AbiStringType
+  --
+  , action "assertNotEq(bytes,bytes)"     $ assertNotEq (AbiBytesDynamicType)
+  , action "assertNotEq(bool,bool)"       $ assertNotEq AbiBoolType
+  , action "assertNotEq(uint256,uint256)" $ assertNotEq (AbiUIntType 256)
+  , action "assertNotEq(int256,int256)"   $ assertNotEq (AbiIntType 256)
+  , action "assertNotEq(address,address)" $ assertNotEq AbiAddressType
+  , action "assertNotEq(bytes32,bytes32)" $ assertNotEq (AbiBytesType 32)
+  , action "assertNotEq(string,string)"   $ assertNotEq AbiStringType
+  , action "assertNotEq(bytes,bytes)"     $ assertNotEq (AbiBytesDynamicType)
+  --
+  , action "assertNotEqMsg(bytes,bytes)"     $ assertNotEqMsg (AbiBytesDynamicType)
+  , action "assertNotEqMsg(bool,bool)"       $ assertNotEqMsg AbiBoolType
+  , action "assertNotEqMsg(uint256,uint256)" $ assertNotEqMsg (AbiUIntType 256)
+  , action "assertNotEqMsg(int256,int256)"   $ assertNotEqMsg (AbiIntType 256)
+  , action "assertNotEqMsg(address,address)" $ assertNotEqMsg AbiAddressType
+  , action "assertNotEqMsg(bytes32,bytes32)" $ assertNotEqMsg (AbiBytesType 32)
+  , action "assertNotEqMsg(string,string)"   $ assertNotEqMsg AbiStringType
+  , action "assertNotEqMsg(bytes,bytes)"     $ assertNotEqMsg (AbiBytesDynamicType)
+  --
+  , action "assertEq(bool,bool,string)"       $ assertEqMsg AbiBoolType
+  , action "assertEq(uint256,uint256,string)" $ assertEqMsg (AbiUIntType 256)
+  , action "assertEq(int256,int256,string)"   $ assertEqMsg (AbiIntType 256)
+  , action "assertEq(address,address,string)" $ assertEqMsg AbiAddressType
+  , action "assertEq(bytes32,bytes32,string)" $ assertEqMsg (AbiBytesType 32)
+  , action "assertEq(string,string,string)"   $ assertEqMsg AbiStringType
+  , action "assertEq(bytes,bytes,string)"     $ assertEqMsg (AbiBytesDynamicType)
+  --
+  , action "assertLt(uint256,uint256)" $ assertLt (AbiUIntType 256)
+  , action "assertLt(int256,int256)"   $ assertLt (AbiIntType 256)
+  , action "assertLe(uint256,uint256)" $ assertLe (AbiUIntType 256)
+  , action "assertLe(int256,int256)"   $ assertLe (AbiIntType 256)
+  , action "assertGt(uint256,uint256)" $ assertGt (AbiUIntType 256)
+  , action "assertGt(int256,int256)"   $ assertGt (AbiIntType 256)
+  , action "assertGe(uint256,uint256)" $ assertGe (AbiUIntType 256)
+  , action "assertGe(int256,int256)"   $ assertGe (AbiIntType 256)
   ]
   where
     action s f = (abiKeccak s, f (abiKeccak s))
@@ -1942,6 +1994,55 @@ cheatActions = Map.fromList
     stringToByteString = Right . Char8.pack
     stringHexToByteString :: String -> Either ByteString ByteString
     stringHexToByteString s = either (const $ Left "invalid bytes value") Right $ BS16.decodeBase16Untyped . Char8.pack . strip0x $ s
+    paramDecodeErr abitype name = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
+      ")  parameter decoding failed"
+    paramDecodeMsgErr abitype name = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
+      ",string)  parameter decoding failed"
+    revertErr a b comp = frameRevert $ "assertion failed: " <>
+      BS8.pack (show a) <> " " <> comp <> " " <> BS8.pack (show b)
+    revertMsgErr a b str comp = frameRevert $ "assertion failed: "
+      <> str <> ": " <> BS8.pack (show a) <> " " <> comp <> " " <> BS8.pack (show b)
+    assertEq abitype sig input = do
+      case decodeBuf [abitype, abitype] input of
+        CAbi [a, b] | a == b -> doStop
+        CAbi [a, b] -> revertErr a b "!="
+        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertEq") sig)
+    assertEqMsg abitype sig input =
+      case decodeBuf [abitype, abitype, AbiStringType] input of
+        CAbi [a, b, _] | a == b -> doStop
+        CAbi [a, b, AbiString str] -> revertMsgErr a b str "!="
+        _ -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertEq") sig)
+    assertNotEq abitype sig input = do
+      case decodeBuf [abitype, abitype] input of
+        CAbi [a, b] | a /= b -> doStop
+        CAbi [a, b] -> revertErr a b "=="
+        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertNotEq") sig)
+    assertNotEqMsg abitype sig input = do
+      case decodeBuf [abitype, abitype] input of
+        CAbi [a, b, _] | a /= b -> doStop
+        CAbi [a, b, AbiString str] -> revertMsgErr a b str "=="
+        _ -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertNotEq") sig)
+    assertLt abitype sig input =
+      case decodeBuf [abitype, abitype] input of
+        CAbi [a, b] | a < b -> doStop
+        CAbi [a, b] -> revertErr a b ">="
+        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertLt") sig)
+    assertGt abitype sig input =
+      case decodeBuf [abitype, abitype] input of
+        CAbi [a, b] | a > b -> doStop
+        CAbi [a, b] -> revertErr a b "<="
+        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertGt") sig)
+    assertLe abitype sig input =
+      case decodeBuf [abitype, abitype] input of
+        CAbi [a, b] | a <= b -> doStop
+        CAbi [a, b] -> revertErr a b "<"
+        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertLe") sig)
+    assertGe abitype sig input =
+      case decodeBuf [abitype, abitype] input of
+        CAbi [a, b] | a >= b -> doStop
+        CAbi [a, b] -> revertErr a b ">"
+        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertGe") sig)
+
 
 -- * General call implementation ("delegateCall")
 -- note that the continuation is ignored in the precompile case
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index 998629bc3..d47d6f6f7 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -29,6 +29,7 @@ import Optics.State
 import Optics.State.Operators
 import Data.Binary.Get (runGet)
 import Data.ByteString (ByteString)
+import Data.ByteString.Char8 qualified as BS
 import Data.ByteString.Lazy qualified as BSLazy
 import Data.Decimal (DecimalRaw(..))
 import Data.Foldable (toList)
@@ -206,13 +207,16 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
                                   Success _ _ _ store -> failed store
                                   _ -> PBool True
           False -> \(_, post) -> case post of
-                                   Success _ _ _ store -> PNeg (failed store)
-                                   Failure _ _ (Revert msg) -> case msg of
-                                     ConcreteBuf b -> PBool $ b /= panicMsg 0x01
-                                     b -> b ./= ConcreteBuf (panicMsg 0x01)
-                                   Failure _ _ _ -> PBool True
-                                   Partial _ _ _ -> PBool True
-                                   _ -> internalError "Invalid leaf node"
+            Success _ _ _ store -> PNeg (failed store)
+            Failure _ _ (Revert msg) -> case msg of
+              ConcreteBuf b -> do
+                if (BS.isPrefixOf (BS.pack "assert failed") b) ||
+                  b == panicMsg 0x01 then PBool True
+                else PBool False
+              b -> b ./= ConcreteBuf (panicMsg 0x01)
+            Failure _ _ _ -> PBool True
+            Partial _ _ _ -> PBool True
+            _ -> internalError "Invalid leaf node"
 
     vm' <- Stepper.interpret (Fetch.oracle solvers rpcInfo) vm $
       Stepper.evm $ do
@@ -287,14 +291,6 @@ execSymTest UnitTestOptions{ .. } method cd = do
   -- Try running the test method
   runExpr
 
-checkSymFailures :: VMOps t => UnitTestOptions RealWorld -> Stepper t RealWorld (VM t RealWorld)
-checkSymFailures UnitTestOptions { .. } = do
-  -- Ask whether any assertions failed
-  Stepper.evm $ do
-    popTrace
-    abiCall testParams (Left ("failed()", emptyAbi))
-  Stepper.runFully
-
 indentLines :: Int -> Text -> Text
 indentLines n s =
   let p = Text.replicate n " "

From 29279b0eba52fb83d4517e2e0516b6bde06c50b3 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Tue, 29 Oct 2024 19:18:40 +0100
Subject: [PATCH 02/27] Fixing some issues with tests

---
 test/EVM/Test/Utils.hs              | 7 +++----
 test/contracts/fail/dsProveFail.sol | 4 ++--
 test/test.hs                        | 2 +-
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs
index 93c89913f..143cca3e4 100644
--- a/test/EVM/Test/Utils.hs
+++ b/test/EVM/Test/Utils.hs
@@ -45,7 +45,7 @@ runSolidityTestCustom testFile match timeout maxIter ffiAllowed rpcinfo projectT
 runSolidityTest
   :: (MonadMask m, App m)
   => FilePath -> Text -> m Bool
-runSolidityTest testFile match = runSolidityTestCustom testFile match Nothing Nothing True Nothing Foundry
+runSolidityTest testFile match = runSolidityTestCustom testFile match Nothing Nothing True Nothing FoundryStdLib
 
 testOpts :: SolverGroup -> FilePath -> Maybe BuildOutput -> Text -> Maybe Integer -> Bool -> RpcInfo -> IO (UnitTestOptions RealWorld)
 testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do
@@ -79,7 +79,7 @@ callProcessCwd cmd args cwd = do
     exit_code <- withCreateProcess (proc cmd args) { cwd = Just cwd, delegate_ctlc = True } $ \_ _ _ p ->
                  waitForProcess p
     case exit_code of
-      ExitSuccess   -> return ()
+      ExitSuccess   -> pure ()
       ExitFailure r -> processFailedException "callProcess" cmd args r
 
 compile :: App m => ProjectType -> FilePath -> FilePath -> m (Either String BuildOutput)
@@ -88,11 +88,10 @@ compile DappTools root src = do
   liftIO $ createDirectory (root </> "out")
   liftIO $ T.writeFile (root </> "out" </> "dapp.sol.json") json
   readBuildOutput root DappTools
-compile CombinedJSON _root _src = error "unsupported"
+compile CombinedJSON _root _src = internalError  "unsupported compile type: CombinedJSON"
 compile foundryType root src = do
   liftIO $ createDirectory (root </> "src")
   liftIO $ writeFile (root </> "src" </> "unit-tests.t.sol") =<< readFile =<< Paths.getDataFileName src
-  liftIO $ initLib (root </> "lib" </> "ds-test") ("test" </> "contracts" </> "lib" </> "test.sol") "test.sol"
   liftIO $ initLib (root </> "lib" </> "tokens") ("test" </> "contracts" </> "lib" </> "erc20.sol") "erc20.sol"
   case foundryType of
     FoundryStdLib -> liftIO $ initStdForgeDir (root </> "lib" </> "forge-std")
diff --git a/test/contracts/fail/dsProveFail.sol b/test/contracts/fail/dsProveFail.sol
index e6ee6f607..f151a7f7c 100644
--- a/test/contracts/fail/dsProveFail.sol
+++ b/test/contracts/fail/dsProveFail.sol
@@ -1,7 +1,7 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 import "tokens/erc20.sol";
 
-contract SolidityTest is DSTest {
+contract SolidityTest is Test {
     ERC20 token;
 
     function setUp() public {
diff --git a/test/test.hs b/test/test.hs
index b428670cd..586b6fdf6 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1477,7 +1477,7 @@ tests = testGroup "hevm"
         runSolidityTest testFile "prove_trivial" >>= assertEqualM "test result" False
         runSolidityTest testFile "prove_trivial_dstest" >>= assertEqualM "test result" False
         runSolidityTest testFile "prove_add" >>= assertEqualM "test result" False
-        runSolidityTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False Nothing Foundry >>= assertEqualM "test result" False
+        runSolidityTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False Nothing FoundryStdLib >>= assertEqualM "test result" False
         runSolidityTest testFile "prove_multi" >>= assertEqualM "test result" False
         -- TODO: implement overflow checking optimizations and enable, currently this runs forever
         --runSolidityTest testFile "prove_distributivity" >>= assertEqualM "test result" False

From 2cb92a985c98d59abd3b6cbad571d6bf9039193d Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 30 Oct 2024 17:32:59 +0100
Subject: [PATCH 03/27] Temporary

---
 cli/cli.hs                                 |   8 +-
 doc/src/exec.md                            |   4 +-
 doc/src/symbolic.md                        |   2 -
 doc/src/test.md                            |   2 -
 funding.json                               |   5 -
 src/EVM.hs                                 | 115 ++++++++++++++++-----
 src/EVM/ABI.hs                             |  64 +++++++++---
 src/EVM/Solidity.hs                        |  10 +-
 src/EVM/UnitTest.hs                        |   5 +-
 test/EVM/Test/Utils.hs                     |  11 +-
 test/contracts/fail/check-prefix.sol       |   4 +-
 test/contracts/fail/trivial.sol            |   4 +-
 test/contracts/pass/abstract.sol           |   4 +-
 test/contracts/pass/cheatCodes.sol         |   4 +-
 test/contracts/pass/constantinople.sol     |   4 +-
 test/contracts/pass/constantinople_min.sol |   4 +-
 test/contracts/pass/dsProvePass.sol        |   4 +-
 test/contracts/pass/loops.sol              |   4 +-
 test/contracts/pass/transfer.sol           |   7 +-
 test/contracts/pass/trivial.sol            |   4 +-
 test/contracts/pass/unwind.sol             |   4 +-
 test/test.hs                               |  20 ++--
 22 files changed, 179 insertions(+), 114 deletions(-)
 delete mode 100644 funding.json

diff --git a/cli/cli.hs b/cli/cli.hs
index 6517e8386..0f5e3b5d8 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -77,7 +77,7 @@ data Command w
 
   -- symbolic execution opts
       , root          :: w ::: Maybe String       <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a Foundry or DappTools project (default: Foundry)"
+      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON | Foundry | FoundryStdLib project (default: Foundry)"
       , initialStorage :: w ::: Maybe (InitialStorage) <?> "Starting state for storage: Empty, Abstract (default Abstract)"
       , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"
       , arg           :: w ::: [String]           <?> "Values to encode"
@@ -147,11 +147,11 @@ data Command w
       , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"
       , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"
       , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"
-      , projectType :: w ::: Maybe ProjectType <?> "Is this a Foundry or DappTools project (default: Foundry)"
+      , projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON | Foundry | FoundryStdLib project (default: Foundry)"
       }
-  | Test -- Run DSTest unit tests
+  | Test -- Run Foundry unit tests
       { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a Foundry or DappTools project (default: Foundry)"
+      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a CombinedJSON | Foundry | FoundryStdLib project (default: Foundry)"
       , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"
       , number        :: w ::: Maybe W256               <?> "Block: number"
       , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"
diff --git a/doc/src/exec.md b/doc/src/exec.md
index ea5db639f..93ffb1d69 100644
--- a/doc/src/exec.md
+++ b/doc/src/exec.md
@@ -39,12 +39,10 @@ Available options:
   --block W256             Block state is be fetched from
   --root STRING            Path to project root directory (default: . )
   --project-type PROJECTTYPE
-                           Is this a Foundry or DappTools project (default:
-                           Foundry)
 ```
 
 Minimum required flags: either you must provide `--code` or you must both pass
-`--rpc` and `--address`. 
+`--rpc` and `--address`.
 
 If the execution returns an output, it will be written
 to stdout. Exit code indicates whether the execution was successful or
diff --git a/doc/src/symbolic.md b/doc/src/symbolic.md
index ed9b74463..b6291313e 100644
--- a/doc/src/symbolic.md
+++ b/doc/src/symbolic.md
@@ -42,8 +42,6 @@ Available options:
   --block W256             Block state is be fetched from
   --root STRING            Path to project root directory (default: . )
   --project-type PROJECTTYPE
-                           Is this a Foundry or DappTools project (default:
-                           Foundry)
   --initial-storage INITIALSTORAGE
                            Starting state for storage: Empty, Abstract (default
                            Abstract)
diff --git a/doc/src/test.md b/doc/src/test.md
index 44f1b186e..7c29255c0 100644
--- a/doc/src/test.md
+++ b/doc/src/test.md
@@ -14,8 +14,6 @@ Available options:
   -h,--help                Show this help text
   --root STRING            Path to project root directory (default: . )
   --project-type PROJECTTYPE
-                           Is this a Foundry or DappTools project (default:
-                           Foundry)
   --rpc TEXT               Fetch state from a remote node
   --number W256            Block: number
   --verbose INT            Append call trace: {1} failures {2} all
diff --git a/funding.json b/funding.json
deleted file mode 100644
index fcef50889..000000000
--- a/funding.json
+++ /dev/null
@@ -1,5 +0,0 @@
-{
-  "opRetro": {
-    "projectId": "0x2c97e213fef2bd3f30a71edf6ed48232640368d0083dc0a134a1b59391639bde"
-  }
-}
diff --git a/src/EVM.hs b/src/EVM.hs
index a85426e9b..817665599 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -1904,40 +1904,51 @@ cheatActions = Map.fromList
   , $(envReadMultipleCheat "envBytes32(string,string)" $ AbiBytesType 32) stringToBytes32
   , $(envReadMultipleCheat "envString(string,string)" AbiStringType) stringToByteString
   , $(envReadMultipleCheat "envBytes(bytes,bytes)" AbiBytesDynamicType) stringHexToByteString
-  , action "asserTrue(bool)" $ \sig input ->
+  , action "assertTrue(bool)" $ \sig input ->
       case decodeBuf [AbiBoolType] input of
         CAbi [AbiBool True] -> doStop
         CAbi [AbiBool False] -> frameRevert "assertion failed"
-        _ -> vmError $ BadCheatCode ("assertTrue(bool) parameter decoding failed") sig
-  , action "asserFalse(bool)" $ \sig input ->
+        SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of
+          Lit 1 -> frameRevert "assertion failed"
+          Lit 0 -> doStop
+          ew -> branch (Expr.iszero ew) $ \case
+            True -> frameRevert "assertion failed"
+            False -> doStop
+        k -> vmError $ BadCheatCode ("assertTrue(bool) parameter decoding failed: " <> show k) sig
+  , action "assertFalse(bool)" $ \sig input ->
       case decodeBuf [AbiBoolType] input of
         CAbi [AbiBool False] -> doStop
         CAbi [AbiBool True] -> frameRevert "assertion failed"
-        _ -> vmError $ BadCheatCode ("assertFalse(bool) parameter decoding failed") sig
+        SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of
+          Lit 0 -> frameRevert "assertion failed"
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False -> frameRevert "assertion failed"
+            True -> doStop
+        k -> vmError $ BadCheatCode ("assertFalse(bool) parameter decoding failed: " <> show k) sig
   , action "assertEq(bool,bool)"       $ assertEq AbiBoolType
   , action "assertEq(uint256,uint256)" $ assertEq (AbiUIntType 256)
   , action "assertEq(int256,int256)"   $ assertEq (AbiIntType 256)
   , action "assertEq(address,address)" $ assertEq AbiAddressType
   , action "assertEq(bytes32,bytes32)" $ assertEq (AbiBytesType 32)
   , action "assertEq(string,string)"   $ assertEq AbiStringType
+  , action "assertEq(bytes,bytes)"     $ assertEq AbiBytesDynamicType
   --
-  , action "assertNotEq(bytes,bytes)"     $ assertNotEq (AbiBytesDynamicType)
   , action "assertNotEq(bool,bool)"       $ assertNotEq AbiBoolType
   , action "assertNotEq(uint256,uint256)" $ assertNotEq (AbiUIntType 256)
   , action "assertNotEq(int256,int256)"   $ assertNotEq (AbiIntType 256)
   , action "assertNotEq(address,address)" $ assertNotEq AbiAddressType
   , action "assertNotEq(bytes32,bytes32)" $ assertNotEq (AbiBytesType 32)
   , action "assertNotEq(string,string)"   $ assertNotEq AbiStringType
-  , action "assertNotEq(bytes,bytes)"     $ assertNotEq (AbiBytesDynamicType)
+  , action "assertNotEq(bytes,bytes)"     $ assertNotEq AbiBytesDynamicType
   --
-  , action "assertNotEqMsg(bytes,bytes)"     $ assertNotEqMsg (AbiBytesDynamicType)
   , action "assertNotEqMsg(bool,bool)"       $ assertNotEqMsg AbiBoolType
   , action "assertNotEqMsg(uint256,uint256)" $ assertNotEqMsg (AbiUIntType 256)
   , action "assertNotEqMsg(int256,int256)"   $ assertNotEqMsg (AbiIntType 256)
   , action "assertNotEqMsg(address,address)" $ assertNotEqMsg AbiAddressType
   , action "assertNotEqMsg(bytes32,bytes32)" $ assertNotEqMsg (AbiBytesType 32)
   , action "assertNotEqMsg(string,string)"   $ assertNotEqMsg AbiStringType
-  , action "assertNotEqMsg(bytes,bytes)"     $ assertNotEqMsg (AbiBytesDynamicType)
+  , action "assertNotEqMsg(bytes,bytes)"     $ assertNotEqMsg AbiBytesDynamicType
   --
   , action "assertEq(bool,bool,string)"       $ assertEqMsg AbiBoolType
   , action "assertEq(uint256,uint256,string)" $ assertEqMsg (AbiUIntType 256)
@@ -1945,7 +1956,7 @@ cheatActions = Map.fromList
   , action "assertEq(address,address,string)" $ assertEqMsg AbiAddressType
   , action "assertEq(bytes32,bytes32,string)" $ assertEqMsg (AbiBytesType 32)
   , action "assertEq(string,string,string)"   $ assertEqMsg AbiStringType
-  , action "assertEq(bytes,bytes,string)"     $ assertEqMsg (AbiBytesDynamicType)
+  , action "assertEq(bytes,bytes,string)"     $ assertEqMsg AbiBytesDynamicType
   --
   , action "assertLt(uint256,uint256)" $ assertLt (AbiUIntType 256)
   , action "assertLt(int256,int256)"   $ assertLt (AbiIntType 256)
@@ -1994,10 +2005,10 @@ cheatActions = Map.fromList
     stringToByteString = Right . Char8.pack
     stringHexToByteString :: String -> Either ByteString ByteString
     stringHexToByteString s = either (const $ Left "invalid bytes value") Right $ BS16.decodeBase16Untyped . Char8.pack . strip0x $ s
-    paramDecodeErr abitype name = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
-      ")  parameter decoding failed"
-    paramDecodeMsgErr abitype name = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
-      ",string)  parameter decoding failed"
+    paramDecodeErr abitype name abivals = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
+      ")  parameter decoding failed. Error: " <> show abivals
+    paramDecodeMsgErr abitype name abivals = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
+      ",string)  parameter decoding failed. Error: " <> show abivals
     revertErr a b comp = frameRevert $ "assertion failed: " <>
       BS8.pack (show a) <> " " <> comp <> " " <> BS8.pack (show b)
     revertMsgErr a b str comp = frameRevert $ "assertion failed: "
@@ -2006,42 +2017,92 @@ cheatActions = Map.fromList
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a == b -> doStop
         CAbi [a, b] -> revertErr a b "!="
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertEq") sig)
-    assertEqMsg abitype sig input =
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.eq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "!="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 "!="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertEq" abivals) sig)
+    --  TODO broken: EWords + AbiString don't mix
+    assertEqMsg abitype sig input = do
       case decodeBuf [abitype, abitype, AbiStringType] input of
         CAbi [a, b, _] | a == b -> doStop
         CAbi [a, b, AbiString str] -> revertMsgErr a b str "!="
-        _ -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertEq") sig)
+        MixAbi ([ew1, ew2], AbiString str) -> case (Expr.simplify (Expr.eq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "!="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertMsgErr ew1 ew2 str "!="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertEq" abivals) sig)
+    --  TODO broken: EWords + AbiString don't mix
     assertNotEq abitype sig input = do
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a /= b -> doStop
-        CAbi [a, b] -> revertErr a b "=="
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertNotEq") sig)
+        CAbi [a, b] -> revertErr a b "!="
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.iszero $ Expr.eq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "!="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 "!="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertNotEq" abivals) sig)
     assertNotEqMsg abitype sig input = do
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b, _] | a /= b -> doStop
-        CAbi [a, b, AbiString str] -> revertMsgErr a b str "=="
-        _ -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertNotEq") sig)
-    assertLt abitype sig input =
+        CAbi [a, b, AbiString str] -> revertMsgErr a b str "!="
+        MixAbi ([ew1, ew2], AbiString str) -> case (Expr.simplify (Expr.iszero $ Expr.eq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "!="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertMsgErr ew1 ew2 str "!="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertEq" abivals) sig)
+    assertLt abitype sig input = do
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a < b -> doStop
         CAbi [a, b] -> revertErr a b ">="
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertLt") sig)
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.lt ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 ">="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 ">="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertLt" abivals) sig)
     assertGt abitype sig input =
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a > b -> doStop
         CAbi [a, b] -> revertErr a b "<="
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertGt") sig)
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.gt ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "<="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 "<="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertGt" abivals) sig)
     assertLe abitype sig input =
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a <= b -> doStop
-        CAbi [a, b] -> revertErr a b "<"
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertLe") sig)
+        CAbi [a, b] -> revertErr a b ">"
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.leq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 ">"
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 ">"
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertLe" abivals) sig)
     assertGe abitype sig input =
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a >= b -> doStop
-        CAbi [a, b] -> revertErr a b ">"
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertGe") sig)
+        CAbi [a, b] -> revertErr a b "<"
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.geq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "<"
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 "<"
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertGe" abivals) sig)
 
 
 -- * General call implementation ("delegateCall")
diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs
index 73920f6f4..a7c846716 100644
--- a/src/EVM/ABI.hs
+++ b/src/EVM/ABI.hs
@@ -58,7 +58,7 @@ module EVM.ABI
   , showAlter
   ) where
 
-import EVM.Expr (readWord, isLitWord)
+import EVM.Expr (readWord, readByte, readBytes, isLitWord)
 import EVM.Types
 
 import Control.Applicative ((<|>))
@@ -71,7 +71,7 @@ import Data.ByteString qualified as BS
 import Data.ByteString.Base16 qualified as BS16
 import Data.ByteString.Char8 qualified as Char8
 import Data.ByteString.Lazy qualified as BSLazy
-import Data.Char (isHexDigit)
+import Data.Char (isHexDigit, chr)
 import Data.Data (Data)
 import Data.DoubleWord (Word256, Int256, signedWord)
 import Data.Functor (($>))
@@ -82,7 +82,7 @@ import Data.Text qualified as Text
 import Data.Text.Encoding (encodeUtf8)
 import Data.Vector (Vector, toList)
 import Data.Vector qualified as Vector
-import Data.Word (Word32)
+import Data.Word (Word32, Word8)
 import GHC.Generics (Generic)
 import Test.QuickCheck hiding ((.&.), label)
 import Numeric (showHex)
@@ -498,7 +498,7 @@ bytesP = do
     Right d -> pure $ ByteStringS d
     Left _ -> pfail
 
-data AbiVals = NoVals | CAbi [AbiValue] | SAbi [Expr EWord]
+data AbiVals = NoVals | CAbi [AbiValue] | SAbi [Expr EWord] | MixAbi ([Expr EWord], AbiValue)
   deriving (Show)
 
 decodeBuf :: [AbiType] -> Expr Buf -> AbiVals
@@ -506,27 +506,57 @@ decodeBuf tps (ConcreteBuf b) =
   case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict b) of
     Right ("", _, args) -> CAbi (toList args)
     _ -> NoVals
-decodeBuf tps buf =
-  if any isDynamic tps then NoVals
-  else
-    let
-      vs = decodeStaticArgs 0 (length tps) buf
-      asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord vs)
-    in if not (all isLitWord vs)
-       then SAbi vs
-       else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of
-         Right ("", _, args) -> CAbi (toList args)
-         _ -> NoVals
-
+decodeBuf tpsOrig bufOrig = go tpsOrig bufOrig 0 NoVals
   where
     isDynamic t = abiKind t == Dynamic
+    go :: [AbiType] -> Expr Buf -> Int -> AbiVals -> AbiVals
+    go [] _ _ ret = ret
+    go [AbiStringType] buf off (SAbi acc) = MixAbi (acc, decodeStringArg off buf)
+    go (x:_) _ _ _ | isDynamic x = internalError "Dynamic type must be last in the list"
+    go (_:tps) buf off (SAbi acc) =
+      let
+        v = readWord (Lit (unsafeInto off)) buf
+      in if not (isLitWord v) then go tps buf (off+32) (SAbi (acc++[v]))
+         else internalError "can't mix Symbolic and Concrete"
+    go (t:tps) buf off (CAbi acc) =
+      let v = readWord (Lit (unsafeInto off)) buf
+          asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord [v])
+      in case runGetOrFail (getAbiSeq 1 [t]) (BSLazy.fromStrict asBS) of
+        Right ("", _, args) -> go tps buf (off+32) $ CAbi (acc++(toList args))
+        _ -> NoVals
+    go _ _ _ _ = internalError "decodeBuf: expected concrete buffer"
+-- decodeBuf tps buf =
+--   let
+--     vs = decodeStaticArgs 0 (length tps) buf
+--     asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord vs)
+--   in if not (all isLitWord vs)
+--      then SAbi vs
+--      else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of
+--        Right ("", _, args) -> CAbi (toList args)
+--        _ -> NoVals
+-- decodeBuf _ _ = internalError "decodeBuf: expected concrete buffer"
 
 decodeStaticArgs :: Int -> Int -> Expr Buf -> [Expr EWord]
 decodeStaticArgs offset numArgs b =
   [readWord (Lit . unsafeInto $ i) b | i <- [offset,(offset+32) .. (offset + (numArgs-1)*32)]]
 
--- QuickCheck instances
+decodeStringArg :: Int -> Expr Buf -> AbiValue
+decodeStringArg offs (ConcreteBuf b) =
+  let len = forceLit $ readBytes 4 (Lit . unsafeInto $ offs) (ConcreteBuf b)
+      str = [readByte (Lit . unsafeInto $ (offs + 4 + (unsafeInto i))) (ConcreteBuf b) | i <- [0..len]]
+      bs = (map toLitByte str)
+  in AbiString $ BS.pack bs
+  where
+    toLitByte :: Expr Byte -> Word8
+    toLitByte (LitByte w) = w
+    toLitByte _ = internalError "String part of calldata should be concrete"
+    forceLit :: Expr EWord -> W256
+    forceLit (Lit w) = w
+    forceLit _ = internalError "String part of calldata should be concrete"
+decodeStringArg _ _  = internalError "decodeStringArg: expected concrete buffer"
 
+-- QuickCheck instances
+--
 genAbiValue :: AbiType -> Gen AbiValue
 genAbiValue = \case
    AbiUIntType n -> AbiUInt n <$> genUInt n
diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
index dfdb0e8d2..4eb2af281 100644
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -185,7 +185,7 @@ instance Monoid BuildOutput where
   mempty = BuildOutput mempty mempty
 
 -- | The various project types understood by hevm
-data ProjectType = DappTools | CombinedJSON | Foundry | FoundryStdLib
+data ProjectType = CombinedJSON | Foundry | FoundryStdLib
   deriving (Eq, Show, Read, ParseField)
 
 data SourceCache = SourceCache
@@ -285,13 +285,6 @@ makeSrcMaps = (\case (_, Fe, _) -> Nothing; x -> Just (done x))
 
 -- | Reads all solc output json files found under the provided filepath and returns them merged into a BuildOutput
 readBuildOutput :: App m => FilePath -> ProjectType -> m (Either String BuildOutput)
-readBuildOutput root DappTools = do
-  let outDir = root </> "out"
-  jsons <- liftIO $ findJsonFiles outDir
-  case jsons of
-    [x] -> readSolc DappTools root (outDir </> x)
-    [] -> pure . Left $ "no json files found in: " <> outDir
-    _ -> pure . Left $ "multiple json files found in: " <> outDir
 readBuildOutput root CombinedJSON = do
   let outDir = root </> "out"
   jsons <- liftIO $ findJsonFiles outDir
@@ -413,7 +406,6 @@ force :: String -> Maybe a -> a
 force s = fromMaybe (internalError s)
 
 readJSON :: ProjectType -> Text -> Text -> Maybe (Contracts, Asts, Sources)
-readJSON DappTools _ json = readStdJSON json
 readJSON CombinedJSON _ json = readCombinedJSON json
 readJSON _ contractName json = readFoundryJSON contractName json
 
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index d47d6f6f7..f2ea78430 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -210,9 +210,8 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
             Success _ _ _ store -> PNeg (failed store)
             Failure _ _ (Revert msg) -> case msg of
               ConcreteBuf b -> do
-                if (BS.isPrefixOf (BS.pack "assert failed") b) ||
-                  b == panicMsg 0x01 then PBool True
-                else PBool False
+                if (BS.isPrefixOf (BS.pack "assert failed") b) || b == panicMsg 0x01 then PBool False
+                else PBool True
               b -> b ./= ConcreteBuf (panicMsg 0x01)
             Failure _ _ _ -> PBool True
             Partial _ _ _ -> PBool True
diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs
index 143cca3e4..34e965099 100644
--- a/test/EVM/Test/Utils.hs
+++ b/test/EVM/Test/Utils.hs
@@ -45,7 +45,7 @@ runSolidityTestCustom testFile match timeout maxIter ffiAllowed rpcinfo projectT
 runSolidityTest
   :: (MonadMask m, App m)
   => FilePath -> Text -> m Bool
-runSolidityTest testFile match = runSolidityTestCustom testFile match Nothing Nothing True Nothing FoundryStdLib
+runSolidityTest testFile match = runSolidityTestCustom testFile match Nothing Nothing True Nothing Foundry
 
 testOpts :: SolverGroup -> FilePath -> Maybe BuildOutput -> Text -> Maybe Integer -> Bool -> RpcInfo -> IO (UnitTestOptions RealWorld)
 testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do
@@ -83,19 +83,12 @@ callProcessCwd cmd args cwd = do
       ExitFailure r -> processFailedException "callProcess" cmd args r
 
 compile :: App m => ProjectType -> FilePath -> FilePath -> m (Either String BuildOutput)
-compile DappTools root src = do
-  json <- liftIO $ compileWithDSTest src
-  liftIO $ createDirectory (root </> "out")
-  liftIO $ T.writeFile (root </> "out" </> "dapp.sol.json") json
-  readBuildOutput root DappTools
 compile CombinedJSON _root _src = internalError  "unsupported compile type: CombinedJSON"
 compile foundryType root src = do
   liftIO $ createDirectory (root </> "src")
   liftIO $ writeFile (root </> "src" </> "unit-tests.t.sol") =<< readFile =<< Paths.getDataFileName src
   liftIO $ initLib (root </> "lib" </> "tokens") ("test" </> "contracts" </> "lib" </> "erc20.sol") "erc20.sol"
-  case foundryType of
-    FoundryStdLib -> liftIO $ initStdForgeDir (root </> "lib" </> "forge-std")
-    Foundry -> pure ()
+  liftIO $ initStdForgeDir (root </> "lib" </> "forge-std")
   (res,out,err) <- liftIO $ readProcessWithExitCode "forge" ["build", "--ast", "--root", root] ""
   case res of
     ExitFailure _ -> pure . Left $ "compilation failed: " <> "exit code: " <> show res <> "\n\nstdout:\n" <> out <> "\n\nstderr:\n" <> err
diff --git a/test/contracts/fail/check-prefix.sol b/test/contracts/fail/check-prefix.sol
index 6e41a400b..9c1c90db2 100644
--- a/test/contracts/fail/check-prefix.sol
+++ b/test/contracts/fail/check-prefix.sol
@@ -1,6 +1,6 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
-contract SolidityTest is DSTest {
+contract SolidityTest is Test {
 
     function setUp() public {
     }
diff --git a/test/contracts/fail/trivial.sol b/test/contracts/fail/trivial.sol
index f8e2bb2a4..98736202e 100644
--- a/test/contracts/fail/trivial.sol
+++ b/test/contracts/fail/trivial.sol
@@ -1,7 +1,7 @@
-import {DSTest} from "ds-test/test.sol";
+import {Test} from "forge-std/Test.sol";
 
 // should run and pass
-contract Trivial is DSTest {
+contract Trivial is Test {
     function prove_false() public {
         assertTrue(false);
     }
diff --git a/test/contracts/pass/abstract.sol b/test/contracts/pass/abstract.sol
index cf3114a3b..ee2848e47 100644
--- a/test/contracts/pass/abstract.sol
+++ b/test/contracts/pass/abstract.sol
@@ -1,7 +1,7 @@
-import {DSTest} from "ds-test/test.sol";
+import {Test} from "forge-std/Test.sol";
 
 // should not be run (no code)
-abstract contract MyTest is DSTest {
+abstract contract MyTest is Test {
     function testAbstract() public {
         assertTrue(true);
     }
diff --git a/test/contracts/pass/cheatCodes.sol b/test/contracts/pass/cheatCodes.sol
index a7a5981d2..36c6702f3 100644
--- a/test/contracts/pass/cheatCodes.sol
+++ b/test/contracts/pass/cheatCodes.sol
@@ -1,6 +1,6 @@
 pragma experimental ABIEncoderV2;
 
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
 interface Hevm {
     function warp(uint256) external;
@@ -50,7 +50,7 @@ contract Payable {
 
 contract Empty {}
 
-contract CheatCodes is DSTest {
+contract CheatCodes is Test {
     address store = address(new HasStorage());
     Hevm hevm = Hevm(HEVM_ADDRESS);
 
diff --git a/test/contracts/pass/constantinople.sol b/test/contracts/pass/constantinople.sol
index 4655bd57c..10c5b9c85 100644
--- a/test/contracts/pass/constantinople.sol
+++ b/test/contracts/pass/constantinople.sol
@@ -1,10 +1,10 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
 contract DeadCode{
     function dummy() external returns (uint256) {}
 }
 
-contract ConstantinopleTests is DSTest {
+contract ConstantinopleTests is Test {
     DeadCode notmuch;
     function setUp() public {
       notmuch = new DeadCode();
diff --git a/test/contracts/pass/constantinople_min.sol b/test/contracts/pass/constantinople_min.sol
index 1c5bbc7b1..01e28c6ae 100644
--- a/test/contracts/pass/constantinople_min.sol
+++ b/test/contracts/pass/constantinople_min.sol
@@ -1,10 +1,10 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
 contract DeadCode{
     function dummy() external returns (uint256) {}
 }
 
-contract ConstantinopleTests is DSTest {
+contract ConstantinopleTests is Test {
     DeadCode notmuch;
     function setUp() public {
       notmuch = new DeadCode();
diff --git a/test/contracts/pass/dsProvePass.sol b/test/contracts/pass/dsProvePass.sol
index da9a60df4..f8321a7a0 100644
--- a/test/contracts/pass/dsProvePass.sol
+++ b/test/contracts/pass/dsProvePass.sol
@@ -1,4 +1,4 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 import "tokens/erc20.sol";
 
 contract ConstructorArg {
@@ -8,7 +8,7 @@ contract ConstructorArg {
     }
 }
 
-contract SolidityTest is DSTest {
+contract SolidityTest is Test {
     ERC20 token;
 
     function setUp() public {
diff --git a/test/contracts/pass/loops.sol b/test/contracts/pass/loops.sol
index 62ed91c88..7d8e4e001 100644
--- a/test/contracts/pass/loops.sol
+++ b/test/contracts/pass/loops.sol
@@ -1,6 +1,6 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
-contract Loops is DSTest {
+contract Loops is Test {
 
     function prove_loop(uint n) public {
         uint counter = 0;
diff --git a/test/contracts/pass/transfer.sol b/test/contracts/pass/transfer.sol
index 884ec85d5..b87bbdee2 100644
--- a/test/contracts/pass/transfer.sol
+++ b/test/contracts/pass/transfer.sol
@@ -1,9 +1,9 @@
 pragma solidity ^0.8.19;
 
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 import {ERC20} from "tokens/erc20.sol";
 
-contract SolidityTestFail2 is DSTest {
+contract SolidityTestFail2 is Test {
     ERC20 token;
 
     function setUp() public {
@@ -11,6 +11,7 @@ contract SolidityTestFail2 is DSTest {
     }
 
     function prove_transfer(uint supply, address usr, uint amt) public {
+        // require(supply >= amt, "supply must be greater than or equal to amt");
         token.mint(address(this), supply);
 
         uint prebal = token.balanceOf(usr);
@@ -20,7 +21,7 @@ contract SolidityTestFail2 is DSTest {
         uint expected = usr == address(this)
                         ? 0    // self transfer is a noop
                         : amt; // otherwise `amt` has been transferred to `usr`
-        assert(expected == postbal - prebal);
+        assertTrue(expected == postbal - prebal);
     }
 }
 
diff --git a/test/contracts/pass/trivial.sol b/test/contracts/pass/trivial.sol
index 93feaa643..d18c95820 100644
--- a/test/contracts/pass/trivial.sol
+++ b/test/contracts/pass/trivial.sol
@@ -1,7 +1,7 @@
-import {DSTest} from "ds-test/test.sol";
+import {Test} from "forge-std/Test.sol";
 
 // should run and pass
-contract Trivial is DSTest {
+contract Trivial is Test {
     function prove_true() public {
         assertTrue(true);
     }
diff --git a/test/contracts/pass/unwind.sol b/test/contracts/pass/unwind.sol
index 683daf36f..b528f0cb4 100644
--- a/test/contracts/pass/unwind.sol
+++ b/test/contracts/pass/unwind.sol
@@ -1,7 +1,7 @@
-import {DSTest} from "ds-test/test.sol";
+import {Test} from "forge-std/Test.sol";
 
 // tests unwind support in precompiles
-contract Unwind is DSTest {
+contract Unwind is Test {
     function prove_invalid_sum() public {
         bytes32 x = hex"01";
         try this.callBn256Add(x, x, x, x) returns (bytes32[2] memory) {
diff --git a/test/test.hs b/test/test.hs
index 586b6fdf6..51f065b3f 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -78,7 +78,7 @@ testEnv = Env { config = defaultConfig {
   dumpQueries = False
   , dumpExprs = False
   , dumpEndStates = False
-  , debug = False
+  , debug = True
   , abstRefineArith = False
   , abstRefineMem   = False
   , dumpTrace = False
@@ -1436,8 +1436,8 @@ tests = testGroup "hevm"
     [ test "Trivial-Pass" $ do
         let testFile = "test/contracts/pass/trivial.sol"
         runSolidityTest testFile ".*" >>= assertEqualM "test result" True
-    , test "DappTools" $ do
-        -- quick smokecheck to make sure that we can parse dapptools style build outputs
+    , test "Foundry" $ do
+        -- quick smokecheck to make sure that we can parse ForgeStdLib style build outputs
         let cases =
               [ ("test/contracts/pass/trivial.sol", ".*", True)
               , ("test/contracts/pass/dsProvePass.sol", "proveEasy", True)
@@ -1445,7 +1445,7 @@ tests = testGroup "hevm"
               , ("test/contracts/fail/dsProveFail.sol", "prove_add", False)
               ]
         results <- forM cases $ \(testFile, match, expected) -> do
-          actual <- runSolidityTestCustom testFile match Nothing Nothing False Nothing DappTools
+          actual <- runSolidityTestCustom testFile match Nothing Nothing False Nothing FoundryStdLib
           pure (actual == expected)
         assertBoolM "test result" (and results)
     , test "Trivial-Fail" $ do
@@ -1474,17 +1474,17 @@ tests = testGroup "hevm"
         runSolidityTestCustom testFile "prove_BadVault_usingExploitLaunchPad"  Nothing Nothing True Nothing FoundryStdLib >>= assertEqualM "Must find counterexample" False
     , test "Prove-Tests-Fail" $ do
         let testFile = "test/contracts/fail/dsProveFail.sol"
-        runSolidityTest testFile "prove_trivial" >>= assertEqualM "test result" False
+        -- runSolidityTest testFile "prove_trivial" >>= assertEqualM "test result" False
         runSolidityTest testFile "prove_trivial_dstest" >>= assertEqualM "test result" False
-        runSolidityTest testFile "prove_add" >>= assertEqualM "test result" False
-        runSolidityTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False Nothing FoundryStdLib >>= assertEqualM "test result" False
-        runSolidityTest testFile "prove_multi" >>= assertEqualM "test result" False
+        -- runSolidityTest testFile "prove_add" >>= assertEqualM "test result" False
+        -- runSolidityTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False Nothing FoundryStdLib >>= assertEqualM "test result" False
+        -- runSolidityTest testFile "prove_multi" >>= assertEqualM "test result" False
         -- TODO: implement overflow checking optimizations and enable, currently this runs forever
         --runSolidityTest testFile "prove_distributivity" >>= assertEqualM "test result" False
     , test "Loop-Tests" $ do
         let testFile = "test/contracts/pass/loops.sol"
-        runSolidityTestCustom testFile "prove_loop" Nothing (Just 10) False Nothing Foundry >>= assertEqualM "test result" True
-        runSolidityTestCustom testFile "prove_loop" Nothing (Just 100) False Nothing Foundry >>= assertEqualM "test result" False
+        runSolidityTestCustom testFile "prove_loop" Nothing (Just 10) False Nothing FoundryStdLib  >>= assertEqualM "test result" True
+        runSolidityTestCustom testFile "prove_loop" Nothing (Just 100) False Nothing FoundryStdLib >>= assertEqualM "test result" False
     , test "Cheat-Codes-Pass" $ do
         let testFile = "test/contracts/pass/cheatCodes.sol"
         runSolidityTest testFile ".*" >>= assertEqualM "test result" True

From 92a70489de084ca9c4af1bb1ed9e767e4510c02b Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Thu, 31 Oct 2024 10:07:15 +0100
Subject: [PATCH 04/27] Making progress

---
 src/EVM/ABI.hs | 54 ++++++++++++++++++++++----------------------------
 1 file changed, 24 insertions(+), 30 deletions(-)

diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs
index a7c846716..a51ba1e5b 100644
--- a/src/EVM/ABI.hs
+++ b/src/EVM/ABI.hs
@@ -328,19 +328,22 @@ abiTailSize x =
         _ -> internalError "impossible"
 
 abiHeadSize :: AbiValue -> Int
-abiHeadSize x =
-  case abiKind (abiValueType x) of
+abiHeadSize x = abiSizeType (abiValueType x)
+
+abiSizeType :: AbiType -> Int
+abiSizeType x =
+  case abiKind x of
     Dynamic -> 32
     Static ->
       case x of
-        AbiUInt _ _  -> 32
-        AbiInt  _ _  -> 32
-        AbiBytes n _ -> roundTo32Bytes n
-        AbiAddress _ -> 32
-        AbiBool _    -> 32
-        AbiTuple v   -> sum (abiHeadSize <$> v)
-        AbiArray _ _ xs -> sum (abiHeadSize <$> xs)
-        AbiFunction _ -> 32
+        AbiUIntType _  -> 32
+        AbiIntType  _  -> 32
+        AbiBytesType n -> roundTo32Bytes n
+        AbiAddressType -> 32
+        AbiBoolType    -> 32
+        AbiTupleType n  -> sum (abiSizeType <$> n)
+        AbiArrayType n t -> n*(abiSizeType t)
+        AbiFunctionType -> 32
         _ -> internalError "impossible"
 
 putAbiSeq :: Vector AbiValue -> Put
@@ -512,29 +515,20 @@ decodeBuf tpsOrig bufOrig = go tpsOrig bufOrig 0 NoVals
     go :: [AbiType] -> Expr Buf -> Int -> AbiVals -> AbiVals
     go [] _ _ ret = ret
     go [AbiStringType] buf off (SAbi acc) = MixAbi (acc, decodeStringArg off buf)
+    go [_] _ _ (SAbi _) = internalError "Currently we can only decode string as last dynamic type"
     go (x:_) _ _ _ | isDynamic x = internalError "Dynamic type must be last in the list"
-    go (_:tps) buf off (SAbi acc) =
-      let
-        v = readWord (Lit (unsafeInto off)) buf
-      in if not (isLitWord v) then go tps buf (off+32) (SAbi (acc++[v]))
-         else internalError "can't mix Symbolic and Concrete"
-    go (t:tps) buf off (CAbi acc) =
-      let v = readWord (Lit (unsafeInto off)) buf
+    go (t:ts) buf off (SAbi acc) =
+      let len = abiSizeType t
+          v = readBytes len (Lit (unsafeInto off)) buf
+      in go ts buf (off+len) (SAbi (acc++[v]))
+    go (t:ts) buf off (CAbi acc) | (not . isDynamic) t =
+      let len = abiSizeType t
+          v = readBytes len (Lit (unsafeInto off)) buf
           asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord [v])
       in case runGetOrFail (getAbiSeq 1 [t]) (BSLazy.fromStrict asBS) of
-        Right ("", _, args) -> go tps buf (off+32) $ CAbi (acc++(toList args))
+        Right ("", _, args) -> go ts buf (off+len) $ CAbi (acc++(toList args))
         _ -> NoVals
     go _ _ _ _ = internalError "decodeBuf: expected concrete buffer"
--- decodeBuf tps buf =
---   let
---     vs = decodeStaticArgs 0 (length tps) buf
---     asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord vs)
---   in if not (all isLitWord vs)
---      then SAbi vs
---      else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of
---        Right ("", _, args) -> CAbi (toList args)
---        _ -> NoVals
--- decodeBuf _ _ = internalError "decodeBuf: expected concrete buffer"
 
 decodeStaticArgs :: Int -> Int -> Expr Buf -> [Expr EWord]
 decodeStaticArgs offset numArgs b =
@@ -542,8 +536,8 @@ decodeStaticArgs offset numArgs b =
 
 decodeStringArg :: Int -> Expr Buf -> AbiValue
 decodeStringArg offs (ConcreteBuf b) =
-  let len = forceLit $ readBytes 4 (Lit . unsafeInto $ offs) (ConcreteBuf b)
-      str = [readByte (Lit . unsafeInto $ (offs + 4 + (unsafeInto i))) (ConcreteBuf b) | i <- [0..len]]
+  let len = forceLit $ readBytes 32 (Lit . unsafeInto $ offs) (ConcreteBuf b)
+      str = [readByte (Lit . unsafeInto $ (offs + 32 + (unsafeInto i))) (ConcreteBuf b) | i <- [0..len]]
       bs = (map toLitByte str)
   in AbiString $ BS.pack bs
   where

From 09057387372c74ba2cd2f1de1d876a4b40c0a63a Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Thu, 31 Oct 2024 12:03:48 +0100
Subject: [PATCH 05/27] Moving to forge-std

---
 cli/cli.hs                             |  6 +-
 doc/src/exec.md                        |  2 +-
 doc/src/symbolic.md                    |  2 +-
 doc/src/test.md                        |  2 +-
 src/EVM.hs                             | 64 +++------------------
 src/EVM/ABI.hs                         | 77 +++++++++-----------------
 src/EVM/Solidity.hs                    |  2 +-
 src/EVM/UnitTest.hs                    |  8 +--
 test/EVM/Test/Utils.hs                 |  2 +-
 test/contracts/pass/cheatCodes.sol     |  2 +
 test/contracts/pass/cheatCodesFork.sol |  8 ++-
 test/test.hs                           | 21 ++++---
 12 files changed, 63 insertions(+), 133 deletions(-)

diff --git a/cli/cli.hs b/cli/cli.hs
index 0f5e3b5d8..36d3de578 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -77,7 +77,7 @@ data Command w
 
   -- symbolic execution opts
       , root          :: w ::: Maybe String       <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON | Foundry | FoundryStdLib project (default: Foundry)"
+      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
       , initialStorage :: w ::: Maybe (InitialStorage) <?> "Starting state for storage: Empty, Abstract (default Abstract)"
       , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"
       , arg           :: w ::: [String]           <?> "Values to encode"
@@ -147,11 +147,11 @@ data Command w
       , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"
       , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"
       , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"
-      , projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON | Foundry | FoundryStdLib project (default: Foundry)"
+      , projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
       }
   | Test -- Run Foundry unit tests
       { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a CombinedJSON | Foundry | FoundryStdLib project (default: Foundry)"
+      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
       , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"
       , number        :: w ::: Maybe W256               <?> "Block: number"
       , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"
diff --git a/doc/src/exec.md b/doc/src/exec.md
index 93ffb1d69..f85d27145 100644
--- a/doc/src/exec.md
+++ b/doc/src/exec.md
@@ -38,7 +38,7 @@ Available options:
   --rpc TEXT               Fetch state from a remote node
   --block W256             Block state is be fetched from
   --root STRING            Path to project root directory (default: . )
-  --project-type PROJECTTYPE
+  --project-type PROJECTTYPE Foundry or CombinedJSON project
 ```
 
 Minimum required flags: either you must provide `--code` or you must both pass
diff --git a/doc/src/symbolic.md b/doc/src/symbolic.md
index b6291313e..f88d6e8b6 100644
--- a/doc/src/symbolic.md
+++ b/doc/src/symbolic.md
@@ -41,7 +41,7 @@ Available options:
   --rpc TEXT               Fetch state from a remote node
   --block W256             Block state is be fetched from
   --root STRING            Path to project root directory (default: . )
-  --project-type PROJECTTYPE
+  --project-type PROJECTTYPE Foundry or CombinedJSON project
   --initial-storage INITIALSTORAGE
                            Starting state for storage: Empty, Abstract (default
                            Abstract)
diff --git a/doc/src/test.md b/doc/src/test.md
index 7c29255c0..6359b6eb1 100644
--- a/doc/src/test.md
+++ b/doc/src/test.md
@@ -13,7 +13,7 @@ Usage: hevm test [--root STRING] [--project-type PROJECTTYPE] [--rpc TEXT]
 Available options:
   -h,--help                Show this help text
   --root STRING            Path to project root directory (default: . )
-  --project-type PROJECTTYPE
+  --project-type PROJECTTYPE Foundry or CombinedJSON project
   --rpc TEXT               Fetch state from a remote node
   --number W256            Block: number
   --verbose INT            Append call trace: {1} failures {2} all
diff --git a/src/EVM.hs b/src/EVM.hs
index 817665599..1223b83e8 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -1911,7 +1911,7 @@ cheatActions = Map.fromList
         SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of
           Lit 1 -> frameRevert "assertion failed"
           Lit 0 -> doStop
-          ew -> branch (Expr.iszero ew) $ \case
+          ew -> branch ew $ \case
             True -> frameRevert "assertion failed"
             False -> doStop
         k -> vmError $ BadCheatCode ("assertTrue(bool) parameter decoding failed: " <> show k) sig
@@ -1922,7 +1922,7 @@ cheatActions = Map.fromList
         SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of
           Lit 0 -> frameRevert "assertion failed"
           Lit 1 -> doStop
-          ew -> branch (ew) $ \case
+          ew -> branch ew $ \case
             False -> frameRevert "assertion failed"
             True -> doStop
         k -> vmError $ BadCheatCode ("assertFalse(bool) parameter decoding failed: " <> show k) sig
@@ -1931,32 +1931,12 @@ cheatActions = Map.fromList
   , action "assertEq(int256,int256)"   $ assertEq (AbiIntType 256)
   , action "assertEq(address,address)" $ assertEq AbiAddressType
   , action "assertEq(bytes32,bytes32)" $ assertEq (AbiBytesType 32)
-  , action "assertEq(string,string)"   $ assertEq AbiStringType
-  , action "assertEq(bytes,bytes)"     $ assertEq AbiBytesDynamicType
   --
   , action "assertNotEq(bool,bool)"       $ assertNotEq AbiBoolType
   , action "assertNotEq(uint256,uint256)" $ assertNotEq (AbiUIntType 256)
   , action "assertNotEq(int256,int256)"   $ assertNotEq (AbiIntType 256)
   , action "assertNotEq(address,address)" $ assertNotEq AbiAddressType
   , action "assertNotEq(bytes32,bytes32)" $ assertNotEq (AbiBytesType 32)
-  , action "assertNotEq(string,string)"   $ assertNotEq AbiStringType
-  , action "assertNotEq(bytes,bytes)"     $ assertNotEq AbiBytesDynamicType
-  --
-  , action "assertNotEqMsg(bool,bool)"       $ assertNotEqMsg AbiBoolType
-  , action "assertNotEqMsg(uint256,uint256)" $ assertNotEqMsg (AbiUIntType 256)
-  , action "assertNotEqMsg(int256,int256)"   $ assertNotEqMsg (AbiIntType 256)
-  , action "assertNotEqMsg(address,address)" $ assertNotEqMsg AbiAddressType
-  , action "assertNotEqMsg(bytes32,bytes32)" $ assertNotEqMsg (AbiBytesType 32)
-  , action "assertNotEqMsg(string,string)"   $ assertNotEqMsg AbiStringType
-  , action "assertNotEqMsg(bytes,bytes)"     $ assertNotEqMsg AbiBytesDynamicType
-  --
-  , action "assertEq(bool,bool,string)"       $ assertEqMsg AbiBoolType
-  , action "assertEq(uint256,uint256,string)" $ assertEqMsg (AbiUIntType 256)
-  , action "assertEq(int256,int256,string)"   $ assertEqMsg (AbiIntType 256)
-  , action "assertEq(address,address,string)" $ assertEqMsg AbiAddressType
-  , action "assertEq(bytes32,bytes32,string)" $ assertEqMsg (AbiBytesType 32)
-  , action "assertEq(string,string,string)"   $ assertEqMsg AbiStringType
-  , action "assertEq(bytes,bytes,string)"     $ assertEqMsg AbiBytesDynamicType
   --
   , action "assertLt(uint256,uint256)" $ assertLt (AbiUIntType 256)
   , action "assertLt(int256,int256)"   $ assertLt (AbiIntType 256)
@@ -2007,12 +1987,8 @@ cheatActions = Map.fromList
     stringHexToByteString s = either (const $ Left "invalid bytes value") Right $ BS16.decodeBase16Untyped . Char8.pack . strip0x $ s
     paramDecodeErr abitype name abivals = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
       ")  parameter decoding failed. Error: " <> show abivals
-    paramDecodeMsgErr abitype name abivals = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
-      ",string)  parameter decoding failed. Error: " <> show abivals
     revertErr a b comp = frameRevert $ "assertion failed: " <>
       BS8.pack (show a) <> " " <> comp <> " " <> BS8.pack (show b)
-    revertMsgErr a b str comp = frameRevert $ "assertion failed: "
-      <> str <> ": " <> BS8.pack (show a) <> " " <> comp <> " " <> BS8.pack (show b)
     assertEq abitype sig input = do
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a == b -> doStop
@@ -2020,23 +1996,10 @@ cheatActions = Map.fromList
         SAbi [ew1, ew2] -> case (Expr.simplify (Expr.eq ew1 ew2)) of
           Lit 0 -> revertErr ew1 ew2 "!="
           Lit 1 -> doStop
-          ew -> branch (ew) $ \case
+          ew -> branch ew $ \case
             False ->revertErr ew1 ew2 "!="
             True -> doStop
         abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertEq" abivals) sig)
-    --  TODO broken: EWords + AbiString don't mix
-    assertEqMsg abitype sig input = do
-      case decodeBuf [abitype, abitype, AbiStringType] input of
-        CAbi [a, b, _] | a == b -> doStop
-        CAbi [a, b, AbiString str] -> revertMsgErr a b str "!="
-        MixAbi ([ew1, ew2], AbiString str) -> case (Expr.simplify (Expr.eq ew1 ew2)) of
-          Lit 0 -> revertErr ew1 ew2 "!="
-          Lit 1 -> doStop
-          ew -> branch (ew) $ \case
-            False ->revertMsgErr ew1 ew2 str "!="
-            True -> doStop
-        abivals -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertEq" abivals) sig)
-    --  TODO broken: EWords + AbiString don't mix
     assertNotEq abitype sig input = do
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a /= b -> doStop
@@ -2044,21 +2007,10 @@ cheatActions = Map.fromList
         SAbi [ew1, ew2] -> case (Expr.simplify (Expr.iszero $ Expr.eq ew1 ew2)) of
           Lit 0 -> revertErr ew1 ew2 "!="
           Lit 1 -> doStop
-          ew -> branch (ew) $ \case
+          ew -> branch ew $ \case
             False ->revertErr ew1 ew2 "!="
             True -> doStop
         abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertNotEq" abivals) sig)
-    assertNotEqMsg abitype sig input = do
-      case decodeBuf [abitype, abitype] input of
-        CAbi [a, b, _] | a /= b -> doStop
-        CAbi [a, b, AbiString str] -> revertMsgErr a b str "!="
-        MixAbi ([ew1, ew2], AbiString str) -> case (Expr.simplify (Expr.iszero $ Expr.eq ew1 ew2)) of
-          Lit 0 -> revertErr ew1 ew2 "!="
-          Lit 1 -> doStop
-          ew -> branch (ew) $ \case
-            False ->revertMsgErr ew1 ew2 str "!="
-            True -> doStop
-        abivals -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertEq" abivals) sig)
     assertLt abitype sig input = do
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a < b -> doStop
@@ -2066,7 +2018,7 @@ cheatActions = Map.fromList
         SAbi [ew1, ew2] -> case (Expr.simplify (Expr.lt ew1 ew2)) of
           Lit 0 -> revertErr ew1 ew2 ">="
           Lit 1 -> doStop
-          ew -> branch (ew) $ \case
+          ew -> branch ew $ \case
             False ->revertErr ew1 ew2 ">="
             True -> doStop
         abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertLt" abivals) sig)
@@ -2077,7 +2029,7 @@ cheatActions = Map.fromList
         SAbi [ew1, ew2] -> case (Expr.simplify (Expr.gt ew1 ew2)) of
           Lit 0 -> revertErr ew1 ew2 "<="
           Lit 1 -> doStop
-          ew -> branch (ew) $ \case
+          ew -> branch ew $ \case
             False ->revertErr ew1 ew2 "<="
             True -> doStop
         abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertGt" abivals) sig)
@@ -2088,7 +2040,7 @@ cheatActions = Map.fromList
         SAbi [ew1, ew2] -> case (Expr.simplify (Expr.leq ew1 ew2)) of
           Lit 0 -> revertErr ew1 ew2 ">"
           Lit 1 -> doStop
-          ew -> branch (ew) $ \case
+          ew -> branch ew $ \case
             False ->revertErr ew1 ew2 ">"
             True -> doStop
         abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertLe" abivals) sig)
@@ -2099,7 +2051,7 @@ cheatActions = Map.fromList
         SAbi [ew1, ew2] -> case (Expr.simplify (Expr.geq ew1 ew2)) of
           Lit 0 -> revertErr ew1 ew2 "<"
           Lit 1 -> doStop
-          ew -> branch (ew) $ \case
+          ew -> branch ew $ \case
             False ->revertErr ew1 ew2 "<"
             True -> doStop
         abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertGe" abivals) sig)
diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs
index a51ba1e5b..58d97dcc2 100644
--- a/src/EVM/ABI.hs
+++ b/src/EVM/ABI.hs
@@ -58,7 +58,7 @@ module EVM.ABI
   , showAlter
   ) where
 
-import EVM.Expr (readWord, readByte, readBytes, isLitWord)
+import EVM.Expr (readWord, isLitWord)
 import EVM.Types
 
 import Control.Applicative ((<|>))
@@ -71,7 +71,7 @@ import Data.ByteString qualified as BS
 import Data.ByteString.Base16 qualified as BS16
 import Data.ByteString.Char8 qualified as Char8
 import Data.ByteString.Lazy qualified as BSLazy
-import Data.Char (isHexDigit, chr)
+import Data.Char (isHexDigit)
 import Data.Data (Data)
 import Data.DoubleWord (Word256, Int256, signedWord)
 import Data.Functor (($>))
@@ -82,7 +82,7 @@ import Data.Text qualified as Text
 import Data.Text.Encoding (encodeUtf8)
 import Data.Vector (Vector, toList)
 import Data.Vector qualified as Vector
-import Data.Word (Word32, Word8)
+import Data.Word (Word32)
 import GHC.Generics (Generic)
 import Test.QuickCheck hiding ((.&.), label)
 import Numeric (showHex)
@@ -328,22 +328,19 @@ abiTailSize x =
         _ -> internalError "impossible"
 
 abiHeadSize :: AbiValue -> Int
-abiHeadSize x = abiSizeType (abiValueType x)
-
-abiSizeType :: AbiType -> Int
-abiSizeType x =
-  case abiKind x of
+abiHeadSize x =
+  case abiKind (abiValueType x) of
     Dynamic -> 32
     Static ->
       case x of
-        AbiUIntType _  -> 32
-        AbiIntType  _  -> 32
-        AbiBytesType n -> roundTo32Bytes n
-        AbiAddressType -> 32
-        AbiBoolType    -> 32
-        AbiTupleType n  -> sum (abiSizeType <$> n)
-        AbiArrayType n t -> n*(abiSizeType t)
-        AbiFunctionType -> 32
+        AbiUInt _ _  -> 32
+        AbiInt  _ _  -> 32
+        AbiBytes n _ -> roundTo32Bytes n
+        AbiAddress _ -> 32
+        AbiBool _    -> 32
+        AbiTuple v   -> sum (abiHeadSize <$> v)
+        AbiArray _ _ xs -> sum (abiHeadSize <$> xs)
+        AbiFunction _ -> 32
         _ -> internalError "impossible"
 
 putAbiSeq :: Vector AbiValue -> Put
@@ -501,7 +498,7 @@ bytesP = do
     Right d -> pure $ ByteStringS d
     Left _ -> pfail
 
-data AbiVals = NoVals | CAbi [AbiValue] | SAbi [Expr EWord] | MixAbi ([Expr EWord], AbiValue)
+data AbiVals = NoVals | CAbi [AbiValue] | SAbi [Expr EWord]
   deriving (Show)
 
 decodeBuf :: [AbiType] -> Expr Buf -> AbiVals
@@ -509,48 +506,26 @@ decodeBuf tps (ConcreteBuf b) =
   case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict b) of
     Right ("", _, args) -> CAbi (toList args)
     _ -> NoVals
-decodeBuf tpsOrig bufOrig = go tpsOrig bufOrig 0 NoVals
+decodeBuf tps buf =
+  if any isDynamic tps then NoVals
+  else
+    let
+      vs = decodeStaticArgs 0 (length tps) buf
+      asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord vs)
+    in if not (all isLitWord vs)
+       then SAbi vs
+       else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of
+         Right ("", _, args) -> CAbi (toList args)
+         _ -> NoVals
   where
     isDynamic t = abiKind t == Dynamic
-    go :: [AbiType] -> Expr Buf -> Int -> AbiVals -> AbiVals
-    go [] _ _ ret = ret
-    go [AbiStringType] buf off (SAbi acc) = MixAbi (acc, decodeStringArg off buf)
-    go [_] _ _ (SAbi _) = internalError "Currently we can only decode string as last dynamic type"
-    go (x:_) _ _ _ | isDynamic x = internalError "Dynamic type must be last in the list"
-    go (t:ts) buf off (SAbi acc) =
-      let len = abiSizeType t
-          v = readBytes len (Lit (unsafeInto off)) buf
-      in go ts buf (off+len) (SAbi (acc++[v]))
-    go (t:ts) buf off (CAbi acc) | (not . isDynamic) t =
-      let len = abiSizeType t
-          v = readBytes len (Lit (unsafeInto off)) buf
-          asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord [v])
-      in case runGetOrFail (getAbiSeq 1 [t]) (BSLazy.fromStrict asBS) of
-        Right ("", _, args) -> go ts buf (off+len) $ CAbi (acc++(toList args))
-        _ -> NoVals
-    go _ _ _ _ = internalError "decodeBuf: expected concrete buffer"
 
 decodeStaticArgs :: Int -> Int -> Expr Buf -> [Expr EWord]
 decodeStaticArgs offset numArgs b =
   [readWord (Lit . unsafeInto $ i) b | i <- [offset,(offset+32) .. (offset + (numArgs-1)*32)]]
 
-decodeStringArg :: Int -> Expr Buf -> AbiValue
-decodeStringArg offs (ConcreteBuf b) =
-  let len = forceLit $ readBytes 32 (Lit . unsafeInto $ offs) (ConcreteBuf b)
-      str = [readByte (Lit . unsafeInto $ (offs + 32 + (unsafeInto i))) (ConcreteBuf b) | i <- [0..len]]
-      bs = (map toLitByte str)
-  in AbiString $ BS.pack bs
-  where
-    toLitByte :: Expr Byte -> Word8
-    toLitByte (LitByte w) = w
-    toLitByte _ = internalError "String part of calldata should be concrete"
-    forceLit :: Expr EWord -> W256
-    forceLit (Lit w) = w
-    forceLit _ = internalError "String part of calldata should be concrete"
-decodeStringArg _ _  = internalError "decodeStringArg: expected concrete buffer"
-
 -- QuickCheck instances
---
+
 genAbiValue :: AbiType -> Gen AbiValue
 genAbiValue = \case
    AbiUIntType n -> AbiUInt n <$> genUInt n
diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
index 4eb2af281..ca9bdf973 100644
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -185,7 +185,7 @@ instance Monoid BuildOutput where
   mempty = BuildOutput mempty mempty
 
 -- | The various project types understood by hevm
-data ProjectType = CombinedJSON | Foundry | FoundryStdLib
+data ProjectType = CombinedJSON | Foundry
   deriving (Eq, Show, Read, ParseField)
 
 data SourceCache = SourceCache
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index f2ea78430..c52ea8bc0 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -204,13 +204,13 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
           Nothing -> And (readStorage' (Lit 0) (testContract store).storage) (Lit 2) .== Lit 2
         postcondition = curry $ case shouldFail of
           True -> \(_, post) -> case post of
-                                  Success _ _ _ store -> failed store
-                                  _ -> PBool True
+            Success _ _ _ store -> failed store
+            _ -> PBool True
           False -> \(_, post) -> case post of
             Success _ _ _ store -> PNeg (failed store)
             Failure _ _ (Revert msg) -> case msg of
-              ConcreteBuf b -> do
-                if (BS.isPrefixOf (BS.pack "assert failed") b) || b == panicMsg 0x01 then PBool False
+              ConcreteBuf b ->
+                if (BS.isPrefixOf (selector "Error(string)") b) || b == panicMsg 0x01 then PBool False
                 else PBool True
               b -> b ./= ConcreteBuf (panicMsg 0x01)
             Failure _ _ _ -> PBool True
diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs
index 34e965099..e44b75534 100644
--- a/test/EVM/Test/Utils.hs
+++ b/test/EVM/Test/Utils.hs
@@ -84,7 +84,7 @@ callProcessCwd cmd args cwd = do
 
 compile :: App m => ProjectType -> FilePath -> FilePath -> m (Either String BuildOutput)
 compile CombinedJSON _root _src = internalError  "unsupported compile type: CombinedJSON"
-compile foundryType root src = do
+compile Foundry root src = do
   liftIO $ createDirectory (root </> "src")
   liftIO $ writeFile (root </> "src" </> "unit-tests.t.sol") =<< readFile =<< Paths.getDataFileName src
   liftIO $ initLib (root </> "lib" </> "tokens") ("test" </> "contracts" </> "lib" </> "erc20.sol") "erc20.sol"
diff --git a/test/contracts/pass/cheatCodes.sol b/test/contracts/pass/cheatCodes.sol
index 36c6702f3..ba246f1d7 100644
--- a/test/contracts/pass/cheatCodes.sol
+++ b/test/contracts/pass/cheatCodes.sol
@@ -52,6 +52,8 @@ contract Empty {}
 
 contract CheatCodes is Test {
     address store = address(new HasStorage());
+    address constant HEVM_ADDRESS =
+        address(bytes20(uint160(uint256(keccak256('hevm cheat code')))));
     Hevm hevm = Hevm(HEVM_ADDRESS);
 
     function prove_warp_concrete() public {
diff --git a/test/contracts/pass/cheatCodesFork.sol b/test/contracts/pass/cheatCodesFork.sol
index 2f716070b..f262e83d0 100644
--- a/test/contracts/pass/cheatCodesFork.sol
+++ b/test/contracts/pass/cheatCodesFork.sol
@@ -1,6 +1,6 @@
 pragma experimental ABIEncoderV2;
 
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
 interface Hevm {
     function warp(uint256) external;
@@ -28,7 +28,9 @@ contract TestState {
 }
 
 /// @dev This contract's state should be persistent across forks, because it's the contract calling `selectFork`
-contract CheatCodesForkDeployee is DSTest {
+contract CheatCodesForkDeployee is Test {
+    address constant HEVM_ADDRESS =
+        address(bytes20(uint160(uint256(keccak256('hevm cheat code')))));
     Hevm hevm = Hevm(HEVM_ADDRESS);
     address stateContract;
     uint256 forkId1;
@@ -91,7 +93,7 @@ contract CheatCodesForkDeployee is DSTest {
 /// @dev This contract's state should be persistent across forks, because it's the `msg.sender` when running `deployee_prove_ForkedState`.
 ///  We need this "deployer/deployee" architecture so that `msg.sender` will be concrete when running `deployee_prove_ForkedState`.
 ///  If we were to only use the `CheatCodesForkDeployee` contract, the `msg.sender` would be abstract.
-contract CheatCodesFork is DSTest {
+contract CheatCodesFork is Test {
   CheatCodesForkDeployee testContract = new CheatCodesForkDeployee();
   function prove_ForkedState() external {
     testContract.deployee_prove_ForkedState();
diff --git a/test/test.hs b/test/test.hs
index 51f065b3f..c49d46cfc 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -78,7 +78,7 @@ testEnv = Env { config = defaultConfig {
   dumpQueries = False
   , dumpExprs = False
   , dumpEndStates = False
-  , debug = True
+  , debug = False
   , abstRefineArith = False
   , abstRefineMem   = False
   , dumpTrace = False
@@ -1445,7 +1445,7 @@ tests = testGroup "hevm"
               , ("test/contracts/fail/dsProveFail.sol", "prove_add", False)
               ]
         results <- forM cases $ \(testFile, match, expected) -> do
-          actual <- runSolidityTestCustom testFile match Nothing Nothing False Nothing FoundryStdLib
+          actual <- runSolidityTestCustom testFile match Nothing Nothing False Nothing Foundry
           pure (actual == expected)
         assertBoolM "test result" (and results)
     , test "Trivial-Fail" $ do
@@ -1471,20 +1471,19 @@ tests = testGroup "hevm"
         runSolidityTest testFile "prove_transfer" >>= assertEqualM "should prove transfer" True
     , test "badvault-sym-branch" $ do
         let testFile = "test/contracts/fail/10_BadVault.sol"
-        runSolidityTestCustom testFile "prove_BadVault_usingExploitLaunchPad"  Nothing Nothing True Nothing FoundryStdLib >>= assertEqualM "Must find counterexample" False
+        runSolidityTestCustom testFile "prove_BadVault_usingExploitLaunchPad"  Nothing Nothing True Nothing Foundry >>= assertEqualM "Must find counterexample" False
     , test "Prove-Tests-Fail" $ do
         let testFile = "test/contracts/fail/dsProveFail.sol"
-        -- runSolidityTest testFile "prove_trivial" >>= assertEqualM "test result" False
+        runSolidityTest testFile "prove_trivial" >>= assertEqualM "test result" False
         runSolidityTest testFile "prove_trivial_dstest" >>= assertEqualM "test result" False
-        -- runSolidityTest testFile "prove_add" >>= assertEqualM "test result" False
-        -- runSolidityTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False Nothing FoundryStdLib >>= assertEqualM "test result" False
-        -- runSolidityTest testFile "prove_multi" >>= assertEqualM "test result" False
-        -- TODO: implement overflow checking optimizations and enable, currently this runs forever
-        --runSolidityTest testFile "prove_distributivity" >>= assertEqualM "test result" False
+        runSolidityTest testFile "prove_add" >>= assertEqualM "test result" False
+        runSolidityTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False Nothing Foundry >>= assertEqualM "test result" False
+        runSolidityTest testFile "prove_multi" >>= assertEqualM "test result" False
+        runSolidityTest testFile "prove_distributivity" >>= assertEqualM "test result" False
     , test "Loop-Tests" $ do
         let testFile = "test/contracts/pass/loops.sol"
-        runSolidityTestCustom testFile "prove_loop" Nothing (Just 10) False Nothing FoundryStdLib  >>= assertEqualM "test result" True
-        runSolidityTestCustom testFile "prove_loop" Nothing (Just 100) False Nothing FoundryStdLib >>= assertEqualM "test result" False
+        runSolidityTestCustom testFile "prove_loop" Nothing (Just 10) False Nothing Foundry  >>= assertEqualM "test result" True
+        runSolidityTestCustom testFile "prove_loop" Nothing (Just 100) False Nothing Foundry >>= assertEqualM "test result" False
     , test "Cheat-Codes-Pass" $ do
         let testFile = "test/contracts/pass/cheatCodes.sol"
         runSolidityTest testFile ".*" >>= assertEqualM "test result" True

From da695e3c4346884df8ffadcd239537b2631590b9 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Thu, 31 Oct 2024 14:37:07 +0100
Subject: [PATCH 06/27] Fixing up

---
 src/EVM.hs | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/EVM.hs b/src/EVM.hs
index 1223b83e8..609c6d3c2 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -1995,7 +1995,7 @@ cheatActions = Map.fromList
         CAbi [a, b] -> revertErr a b "!="
         SAbi [ew1, ew2] -> case (Expr.simplify (Expr.eq ew1 ew2)) of
           Lit 0 -> revertErr ew1 ew2 "!="
-          Lit 1 -> doStop
+          Lit _ -> doStop
           ew -> branch ew $ \case
             False ->revertErr ew1 ew2 "!="
             True -> doStop
@@ -2003,13 +2003,13 @@ cheatActions = Map.fromList
     assertNotEq abitype sig input = do
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a /= b -> doStop
-        CAbi [a, b] -> revertErr a b "!="
-        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.iszero $ Expr.eq ew1 ew2)) of
-          Lit 0 -> revertErr ew1 ew2 "!="
-          Lit 1 -> doStop
+        CAbi [a, b] -> revertErr a b "=="
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.eq ew1 ew2)) of
+          Lit 1 -> revertErr ew1 ew2 "=="
+          Lit _ -> doStop
           ew -> branch ew $ \case
-            False ->revertErr ew1 ew2 "!="
-            True -> doStop
+            True ->revertErr ew1 ew2 "=="
+            False -> doStop
         abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertNotEq" abivals) sig)
     assertLt abitype sig input = do
       case decodeBuf [abitype, abitype] input of
@@ -2017,7 +2017,7 @@ cheatActions = Map.fromList
         CAbi [a, b] -> revertErr a b ">="
         SAbi [ew1, ew2] -> case (Expr.simplify (Expr.lt ew1 ew2)) of
           Lit 0 -> revertErr ew1 ew2 ">="
-          Lit 1 -> doStop
+          Lit _ -> doStop
           ew -> branch ew $ \case
             False ->revertErr ew1 ew2 ">="
             True -> doStop
@@ -2028,7 +2028,7 @@ cheatActions = Map.fromList
         CAbi [a, b] -> revertErr a b "<="
         SAbi [ew1, ew2] -> case (Expr.simplify (Expr.gt ew1 ew2)) of
           Lit 0 -> revertErr ew1 ew2 "<="
-          Lit 1 -> doStop
+          Lit _ -> doStop
           ew -> branch ew $ \case
             False ->revertErr ew1 ew2 "<="
             True -> doStop
@@ -2039,7 +2039,7 @@ cheatActions = Map.fromList
         CAbi [a, b] -> revertErr a b ">"
         SAbi [ew1, ew2] -> case (Expr.simplify (Expr.leq ew1 ew2)) of
           Lit 0 -> revertErr ew1 ew2 ">"
-          Lit 1 -> doStop
+          Lit _ -> doStop
           ew -> branch ew $ \case
             False ->revertErr ew1 ew2 ">"
             True -> doStop

From fed5b2a57f044d14d02f63ac0cbb67970b812039 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Thu, 31 Oct 2024 17:26:12 +0100
Subject: [PATCH 07/27] Better error reporting

---
 src/EVM.hs          | 4 ++--
 src/EVM/UnitTest.hs | 8 +++++++-
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/EVM.hs b/src/EVM.hs
index 609c6d3c2..5fb013ae0 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -2381,10 +2381,10 @@ finishFrame how = do
               push 0
 
             -- Case 3: Error during a call?
-            FrameErrored _ -> do
+            FrameErrored e -> do
               revertContracts
               revertSubstate
-              assign (#state % #returndata) mempty
+              assign (#state % #returndata) (ConcreteBuf (BS8.pack $ show e))
               push 0
         -- Or were we creating?
         CreationContext _ _ reversion subState' -> do
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index c52ea8bc0..f66b1400b 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -21,7 +21,7 @@ import EVM.Transaction (initTx)
 import EVM.Stepper (Stepper)
 import EVM.Stepper qualified as Stepper
 
-import Control.Monad (void, when, forM, forM_)
+import Control.Monad (void, when, forM, forM_, unless)
 import Control.Monad.ST (RealWorld, ST, stToIO)
 import Control.Monad.State.Strict (execState, get, put, liftIO)
 import Optics.Core
@@ -227,6 +227,12 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     -- check postconditions against vm
     (e, results) <- verify solvers (makeVeriOpts opts) (symbolify vm') (Just postcondition)
     let allReverts = not . (any Expr.isSuccess) . flattenExpr $ e
+    let fails = filter (Expr.isFailure) $ flattenExpr e
+    unless (null fails) $ liftIO $ do
+      putStrLn $ "      \x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the test " <> Text.unpack testName <> " due to: ";
+      forM_ (fails) $ \case
+        (Failure _ _ err) -> putStrLn $ "      -> " <> show err
+        _ -> internalError "unexpected failure"
     when (any isUnknown results || any isError results) $ liftIO $ do
       putStrLn $ "      \x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the test " <> Text.unpack testName <> " due to: ";
       forM_ (groupIssues (filter isError results)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str

From b00abc9a9a7f34f6a1b9637beb9864c935210116 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Fri, 8 Nov 2024 05:56:46 +0100
Subject: [PATCH 08/27] Update to bubble hevm errors back up

---
 src/EVM.hs               | 30 ++++++++++++++++--------------
 src/EVM/Types.hs         | 40 ++++++++++++++++++++++++++++++++++++++++
 src/EVM/UnitTest.hs      | 13 +++++++++----
 test/EVM/Test/Tracing.hs | 21 +--------------------
 4 files changed, 66 insertions(+), 38 deletions(-)

diff --git a/src/EVM.hs b/src/EVM.hs
index 5fb013ae0..f5888c609 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -1696,7 +1696,7 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
     Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi])
     Just (unsafeInto -> abi') ->
       case Map.lookup abi' cheatActions of
-        Nothing -> vmError (BadCheatCode "cannot understand cheatcode, maybe cheatcode not supported?" abi')
+        Nothing -> vmError (BadCheatCode "Cannot understand cheatcode. " abi')
         Just action -> action input
 
 type CheatAction t s = Expr Buf -> EVM t s ()
@@ -1931,12 +1931,14 @@ cheatActions = Map.fromList
   , action "assertEq(int256,int256)"   $ assertEq (AbiIntType 256)
   , action "assertEq(address,address)" $ assertEq AbiAddressType
   , action "assertEq(bytes32,bytes32)" $ assertEq (AbiBytesType 32)
+  , action "assertEq(string,string)"   $ assertEq (AbiStringType)
   --
   , action "assertNotEq(bool,bool)"       $ assertNotEq AbiBoolType
   , action "assertNotEq(uint256,uint256)" $ assertNotEq (AbiUIntType 256)
   , action "assertNotEq(int256,int256)"   $ assertNotEq (AbiIntType 256)
   , action "assertNotEq(address,address)" $ assertNotEq AbiAddressType
   , action "assertNotEq(bytes32,bytes32)" $ assertNotEq (AbiBytesType 32)
+  , action "assertNotEq(string,string)"   $ assertNotEq (AbiStringType)
   --
   , action "assertLt(uint256,uint256)" $ assertLt (AbiUIntType 256)
   , action "assertLt(int256,int256)"   $ assertLt (AbiIntType 256)
@@ -2326,14 +2328,10 @@ finishFrame how = do
     nextFrame : remainingFrames -> do
 
       -- Insert a debug trace.
-      insertTrace $
-        case how of
-          FrameErrored e ->
-            ErrorTrace e
-          FrameReverted e ->
-            ErrorTrace (Revert e)
-          FrameReturned output ->
-            ReturnTrace output nextFrame.context
+      insertTrace $ case how of
+        FrameReturned output -> ReturnTrace output nextFrame.context
+        FrameReverted e -> ErrorTrace (Revert e)
+        FrameErrored e -> ErrorTrace e
       -- Pop to the previous level of the debug trace stack.
       popTrace
 
@@ -2384,8 +2382,10 @@ finishFrame how = do
             FrameErrored e -> do
               revertContracts
               revertSubstate
-              assign (#state % #returndata) (ConcreteBuf (BS8.pack $ show e))
-              push 0
+              if (isInterpretFailure e) then finishFrame (FrameErrored e)
+              else do
+                assign (#state % #returndata) mempty
+                push 0
         -- Or were we creating?
         CreationContext _ _ reversion subState' -> do
           creator <- use (#state % #contract)
@@ -2428,11 +2428,13 @@ finishFrame how = do
               push 0
 
             -- Case 6: Error during a creation?
-            FrameErrored _ -> do
+            FrameErrored e -> do
               revertContracts
               revertSubstate
-              assign (#state % #returndata) mempty
-              push 0
+              if (isInterpretFailure e) then finishFrame (FrameErrored e)
+              else do
+                assign (#state % #returndata) mempty
+                push 0
 
 
 -- * Memory helpers
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index d03f2ee94..3b67fc557 100644
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -550,6 +550,46 @@ data EvmError
   | NonexistentFork Int
   deriving (Show, Eq, Ord)
 
+isInterpretFailure :: EvmError -> Bool
+isInterpretFailure = \case
+  (BadCheatCode {}) -> True
+  (NonexistentFork {}) -> True
+  PrecompileFailure -> True
+  StateChangeWhileStatic -> True
+  UnrecognizedOpcode _ -> True
+  _ -> False
+
+isInterpretFailEnd :: Expr a -> Bool
+isInterpretFailEnd = \case
+  (Failure _ _ k) -> isInterpretFailure k
+  _ -> False
+
+evmErrToString :: EvmError -> String
+evmErrToString = \case
+  -- NOTE: error text made to closely match go-ethereum's errors.go file
+  OutOfGas {}             -> "Out of gas"
+  -- TODO "contract creation code storage out of gas" not handled
+  CallDepthLimitReached   -> "Max call depth exceeded"
+  BalanceTooLow {}        -> "Insufficient balance for transfer"
+  -- TODO "contract address collision" not handled
+  Revert {}               -> "Execution reverted"
+  -- TODO "max initcode size exceeded" not handled
+  MaxCodeSizeExceeded {}  -> "Max code size exceeded"
+  BadJumpDestination      -> "Invalid jump destination"
+  StateChangeWhileStatic  -> "Attempting to modify state while in static context"
+  ReturnDataOutOfBounds   -> "Return data out of bounds"
+  IllegalOverflow         -> "Gas uint64 overflow"
+  UnrecognizedOpcode op   -> "Invalid opcode: 0x" <> showHex op ""
+  NonceOverflow           -> "Nonce uint64 overflow"
+  StackUnderrun           -> "Stack underflow"
+  StackLimitExceeded      -> "Stack limit reached"
+  InvalidMemoryAccess     -> "Write protection"
+  (BadCheatCode err fun)  -> err <> " Cheatcode function selector: " <> show fun
+  NonexistentFork fork    -> "Nonexistent fork: " <> show fork
+  PrecompileFailure       -> "Precompile failure"
+  err                     -> "hevm error: " <> show err
+
+
 -- | Sometimes we can only partially execute a given program
 data PartialExec
   = UnexpectedSymbolicArg { pc :: Int, opcode :: String, msg  :: String, args  :: [SomeExpr] }
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index f66b1400b..8b4b7afeb 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -227,11 +227,16 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     -- check postconditions against vm
     (e, results) <- verify solvers (makeVeriOpts opts) (symbolify vm') (Just postcondition)
     let allReverts = not . (any Expr.isSuccess) . flattenExpr $ e
-    let fails = filter (Expr.isFailure) $ flattenExpr e
-    unless (null fails) $ liftIO $ do
+    let interpFails = filter (isInterpretFailEnd) $ flattenExpr e
+
+    conf <- readConfig
+    when conf.debug $ liftIO $ forM_ (filter Expr.isFailure (flattenExpr e)) $ \case
+      (Failure _ _ a) ->  putStrLn $ "   -> debug of func: " <> Text.unpack testName <> " Failure at the end of expr: " <> show a;
+      _ -> internalError "cannot be, filtered for failure"
+    unless (null interpFails) $ liftIO $ do
       putStrLn $ "      \x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the test " <> Text.unpack testName <> " due to: ";
-      forM_ (fails) $ \case
-        (Failure _ _ err) -> putStrLn $ "      -> " <> show err
+      forM_ (interpFails) $ \case
+        (Failure _ _ f) -> putStrLn $ "      -> " <> evmErrToString f
         _ -> internalError "unexpected failure"
     when (any isUnknown results || any isError results) $ liftIO $ do
       putStrLn $ "      \x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the test " <> Text.unpack testName <> " due to: ";
diff --git a/test/EVM/Test/Tracing.hs b/test/EVM/Test/Tracing.hs
index a791c4d7b..7db641265 100644
--- a/test/EVM/Test/Tracing.hs
+++ b/test/EVM/Test/Tracing.hs
@@ -513,26 +513,7 @@ vmtrace vm =
              }
   where
     readoutError :: Maybe (VMResult t s) -> Maybe String
-    readoutError (Just (VMFailure e)) = case e of
-      -- NOTE: error text made to closely match go-ethereum's errors.go file
-      OutOfGas {}             -> Just "out of gas"
-      -- TODO "contract creation code storage out of gas" not handled
-      CallDepthLimitReached   -> Just "max call depth exceeded"
-      BalanceTooLow {}        -> Just "insufficient balance for transfer"
-      -- TODO "contract address collision" not handled
-      Revert {}           -> Just "execution reverted"
-      -- TODO "max initcode size exceeded" not handled
-      MaxCodeSizeExceeded {}  -> Just "max code size exceeded"
-      BadJumpDestination  -> Just "invalid jump destination"
-      StateChangeWhileStatic  -> Just "write protection"
-      ReturnDataOutOfBounds   -> Just "return data out of bounds"
-      IllegalOverflow     -> Just "gas uint64 overflow"
-      UnrecognizedOpcode op   -> Just $ "invalid opcode: 0x" <> showHex op ""
-      NonceOverflow       -> Just "nonce uint64 overflow"
-      StackUnderrun       -> Just "stack underflow"
-      StackLimitExceeded  -> Just "stack limit reached"
-      InvalidMemoryAccess -> Just "write protection"
-      err                     -> Just $ "HEVM error: " <> show err
+    readoutError (Just (VMFailure e)) = Just $ evmErrToString e
     readoutError _ = Nothing
 
 vmres :: VM Concrete s -> VMTraceResult

From 0f7eb145a7f28f7727ee3f7d50b4949f079a0d4f Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 25 Nov 2024 14:39:54 +0100
Subject: [PATCH 09/27] Temporarily ignoring test while we figure out what to
 do with it

---
 test/test.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/test.hs b/test/test.hs
index c49d46cfc..8aa2ef3cd 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1768,7 +1768,7 @@ tests = testGroup "hevm"
           check coinbase (SymAddr "coinbase")
           check a (SymAddr "freshSymAddr1")
           check arg (SymAddr "arg1")
-    , test "vm.load fails for a potentially aliased address" $ do
+    , ignoreTest $ test "vm.load fails for a potentially aliased address" $ do
         Just c <- solcRuntime "C"
           [i|
             interface Vm {
@@ -1784,7 +1784,7 @@ tests = testGroup "hevm"
         (_, [Cex _]) <- withDefaultSolver $ \s ->
           verifyContract s c Nothing [] defaultVeriOpts Nothing (Just $ checkBadCheatCode "load(address,bytes32)")
         pure ()
-    , test "vm.store fails for a potentially aliased address" $ do
+    , ignoreTest $ test "vm.store fails for a potentially aliased address" $ do
         Just c <- solcRuntime "C"
           [i|
             interface Vm {

From ad1e91a3012059385d54e0c0fc495ad8460d12df Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 25 Nov 2024 15:06:28 +0100
Subject: [PATCH 10/27] Fixing interpretFailure

---
 src/EVM/Types.hs | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index 3b67fc557..9a2a9e59f 100644
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -554,9 +554,6 @@ isInterpretFailure :: EvmError -> Bool
 isInterpretFailure = \case
   (BadCheatCode {}) -> True
   (NonexistentFork {}) -> True
-  PrecompileFailure -> True
-  StateChangeWhileStatic -> True
-  UnrecognizedOpcode _ -> True
   _ -> False
 
 isInterpretFailEnd :: Expr a -> Bool

From e155fb7465f061df07bfbcde83a4ebc8b4d095cf Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 25 Nov 2024 15:37:57 +0100
Subject: [PATCH 11/27] Ripping out interpretFailure idea

As per discussion with @dxo
---
 src/EVM.hs          | 12 ++++--------
 src/EVM/Types.hs    | 11 -----------
 src/EVM/UnitTest.hs |  6 ------
 3 files changed, 4 insertions(+), 25 deletions(-)

diff --git a/src/EVM.hs b/src/EVM.hs
index f5888c609..5a8589990 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -2382,10 +2382,8 @@ finishFrame how = do
             FrameErrored e -> do
               revertContracts
               revertSubstate
-              if (isInterpretFailure e) then finishFrame (FrameErrored e)
-              else do
-                assign (#state % #returndata) mempty
-                push 0
+              assign (#state % #returndata) mempty
+              push 0
         -- Or were we creating?
         CreationContext _ _ reversion subState' -> do
           creator <- use (#state % #contract)
@@ -2431,10 +2429,8 @@ finishFrame how = do
             FrameErrored e -> do
               revertContracts
               revertSubstate
-              if (isInterpretFailure e) then finishFrame (FrameErrored e)
-              else do
-                assign (#state % #returndata) mempty
-                push 0
+              assign (#state % #returndata) mempty
+              push 0
 
 
 -- * Memory helpers
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index 9a2a9e59f..2eaf32788 100644
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -550,17 +550,6 @@ data EvmError
   | NonexistentFork Int
   deriving (Show, Eq, Ord)
 
-isInterpretFailure :: EvmError -> Bool
-isInterpretFailure = \case
-  (BadCheatCode {}) -> True
-  (NonexistentFork {}) -> True
-  _ -> False
-
-isInterpretFailEnd :: Expr a -> Bool
-isInterpretFailEnd = \case
-  (Failure _ _ k) -> isInterpretFailure k
-  _ -> False
-
 evmErrToString :: EvmError -> String
 evmErrToString = \case
   -- NOTE: error text made to closely match go-ethereum's errors.go file
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index 8b4b7afeb..9edfa6611 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -227,17 +227,11 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     -- check postconditions against vm
     (e, results) <- verify solvers (makeVeriOpts opts) (symbolify vm') (Just postcondition)
     let allReverts = not . (any Expr.isSuccess) . flattenExpr $ e
-    let interpFails = filter (isInterpretFailEnd) $ flattenExpr e
 
     conf <- readConfig
     when conf.debug $ liftIO $ forM_ (filter Expr.isFailure (flattenExpr e)) $ \case
       (Failure _ _ a) ->  putStrLn $ "   -> debug of func: " <> Text.unpack testName <> " Failure at the end of expr: " <> show a;
       _ -> internalError "cannot be, filtered for failure"
-    unless (null interpFails) $ liftIO $ do
-      putStrLn $ "      \x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the test " <> Text.unpack testName <> " due to: ";
-      forM_ (interpFails) $ \case
-        (Failure _ _ f) -> putStrLn $ "      -> " <> evmErrToString f
-        _ -> internalError "unexpected failure"
     when (any isUnknown results || any isError results) $ liftIO $ do
       putStrLn $ "      \x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the test " <> Text.unpack testName <> " due to: ";
       forM_ (groupIssues (filter isError results)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str

From c8bd6b7cc0cf3680fbd6005fc02a20a0fbfa0552 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 25 Nov 2024 17:50:21 +0100
Subject: [PATCH 12/27] More debug printing, enabling tests

---
 src/EVM/SymExec.hs | 2 ++
 test/test.hs       | 4 ++--
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 72ba513e8..ba128965f 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -627,8 +627,10 @@ verify solvers opts preState maybepost = do
         -- Dispatch the remaining branches to the solver to check for violations
         results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
           res <- checkSat solvers query
+          when conf.debug $ putStrLn $ "   SMT result: " <> show res
           pure (res, leaf)
         let cexs = filter (\(res, _) -> not . isUnsat $ res) results
+        when conf.debug $ putStrLn $ "   Found " <> show (length cexs) <> " potential counterexample(s) in call " <> call
         pure $ if Prelude.null cexs then (expr, [Qed ()]) else (expr, fmap toVRes cexs)
   where
     getCallPrefix :: Expr Buf -> String
diff --git a/test/test.hs b/test/test.hs
index 8aa2ef3cd..c49d46cfc 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1768,7 +1768,7 @@ tests = testGroup "hevm"
           check coinbase (SymAddr "coinbase")
           check a (SymAddr "freshSymAddr1")
           check arg (SymAddr "arg1")
-    , ignoreTest $ test "vm.load fails for a potentially aliased address" $ do
+    , test "vm.load fails for a potentially aliased address" $ do
         Just c <- solcRuntime "C"
           [i|
             interface Vm {
@@ -1784,7 +1784,7 @@ tests = testGroup "hevm"
         (_, [Cex _]) <- withDefaultSolver $ \s ->
           verifyContract s c Nothing [] defaultVeriOpts Nothing (Just $ checkBadCheatCode "load(address,bytes32)")
         pure ()
-    , ignoreTest $ test "vm.store fails for a potentially aliased address" $ do
+    , test "vm.store fails for a potentially aliased address" $ do
         Just c <- solcRuntime "C"
           [i|
             interface Vm {

From ed0894851455335c5e0c9fced491a4f7b6361141 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 25 Nov 2024 19:00:55 +0100
Subject: [PATCH 13/27] Adding notes

---
 test/test.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test/test.hs b/test/test.hs
index c49d46cfc..7c24c8a74 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1781,6 +1781,7 @@ tests = testGroup "hevm"
               }
             }
           |]
+        -- NOTE: we have a postcondition here, not just a regular verification
         (_, [Cex _]) <- withDefaultSolver $ \s ->
           verifyContract s c Nothing [] defaultVeriOpts Nothing (Just $ checkBadCheatCode "load(address,bytes32)")
         pure ()
@@ -1797,6 +1798,7 @@ tests = testGroup "hevm"
               }
             }
           |]
+        -- NOTE: we have a postcondition here, not just a regular verification
         (_, [Cex _]) <- withDefaultSolver $ \s ->
           verifyContract s c Nothing [] defaultVeriOpts Nothing (Just $ checkBadCheatCode "store(address,bytes32,bytes32)")
         pure ()

From 3797dc0dbba3b26591e73847e54d99b147bd29bc Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Tue, 26 Nov 2024 12:39:11 +0100
Subject: [PATCH 14/27] Much easier to review and more compact thanks to @d-xo

---
 src/EVM.hs | 77 ++++++++++--------------------------------------------
 1 file changed, 14 insertions(+), 63 deletions(-)

diff --git a/src/EVM.hs b/src/EVM.hs
index 5a8589990..7e76698d4 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -1991,72 +1991,23 @@ cheatActions = Map.fromList
       ")  parameter decoding failed. Error: " <> show abivals
     revertErr a b comp = frameRevert $ "assertion failed: " <>
       BS8.pack (show a) <> " " <> comp <> " " <> BS8.pack (show b)
-    assertEq abitype sig input = do
+    genAssert comp exprComp invComp name abitype sig input = do
       case decodeBuf [abitype, abitype] input of
-        CAbi [a, b] | a == b -> doStop
-        CAbi [a, b] -> revertErr a b "!="
-        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.eq ew1 ew2)) of
-          Lit 0 -> revertErr ew1 ew2 "!="
-          Lit _ -> doStop
-          ew -> branch ew $ \case
-            False ->revertErr ew1 ew2 "!="
-            True -> doStop
-        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertEq" abivals) sig)
-    assertNotEq abitype sig input = do
-      case decodeBuf [abitype, abitype] input of
-        CAbi [a, b] | a /= b -> doStop
-        CAbi [a, b] -> revertErr a b "=="
-        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.eq ew1 ew2)) of
-          Lit 1 -> revertErr ew1 ew2 "=="
-          Lit _ -> doStop
+        CAbi [a, b] | a `comp` b -> doStop
+        CAbi [a, b] -> revertErr a b invComp
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.iszero $ exprComp ew1 ew2)) of
+          Lit 0 -> doStop
+          Lit _ -> revertErr ew1 ew2 invComp
           ew -> branch ew $ \case
-            True ->revertErr ew1 ew2 "=="
             False -> doStop
-        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertNotEq" abivals) sig)
-    assertLt abitype sig input = do
-      case decodeBuf [abitype, abitype] input of
-        CAbi [a, b] | a < b -> doStop
-        CAbi [a, b] -> revertErr a b ">="
-        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.lt ew1 ew2)) of
-          Lit 0 -> revertErr ew1 ew2 ">="
-          Lit _ -> doStop
-          ew -> branch ew $ \case
-            False ->revertErr ew1 ew2 ">="
-            True -> doStop
-        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertLt" abivals) sig)
-    assertGt abitype sig input =
-      case decodeBuf [abitype, abitype] input of
-        CAbi [a, b] | a > b -> doStop
-        CAbi [a, b] -> revertErr a b "<="
-        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.gt ew1 ew2)) of
-          Lit 0 -> revertErr ew1 ew2 "<="
-          Lit _ -> doStop
-          ew -> branch ew $ \case
-            False ->revertErr ew1 ew2 "<="
-            True -> doStop
-        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertGt" abivals) sig)
-    assertLe abitype sig input =
-      case decodeBuf [abitype, abitype] input of
-        CAbi [a, b] | a <= b -> doStop
-        CAbi [a, b] -> revertErr a b ">"
-        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.leq ew1 ew2)) of
-          Lit 0 -> revertErr ew1 ew2 ">"
-          Lit _ -> doStop
-          ew -> branch ew $ \case
-            False ->revertErr ew1 ew2 ">"
-            True -> doStop
-        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertLe" abivals) sig)
-    assertGe abitype sig input =
-      case decodeBuf [abitype, abitype] input of
-        CAbi [a, b] | a >= b -> doStop
-        CAbi [a, b] -> revertErr a b "<"
-        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.geq ew1 ew2)) of
-          Lit 0 -> revertErr ew1 ew2 "<"
-          Lit 1 -> doStop
-          ew -> branch ew $ \case
-            False ->revertErr ew1 ew2 "<"
-            True -> doStop
-        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertGe" abivals) sig)
+            True -> revertErr ew1 ew2 invComp
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype name abivals) sig)
+    assertEq = genAssert (==) Expr.eq "!=" "assertEq"
+    assertNotEq = genAssert (/=) (\a b -> Expr.iszero $ Expr.eq a b) "==" "assertNotEq"
+    assertLt = genAssert (<) Expr.lt ">=" "assertLt"
+    assertGt = genAssert (>) Expr.gt "<=" "assertGt"
+    assertLe = genAssert (<=) Expr.leq ">" "assertLe"
+    assertGe = genAssert (>=) Expr.geq "<" "assertGe"
 
 
 -- * General call implementation ("delegateCall")

From 65a8103e002ace21efa4a6ae16697b65025c6a37 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Tue, 26 Nov 2024 14:24:26 +0100
Subject: [PATCH 15/27] One more test on mem pairs

---
 test/test.hs | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/test/test.hs b/test/test.hs
index 7c24c8a74..2037897de 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1562,6 +1562,28 @@ tests = testGroup "hevm"
         (e, [Qed _]) <- withDefaultSolver $
           \s -> checkAssert s defaultPanicCodes c sig [] opts
         assertBoolM "The expression is not partial" $ Expr.containsNode isPartial e
+    , test "mem-tuple" $ do
+        Just c <- solcRuntime "C"
+          [i|
+            contract C {
+              struct Pair {
+                uint x;
+                uint y;
+              }
+              function prove_tuple_pass(Pair memory p) public pure {
+                uint256 f = p.x;
+                uint256 g = p.y;
+                unchecked {
+                  p.x+=p.y;
+                  assert(p.x == (f + g));
+                }
+              }
+            }
+          |]
+        let opts = defaultVeriOpts
+        let sig = Nothing
+        (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] opts
+        putStrLnM "Qed, memory tuple is good"
     , test "symbolic-loops-not-reached" $ do
         Just c <- solcRuntime "C"
             [i|

From a6124bb6d8086271f9caf4a0d1d8ff1b1828dc87 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Tue, 26 Nov 2024 17:08:11 +0100
Subject: [PATCH 16/27] Fixing up call signature generation

---
 src/EVM/Dapp.hs     |  2 +-
 src/EVM/Solvers.hs  |  4 ++--
 src/EVM/SymExec.hs  |  6 +++---
 src/EVM/UnitTest.hs | 28 ++++++++++++----------------
 test/test.hs        |  2 +-
 5 files changed, 19 insertions(+), 23 deletions(-)

diff --git a/src/EVM/Dapp.hs b/src/EVM/Dapp.hs
index c9ea02024..c6e1e4e9f 100644
--- a/src/EVM/Dapp.hs
+++ b/src/EVM/Dapp.hs
@@ -100,7 +100,7 @@ mkSig method
   | "check" `isPrefixOf` testname = Just (Sig testname argtypes)
   | otherwise = Nothing
   where
-    testname = method.methodSignature
+    testname = method.name
     argtypes = snd <$> method.inputs
 
 findUnitTests :: Text -> ([SolcContract] -> [(Text, [Sig])])
diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index 3a8a90e06..25055c013 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -129,10 +129,10 @@ withSolvers solver count threads timeout cont = do
         when (conf.dumpQueries) $ writeSMT2File smt2 fileCounter "abstracted"
         if (isJust fuzzResult)
           then do
-            when (conf.debug) $ putStrLn $ "Cex found via fuzzing:" <> (show fuzzResult)
+            when (conf.debug) $ putStrLn $ "   Cex found via fuzzing:" <> (show fuzzResult)
             writeChan r (Sat $ fromJust fuzzResult)
           else if not conf.onlyCexFuzz then do
-            when (conf.debug) $ putStrLn "Fuzzing failed to find a Cex"
+            when (conf.debug) $ putStrLn "   Fuzzing failed to find a Cex"
             -- reset solver and send all lines of provided script
             out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty ps)
             case out of
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index ba128965f..16c312255 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -596,16 +596,16 @@ verify
 verify solvers opts preState maybepost = do
   conf <- readConfig
   let call = mconcat ["prefix 0x", getCallPrefix preState.state.calldata]
-  when conf.debug $ liftIO $ putStrLn $ "Exploring call " <> call
+  when conf.debug $ liftIO $ putStrLn $ "   Exploring call " <> call
 
   exprInter <- interpret (Fetch.oracle solvers opts.rpcInfo) opts.maxIter opts.askSmtIters opts.loopHeuristic preState runExpr
   when conf.dumpExprs $ liftIO $ T.writeFile "unsimplified.expr" (formatExpr exprInter)
   liftIO $ do
-    when conf.debug $ putStrLn "Simplifying expression"
+    when conf.debug $ putStrLn "   Simplifying expression"
     let expr = if opts.simp then (Expr.simplify exprInter) else exprInter
     when conf.dumpExprs $ T.writeFile "simplified.expr" (formatExpr expr)
 
-    when conf.debug $ putStrLn $ "Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
+    when conf.debug $ putStrLn $ "   Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
 
     let flattened = flattenExpr expr
     when (any isPartial flattened) $ do
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index 9edfa6611..ab7d944a6 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -114,15 +114,19 @@ makeVeriOpts opts =
 -- | Top level CLI endpoint for hevm test
 unitTest :: App m => UnitTestOptions RealWorld -> Contracts -> m Bool
 unitTest opts (Contracts cs) = do
-  let unitTests = findUnitTests opts.match $ Map.elems cs
-  results <- concatMapM (runUnitTestContract opts cs) unitTests
+  let unitTestContrs = findUnitTests opts.match $ Map.elems cs
+  conf <- readConfig
+  when conf.debug $ liftIO $ do
+    putStrLn $ "Found " ++ show (length unitTestContrs) ++ " unit test contract(s) to test:"
+    let x = map (\(a,b) -> "  --> " <> a <> "  ---  functions: " <> (Text.pack $ show b)) unitTestContrs
+    putStrLn $ unlines $ map Text.unpack x
+  results <- concatMapM (runUnitTestContract opts cs) unitTestContrs
   pure $ and results
 
 -- | Assuming a constructor is loaded, this stepper will run the constructor
 -- to create the test contract, give it an initial balance, and run `setUp()'.
 initializeUnitTest :: UnitTestOptions s -> SolcContract -> Stepper Concrete s ()
 initializeUnitTest opts theContract = do
-
   let addr = opts.testParams.address
 
   Stepper.evm $ do
@@ -161,7 +165,7 @@ runUnitTestContract
   opts@(UnitTestOptions {..}) contractMap (name, testSigs) = do
 
   -- Print a header
-  liftIO $ putStrLn $ "\nChecking " ++ show (length testSigs) ++ " function(s) in contract " ++ unpack name
+  liftIO $ putStrLn $ "Checking " ++ show (length testSigs) ++ " function(s) in contract " ++ unpack name
 
   -- Look for the wanted contract by name from the Solidity info
   case Map.lookup name contractMap of
@@ -190,9 +194,10 @@ runUnitTestContract
 -- | Define the thread spawner for symbolic tests
 symRun :: App m => UnitTestOptions RealWorld -> VM Concrete RealWorld -> Sig -> m Bool
 symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
-    liftIO $ putStrLn $ "\x1b[96m[RUNNING]\x1b[0m " <> Text.unpack testName
-    let cd = symCalldata testName types [] (AbstractBuf "txdata")
-        shouldFail = "proveFail" `isPrefixOf` testName
+    let callSig = testName <> "(" <> (Text.intercalate "," (map abiTypeSolidity types)) <> ")"
+    liftIO $ putStrLn $ "\x1b[96m[RUNNING]\x1b[0m " <> Text.unpack callSig
+    let cd = symCalldata callSig types [] (AbstractBuf "txdata")
+        shouldFail = "proveFail" `isPrefixOf` callSig
         testContract store = fromMaybe (internalError "test contract not found in state") (Map.lookup vm.state.contract store)
 
     -- define postcondition depending on `shouldFail`
@@ -286,15 +291,6 @@ symFailure UnitTestOptions {..} testName cd types failures' =
       dappContext TraceContext { contracts, labels } =
         DappContext { info = dapp, contracts, labels }
 
-execSymTest :: UnitTestOptions RealWorld -> ABIMethod -> (Expr Buf, [Prop]) -> Stepper Symbolic RealWorld (Expr End)
-execSymTest UnitTestOptions{ .. } method cd = do
-  -- Set up the call to the test method
-  Stepper.evm $ do
-    makeTxCall testParams cd
-    pushTrace (EntryTrace method)
-  -- Try running the test method
-  runExpr
-
 indentLines :: Int -> Text -> Text
 indentLines n s =
   let p = Text.replicate n " "
diff --git a/test/test.hs b/test/test.hs
index 2037897de..7ab2b7280 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1581,7 +1581,7 @@ tests = testGroup "hevm"
             }
           |]
         let opts = defaultVeriOpts
-        let sig = Nothing
+        let sig = Just $ Sig "prove_tuple_pass((uint256,uint256))" [AbiTupleType (V.fromList [AbiUIntType 256, AbiUIntType 256])]
         (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] opts
         putStrLnM "Qed, memory tuple is good"
     , test "symbolic-loops-not-reached" $ do

From a6151dd67718ed9d268df3298b9b7d3b90070baf Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Tue, 26 Nov 2024 17:34:52 +0100
Subject: [PATCH 17/27] Removing warnings

---
 src/EVM.hs          | 4 ++--
 src/EVM/UnitTest.hs | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/EVM.hs b/src/EVM.hs
index 7e76698d4..519c7ab78 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -2330,7 +2330,7 @@ finishFrame how = do
               push 0
 
             -- Case 3: Error during a call?
-            FrameErrored e -> do
+            FrameErrored _ -> do
               revertContracts
               revertSubstate
               assign (#state % #returndata) mempty
@@ -2377,7 +2377,7 @@ finishFrame how = do
               push 0
 
             -- Case 6: Error during a creation?
-            FrameErrored e -> do
+            FrameErrored _ -> do
               revertContracts
               revertSubstate
               assign (#state % #returndata) mempty
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index ab7d944a6..0c39609fb 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -15,13 +15,13 @@ import EVM.FeeSchedule (feeSchedule)
 import EVM.Fetch qualified as Fetch
 import EVM.Format
 import EVM.Solidity
-import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr, isUnknown, isError, groupIssues)
+import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr, isUnknown, isError, groupIssues)
 import EVM.Types
 import EVM.Transaction (initTx)
 import EVM.Stepper (Stepper)
 import EVM.Stepper qualified as Stepper
 
-import Control.Monad (void, when, forM, forM_, unless)
+import Control.Monad (void, when, forM, forM_)
 import Control.Monad.ST (RealWorld, ST, stToIO)
 import Control.Monad.State.Strict (execState, get, put, liftIO)
 import Optics.Core

From 753a8f05f3c64efd54bfb8674361aa269ac44a35 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Tue, 26 Nov 2024 17:41:28 +0100
Subject: [PATCH 18/27] Fixing up rpc tests

---
 test/contracts/pass/rpc.sol | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/test/contracts/pass/rpc.sol b/test/contracts/pass/rpc.sol
index e6fd51da9..2dfc54fec 100644
--- a/test/contracts/pass/rpc.sol
+++ b/test/contracts/pass/rpc.sol
@@ -1,7 +1,9 @@
-import {DSTest} from "ds-test/test.sol";
+pragma solidity ^0.8.19;
+
+import {Test} from "forge-std/Test.sol";
 import {ERC20} from "tokens/erc20.sol";
 
-contract C is DSTest {
+contract C is Test {
     // BAL: https://etherscan.io/address/0xba100000625a3754423978a60c9317c58a424e3D#code
     ERC20 bal = ERC20(0xba100000625a3754423978a60c9317c58a424e3D);
 

From 66dbc56632fba8dbd3ccefbc55fdbc6bb31c4a9a Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Tue, 26 Nov 2024 18:03:04 +0100
Subject: [PATCH 19/27] Updating changelog

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 38e30de38..52b006317 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -43,6 +43,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   partial results instead of erroring out
 - Fix interpreter's MCOPY handling so that it doesn't error out on symbolic arguments
 - More desciptive errors in case of a cheatcode issue
+- Better and more pretty debug messages
 
 ## Fixed
 - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing
@@ -65,6 +66,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Respect --smt-timeout in equivalence checking
 - Fixed the handling of returndata with an abstract size during transaction finalization
 - Error handling for user-facing cli commands is much improved
+- Fixed call signature generation for test cases
 
 ## [0.53.0] - 2024-02-23
 

From a01a83e8fa08d7da0cfdd51e7a7b2dbbfc605367 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Tue, 26 Nov 2024 18:08:28 +0100
Subject: [PATCH 20/27] Removing DSTest, replacing with forge-std

---
 doc/src/getting-started.md |  8 ++---
 doc/src/when-to-use.md     |  8 ++---
 src/EVM/UnitTest.hs        |  2 +-
 test/EVM/Test/Utils.hs     | 65 --------------------------------------
 4 files changed, 9 insertions(+), 74 deletions(-)

diff --git a/doc/src/getting-started.md b/doc/src/getting-started.md
index 25bbbcb7e..f057b72f9 100644
--- a/doc/src/getting-started.md
+++ b/doc/src/getting-started.md
@@ -28,9 +28,9 @@ be larger than or equal to 100. Let's see the contract and its associated check:
 
 ```solidity
 pragma solidity ^0.8.19;
-import "ds-test/test.sol";
+import "foge-std/Test.sol";
 
-contract MyContract is DSTest {
+contract MyContract is Test {
   mapping (address => uint) balances;
   function prove_add_value(address recv, uint amt) public {
     require(balances[recv] < 100);
@@ -65,9 +65,9 @@ $ chmod +x ./hevm-x86_64-linux
 $ forge init .
 $ cat <<EOF > src/contract.sol
 pragma solidity ^0.8.19;
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
-contract MyContract is DSTest {
+contract MyContract is Test {
   mapping (address => uint) balances;
   function prove_add_value(address recv, uint amt) public {
     require(balances[recv] < 100);
diff --git a/doc/src/when-to-use.md b/doc/src/when-to-use.md
index e40b4dc08..4b98a9dfb 100644
--- a/doc/src/when-to-use.md
+++ b/doc/src/when-to-use.md
@@ -26,9 +26,9 @@ bytecode, postconditions need to be explicit. Let's see an example:
 ```solidity
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.19;
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
-contract MyContract is DSTest {
+contract MyContract is Test {
   uint balance;
   function test_overflow(uint amt) public {
     unchecked {
@@ -50,9 +50,9 @@ towards them. Let's see a simple one:
 ```solidity
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.19;
-import "ds-test/test.sol";
+import "foge-std/Test.sol";
 
-contract MyContract is DSTest {
+contract MyContract is Test {
   uint balance;
   function prove_multiply(uint amt, uint amt2) public {
     require(amt != 1);
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index 0c39609fb..408bb399e 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -275,7 +275,7 @@ symFailure UnitTestOptions {..} testName cd types failures' =
       showRes = \case
         Success _ _ _ _ -> if "proveFail" `isPrefixOf` testName
                            then "Successful execution"
-                           else "Failed: DSTest Assertion Violation"
+                           else "Failed: Test Assertion Violation"
         res ->
           let ?context = dappContext (traceContext res)
           in Text.pack $ prettyvmresult res
diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs
index e44b75534..e83762d67 100644
--- a/test/EVM/Test/Utils.hs
+++ b/test/EVM/Test/Utils.hs
@@ -1,11 +1,6 @@
-{-# LANGUAGE QuasiQuotes #-}
-
 module EVM.Test.Utils where
 
-import Data.String.Here
 import Data.Text (Text)
-import Data.Text qualified as T
-import Data.Text.IO qualified as T
 import GHC.IO.Exception (IOErrorType(..))
 import GHC.Natural
 import Paths_hevm qualified as Paths
@@ -14,7 +9,6 @@ import System.FilePath ((</>))
 import System.IO.Temp
 import System.Process
 import System.Exit
-import System.IO
 import System.IO.Error (mkIOError)
 
 import EVM.Dapp (dappInfo, emptyDapp)
@@ -110,62 +104,3 @@ compile Foundry root src = do
       callProcessCwd "git" ["add", "."] tld
       callProcessCwd "git" ["commit", "-m", "", "--allow-empty-message", "--no-gpg-sign"] tld
       pure ()
-
--- We don't want to depend on dapptools here, so we cheat and just call solc with the same options that dapp itself uses
-compileWithDSTest :: FilePath -> IO Text
-compileWithDSTest src =
-  withSystemTempFile "input.json" $ \file handle -> do
-    hClose handle
-    dsTest <- readFile =<< Paths.getDataFileName ("test" </> "contracts" </> "lib" </> "test.sol")
-    erc20 <- readFile =<< Paths.getDataFileName ("test" </> "contracts" </> "lib" </> "erc20.sol")
-    testFilePath <- Paths.getDataFileName src
-    testFile <- readFile testFilePath
-    T.writeFile file
-      [i|
-      {
-        "language": "Solidity",
-        "sources": {
-          "ds-test/test.sol": {
-            "content": ${dsTest}
-          },
-          "tokens/erc20.sol": {
-            "content": ${erc20}
-          },
-          "unit-tests.sol": {
-            "content": ${testFile}
-          }
-        },
-        "settings": {
-          "metadata": {
-            "useLiteralContent": true
-          },
-          "outputSelection": {
-            "*": {
-              "*": [
-                "metadata",
-                "evm.bytecode",
-                "evm.deployedBytecode",
-                "abi",
-                "storageLayout",
-                "evm.bytecode.sourceMap",
-                "evm.bytecode.linkReferences",
-                "evm.bytecode.generatedSources",
-                "evm.deployedBytecode.sourceMap",
-                "evm.deployedBytecode.linkReferences",
-                "evm.deployedBytecode.generatedSources"
-              ],
-              "": [
-                "ast"
-              ]
-            }
-          }
-        }
-      }
-      |]
-    x <- T.pack <$>
-      readProcess
-        "solc"
-        ["--allow-paths", file, "--standard-json", file]
-        ""
-    return x
-

From dab414a308fff45d6beaaa3f0b46279fe24c0557 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Tue, 26 Nov 2024 18:09:30 +0100
Subject: [PATCH 21/27] Update changelog

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 52b006317..a7b81155e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,7 +10,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - More complete and precise array/mapping slot rewrite, along with a copySlice improvement
 - Use a let expression in copySlice to decrease expression size
 - The `--debug` flag now dumps the internal expressions as well
-- hevm now uses the std-forge library's way of detecting failures, i.e. through
+- hevm now uses the forge-std library's way of detecting failures, i.e. through
   reverting with a specific error code
 
 ## Added

From a4c6a9577c7d797234037df9f801e359d98738ad Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 27 Nov 2024 12:39:55 +0100
Subject: [PATCH 22/27] Cleanup of changelog

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a7b81155e..52b006317 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,7 +10,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - More complete and precise array/mapping slot rewrite, along with a copySlice improvement
 - Use a let expression in copySlice to decrease expression size
 - The `--debug` flag now dumps the internal expressions as well
-- hevm now uses the forge-std library's way of detecting failures, i.e. through
+- hevm now uses the std-forge library's way of detecting failures, i.e. through
   reverting with a specific error code
 
 ## Added

From 1d5549654c640f3df86781eb7fa65de4417b6cb9 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 27 Nov 2024 12:40:04 +0100
Subject: [PATCH 23/27] This is not needed anymore, it's not encoded there

---
 src/EVM/UnitTest.hs | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index 408bb399e..e6309150f 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -9,7 +9,6 @@ import EVM.Solvers
 import EVM.Dapp
 import EVM.Effects
 import EVM.Exec
-import EVM.Expr (readStorage')
 import EVM.Expr qualified as Expr
 import EVM.FeeSchedule (feeSchedule)
 import EVM.Fetch qualified as Fetch
@@ -198,21 +197,14 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     liftIO $ putStrLn $ "\x1b[96m[RUNNING]\x1b[0m " <> Text.unpack callSig
     let cd = symCalldata callSig types [] (AbstractBuf "txdata")
         shouldFail = "proveFail" `isPrefixOf` callSig
-        testContract store = fromMaybe (internalError "test contract not found in state") (Map.lookup vm.state.contract store)
 
     -- define postcondition depending on `shouldFail`
-    -- We directly encode the failure conditions from failed() in ds-test since this is easier to encode than a call into failed()
-    -- we need to read from slot 0 in the test contract and mask it with 0x10 to get the value of _failed
-    -- we don't need to do this when reading the failed from the cheatcode address since we don't do any packing there
-    let failed store = case Map.lookup cheatCode store of
-          Just cheatContract -> readStorage' (Lit 0x6661696c65640000000000000000000000000000000000000000000000000000) cheatContract.storage .== Lit 1
-          Nothing -> And (readStorage' (Lit 0) (testContract store).storage) (Lit 2) .== Lit 2
-        postcondition = curry $ case shouldFail of
+    let postcondition = curry $ case shouldFail of
           True -> \(_, post) -> case post of
-            Success _ _ _ store -> failed store
+            Success {} -> PBool False
             _ -> PBool True
           False -> \(_, post) -> case post of
-            Success _ _ _ store -> PNeg (failed store)
+            Success _ _ _ _ -> PBool True
             Failure _ _ (Revert msg) -> case msg of
               ConcreteBuf b ->
                 if (BS.isPrefixOf (selector "Error(string)") b) || b == panicMsg 0x01 then PBool False

From 4de8f7012d8f5a9931ee2ce3120f3dd0af5e747a Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 27 Nov 2024 12:40:59 +0100
Subject: [PATCH 24/27] Removing space

---
 src/EVM.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/EVM.hs b/src/EVM.hs
index 519c7ab78..a8d941d69 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -1696,7 +1696,7 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
     Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi])
     Just (unsafeInto -> abi') ->
       case Map.lookup abi' cheatActions of
-        Nothing -> vmError (BadCheatCode "Cannot understand cheatcode. " abi')
+        Nothing -> vmError (BadCheatCode "Cannot understand cheatcode." abi')
         Just action -> action input
 
 type CheatAction t s = Expr Buf -> EVM t s ()

From 88ccb4144b778dacf9991d023f69f75de3541b03 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 2 Dec 2024 11:34:57 +0100
Subject: [PATCH 25/27] Allowing backwards compatibility with ds-test

---
 cli/cli.hs             | 11 +++++++----
 src/EVM/Solidity.hs    |  2 +-
 src/EVM/UnitTest.hs    | 11 ++++++++---
 test/EVM/Test/Utils.hs |  3 ++-
 4 files changed, 18 insertions(+), 9 deletions(-)

diff --git a/cli/cli.hs b/cli/cli.hs
index 36d3de578..fcb10535b 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -77,7 +77,7 @@ data Command w
 
   -- symbolic execution opts
       , root          :: w ::: Maybe String       <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
+      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON, Foundry, or DSTest project (default: Foundry)"
       , initialStorage :: w ::: Maybe (InitialStorage) <?> "Starting state for storage: Empty, Abstract (default Abstract)"
       , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"
       , arg           :: w ::: [String]           <?> "Values to encode"
@@ -147,11 +147,11 @@ data Command w
       , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"
       , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"
       , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"
-      , projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
+      , projectType :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON, Foundry, or DSTest project (default: Foundry)"
       }
   | Test -- Run Foundry unit tests
       { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
+      , projectType :: w ::: Maybe ProjectType          <?> "Is this a CombinedJSON, Foundry, or DSTest project (default: Foundry)"
       , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"
       , number        :: w ::: Maybe W256               <?> "Block: number"
       , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"
@@ -308,7 +308,9 @@ getSrcInfo cmd = do
     else pure emptyDapp
 
 getProjectType :: Command Options.Unwrapped -> ProjectType
-getProjectType cmd = fromMaybe Foundry cmd.projectType
+getProjectType cmd =
+  let pt = fromMaybe Foundry cmd.projectType
+  in if elem pt [Foundry, DSTest] then Foundry else CombinedJSON
 
 getRoot :: Command Options.Unwrapped -> IO FilePath
 getRoot cmd = maybe getCurrentDirectory makeAbsolute (cmd.root)
@@ -674,6 +676,7 @@ unitTestOptions cmd solvers buildOutput = do
     , testParams = params
     , dapp = srcInfo
     , ffiAllowed = cmd.ffi
+    , checkFailBit = cmd.projectType == Just DSTest
     }
 parseInitialStorage :: InitialStorage -> BaseState
 parseInitialStorage Empty = EmptyBase
diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
index ca9bdf973..42715b66b 100644
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -185,7 +185,7 @@ instance Monoid BuildOutput where
   mempty = BuildOutput mempty mempty
 
 -- | The various project types understood by hevm
-data ProjectType = CombinedJSON | Foundry
+data ProjectType = CombinedJSON | Foundry | DSTest
   deriving (Eq, Show, Read, ParseField)
 
 data SourceCache = SourceCache
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index e6309150f..707c15ade 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -56,6 +56,7 @@ data UnitTestOptions s = UnitTestOptions
   , dapp        :: DappInfo
   , testParams  :: TestVMParams
   , ffiAllowed  :: Bool
+  , checkFailBit:: Bool
   }
 
 data TestVMParams = TestVMParams
@@ -199,12 +200,16 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
         shouldFail = "proveFail" `isPrefixOf` callSig
 
     -- define postcondition depending on `shouldFail`
-    let postcondition = curry $ case shouldFail of
+    let testContract store = fromMaybe (internalError "test contract not found in state") (Map.lookup vm.state.contract store)
+        failed store = case Map.lookup cheatCode store of
+          Just cheatContract -> Expr.readStorage' (Lit 0x6661696c65640000000000000000000000000000000000000000000000000000) cheatContract.storage .== Lit 1
+          Nothing -> And (Expr.readStorage' (Lit 0) (testContract store).storage) (Lit 2) .== Lit 2
+        postcondition = curry $ case shouldFail of
           True -> \(_, post) -> case post of
-            Success {} -> PBool False
+            Success _ _ _ store -> if opts.checkFailBit then failed store else PBool False
             _ -> PBool True
           False -> \(_, post) -> case post of
-            Success _ _ _ _ -> PBool True
+            Success _ _ _ store -> if opts.checkFailBit then PNeg (failed store) else PBool True
             Failure _ _ (Revert msg) -> case msg of
               ConcreteBuf b ->
                 if (BS.isPrefixOf (selector "Error(string)") b) || b == panicMsg 0x01 then PBool False
diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs
index e83762d67..f23f701a8 100644
--- a/test/EVM/Test/Utils.hs
+++ b/test/EVM/Test/Utils.hs
@@ -59,6 +59,7 @@ testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do
     , testParams = params
     , dapp = srcInfo
     , ffiAllowed = allowFFI
+    , checkFailBit = False
     }
 
 processFailedException :: String -> String -> [String] -> Int -> IO a
@@ -78,7 +79,7 @@ callProcessCwd cmd args cwd = do
 
 compile :: App m => ProjectType -> FilePath -> FilePath -> m (Either String BuildOutput)
 compile CombinedJSON _root _src = internalError  "unsupported compile type: CombinedJSON"
-compile Foundry root src = do
+compile _ root src = do
   liftIO $ createDirectory (root </> "src")
   liftIO $ writeFile (root </> "src" </> "unit-tests.t.sol") =<< readFile =<< Paths.getDataFileName src
   liftIO $ initLib (root </> "lib" </> "tokens") ("test" </> "contracts" </> "lib" </> "erc20.sol") "erc20.sol"

From 0d0749713df58a46f58e2d0ede60d06079a88535 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 2 Dec 2024 15:53:53 +0100
Subject: [PATCH 26/27] Separate option for DSTest-type assertion type

As requested by @d-xo
---
 cli/cli.hs          | 18 +++++++++++-------
 src/EVM/Solidity.hs |  2 +-
 2 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/cli/cli.hs b/cli/cli.hs
index fcb10535b..3015cecb2 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -47,6 +47,9 @@ import EVM.Types qualified
 import EVM.UnitTest
 import EVM.Effects
 
+data AssertionType = DSTest | Forge
+  deriving (Eq, Show, Read, ParseField)
+
 -- This record defines the program's command-line options
 -- automatically via the `optparse-generic` package.
 data Command w
@@ -77,7 +80,8 @@ data Command w
 
   -- symbolic execution opts
       , root          :: w ::: Maybe String       <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON, Foundry, or DSTest project (default: Foundry)"
+      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
+      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"
       , initialStorage :: w ::: Maybe (InitialStorage) <?> "Starting state for storage: Empty, Abstract (default Abstract)"
       , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"
       , arg           :: w ::: [String]           <?> "Values to encode"
@@ -147,11 +151,13 @@ data Command w
       , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"
       , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"
       , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"
-      , projectType :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON, Foundry, or DSTest project (default: Foundry)"
+      , projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
+      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"
       }
   | Test -- Run Foundry unit tests
       { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"
-      , projectType :: w ::: Maybe ProjectType          <?> "Is this a CombinedJSON, Foundry, or DSTest project (default: Foundry)"
+      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
+      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"
       , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"
       , number        :: w ::: Maybe W256               <?> "Block: number"
       , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"
@@ -308,9 +314,7 @@ getSrcInfo cmd = do
     else pure emptyDapp
 
 getProjectType :: Command Options.Unwrapped -> ProjectType
-getProjectType cmd =
-  let pt = fromMaybe Foundry cmd.projectType
-  in if elem pt [Foundry, DSTest] then Foundry else CombinedJSON
+getProjectType cmd = fromMaybe Foundry cmd.projectType
 
 getRoot :: Command Options.Unwrapped -> IO FilePath
 getRoot cmd = maybe getCurrentDirectory makeAbsolute (cmd.root)
@@ -676,7 +680,7 @@ unitTestOptions cmd solvers buildOutput = do
     , testParams = params
     , dapp = srcInfo
     , ffiAllowed = cmd.ffi
-    , checkFailBit = cmd.projectType == Just DSTest
+    , checkFailBit = (fromMaybe Forge cmd.assertionType) == DSTest
     }
 parseInitialStorage :: InitialStorage -> BaseState
 parseInitialStorage Empty = EmptyBase
diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
index 42715b66b..ca9bdf973 100644
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -185,7 +185,7 @@ instance Monoid BuildOutput where
   mempty = BuildOutput mempty mempty
 
 -- | The various project types understood by hevm
-data ProjectType = CombinedJSON | Foundry | DSTest
+data ProjectType = CombinedJSON | Foundry
   deriving (Eq, Show, Read, ParseField)
 
 data SourceCache = SourceCache

From f7219b9e052e9677579ce3de3a9291144013fdfd Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 2 Dec 2024 15:59:07 +0100
Subject: [PATCH 27/27] Updating changelog

---
 CHANGELOG.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 24db3ae53..06cc26dc7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,8 +10,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - More complete and precise array/mapping slot rewrite, along with a copySlice improvement
 - Use a let expression in copySlice to decrease expression size
 - The `--debug` flag now dumps the internal expressions as well
-- hevm now uses the std-forge library's way of detecting failures, i.e. through
-  reverting with a specific error code
+- hevm now uses the forge-std library's way of detecting failures, i.e. through
+  reverting with a specific error code unless --assertion-type DSTest is passed
 
 ## Added
 - More POr and PAnd rules