hevm 0.50.0 → 0.50.1

raw patch · 28 files changed

+1063/−1817 lines, 28 filesdep +filemanipdep ~QuickCheckdep ~aesondep ~basesetup-changedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: filemanip

Dependency ranges changed: QuickCheck, aeson, base, base16-bytestring, binary, brick, bytestring, containers, cryptonite, data-dword, directory, filepath, here, lens, lens-aeson, mtl, parsec, process, regex-tdfa, temporary, text, time, vector, vty, witherable

API changes (from Hackage documentation)

Files

• CHANGELOG.md +24/−2
• Setup.hs +0/−2
• hevm-cli/hevm-cli.hs +25/−215
• hevm.cabal +39/−35
• run-blockchain-tests +0/−150
• run-consensus-tests +0/−110
• src/EVM.hs +88/−66
• src/EVM/ABI.hs +10/−8
• src/EVM/Dapp.hs +7/−3
• src/EVM/Dev.hs +2/−3
• src/EVM/Exec.hs +1/−1
• src/EVM/Expr.hs +5/−2
• src/EVM/Facts.hs +2/−3
• src/EVM/Fetch.hs +3/−4
• src/EVM/Flatten.hs +0/−466
• src/EVM/Format.hs +23/−15
• src/EVM/SMT.hs +3/−4
• src/EVM/Solidity.hs +20/−16
• src/EVM/SymExec.hs +19/−30
• src/EVM/TTY.hs +215/−231
• src/EVM/Transaction.hs +6/−6
• src/EVM/Traversals.hs +3/−28
• src/EVM/Types.hs +27/−8
• src/EVM/UnitTest.hs +27/−11
• src/EVM/VMTest.hs +0/−374
• test/BlockchainTests.hs +466/−0
• test/rpc.hs +6/−2
• test/test.hs +42/−22

@@ -5,6 +5,19 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.50.1] - 2022-12-29++## Fixed++- `hevm exec` no longer fails with `hevm: No match in record selector smttimeout`+- the `gas`, `gaslimit`, `priorityfee`, and `gasprice` cli options are now respected+- cleaner formatting for the gas value in the visual debugger++### Changed++- we now build with ghc 9.2.4 by default+- various perf improvements for concrete execution ([#157](https://github.com/ethereum/hevm/pull/157), [#152](https://github.com/ethereum/hevm/pull/152))+ ## [0.50.0] - 2022-12-19  ### Changed@@ -13,13 +26,22 @@ symbolic execution decompiles bytecode into a custom IR, and smt queries are constructed based on the structure of the term in this IR. -This gives us much deeper control over the encoding, and makes the addition of custom static-analysis and simplification passes much easier to implement.+This gives us much deeper control over the encoding, and makes custom static analysis and+simplification passes much easier to implement.  The symbolic execution engine is now parallel by default, and will distribute granular SMT queries across a pool of solvers, allowing analysis to be scaled out horizontally across many CPUs.  more details can be found in the [architecuture](../../architecture.md) docs.++### Removed++The following cli commands have been removed:++- `abiencode`+- `rlp`+- `flatten`+- `strip-metadata`  ## [0.49.0] - 2021-11-12 

@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain

@@ -1,9 +1,7 @@ -- Main file of the hevm CLI program -{-# Language CPP #-} {-# Language DataKinds #-} {-# Language DeriveAnyClass #-}-{-# Language GADTs #-}  module Main where @@ -14,13 +12,8 @@ import qualified EVM.Fetch import qualified EVM.Stepper --import qualified EVM.VMTest as VMTest-- import EVM.SymExec import EVM.Debug-import EVM.ABI import qualified EVM.Expr as Expr import EVM.SMT import qualified EVM.TTY as TTY@@ -31,36 +24,25 @@ import EVM.Dapp (findUnitTests, dappInfo, DappInfo, emptyDapp) import GHC.Natural import EVM.Format (showTraceTree, formatExpr)-import qualified EVM.Patricia as Patricia-import Data.Map (Map)+import Data.Word (Word64)  import qualified EVM.Facts     as Facts import qualified EVM.Facts.Git as Git import qualified EVM.UnitTest -import GHC.Stack import GHC.Conc-import Control.Concurrent.Async   (async, waitCatch) import Control.Lens hiding (pre, passing) import Control.Monad              (void, when, forM_, unless) import Control.Monad.State.Strict (execStateT, liftIO) import Data.ByteString            (ByteString) import Data.List                  (intercalate, isSuffixOf) import Data.Text                  (unpack, pack)-import Data.Text.Encoding         (encodeUtf8)-import Data.Maybe                 (fromMaybe, fromJust, mapMaybe)+import Data.Maybe                 (fromMaybe, mapMaybe) import Data.Version               (showVersion) import Data.DoubleWord            (Word256)-import System.IO                  (hFlush, stdout, stderr)+import System.IO                  (stderr) import System.Directory           (withCurrentDirectory, listDirectory) import System.Exit                (exitFailure, exitWith, ExitCode(..))-import System.Process             (callProcess)-import qualified Data.Aeson        as JSON-import qualified Data.Aeson.Types  as JSON-import Data.Aeson (FromJSON (..), (.:))-import Data.Aeson.Lens hiding (values)-import qualified Data.Vector as V-import qualified Data.ByteString.Lazy  as Lazy  import qualified Data.ByteString        as ByteString import qualified Data.ByteString.Char8  as Char8@@ -68,11 +50,11 @@ import qualified Data.Map               as Map import qualified Data.Text              as T import qualified Data.Text.IO           as T-import qualified System.Timeout         as Timeout  import qualified Paths_hevm      as Paths  import Options.Generic as Options+import qualified EVM.Transaction  -- This record defines the program's command-line options -- automatically via the `optparse-generic` package.@@ -87,12 +69,12 @@       , coinbase      :: w ::: Maybe Addr       <?> "Block: coinbase"       , value         :: w ::: Maybe W256       <?> "Tx: Eth amount"       , nonce         :: w ::: Maybe W256       <?> "Nonce of origin"-      , gas           :: w ::: Maybe W256       <?> "Tx: gas amount"+      , gas           :: w ::: Maybe Word64     <?> "Tx: gas amount"       , number        :: w ::: Maybe W256       <?> "Block: number"       , timestamp     :: w ::: Maybe W256       <?> "Block: timestamp"       , basefee       :: w ::: Maybe W256       <?> "Block: base fee"       , priorityFee   :: w ::: Maybe W256       <?> "Tx: priority fee"-      , gaslimit      :: w ::: Maybe W256       <?> "Tx: gas limit"+      , gaslimit      :: w ::: Maybe Word64     <?> "Tx: gas limit"       , gasprice      :: w ::: Maybe W256       <?> "Tx: gas price"       , create        :: w ::: Bool             <?> "Tx: creation"       , maxcodesize   :: w ::: Maybe W256       <?> "Block: max code size"@@ -142,12 +124,12 @@       , coinbase    :: w ::: Maybe Addr       <?> "Block: coinbase"       , value       :: w ::: Maybe W256       <?> "Tx: Eth amount"       , nonce       :: w ::: Maybe W256       <?> "Nonce of origin"-      , gas         :: w ::: Maybe W256       <?> "Tx: gas amount"+      , gas         :: w ::: Maybe Word64     <?> "Tx: gas amount"       , number      :: w ::: Maybe W256       <?> "Block: number"       , timestamp   :: w ::: Maybe W256       <?> "Block: timestamp"       , basefee     :: w ::: Maybe W256       <?> "Block: base fee"       , priorityFee :: w ::: Maybe W256       <?> "Tx: priority fee"-      , gaslimit    :: w ::: Maybe W256       <?> "Tx: gas limit"+      , gaslimit    :: w ::: Maybe Word64     <?> "Tx: gas limit"       , gasprice    :: w ::: Maybe W256       <?> "Tx: gas price"       , create      :: w ::: Bool             <?> "Tx: creation"       , maxcodesize :: w ::: Maybe W256       <?> "Block: max code size"@@ -185,25 +167,6 @@       , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point"       , askSmtIterations :: w ::: Maybe Integer         <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)"       }-  | BcTest -- Run an Ethereum Blockchain/GeneralState test-      { file      :: w ::: String    <?> "Path to .json test file"-      , test      :: w ::: [String]  <?> "Test case filter - only run specified test method(s)"-      , debug     :: w ::: Bool      <?> "Run interactively"-      , jsontrace :: w ::: Bool      <?> "Print json trace output at every step"-      , diff      :: w ::: Bool      <?> "Print expected vs. actual state on failure"-      , timeout   :: w ::: Maybe Int <?> "Execution timeout (default: 10 sec.)"-      }-  | Compliance -- Run Ethereum Blockchain compliance report-      { tests   :: w ::: String       <?> "Path to Ethereum Tests directory"-      , group   :: w ::: Maybe String <?> "Report group to run: VM or Blockchain (default: Blockchain)"-      , match   :: w ::: Maybe String <?> "Test case filter - only run methods matching regex"-      , skip    :: w ::: Maybe String <?> "Test case filter - skip tests containing string"-      , html    :: w ::: Bool         <?> "Output html report"-      , timeout :: w ::: Maybe Int    <?> "Execution timeout (default: 10 sec.)"-      }-  | MerkleTest -- Insert a set of key values and check against the given root-      { file :: w ::: String <?> "Path to .json test file"-      }   | Version    deriving (Options.Generic)@@ -299,8 +262,6 @@     Equivalence {} -> equivalence cmd     Exec {} ->       launchExec cmd-    BcTest {} ->-      launchTest cmd     DappTest {} ->       withCurrentDirectory root $ do         cores <- num <$> getNumProcessors@@ -314,26 +275,7 @@             (False, Debug) -> liftIO $ TTY.main testOpts root testFile             (False, JsonTrace) -> error "json traces not implemented for dappTest"             (True, _) -> liftIO $ dappCoverage testOpts (optsMode cmd) testFile-    Compliance {} ->-      case (group cmd) of-        Just "Blockchain" -> launchScript "/run-blockchain-tests" cmd-        Just "VM" -> launchScript "/run-consensus-tests" cmd-        _ -> launchScript "/run-blockchain-tests" cmd-    MerkleTest {} -> merkleTest cmd -launchScript :: String -> Command Options.Unwrapped -> IO ()-launchScript script cmd =-  withCurrentDirectory (tests cmd) $ do-    dataDir <- Paths.getDataDir-    callProcess "bash"-      [ dataDir ++ script-      , "."-      , show (html cmd)-      , fromMaybe "" (match cmd)-      , fromMaybe "" (skip cmd)-      , show $ fromMaybe 10 (timeout cmd)-      ]- findJsonFile :: Maybe String -> IO String findJsonFile (Just s) = pure s findJsonFile Nothing = do@@ -377,19 +319,6 @@         putStrLn $ "Not equivalent. Counterexample(s):" <> show res         exitFailure -checkForVMErrors :: [EVM.VM] -> [String]-checkForVMErrors [] = []-checkForVMErrors (vm:vms) =-  case view EVM.result vm of-    Just (EVM.VMFailure (EVM.UnexpectedSymbolicArg pc msg _)) ->-      ("Unexpected symbolic argument at opcode: "-      <> show pc-      <> ". "-      <> msg-      ) : checkForVMErrors vms-    _ ->-      checkForVMErrors vms- getSrcInfo :: Command Options.Unwrapped -> IO DappInfo getSrcInfo cmd =   let root = fromMaybe "." (dappRoot cmd)@@ -536,8 +465,8 @@ launchExec cmd = do   dapp <- getSrcInfo cmd   vm <- vmFromCommand cmd-  smtjobs <- fromIntegral <$> getNumProcessors-  withSolvers Z3 smtjobs (smttimeout cmd) $ \solvers -> do+  -- TODO: we shouldn't need solvers to execute this code+  withSolvers Z3 0 Nothing $ \solvers -> do     case optsMode cmd of       Run -> do         vm' <- execStateT (EVM.Stepper.interpret (EVM.Fetch.oracle solvers rpcinfo) . void $ EVM.Stepper.execFully) vm@@ -574,65 +503,6 @@      where block' = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)            rpcinfo = (,) block' <$> rpc cmd -data Testcase = Testcase {-  _entries :: [(Text, Maybe Text)],-  _root :: Text-} deriving Show--parseTups :: JSON.Value -> JSON.Parser [(Text, Maybe Text)]-parseTups (JSON.Array arr) = do-  tupList <- mapM parseJSON (V.toList arr)-  mapM (\[k, v] -> do-                  rhs <- parseJSON v-                  lhs <- parseJSON k-                  return (lhs, rhs))-         tupList-parseTups invalid = JSON.typeMismatch "Malformed array" invalid---parseTrieTest :: JSON.Object -> JSON.Parser Testcase-parseTrieTest p = do-  kvlist <- p .: "in"-  entries <- parseTups kvlist-  root <- p .: "root"-  return $ Testcase entries root--instance FromJSON Testcase where-  parseJSON (JSON.Object p) = parseTrieTest p-  parseJSON invalid = JSON.typeMismatch "Merkle test case" invalid--parseTrieTests :: Lazy.ByteString -> Either String (Map String Testcase)-parseTrieTests = JSON.eitherDecode'--merkleTest :: Command Options.Unwrapped -> IO ()-merkleTest cmd = do-  parsed <- parseTrieTests <$> LazyByteString.readFile (file cmd)-  case parsed of-    Left err -> print err-    Right testcases -> mapM_ runMerkleTest testcases--runMerkleTest :: Testcase -> IO ()-runMerkleTest (Testcase entries root) =-  case Patricia.calcRoot entries' of-    Nothing ->-      error "Test case failed"-    Just n ->-      case n == strip0x (hexText root) of-        True ->-          putStrLn "Test case success"-        False ->-          error ("Test case failure; expected " <> show root-                 <> " but got " <> show (ByteStringS n))-  where entries' = fmap (\(k, v) ->-                           (tohexOrText k,-                            tohexOrText (fromMaybe mempty v)))-                   entries--tohexOrText :: Text -> ByteString-tohexOrText s = case "0x" `Char8.isPrefixOf` encodeUtf8 s of-                  True -> hexText s-                  False -> encodeUtf8 s- -- | Creates a (concrete) VM from command line options vmFromCommand :: Command Options.Unwrapped -> IO EVM.VM vmFromCommand cmd = do@@ -680,7 +550,7 @@         Just t -> t         Nothing -> error "unexpected symbolic timestamp when executing vm test" -  return $ VMTest.initTx $ withCache (vm0 baseFee miner ts' blockNum prevRan contract)+  return $ EVM.Transaction.initTx $ withCache (vm0 baseFee miner ts' blockNum prevRan contract)     where         block'   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)         value'   = word value 0@@ -690,7 +560,7 @@         decipher = hexByteString "bytes" . strip0x         mkCode bs = if create cmd                     then EVM.InitCode bs mempty-                    else EVM.RuntimeCode (fromJust $ Expr.toList (ConcreteBuf bs))+                    else EVM.RuntimeCode (EVM.ConcreteRuntimeCode bs)         address' = if create cmd               then addr address (createAddress origin' (word nonce 0))               else addr address 0xacab@@ -702,15 +572,15 @@           , EVM.vmoptAddress       = address'           , EVM.vmoptCaller        = litAddr caller'           , EVM.vmoptOrigin        = origin'-          , EVM.vmoptGas           = 0+          , EVM.vmoptGas           = word64 gas 0xffffffffffffffff           , EVM.vmoptBaseFee       = baseFee-          , EVM.vmoptPriorityFee   = 0-          , EVM.vmoptGaslimit      = 0+          , EVM.vmoptPriorityFee   = word priorityFee 0+          , EVM.vmoptGaslimit      = word64 gaslimit 0xffffffffffffffff           , EVM.vmoptCoinbase      = addr coinbase miner           , EVM.vmoptNumber        = word number blockNum           , EVM.vmoptTimestamp     = Lit $ word timestamp ts-          , EVM.vmoptBlockGaslimit = 0-          , EVM.vmoptGasprice      = 0+          , EVM.vmoptBlockGaslimit = word64 gaslimit 0xffffffffffffffff+          , EVM.vmoptGasprice      = word gasprice 0           , EVM.vmoptMaxCodeSize   = word maxcodesize 0xffffffff           , EVM.vmoptPrevRandao    = word prevRandao prevRan           , EVM.vmoptSchedule      = FeeSchedule.berlin@@ -721,6 +591,7 @@           , EVM.vmoptAllowFFI      = False           }         word f def = fromMaybe def (f cmd)+        word64 f def = fromMaybe def (f cmd)         addr f def = fromMaybe def (f cmd)         bytes f def = maybe def decipher (f cmd) @@ -776,7 +647,7 @@     (_, _, Nothing) ->       error "must provide at least (rpc + address) or code" -  return $ (VMTest.initTx $ withCache $ vm0 baseFee miner ts blockNum prevRan calldata' callvalue' caller' contract')+  return $ (EVM.Transaction.initTx $ withCache $ vm0 baseFee miner ts blockNum prevRan calldata' callvalue' caller' contract')     & set (EVM.env . EVM.storage) store    where@@ -785,7 +656,7 @@     origin'  = addr origin 0     mkCode bs = if create cmd                    then EVM.InitCode bs mempty-                   else EVM.RuntimeCode (fromJust . Expr.toList $ ConcreteBuf bs)+                   else EVM.RuntimeCode (EVM.ConcreteRuntimeCode bs)     address' = if create cmd           then addr address (createAddress origin' (word nonce 0))           else addr address 0xacab@@ -796,15 +667,15 @@       , EVM.vmoptAddress       = address'       , EVM.vmoptCaller        = caller'       , EVM.vmoptOrigin        = origin'-      , EVM.vmoptGas           = 0xffffffffffffffff-      , EVM.vmoptGaslimit      = 0xffffffffffffffff+      , EVM.vmoptGas           = word64 gas 0xffffffffffffffff+      , EVM.vmoptGaslimit      = word64 gaslimit 0xffffffffffffffff       , EVM.vmoptBaseFee       = baseFee       , EVM.vmoptPriorityFee   = word priorityFee 0       , EVM.vmoptCoinbase      = addr coinbase miner       , EVM.vmoptNumber        = word number blockNum       , EVM.vmoptTimestamp     = ts-      , EVM.vmoptBlockGaslimit = 0-      , EVM.vmoptGasprice      = 0+      , EVM.vmoptBlockGaslimit = word64 gaslimit 0xffffffffffffffff+      , EVM.vmoptGasprice      = word gasprice 0       , EVM.vmoptMaxCodeSize   = word maxcodesize 0xffffffff       , EVM.vmoptPrevRandao    = word prevRandao prevRan       , EVM.vmoptSchedule      = FeeSchedule.berlin@@ -816,65 +687,4 @@       }     word f def = fromMaybe def (f cmd)     addr f def = fromMaybe def (f cmd)--launchTest :: HasCallStack => Command Options.Unwrapped ->  IO ()-launchTest cmd = do-  parsed <- VMTest.parseBCSuite <$> LazyByteString.readFile (file cmd)-  case parsed of-     Left "No cases to check." -> putStrLn "no-cases ok"-     Left err -> print err-     Right allTests ->-       let testFilter =-             if null (test cmd)-             then id-             else filter (\(x, _) -> elem x (test cmd))-       in-         mapM_ (runVMTest (diff cmd) (optsMode cmd) (timeout cmd)) $-           testFilter (Map.toList allTests)--runVMTest :: HasCallStack => Bool -> Mode -> Maybe Int -> (String, VMTest.Case) -> IO Bool-runVMTest diffmode mode timelimit (name, x) =- do-  let vm0 = VMTest.vmForCase x-  putStr (name ++ " ")-  hFlush stdout-  result <- do-    action <- async $-      case mode of-        Run ->-          Timeout.timeout (1000000 * (fromMaybe 10 timelimit)) $-            execStateT (EVM.Stepper.interpret (EVM.Fetch.zero 0 (Just 0)) . void $ EVM.Stepper.execFully) vm0-        Debug ->-          withSolvers Z3 0 Nothing $ \solvers -> Just <$> TTY.runFromVM solvers Nothing Nothing emptyDapp vm0-        JsonTrace ->-          error "JsonTrace: implement me"-          -- Just <$> execStateT (EVM.UnitTest.interpretWithCoverage EVM.Fetch.zero EVM.Stepper.runFully) vm0-    waitCatch action-  case result of-    Right (Just vm1) -> do-      ok <- VMTest.checkExpectation diffmode x vm1-      putStrLn (if ok then "ok" else "")-      return ok-    Right Nothing -> do-      putStrLn "timeout"-      return False-    Left e -> do-      putStrLn $ "error: " ++ if diffmode-        then show e-        else (head . lines . show) e-      return False--parseAbi :: (AsValue s) => s -> (Text, [AbiType])-parseAbi abijson =-  (signature abijson, snd-    <$> parseMethodInput-    <$> V.toList-      (fromMaybe (error "Malformed function abi") (abijson ^? key "inputs" . _Array)))--abiencode :: (AsValue s) => Maybe s -> [String] -> ByteString-abiencode Nothing _ = error "missing required argument: abi"-abiencode (Just abijson) args =-  let (sig', declarations) = parseAbi abijson-  in if length declarations == length args-     then abiMethod sig' $ AbiTuple . V.fromList $ zipWith makeAbiValue declarations args-     else error $ "wrong number of arguments:" <> show (length args) <> ": " <> show args+    word64 f def = fromMaybe def (f cmd)

@@ -2,7 +2,7 @@ name:   hevm version:-  0.50.0+  0.50.1 synopsis:   Ethereum virtual machine evaluator description:@@ -22,9 +22,6 @@   Ethereum build-type:   Simple-data-files:-  run-blockchain-tests-  run-consensus-tests extra-source-files:   CHANGELOG.md   test/contracts/lib/test.sol@@ -43,32 +40,25 @@   test/contracts/fail/dsProveFail.sol   test/contracts/fail/invariantFail.sol +flag ci+  description: Sets flags for compilation in CI+  default:     False+  manual:      True++source-repository head+  type:     git+  location: https://github.com/ethereum/hevm.git+ common shared-  default-language:-    Haskell2010+  if flag(ci)+    ghc-options: -Werror+  default-language: GHC2021   default-extensions:     LambdaCase     OverloadedStrings     RecordWildCards     TypeFamilies     ViewPatterns-    -- GHC2021 default extensions, remove me when GHC is updated to 9.2-    BangPatterns-    ConstraintKinds-    DeriveDataTypeable-    DeriveFunctor-    DeriveGeneric-    DoAndIfThenElse-    EmptyDataDecls-    FlexibleContexts-    FlexibleInstances-    ForeignFunctionInterface-    GeneralizedNewtypeDeriving-    PolyKinds-    RankNTypes-    ScopedTypeVariables-    StandaloneDeriving-    TypeOperators  library   import: shared@@ -85,7 +75,6 @@     EVM.Exec,     EVM.Facts,     EVM.Facts.Git,-    EVM.Flatten,     EVM.Format,     EVM.Fetch,     EVM.FeeSchedule,@@ -106,7 +95,6 @@     EVM.TTYCenteredList,     EVM.Types,     EVM.UnitTest,-    EVM.VMTest   other-modules:     Paths_hevm   autogen-modules:@@ -130,12 +118,12 @@     Decimal                           >= 0.5.1 && < 0.6,     containers                        >= 0.6.0 && < 0.7,     deepseq                           >= 1.4.4 && < 1.5,-    time                              >= 1.8.0 && < 1.11,+    time                              >= 1.11.1.1 && < 1.12,     transformers                      >= 0.5.6 && < 0.6,     tree-view                         >= 0.5 && < 0.6,     abstract-par                      >= 0.3.3 && < 0.4,     aeson                             >= 2.0.0 && < 2.1,-    bytestring                        >= 0.10.8 && < 0.11,+    bytestring                        >= 0.11.3.1 && < 0.12,     scientific                        >= 0.3.6 && < 0.4,     binary                            >= 0.8.6 && < 0.9,     text                              >= 1.2.3 && < 1.3,@@ -143,22 +131,22 @@     vector                            >= 0.12.1 && < 0.13,     ansi-wl-pprint                    >= 0.6.9 && < 0.7,     base16-bytestring                 >= 1.0.0 && < 2.0,-    brick                             >= 0.68 && < 0.69,+    brick                             >= 1.4 && < 1.5,     megaparsec                        >= 9.0.0 && < 10.0,     mtl                               >= 2.2.2 && < 2.3,     directory                         >= 1.3.3 && < 1.4,     filepath                          >= 1.4.2 && < 1.5,-    vty                               >= 5.25.1 && < 5.34,+    vty                               >= 5.37 && < 5.38,     cereal                            >= 0.5.8 && < 0.6,-    cryptonite                        >= 0.27 && <= 0.29,+    cryptonite                        >= 0.30 && < 0.31,     memory                            >= 0.16.0 && < 0.20,     data-dword                        >= 0.3.1 && < 0.4,     fgl                               >= 5.7.0 && < 5.8,     free                              >= 5.1.3 && < 5.2,     haskeline                         >= 0.8.0 && < 0.9,     process                           >= 1.6.5 && < 1.7,-    lens                              >= 5.0.0 && < 5.1,-    lens-aeson                        >= 1.0.2 && < 1.2,+    lens                              >= 5.1.1 && < 5.2,+    lens-aeson                        >= 1.2.2 && < 1.3,     monad-par                         >= 0.3.5 && < 0.4,     async                             >= 2.2.4 && < 2.3,     multiset                          >= 0.3.4 && < 0.4,@@ -179,7 +167,7 @@     smt2-parser                       >= 0.1.0.1,     word-wrap                         >= 0.5 && < 0.6,     spool                             >= 0.1 && < 0.2,-    parsec                            >= 3.1.14.0 && < 3.1.15+    parsec                            >= 3.1.15 && < 3.2,   hs-source-dirs:     src @@ -247,12 +235,15 @@     HUnit >= 1.6,     QuickCheck,     quickcheck-instances,+    aeson,     base,     base16-bytestring,     binary,     containers,     directory,     bytestring,+    filemanip,+    filepath,     here,     hevm,     lens,@@ -270,6 +261,7 @@     time,     array,     vector,+    witherable,     smt2-parser >= 0.1.0.1  library test-utils@@ -283,10 +275,14 @@     test-base   build-depends:     test-utils+  other-modules:+    EVM.TestUtils   if os(darwin)-     extra-libraries: c+++    extra-libraries: c+++    -- https://gitlab.haskell.org/ghc/ghc/-/issues/11829+    ld-options: -Wl,-keep_dwarf_unwind   else-     extra-libraries: stdc+++    extra-libraries: stdc++  --- Test Suites --- @@ -307,3 +303,11 @@     exitcode-stdio-1.0   main-is:     rpc.hs++test-suite ethereum-tests+  import:+    test-common+  type:+    exitcode-stdio-1.0+  main-is:+    BlockchainTests.hs

@@ -1,150 +0,0 @@-#!/usr/bin/env bash-set -e--# Invoke with hevm e.g.-# hevm compliance --tests ~/ethereum-tests --skip modexp --timeout 20 --html--HEVM=${HEVM:-hevm}--if [[ "$#" -lt 1 ]]; then-  echo >&2 "usage: $(basename "$0") <tests-dir>"-  exit 1-fi--tests=$1-html=$2-match=$3-skip=$4-timeout=${5:-10}--_html () {-cat <<.-<!doctype html>-<title>hevm test results</title>-<style>-* { font-family:-"latin modern mono", "fantasque sans mono",-inconsolata, menlo, monospace;-font-size: 22px;-line-height: 26px; }-body { margin: 2rem; }-header { text-align: center; margin: 4rem 0; }-table { border-collapse: collapse; width: 100%; }-tr:nth-child(even) { background: rgba(0, 0, 0, 0.05); }-td:not(:first-child):not(:last-child) { padding: 0 1rem; }-.category { opacity: 0.6; text-align: right }-a { color: darkblue; text-decoration: none; }-h1, h2 { text-align: center; margin-top: 2rem  }-.testcase { font-weight: bold }-#failed .testcase { color: rgb(200, 0, 0) }-#balancefailed .testcase { color: rgb(200, 200, 0) }-#passed .testcase { color: rgb(0, 150, 0) }-#skipped .testcase { color: rgb(0, 100, 250) }-#timeout .testcase { color: rgb(0, 0, 250) }-</style>-<header>-<h1>hevm consensus test report</h1>-<p>$(date +%Y-%m-%d)</p>-<p>$(echo "$npass passed, $nbal bad-balance, $nnon bad-nonce, $nstr bad-storage, $nfail failed, $nskip skipped, $ntime timeout")</p>-(Test suite: <span class=GeneralStateTests</span>GeneralStateTests</span> for Berlin)-</header>-<h2>Failed tests</h2>-<table id=failed>-<tbody>-$(echo $noncefailed)-$(echo $storagefailed)-$(echo $failed)-</table>-<h2>Failed tests (due to balance only)</h2>-<table id=balancefailed>-<tbody>-$(echo $balancefailed)-</table>-<h2>Timeout tests</h2>-<table id=timeout>-<tbody>-$(echo $timeouts)-</table>-<h2>Skipped tests</h2>-<table id=skipped>-<tbody>-$(echo $skipped)-</table>-<h2>Passed tests</h2>-<table id=passed>-<tbody>-$(echo $passed)-</table>-.-}--shopt -s nocasematch-{-  cd "$tests"-  for x in BlockchainTests/GeneralStateTests/*/*; do-    if [ -d $x ]; then-      for y in $x/*; do-        if [[ $y =~ .*$match.* ]] && [[ -n $skip && $y =~ .*$skip.* ]]; then-          for job in $(<$y jq '.|keys[]' -r); do-            echo -n "$job " ; echo "skip"-          done-        elif [[ $y =~ .*$match.* ]]; then-          set +e-          "$HEVM" bc-test --file $y --timeout $timeout 2>&1-          set -e-        fi-      done-    else-      if [[ $x =~ .*$match.* ]] && [[ -n $skip && $x =~ .*$skip.* ]]; then-        for job in $(<$x jq '.|keys[]' -r); do-          echo -n "$job " ; echo "skip"-        done-      elif [[ $x =~ .*$match.* ]]; then-        set +e-        "$HEVM" bc-test --file $x --timeout $timeout 2>&1-        set -e-      fi-    fi-  done-} | {-  while read test outcome; do-    echo >&2 "$test $outcome"-    row="<tr><td class=testcase>$test<td>$outcome"-    row+=$'\n'-    case $outcome in-      ok)          passed+=$row ;;-      bad-balance) balancefailed+=$row ;;-      bad-nonce)   noncefailed+=$row ;;-      bad-storage) storagefailed+=$row ;;-      timeout)     timeouts+=$row ;;-      skip)        skipped+=$row ;;-      *)           failed+=$row ;;-    esac-  done--  sum () { echo -ne "$1" | wc -l | awk '{print $1}'; }--  npass=$(sum "$passed")-  nbal=$(sum "$balancefailed")-  nnon=$(sum "$noncefailed")-  nstr=$(sum "$storagefailed")-  nfail=$(sum "$failed")-  ntime=$(sum "$timeouts")-  nskip=$(sum "$skipped")--  echo >&2 "passed: $npass"-  echo >&2 "bad-balance: $nbal"-  echo >&2 "bad-nonce: $nnon"-  echo >&2 "bad-storage: $nstr"-  echo >&2 "failed: $nfail"-  echo >&2 "timeout: $ntime"-  echo >&2 "skipped: $nskip"--  if [[ $html == "True" ]]; then-    _html-  fi--  nbad=$(($nbal + $nnon + $nstr + $nfail))--  [[ $nbad -gt 0 ]] && exit 1 || exit 0-}

@@ -1,110 +0,0 @@-#!/usr/bin/env bash-set -e--# Invoke with hevm e.g.-# hevm compliance --tests ~/ethereum-tests --group VM --skip quadratic --html--HEVM=${HEVM:-hevm}--if [[ "$#" -lt 1 ]]; then-  echo >&2 "usage: $(basename "$0") <tests-dir>"-  exit 1-fi--tests=$1-html=$2-match=$3-skip=$4-timeout=${5:-10}--_html() {-cat <<.-<!doctype html>-<title>hevm test results</title>-<style>-* { font-family:-"latin modern mono", "fantasque sans mono",-inconsolata, menlo, monospace;-font-size: 22px;-line-height: 26px; }-body { margin: 2rem; }-header { text-align: center; margin: 4rem 0; }-table { border-collapse: collapse; width: 100%; }-tr:nth-child(even) { background: rgba(0, 0, 0, 0.05); }-td:not(:first-child):not(:last-child) { padding: 0 1rem; }-.category { opacity: 0.6; text-align: right }-a { color: darkblue; text-decoration: none; }-h1, h2 { text-align: center; margin-top: 2rem  }-.testcase { font-weight: bold }-#failed .testcase { color: rgb(200, 0, 0) }-#passed .testcase { color: rgb(0, 150, 0) }-#skipped .testcase { color: rgb(0, 100, 250) }-</style>-<header>-<h1>hevm consensus test report</h1>-<p>$(date +%Y-%m-%d)</p>-<p>$(echo "$npass passed, $nfail failed, $nskip skipped")</p>-(Test suite: <span class=VMTests</span>VMTests</span> for ConstantinopleFix)-</header>-<h2>Failed tests</h2>-<table id=failed>-<tbody>-$(echo $failed)-</table>-<h2>Skipped tests</h2>-<table id=skipped>-<tbody>-$(echo $skipped)-</table>-<h2>Passed tests</h2>-<table id=passed>-<tbody>-$(echo $passed)-</table>-.-}--{-  cd "$tests"-  for x in VMTests/*/*; do-    if [[ $x =~ .*$match.* ]] && [[ -n $skip && $x =~ .*$skip.* ]]; then-      for job in $(<$x jq '.|keys[]' -r); do-        echo "$x $job skip"-      done-    elif [[ $x =~ .*$match.* ]]; then-      echo -n "$x " ; "$HEVM" vm-test --file $x --timeout $timeout 2>&1-    fi-  done-} | {-  while read path test outcome; do-    echo >&2 "$path $test $outcome"-    category=$(dirname "$path")-    testcase=$(basename "${path%.json}")-    row="<tr><td class=testcase>$testcase<td>$outcome<td class=category>$category"-    row+=$'\n'-    case $outcome in-      ok)      passed+=$row ;;-      skip)    skipped+=$row ;;-      timeout) timouts+=row ;;-      *)       failed+=$row ;;-    esac-  done--  sum () { echo -ne "$1" | wc -l | awk '{print $1}'; }--  nfail=$(sum "$failed")-  npass=$(sum "$passed")-  nskip=$(sum "$skipped")-  ntime=$(sum "$timeouts")--  echo >&2 "passed: $npass"-  echo >&2 "failed: $nfail"-  echo >&2 "timeout: $ntime"-  echo >&2 "skipped: $nskip"--  if [[ $html == "True" ]]; then-    _html-  fi--  [[ $nfail -gt 0 ]] && exit 1 || exit 0-}

@@ -11,11 +11,11 @@ import Data.Text (unpack) import Data.Text.Encoding (decodeUtf8, encodeUtf8) import EVM.ABI-import EVM.Types hiding (IllegalOverflow)+import EVM.Types hiding (IllegalOverflow, Error) import EVM.Solidity import EVM.Concrete (createAddress, create2Address) import EVM.Op-import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord, writeByte, bufLength, indexWord, litAddr, readBytes, word256At, copySlice, isLitByte)+import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord, writeByte, bufLength, indexWord, litAddr, readBytes, word256At, copySlice) import EVM.FeeSchedule (FeeSchedule (..)) import Options.Generic as Options import qualified EVM.Precompiled@@ -28,7 +28,7 @@ import Data.ByteString.Lazy         (fromStrict) import Data.Map.Strict              (Map) import Data.Set                     (Set, insert, member, fromList)-import Data.Maybe                   (fromMaybe)+import Data.Maybe                   (fromMaybe, fromJust) import Data.Sequence                (Seq) import Data.Vector.Storable         (Vector) import Data.Foldable                (toList)@@ -58,7 +58,6 @@ import Crypto.PubKey.ECC.ECDSA (signDigestWith, PrivateKey(..), Signature(..)) import Crypto.PubKey.ECC.Types (getCurveByName, CurveName(..), Point(..)) import Crypto.PubKey.ECC.Generate (generateQ)-import Data.DoubleWord (Word256(Word256), Word128 (Word128))  -- * Data types @@ -305,10 +304,18 @@   hopefully we do not have to deal with dynamic immutable before we get a real data section... -} data ContractCode-  = InitCode ByteString (Expr Buf)     -- ^ "Constructor" code, during contract creation-  | RuntimeCode (V.Vector (Expr Byte)) -- ^ "Instance" code, after contract creation+  = InitCode ByteString (Expr Buf) -- ^ "Constructor" code, during contract creation+  | RuntimeCode RuntimeCode -- ^ "Instance" code, after contract creation   deriving (Show) +-- | We have two variants here to optimize the fully concrete case.+-- ConcreteRuntimeCode just wraps a ByteString+-- SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).+data RuntimeCode+  = ConcreteRuntimeCode ByteString+  | SymbolicRuntimeCode (V.Vector (Expr Byte))+  deriving (Show, Eq, Ord)+ -- runtime err when used for symbolic code instance Eq ContractCode where   (InitCode a b) == (InitCode c d) = a == c && b == d@@ -392,7 +399,7 @@ blankState = FrameState   { _contract     = 0   , _codeContract = 0-  , _code         = RuntimeCode mempty+  , _code         = RuntimeCode (ConcreteRuntimeCode "")   , _pc           = 0   , _stack        = mempty   , _memory       = mempty@@ -421,7 +428,8 @@ bytecode :: Getter Contract (Expr Buf) bytecode = contractcode . to f   where f (InitCode _ _) = mempty-        f (RuntimeCode ops) = Expr.fromList ops+        f (RuntimeCode (ConcreteRuntimeCode bs)) = ConcreteBuf bs+        f (RuntimeCode (SymbolicRuntimeCode ops)) = Expr.fromList ops  instance Semigroup Cache where   a <> b = Cache@@ -603,7 +611,8 @@     else do       let ?op = case (the state code) of                   InitCode conc _ -> BS.index conc (the state pc)-                  RuntimeCode ops ->+                  RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs (the state pc)+                  RuntimeCode (SymbolicRuntimeCode ops) ->                     fromMaybe (error "could not analyze symbolic code") $                       unlitByte $ ops V.! the state pc @@ -614,13 +623,10 @@           let !n = num x - 0x60 + 1               !xs = case the state code of                 InitCode conc _ -> Lit $ word $ padRight n $ BS.take n (BS.drop (1 + the state pc) conc)-                RuntimeCode ops ->+                RuntimeCode (ConcreteRuntimeCode bs) -> Lit $ word $ BS.take n $ BS.drop (1 + the state pc) bs+                RuntimeCode (SymbolicRuntimeCode ops) ->                   let bytes = V.take n $ V.drop (1 + the state pc) ops-                  in if all isLitByte bytes then -- optimize concrete path-                       let litBytes = V.toList $ V.catMaybes $ unlitByte <$> bytes-                           padded = BS.replicate (32 - length litBytes) 0 <> BS.pack litBytes-                       in Lit $ word padded-                     else readWord (Lit 0) $ Expr.fromList $ padLeft' 32 bytes+                  in readWord (Lit 0) $ Expr.fromList $ padLeft' 32 bytes           limitStack 1 $             burn g_verylow $ do               next@@ -1075,7 +1081,9 @@           case stk of             (x:xs) ->               burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' ->-                checkJump x' xs+                case toInt x' of+                  Nothing -> vmError EVM.BadJumpDestination+                  Just i -> checkJump i xs             _ -> underrun          -- op: JUMPI@@ -1085,7 +1093,9 @@                 burn g_high $                   let jump :: Bool -> EVM ()                       jump False = assign (state . stack) xs >> next-                      jump _    = checkJump x' xs+                      jump _    = case toInt x' of+                        Nothing -> vmError EVM.BadJumpDestination+                        Just i -> checkJump i xs                   in case maybeLitWord y of                       Just y' -> jump (0 /= y')                       -- if the jump condition is symbolic, we explore both sides@@ -1674,7 +1684,8 @@ accountEmpty :: Contract -> Bool accountEmpty c =   case view contractcode c of-    RuntimeCode b -> null b+    RuntimeCode (ConcreteRuntimeCode "") -> True+    RuntimeCode (SymbolicRuntimeCode b) -> null b     _ -> False   && (view nonce c == 0)   && (view balance c == 0)@@ -1703,10 +1714,17 @@       creation <- use (tx . isCreate)       createe  <- use (state . contract)       createeExists <- (Map.member createe) <$> use (env . contracts)-      case Expr.toList output of-        Nothing -> vmError $ UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" [output]-        Just ops ->-          when (creation && createeExists) $ replaceCode createe (RuntimeCode ops)+      let onContractCode contractCode =+            when (creation && createeExists) $ replaceCode createe contractCode+      case output of+        ConcreteBuf bs ->+          onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)+        _ ->+          case Expr.toList output of+            Nothing ->+              vmError $ UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" [output]+            Just ops ->+              onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)    -- compute and pay the refund to the caller and the   -- corresponding payment to the miner@@ -1735,7 +1753,7 @@   -- pay out the block reward, recreating the miner if necessary   preuse (env . contracts . ix miner) >>= \case     Nothing -> modifying (env . contracts)-      (Map.insert miner (initialContract (EVM.RuntimeCode mempty)))+      (Map.insert miner (initialContract (EVM.RuntimeCode (ConcreteRuntimeCode ""))))     Just _  -> noop   modifying (env . contracts)     (Map.adjust (over balance (+ blockReward)) miner)@@ -2119,7 +2137,8 @@ collision :: Maybe Contract -> Bool collision c' = case c' of   Just c -> (view nonce c /= 0) || case view contractcode c of-    RuntimeCode b -> not $ null b+    RuntimeCode (ConcreteRuntimeCode "") -> False+    RuntimeCode (SymbolicRuntimeCode b) -> not $ null b     _ -> True   Nothing -> False @@ -2368,17 +2387,23 @@           case how of             -- Case 4: Returning during a creation?             FrameReturned output -> do-                case Expr.toList output of-                  Nothing -> vmError $-                    UnexpectedSymbolicArg-                      (view (state . pc) oldVm)-                      "runtime code cannot have an abstract length"-                      [output]-                  Just newCode -> do-                    replaceCode createe (RuntimeCode newCode)+              let onContractCode contractCode = do+                    replaceCode createe contractCode                     assign (state . returndata) mempty                     reclaimRemainingGasAllowance                     push (num createe)+              case output of+                ConcreteBuf bs ->+                  onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)+                _ ->+                  case Expr.toList output of+                    Nothing -> vmError $+                      UnexpectedSymbolicArg+                        (view (state . pc) oldVm)+                        "runtime code cannot have an abstract length"+                        [output]+                    Just newCode -> do+                      onContractCode $ RuntimeCode (SymbolicRuntimeCode newCode)              -- Case 5: Reverting during a creation?             FrameReverted output -> do@@ -2459,9 +2484,7 @@   :: (MonadState VM m) => TraceData -> m Trace withTraceLocation x = do   vm <- get-  let-    Just this =-      currentContract vm+  let this = fromJust $ currentContract vm   pure Trace     { _traceData = x     , _traceContract = this@@ -2558,19 +2581,16 @@  -- * Bytecode data functions -checkJump :: (Integral n) => n -> [Expr EWord] -> EVM ()+checkJump :: Int -> [Expr EWord] -> EVM () checkJump x xs = do   theCode <- use (state . code)   self <- use (state . codeContract)   theCodeOps <- use (env . contracts . ix self . codeOps)   theOpIxMap <- use (env . contracts . ix self . opIxMap)-  let ops = case theCode of-        InitCode ops' _ -> V.fromList $ LitByte <$> BS.unpack ops'-        RuntimeCode ops' -> ops'-      op = do-        -- TODO: not a big fan of how bounds are checked, change this-        b <- if x < num (length ops) then ops V.!? num x else Nothing-        unlitByte b+  let op = case theCode of+        InitCode ops _ -> BS.indexMaybe ops x+        RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x+        RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= unlitByte   case op of     Nothing -> vmError EVM.BadJumpDestination     Just b ->@@ -2606,7 +2626,10 @@         go v (n, !i, !j, !m) _ =           {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j) -mkOpIxMap (RuntimeCode ops)+mkOpIxMap (RuntimeCode (ConcreteRuntimeCode ops)) =+  mkOpIxMap (InitCode ops mempty) -- a bit hacky++mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))   = Vector.create $ Vector.new (length ops) >>= \v ->       let (_, _, _, m) = foldl (go v) (0, 0, 0, return ()) (stripBytecodeMetadataSym $ V.toList ops)       in m >> return v@@ -2632,7 +2655,9 @@       (op, pushdata) = case code' of         InitCode xs' _ ->           (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')-        RuntimeCode xs' ->+        RuntimeCode (ConcreteRuntimeCode xs') ->+          (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')+        RuntimeCode (SymbolicRuntimeCode xs') ->           ( fromMaybe (error "unexpected symbolic code") . unlitByte $ xs' V.! i , V.toList $ V.drop i xs')   in if (opslen code' < i)      then Nothing@@ -2756,25 +2781,24 @@  -- Maps operation indicies into a pair of (bytecode index, operation) mkCodeOps :: ContractCode -> RegularVector.Vector (Int, Op)-mkCodeOps (InitCode bytes _) = RegularVector.fromList . toList $ go 0 bytes+mkCodeOps contractCode =+  let l = case contractCode of+            InitCode bytes _ ->+              LitByte <$> (BS.unpack bytes)+            RuntimeCode (ConcreteRuntimeCode ops) ->+              LitByte <$> (BS.unpack $ stripBytecodeMetadata ops)+            RuntimeCode (SymbolicRuntimeCode ops) ->+              stripBytecodeMetadataSym $ V.toList ops+  in RegularVector.fromList . toList $ go 0 l   where     go !i !xs =-      case BS.uncons xs of-        Nothing ->-          mempty-        Just (x, xs') ->-          let j = opSize x-          in (i, readOp x (fmap LitByte $ BS.unpack xs')) Seq.<| go (i + j) (BS.drop j xs)-mkCodeOps (RuntimeCode ops) = RegularVector.fromList . toList $ go' 0 (stripBytecodeMetadataSym $ V.toList ops)-  where-    go' !i !xs =       case uncons xs of         Nothing ->           mempty         Just (x, xs') ->           let x' = fromMaybe (error "unexpected symbolic code argument") $ unlitByte x               j = opSize x'-          in (i, readOp x' xs') Seq.<| go' (i + j) (drop j xs)+          in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)  -- * Gas cost calculation helpers @@ -2889,23 +2913,27 @@  hashcode :: ContractCode -> Expr EWord hashcode (InitCode ops args) = keccak $ (ConcreteBuf ops) <> args-hashcode (RuntimeCode ops) = keccak . Expr.fromList $ ops+hashcode (RuntimeCode (ConcreteRuntimeCode ops)) = keccak (ConcreteBuf ops)+hashcode (RuntimeCode (SymbolicRuntimeCode ops)) = keccak . Expr.fromList $ ops  -- | The length of the code ignoring any constructor args. -- This represents the region that can contain executable opcodes opslen :: ContractCode -> Int opslen (InitCode ops _) = BS.length ops-opslen (RuntimeCode ops) = length ops+opslen (RuntimeCode (ConcreteRuntimeCode ops)) = BS.length ops+opslen (RuntimeCode (SymbolicRuntimeCode ops)) = length ops  -- | The length of the code including any constructor args. -- This can return an abstract value codelen :: ContractCode -> Expr EWord codelen c@(InitCode {}) = bufLength $ toBuf c-codelen (RuntimeCode ops) = Lit . num $ length ops+codelen (RuntimeCode (ConcreteRuntimeCode ops)) = Lit . num $ BS.length ops+codelen (RuntimeCode (SymbolicRuntimeCode ops)) = Lit . num $ length ops  toBuf :: ContractCode -> Expr Buf toBuf (InitCode ops args) = ConcreteBuf ops <> args-toBuf (RuntimeCode ops) = Expr.fromList ops+toBuf (RuntimeCode (ConcreteRuntimeCode ops)) = ConcreteBuf ops+toBuf (RuntimeCode (SymbolicRuntimeCode ops)) = Expr.fromList ops   codeloc :: EVM CodeLocation@@ -2914,12 +2942,6 @@   let self = view (state . contract) vm       loc = view (state . pc) vm   pure (self, loc)--toWord64 :: W256 -> Maybe Word64-toWord64 n =-  if n <= num (maxBound :: Word64)-    then let (W256 (Word256 _ (Word128 _ n'))) = n in Just n'-    else Nothing  -- * Emacs setup 

@@ -384,7 +384,9 @@       | (x, i) <- zip (map fromIntegral xs) [1..] ]  asUInt :: Integral i => Int -> (i -> a) -> Get a-asUInt n f = (\(AbiUInt _ x) -> f (fromIntegral x)) <$> getAbi (AbiUIntType n)+asUInt n f = y <$> getAbi (AbiUIntType n)+  where y (AbiUInt _ x) = f (fromIntegral x)+        y _ = error "can't happen"  getWord256 :: Get Word256 getWord256 = pack32 8 <$> replicateM 8 getWord32be@@ -405,13 +407,12 @@  genAbiValue :: AbiType -> Gen AbiValue genAbiValue = \case-   AbiUIntType n -> genUInt n-   AbiIntType n ->-     do a <- genUInt n-        let AbiUInt _ x = a-        pure $ AbiInt n (signedWord (x - 2^(n-1)))+   AbiUIntType n -> AbiUInt n <$> genUInt n+   AbiIntType n -> do+     x <- genUInt n+     pure $ AbiInt n (signedWord (x - 2^(n-1)))    AbiAddressType ->-     (\(AbiUInt _ x) -> AbiAddress (fromIntegral x)) <$> genUInt 20+     AbiAddress . fromIntegral <$> genUInt 20    AbiBoolType ->      elements [AbiBool False, AbiBool True]    AbiBytesType n ->@@ -430,7 +431,8 @@    AbiTupleType ts ->      AbiTuple <$> mapM genAbiValue ts   where-    genUInt n = AbiUInt n <$> arbitraryIntegralWithMax (2^n-1)+    genUInt :: Int -> Gen Word256+    genUInt n = arbitraryIntegralWithMax (2^n-1) :: Gen Word256  instance Arbitrary AbiType where   arbitrary = oneof

@@ -2,7 +2,7 @@  module EVM.Dapp where -import EVM (Trace, traceContract, traceOpIx, ContractCode(..), Contract(..), codehash, contractcode)+import EVM (Trace, traceContract, traceOpIx, ContractCode(..), Contract(..), codehash, contractcode, RuntimeCode (..)) import EVM.ABI (Event, AbiType, SolError) import EVM.Debug (srcMapCodePos) import EVM.Solidity@@ -68,7 +68,7 @@   let     solcs = Map.elems solcByName     astIds = astIdMap $ snd <$> toList (view sourceAsts sources)-    immutables = filter ((/=) mempty . _immutableReferences) solcs+    immutables = filter ((/=) mempty . (view immutableReferences)) solcs    in DappInfo     { _dappRoot = root@@ -176,7 +176,11 @@ lookupCode :: ContractCode -> DappInfo -> Maybe SolcContract lookupCode (InitCode c _) a =   snd <$> preview (dappSolcByHash . ix (keccak' (stripBytecodeMetadata c))) a-lookupCode (RuntimeCode c) a = let+lookupCode (RuntimeCode (ConcreteRuntimeCode c)) a =+  case snd <$> preview (dappSolcByHash . ix (keccak' (stripBytecodeMetadata c))) a of+    Just x -> return x+    Nothing -> snd <$> find (compareCode c . fst) (view dappSolcByCode a)+lookupCode (RuntimeCode (SymbolicRuntimeCode c)) a = let     code = BS.pack $ mapMaybe unlitByte $ V.toList c   in case snd <$> preview (dappSolcByHash . ix (keccak' (stripBytecodeMetadata code))) a of     Just x -> return x

@@ -7,7 +7,7 @@ -} module EVM.Dev where -import Data.ByteString hiding (putStrLn, writeFile, zip)+import Data.ByteString hiding (writeFile, zip) import Control.Monad.State.Strict hiding (state) import Data.Maybe (fromJust) import System.Directory@@ -30,7 +30,6 @@ import System.Exit (exitFailure) import qualified EVM.Fetch as Fetch import qualified EVM.FeeSchedule as FeeSchedule-import qualified Data.Vector as V  checkEquiv :: (Typeable a) => Expr a -> Expr a -> IO () checkEquiv a b = withSolvers Z3 1 Nothing $ \s -> do@@ -363,7 +362,7 @@ initVm :: ByteString -> VM initVm bs = vm   where-    contractCode = RuntimeCode $ V.fromList $ LitByte <$> unpack bs+    contractCode = RuntimeCode (ConcreteRuntimeCode bs)     c = Contract       { _contractcode = contractCode       , _balance      = 0

@@ -45,7 +45,7 @@     , vmoptTxAccessList = mempty     , vmoptAllowFFI = False     }) & set (env . contracts . at ethrunAddress)-             (Just (initialContract (RuntimeCode mempty)))+             (Just (initialContract (RuntimeCode (ConcreteRuntimeCode ""))))  exec :: MonadState VM m => m VMResult exec =

@@ -8,7 +8,7 @@ module EVM.Expr where  import Prelude hiding (LT, GT)-import Data.Bits+import Data.Bits hiding (And, Xor) import Data.DoubleWord (Int256, Word256(Word256), Word128(Word128)) import Data.Int (Int32) import Data.Word@@ -266,13 +266,16 @@ -- Attempts to read a concrete word from a buffer by reading 32 individual bytes and joining them together -- returns an abstract ReadWord expression if a concrete word cannot be constructed readWordFromBytes :: Expr EWord -> Expr Buf -> Expr EWord+readWordFromBytes (Lit idx) (ConcreteBuf bs) =+  case toInt idx of+    Nothing -> Lit 0+    Just i -> Lit $ word $ padRight 32 $ BS.take 32 $ BS.drop i bs readWordFromBytes i@(Lit idx) buf = let     bytes = [readByte (Lit i') buf | i' <- [idx .. idx + 31]]   in if Prelude.and . (fmap isLitByte) $ bytes      then Lit (bytesToW256 . mapMaybe unlitByte $ bytes)      else ReadWord i buf readWordFromBytes idx buf = ReadWord idx buf-  {- | Copies a slice of src into dst. 

@@ -54,7 +54,6 @@ import qualified Data.ByteString.Char8 as Char8 import qualified Data.Map as Map import qualified Data.Set as Set-import qualified Data.Vector as V  -- We treat everything as ASCII byte strings because -- we only use hex digits (and the letter 'x').@@ -159,7 +158,7 @@ apply1 vm fact =   case fact of     CodeFact    {..} -> flip execState vm $ do-      assign (env . contracts . at addr) (Just (EVM.initialContract (EVM.RuntimeCode (V.fromList $ LitByte <$> BS.unpack blob))))+      assign (env . contracts . at addr) (Just (EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode blob))))       when (view (state . contract) vm == addr) $ EVM.loadContract addr     StorageFact {..} ->       vm & over (env . storage) (writeStorage (litAddr addr) (Lit which) (Lit what))@@ -172,7 +171,7 @@ apply2 vm fact =   case fact of     CodeFact    {..} -> flip execState vm $ do-      assign (cache . fetchedContracts . at addr) (Just (EVM.initialContract (EVM.RuntimeCode (V.fromList $ LitByte <$> BS.unpack blob))))+      assign (cache . fetchedContracts . at addr) (Just (EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode blob))))       when (view (state . contract) vm == addr) $ EVM.loadContract addr     StorageFact {..} -> let         store = view (cache . fetchedStorage) vm

@@ -6,7 +6,7 @@ import Prelude hiding (Word)  import EVM.ABI-import EVM.Types    (Addr, W256, hexText, Expr(Lit, LitByte), Expr(..), Prop(..), (.&&), (./=))+import EVM.Types    (Addr, W256, hexText, Expr(Lit), Expr(..), Prop(..), (.&&), (./=)) import EVM.SMT import EVM          (EVM, Contract, Block, initialContract, nonce, balance, external) import qualified EVM.FeeSchedule as FeeSchedule@@ -29,7 +29,6 @@ import System.Process  import qualified Network.Wreq.Session as Session-import qualified Data.Vector as V import Numeric.Natural (Natural)  -- | Abstract representation of an RPC fetch request@@ -143,7 +142,7 @@   theBalance <- MaybeT $ fetch (QueryBalance addr)    return $-    initialContract (EVM.RuntimeCode (V.fromList $ LitByte <$> BS.unpack theCode))+    initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode theCode))       & set nonce    theNonce       & set balance  theBalance       & set external True@@ -203,7 +202,7 @@     -- we generate a new array to the fetched contract here     EVM.PleaseFetchContract addr continue -> do       contract <- case info of-                    Nothing -> return $ Just $ initialContract (EVM.RuntimeCode mempty)+                    Nothing -> return $ Just $ initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode ""))                     Just (n, url) -> fetchContractFrom n url addr       case contract of         Just x -> return $ continue x

@@ -1,466 +0,0 @@-module EVM.Flatten (flatten) where---- This module concatenates all the imported dependencies--- of a given source file, so that you can paste the result--- into Remix or the Etherscan contract verification page.------ The concatenated files are stripped of import directives--- and compiler version pragmas are merged into just one.------ This module is mostly independent from the rest of Hevm,--- using only the source code metadata support modules.--import EVM.Dapp (DappInfo, dappSources)-import EVM.Types (regexMatches)-import EVM.Solidity (sourceAsts)-import EVM.Demand (demand)---- We query and alter the Solidity code using the compiler's AST.--- The AST is a deep JSON structure, so we use Aeson and Lens.-import Control.Lens (preview, view, universe)-import Data.Aeson (Value (String))-import Data.Aeson.Lens (key, _String, _Array, _Integer)---- We use the FGL graph library for the topological sort.--- (We use four FGL functions and they're all in different modules!)-import qualified Data.Graph.Inductive.Graph as Fgl-import qualified Data.Graph.Inductive.PatriciaTree as Fgl-import qualified Data.Graph.Inductive.Query.BFS as Fgl-import qualified Data.Graph.Inductive.Query.DFS as Fgl---- The Solidity version pragmas can be arbitrary SemVer ranges,--- so we use this library to parse them.-import Data.SemVer (SemVerRange, parseSemVerRange)-import qualified Data.SemVer as SemVer--import Control.Monad (forM)-import Data.ByteString (ByteString)-import Data.Foldable (foldl', toList)-import Data.List (sort, nub, (\\))-import Data.Map (Map, (!), (!?))-import Data.Maybe (mapMaybe, isJust, catMaybes, fromMaybe)-import Data.Text (Text, unpack, pack, intercalate)-import Data.Text.Encoding (encodeUtf8, decodeUtf8)-import Text.Read (readMaybe)--import qualified Data.Map as Map-import qualified Data.Text as Text-import qualified Data.ByteString as BS---- Define an alias for FGL graphs with text nodes and unlabeled edges.-type FileGraph = Fgl.Gr Text ()---- | Get field either inside 'attributes' object (combined-json format)--- or directly.-getAttribute :: Text -> Value -> Maybe Value-getAttribute s v = case preview (key "attributes" . key s) v of-  Nothing -> preview (key s) v-  Just r  -> Just r---- Given the AST of a source file, resolve all its imported paths.-importsFrom :: Value -> [Text]-importsFrom ast =-  let-    -- We use the astonishing `universe` function from Lens-    -- to get a lazy list of every node in the AST structure.-    allNodes :: [Value]-    allNodes = universe ast--    -- Given some subvalue in the AST, we check if it's an import,-    -- and if so, return its resolved import path.-    resolveImport :: Value -> Maybe Text-    resolveImport node =-      case preview (key "nodeType") node of-        Just (String "ImportDirective") -> view _String <$> getAttribute "absolutePath" node-        _ ->-          case preview (key "name") node of-            Just (String "ImportDirective") ->-              view _String <$> getAttribute "absolutePath" node-            _ ->-              Nothing--  -- Now we just try to resolve import paths at all subnodes.-  in mapMaybe resolveImport allNodes--flatten :: DappInfo -> Text -> IO ()-flatten dapp target = do-  let-    -- The nodes and edges are defined below.-    graph :: FileGraph-    graph = Fgl.mkGraph nodes edges--    -- The graph nodes are ints with source paths as labels.-    nodes :: [(Int, Text)]-    nodes = zip [1..] (Map.keys asts)--    -- The graph edges are defined by module imports.-    edges =-      [ (indices ! s, indices ! t, ()) -- Edge from S to T-      | (s, v) <- Map.toList asts      -- for every file S-      , t      <- importsFrom v ]      -- and every T imported by S.--    -- We can look up the node index for a source file path.-    indices :: Map Text Int-    indices = Map.fromList [(v, k) | (k, v) <- nodes]--    -- The JSON ASTs are indexed by source file path.-    asts :: Map Text Value-    asts = view (dappSources . sourceAsts) dapp--    topScopeIds :: [Integer]-    topScopeIds = mconcat $ fmap f $ Map.elems asts-      where-        id' = preview (key "id" . _Integer)-        f ast =-          [ fromJust' "no id for SourceUnit" $ id' node-          | node <- universe ast-          , nodeIs "SourceUnit" node-          ]--    contractsAndStructsToRename :: Map Integer Text-    contractsAndStructsToRename =-      Map.fromList-        $ indexed [ x | x <- xs, (snd x) `elem` xs' ]-      where-        xs = concatMap f $ Map.elems asts-        xs' = repeated $ fmap snd xs-        scope x = getAttribute "scope" x >>= preview _Integer-        name x = getAttribute "name" x >>= preview _String-        id' = preview (key "id" . _Integer)-        p x = (nodeIs "ContractDefinition" x || nodeIs "StructDefinition" x)-          && (fromJust' "no contract/struct scope" $ scope x) `elem` topScopeIds-        f ast =-          [ ( fromJust' "no id for top scoped contract or struct" $ id' node-            , fromJust' "no id for top scoped contract or struct" $ name node-            )-          | node <- universe ast-          , p node-          ]--    contractStructs :: [(Integer, (Integer, Text))]-    contractStructs = mconcat $ fmap f $ Map.elems asts-      where-        scope x = getAttribute "scope" x >>= preview _Integer-        cname x = getAttribute "canonicalName" x >>= preview _String-        id' = preview (key "id" . _Integer)-        p x = (nodeIs "StructDefinition" x)-          && (fromJust' "nested struct" $ scope x) `Map.member` contractsAndStructsToRename-        f ast =-          [ let-              id'' = fromJust' "no id for nested struct" $ id' node-              cname' = fromJust'-                ("no canonical name of nested struct with id:" ++ show id'') $ cname node-              ref = fromJust'-                ("no scope of nested struct with id:" ++ show id'') $ scope node-            in-              (id'', (ref, cname'))-          | node <- universe ast-          , p node-          ]--  -- We use the target source file to make a relevant subgraph-  -- with only files transitively depended on from the target.-  case Map.lookup target indices of-    Nothing ->-      error "didn't find contract AST"-    Just root -> do-      let-        -- Restrict the graph to only the needed nodes,-        -- discovered via breadth-first search from the target.-        subgraph :: Fgl.Gr Text ()-        subgraph = Fgl.subgraph (Fgl.bfs root graph) graph--        -- Now put the source file paths in the right order-        -- by sorting topologically.-        ordered :: [Text]-        ordered = reverse (Fgl.topsort' subgraph)--        -- Take the highest Solidity version from all pragmas.-        pragma :: Text-        pragma = maximalPragma (Map.elems (Map.filterWithKey (\k _ -> k `elem` ordered) asts))--        license :: Text-        license = joinLicenses (Map.elems (Map.filterWithKey (\k _ -> k `elem` ordered) asts))-      -- Read the source files in order and strip unwanted directives.-      -- Also add an informative comment with the original source file path.-      sources <--        forM ordered $ \path -> do-          src <- BS.readFile (unpack path)-          pure $ mconcat-            [ "////// ", encodeUtf8 path, "\n"-            -- Fold over a list of source transforms-            , fst-                (prefixContractAst-                  contractsAndStructsToRename-                  contractStructs-                  (stripImportsAndPragmas (stripLicense src) (asts ! path))-                  (asts ! path))-            , "\n"-            ]--      -- Force all evaluation before any printing happens, to avoid-      -- partial output.-      demand target; demand pragma; demand sources--      -- Finally print the whole concatenation.-      putStrLn $ "// hevm: flattened sources of " <> unpack target-      putStrLn (unpack license)-      putStrLn (unpack pragma)-      BS.putStr (mconcat sources)--joinLicenses :: [Value] -> Text-joinLicenses asts =-  case nub $ mapMaybe (\ast -> getAttribute "license" ast >>= preview _String) asts of-    [] -> ""-    x -> "// SPDX-License-Identifier: " <> intercalate " AND " x---- | Construct a new Solidity version pragma for the highest mentioned version---  given a list of source file ASTs.-maximalPragma :: [Value] -> Text-maximalPragma asts = (-    case mapMaybe versions asts of-      [] -> "" -- allow for no pragma-      xs ->-        "pragma solidity "-          <> pack (show (rangeIntersection xs))-          <> ";\n"-  )-  <> (-    mconcat . nub . sort . fmap (\ast ->-      mconcat $ fmap-        (\xs -> "pragma "-          <> intercalate " " [x | String x <- xs]-          <> ";\n")-        (otherPragmas ast)-    )-  ) asts---  where-    isVersionPragma :: [Value] -> Bool-    isVersionPragma (String "solidity" : _) = True-    isVersionPragma _ = False--    pragmaComponents :: Value -> [[Value]]-    pragmaComponents ast = components-      where-        ps :: [Value]-        ps = filter (nodeIs "PragmaDirective") (universe ast)--        components :: [[Value]]-        components = catMaybes $-          fmap-          ((fmap toList) . (\x -> getAttribute "literals" x >>= preview _Array))-          ps--    -- Simple way to combine many SemVer ranges.  We don't actually-    -- optimize these boolean expressions, so the resulting pragma-    -- might be redundant, like ">=0.4.23 >=0.5.0 <0.6.0".-    rangeIntersection :: [SemVerRange] -> SemVerRange-    rangeIntersection = foldr1 SemVer.And . nub . sort--    -- Get the semantic version range from a source file's pragma,-    -- or nothing if no pragma present.-    versions :: Value -> Maybe SemVerRange-    versions ast = fmap grok components-      where-        components :: Maybe [Value]-        components =-          case filter isVersionPragma (pragmaComponents ast) of-            [_:xs] -> Just xs-            []  -> Nothing-            x   -> error $ "multiple version pragmas" ++ show x--        grok :: [Value] -> SemVerRange-        grok xs =-          let-            rangeText = mconcat [x | String x <- xs]-          in-            case parseSemVerRange rangeText of-              Right r -> r-              Left _ ->-                error ("failed to parse SemVer range " ++ show rangeText)--    otherPragmas :: Value -> [[Value]]-    otherPragmas = (filter (not . isVersionPragma)) . pragmaComponents--nodeIs :: Text -> Value -> Bool-nodeIs t x = isSourceNode && hasRightName-  where-    isSourceNode =-      isJust (preview (key "src") x)-    hasRightName =-      Just t == preview (key "name" . _String) x-      || Just t == preview (key "nodeType" . _String) x---- | Removes all lines containing "SPDX-License-Identifier"-stripLicense :: ByteString -> (ByteString, Int)-stripLicense bs =-  (encodeUtf8 $ Text.unlines (lines' \\ licenseLines), - sum (((1 +) . Text.length) <$> licenseLines))-  where lines' = Text.lines $ decodeUtf8 bs-        licenseLines = filter (regexMatches "SPDX-License-Identifier") lines'---- | (bytes, offset) where offset is added or incremeneted as text is--- inserted or removed from the source file-stripImportsAndPragmas :: (ByteString, Int) -> Value -> (ByteString, Int)-stripImportsAndPragmas bso ast = stripAstNodes bso ast p-  where-    p x = nodeIs "ImportDirective" x || nodeIs "PragmaDirective" x--stripAstNodes :: (ByteString, Int)-> Value -> (Value -> Bool) -> (ByteString, Int)-stripAstNodes bso ast p =-  cutRanges [sourceRange node | node <- universe ast, p node]--  where-    -- Removes a set of non-overlapping ranges from a bytestring-    -- by commenting them out.-    cutRanges :: [(Int, Int)] -> (ByteString, Int)-    cutRanges (sort -> rs) = foldl' f bso rs-      where-        f (bs', n) (i, j) =-          ( cut bs' (i + n) (j + n)-          , n + length ("/*  */" :: String))--    -- Comments out the bytes between two indices from a bytestring.-    cut :: ByteString -> Int -> Int -> ByteString-    cut x i j =-      let (a, b) = BS.splitAt i x-      in a <> "/* " <> BS.take (j - i) b <> " */" <> BS.drop (j - i) b--readAs :: Read a => Text -> Maybe a-readAs = readMaybe . Text.unpack--prefixContractAst :: Map Integer Text -> [(Integer, (Integer, Text))] -> (ByteString, Int) -> Value -> (ByteString, Int)-prefixContractAst castr cs bso ast = prefixAstNodes-  where-    bs = fst bso-    refDec x = getAttribute "referencedDeclaration" x >>= preview _Integer-    name x = getAttribute "name" x >>= preview _String-    id' = preview (key "id" . _Integer)--    -- Is node top level defined type (contract/interface/struct)-    p x = (nodeIs "ContractDefinition" x || nodeIs "StructDefinition" x)-      && (fromJust' "id of any" $ id' x) `Map.member` castr--    -- Is node identifier that is referencing top level defined type-    p' x =-      (nodeIs "Identifier" x || nodeIs "UserDefinedTypeName" x)-        && (isJust $ refDec x) && (fromJust' "refDec of ident/userdef" $ refDec x) `Map.member` castr--    -- Is node identifier that is referencing a struct nested in a top level-    -- defined contract/interface-    p'' x =-      (nodeIs "Identifier" x || nodeIs "UserDefinedTypeName" x)-      && (isJust $ name x)-      && (-        let-          refs = fmap fst cs-          i = fromJust' "no id for ident/userdef" $ id' x-          ref = fromJust' ("no refDec for ident/userdef: " ++ show i) $ refDec x-          n = fromJust' ("no name for ident/userdef: " ++ show i) $ name x-          cn = fromJust'-            ("no match for lookup in nested structs: "-              ++ show i-              ++ " -> "-              ++ show ref-            ) $ lookup ref cs-        in-          -- XXX: comparing canonical name with name of nested structs-          -- might not be super great-          ref `elem` refs && n == snd cn-      )--    p''' x = p x || p' x || p'' x--    prefixAstNodes :: (ByteString, Int)-    prefixAstNodes  =-      cutRanges [sourceId node | node <- universe ast, p''' node]--    -- Parses the `id` and `attributes.referencedDeclaration` field of an AST node-    -- into a pair of byte indices.-    sourceId :: Value -> (Int, Integer)-    sourceId v =-      if (not $ p v || p' v) &&  p'' v then (-        let-          ref = fromJust' "refDec of nested struct ref" $ refDec v-          cn = fromJust' "no match for lookup in nested structs" $ lookup ref cs-        in-          (end, fst cn)-      ) else-        fromJust' "internal error: no id found for contract reference" x--      where-        (start, end) = sourceRange v-        f :: Text -> Maybe (Int, Integer)-        f t | t `elem` ["ContractDefinition", "StructDefinition"] =-              let-                name' = encodeUtf8 $ fromJust' "no name for contract/struct" $ name v-                bs' = snd $ BS.splitAt (start + snd bso) bs-                pos = start-                  + (BS.length $ fst $ BS.breakSubstring name' bs')-                  + (BS.length name')-              in-                fmap ((,) pos) $ id' v-            | t `elem` ["UserDefinedTypeName", "Identifier"] =-              fmap ((,) end) $ refDec v-            | otherwise =-                error $ "internal error: not a contract reference: " ++ show t--        x :: Maybe (Int, Integer)-        x = case preview (key "nodeType" . _String) v of-          Just t -> f t-          Nothing -> case preview (key "name" . _String) v of-            Just t -> f t-            Nothing ->-              error "internal error: not a contract reference"--    -- Prefix a set of non-overlapping ranges from a bytestring-    -- by commenting them out.-    cutRanges :: [(Int, Integer)] -> (ByteString, Int)-    cutRanges (sort -> rs) = foldl' f bso rs-      where-        f (bs', n) (i, t) =-          let-            t' = "_" <> (castr ! t)-          in-            ( prefix t' bs' (i + n)-            , n + Text.length t' )--    -- Comments out the bytes between two indices from a bytestring.-    prefix :: Text -> ByteString -> Int -> ByteString-    prefix t x i =-      let (a, b) = BS.splitAt i x-      in a <> encodeUtf8 t <> b---- Parses the `src` field of an AST node into a pair of byte indices.-sourceRange :: Value -> (Int, Int)-sourceRange v =-  case preview (key "src" . _String) v of-    Just (Text.splitOn ":" -> [readAs -> Just i, readAs -> Just n, _]) ->-      (i, i + n)-    _ ->-      error "internal error: no source position for AST node"--fromJust' :: String -> Maybe a -> a-fromJust' msg = \case-  Just x -> x-  Nothing -> error msg--repeated :: Eq a => [a] -> [a]-repeated = fmap fst $ foldl' f ([], [])-  where-    f (acc, seen) x =-      ( if (x `elem` seen) && (not $ x `elem` acc)-        then x : acc-        else acc-      , x : seen-      )--indexed :: [(Integer, Text)] -> [(Integer, Text)]-indexed = fst . foldl' f ([], Map.empty) -- (zip (fmap snd xs) $ replicate (length xs) 0) xs-  where-    f (acc, seen) (id', n) =-      let-        count = (fromMaybe 0 $ seen !? n) + 1-      in-        ((id', pack $ show count) : acc, Map.insert n count seen)

@@ -6,8 +6,10 @@   ( formatExpr   , contractNamePart   , contractPathPart+  , showError   , showTree   , showTraceTree+  , showValues   , prettyvmresult   , showCall   , showWordExact@@ -31,7 +33,7 @@ import EVM (VM, cheatCode, traceForest, traceData, Error (..)) import EVM (Trace, TraceData (..), Query (..), FrameContext (..)) import EVM.Types (maybeLitWord, W256 (..), num, word, Expr(..), EType(..))-import EVM.Types (Addr, ByteStringS(..))+import EVM.Types (Addr, ByteStringS(..), Error(..)) import EVM.ABI (AbiValue (..), Event (..), AbiType (..), SolError (..)) import EVM.ABI (Indexed (NotIndexed), getAbiSeq) import EVM.ABI (parseTypeName, formatString)@@ -48,7 +50,7 @@ import Data.ByteString.Lazy (toStrict, fromStrict) import Data.DoubleWord (signedWord) import Data.Foldable (toList)-import Data.Maybe (catMaybes, fromMaybe)+import Data.Maybe (catMaybes, fromMaybe, fromJust) import Data.Text (Text, pack, unpack, intercalate) import Data.Text (dropEnd, splitOn) import Data.Text.Encoding (decodeUtf8, decodeUtf8')@@ -68,20 +70,17 @@   deriving (Show)  showDec :: Signedness -> W256 -> Text-showDec signed (W256 w) =-  let+showDec signed (W256 w)+  | i == num cheatCode = "<hevm cheat address>"+  | (i :: Integer) == 2 ^ (256 :: Integer) - 1 = "MAX_UINT256"+  | otherwise = Text.pack (show (i :: Integer))+  where     i = case signed of           Signed   -> num (signedWord w)           Unsigned -> num w-  in-    if i == num cheatCode-    then "<hevm cheat address>"-    else if (i :: Integer) == 2 ^ (256 :: Integer) - 1-    then "MAX_UINT256"-    else Text.pack (show (i :: Integer))  showWordExact :: W256 -> Text-showWordExact w = humanizeInteger w+showWordExact w = humanizeInteger (toInteger w)  showWordExplanation :: W256 -> DappInfo -> Text showWordExplanation w _ | w > 0xffffffff = showDec Unsigned w@@ -318,7 +317,7 @@       let calltype = if target == context                      then "call "                      else "delegatecall "-          Lit hash' = hash -- FIXME: irrefutable pattern, handle symbolic+          hash' = fromJust $ maybeLitWord hash       in case preview (dappSolcByHash . ix hash' . _2) dapp of         Nothing ->           calltype@@ -372,18 +371,27 @@ contractPathPart :: Text -> Text contractPathPart x = Text.split (== ':') x !! 0 +prettyError :: EVM.Types.Error -> String+prettyError= \case+  Invalid -> "Invalid Opcode"+  EVM.Types.IllegalOverflow -> "Illegal Overflow"+  SelfDestruct -> "Self Destruct"+  EVM.Types.StackLimitExceeded -> "Stack limit exceeded"+  EVM.Types.InvalidMemoryAccess -> "Invalid memory access"+  EVM.Types.BadJumpDestination -> "Bad jump destination"+  TmpErr err -> "Temp error: " <> err++ prettyvmresult :: (?context :: DappContext) => Expr End -> String prettyvmresult (EVM.Types.Revert _ (ConcreteBuf "")) = "Revert" prettyvmresult (EVM.Types.Revert _ msg) = "Revert: " ++ (unpack $ showError msg)-prettyvmresult (EVM.Types.Invalid _) = "Invalid Opcode" prettyvmresult (EVM.Types.Return _ (ConcreteBuf msg) _) =   if BS.null msg   then "Stop"   else "Return: " <> show (ByteStringS msg) prettyvmresult (EVM.Types.Return _ _ _) =   "Return: <symbolic>"-prettyvmresult (EVM.Types.IllegalOverflow _) = "Illegal Overflow"-prettyvmresult (EVM.Types.SelfDestruct _) = "Self Destruct"+prettyvmresult (Failure _ err) = prettyError err prettyvmresult e = error "Internal Error: Invalid Result: " <> show e  indent :: Int -> Text -> Text

@@ -25,7 +25,6 @@ import Data.Word import Numeric (readHex) import Data.ByteString (ByteString)-import Data.Maybe (fromMaybe)  import qualified Data.ByteString as BS import qualified Data.List as List@@ -785,10 +784,10 @@   t -> error $ "Internal Error: cannot parse " <> t <> " into an Expr"  getVars :: (TS.Text -> Expr EWord) -> SolverInstance -> [TS.Text] -> IO (Map (Expr EWord) W256)-getVars parseFn inst names = Map.mapKeys parseFn <$> foldM getVar mempty names+getVars parseFn inst names = Map.mapKeys parseFn <$> foldM getOne mempty names   where-    getVar :: Map TS.Text W256 -> TS.Text -> IO (Map TS.Text W256)-    getVar acc name = do+    getOne :: Map TS.Text W256 -> TS.Text -> IO (Map TS.Text W256)+    getOne acc name = do       raw <- getValue inst (T.fromStrict name)       let         parsed = case parseCommentFreeFileMsg getValueRes (T.toStrict raw) of

@@ -47,6 +47,7 @@   , sourceFiles   , sourceLines   , sourceAsts+  , immutableReferences   , stripBytecodeMetadata   , stripBytecodeMetadataSym   , signature@@ -94,6 +95,7 @@ import System.Process import Text.Read            (readMaybe) +import qualified Data.Aeson.Key as Key import qualified Data.ByteString        as BS import qualified Data.ByteString.Base16 as BS16 import qualified Data.HashMap.Strict    as HMap@@ -131,7 +133,9 @@  instance Read SlotType where   readsPrec _ ('m':'a':'p':'p':'i':'n':'g':'(':s) =-    let (lhs:rhs) = Text.splitOn " => " (pack s)+    let (lhs,rhs) = case Text.splitOn " => " (pack s) of+          (l:r) -> (l,r)+          _ -> error "could not parse storage item"         first = fromJust $ parseTypeName mempty lhs         target = fromJust $ parseTypeName mempty (Text.replace ")" "" (last rhs))         rest = fmap (fromJust . (parseTypeName mempty . (Text.replace "mapping(" ""))) (take (length rhs - 1) rhs)@@ -303,35 +307,35 @@ yul :: Text -> Text -> IO (Maybe ByteString) yul contract src = do   (json, path) <- yul' src-  let (Just f) = json ^?! key "contracts" ^? key path-      (Just c) = f ^? key (if Text.null contract then "object" else contract)+  let f = (json ^?! key "contracts") ^?! key (Key.fromText path)+      c = f ^?! key (Key.fromText $ if Text.null contract then "object" else contract)       bytecode = c ^?! key "evm" ^?! key "bytecode" ^?! key "object" . _String   pure $ toCode <$> (Just bytecode)  yulRuntime :: Text -> Text -> IO (Maybe ByteString) yulRuntime contract src = do   (json, path) <- yul' src-  let (Just f) = json ^?! key "contracts" ^? key path-      (Just c) = f ^? key (if Text.null contract then "object" else contract)+  let f = (json ^?! key "contracts") ^?! key (Key.fromText path)+      c = f ^?! key (Key.fromText $ if Text.null contract then "object" else contract)       bytecode = c ^?! key "evm" ^?! key "deployedBytecode" ^?! key "object" . _String   pure $ toCode <$> (Just bytecode)  solidity :: Text -> Text -> IO (Maybe ByteString) solidity contract src = do   (json, path) <- solidity' src-  let Just (sol, _, _) = readJSON json+  let (sol, _, _) = fromJust $ readJSON json   return (sol ^? ix (path <> ":" <> contract) . creationCode)  solcRuntime :: Text -> Text -> IO (Maybe ByteString) solcRuntime contract src = do   (json, path) <- solidity' src-  let Just (sol, _, _) = readJSON json+  let (sol, _, _) = fromJust $ readJSON json   return (sol ^? ix (path <> ":" <> contract) . runtimeCode)  functionAbi :: Text -> IO Method functionAbi f = do   (json, path) <- solidity' ("contract ABI { function " <> f <> " public {}}")-  let Just (sol, _, _) = readJSON json+  let (sol, _, _) = fromJust $ readJSON json   case Map.toList $ sol ^?! ix (path <> ":ABI") . abiMap of      [(_,b)] -> return b      _ -> error "hevm internal error: unexpected abi format"@@ -347,11 +351,11 @@ -- deprecate me soon readCombinedJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)]) readCombinedJSON json = do-  contracts <- f <$> (json ^? key "contracts" . _Object)+  contracts <- f . KeyMap.toHashMapText <$> (json ^? key "contracts" . _Object)   sources <- toList . fmap (view _String) <$> json ^? key "sourceList" . _Array   return (contracts, Map.fromList (HMap.toList asts), [ (x, Nothing) | x <- sources])   where-    asts = fromMaybe (error "JSON lacks abstract syntax trees.") (json ^? key "sources" . _Object)+    asts = KeyMap.toHashMapText $ fromMaybe (error "JSON lacks abstract syntax trees.") (json ^? key "sources" . _Object)     f x = Map.fromList . HMap.toList $ HMap.mapWithKey g x     g s x =       let@@ -378,9 +382,9 @@  readStdJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)]) readStdJSON json = do-  contracts <- json ^? key "contracts" ._Object+  contracts <- KeyMap.toHashMapText <$> json ^? key "contracts" ._Object   -- TODO: support the general case of "urls" and "content" in the standard json-  sources <- json ^? key "sources" . _Object+  sources <- KeyMap.toHashMapText <$>  json ^? key "sources" . _Object   let asts = force "JSON lacks abstract syntax trees." . preview (key "ast") <$> sources       contractMap = f contracts       contents src = (src, encodeUtf8 <$> HMap.lookup src (mconcat $ Map.elems $ snd <$> contractMap))@@ -388,7 +392,7 @@   where     f :: (AsValue s) => HMap.HashMap Text s -> (Map Text (SolcContract, (HMap.HashMap Text Text)))     f x = Map.fromList . (concatMap g) . HMap.toList $ x-    g (s, x) = h s <$> HMap.toList (view _Object x)+    g (s, x) = h s <$> HMap.toList (KeyMap.toHashMapText (view _Object x))     h :: Text -> (Text, Value) -> (Text, (SolcContract, HMap.HashMap Text Text))     h s (c, x) =       let@@ -399,7 +403,7 @@         theCreationCode = toCode $ fromMaybe "" $ creation ^? key "object" . _String         srcContents :: Maybe (HMap.HashMap Text Text)         srcContents = do metadata <- x ^? key "metadata" . _String-                         srcs <- metadata ^? key "sources" . _Object+                         srcs <- KeyMap.toHashMapText <$> metadata ^? key "sources" . _Object                          return $ (view (key "content" . _String)) <$> (HMap.filter (isJust . preview (key "content")) srcs)         abis = force ("abi key not found in " <> show x) $           toList <$> x ^? key "abi" . _Array@@ -498,7 +502,7 @@     do name <- item ^? key "label" . _String        offset <- item ^? key "offset" . _Number >>= toBoundedInteger        slot <- item ^? key "slot" . _String-       typ <- item ^? key "type" . _String+       typ <- Key.fromText <$> item ^? key "type" . _String        slotType <- types ^?! key typ ^? key "label" . _String        return (name, StorageItem (read $ Text.unpack slotType) offset (read $ Text.unpack slot))) @@ -688,7 +692,7 @@     candidates = (flip Data.List.isInfixOf concretes) <$> bzzrs   in case elemIndex True candidates of     Nothing -> b-    Just i -> let Just ind = infixIndex (bzzrs !! i) concretes+    Just i -> let ind = fromJust $ infixIndex (bzzrs !! i) concretes               in take ind b  infixIndex :: (Eq a) => [a] -> [a] -> Maybe Int

@@ -173,7 +173,7 @@               ConcreteS -> ConcreteStore mempty     caller' = Caller 0     value' = CallValue 0-    code' = RuntimeCode $ fromJust $ Expr.toList (ConcreteBuf contractCode)+    code' = RuntimeCode (ConcreteRuntimeCode contractCode)     vm' = loadSymVM code' store caller' value' calldata' calldataProps     precond = case maybepre of                 Nothing -> []@@ -346,14 +346,14 @@     Nothing -> error "Internal Error: vm in intermediate state after call to runFully"     Just (VMSuccess buf) -> Return asserts buf (view (env . EVM.storage) vm)     Just (VMFailure e) -> case e of-      UnrecognizedOpcode _ -> Invalid asserts-      SelfDestruction -> SelfDestruct asserts-      EVM.StackLimitExceeded -> EVM.Types.StackLimitExceeded asserts-      EVM.IllegalOverflow -> EVM.Types.IllegalOverflow asserts+      UnrecognizedOpcode _ -> Failure asserts Invalid+      SelfDestruction -> Failure asserts SelfDestruct+      EVM.StackLimitExceeded -> Failure asserts EVM.Types.StackLimitExceeded+      EVM.IllegalOverflow -> Failure asserts EVM.Types.IllegalOverflow       EVM.Revert buf -> EVM.Types.Revert asserts buf-      EVM.InvalidMemoryAccess -> EVM.Types.InvalidMemoryAccess asserts-      EVM.BadJumpDestination -> EVM.Types.BadJumpDestination asserts-      e' -> EVM.Types.TmpErr asserts $ show e'+      EVM.InvalidMemoryAccess -> Failure asserts EVM.Types.InvalidMemoryAccess+      EVM.BadJumpDestination -> Failure asserts EVM.Types.BadJumpDestination+      e' -> Failure asserts $ EVM.Types.TmpErr (show e')  -- | Converts a given top level expr into a list of final states and the associated path conditions for each state flattenExpr :: Expr End -> [([Prop], Expr End)]@@ -362,15 +362,10 @@     go :: [Prop] -> Expr End -> [([Prop], Expr End)]     go pcs = \case       ITE c t f -> go (PNeg ((PEq c (Lit 0))) : pcs) t <> go (PEq c (Lit 0) : pcs) f-      e@(Invalid _)  -> [(pcs, e)]-      e@(SelfDestruct _) -> [(pcs, e)]       e@(Revert _ _) -> [(pcs, e)]       e@(Return _ _ _) -> [(pcs, e)]-      e@(EVM.Types.IllegalOverflow _) -> [(pcs, e)]-      e@(EVM.Types.StackLimitExceeded _ ) -> [(pcs, e)]-      e@(EVM.Types.InvalidMemoryAccess _) -> [(pcs, e)]-      e@(EVM.Types.BadJumpDestination _) -> [(pcs, e)]-      TmpErr _ s -> error s+      Failure _ (TmpErr s) -> error s+      e@(Failure _ _) -> [(pcs, e)]       GVar _ -> error "cannot flatten an Expr containing a GVar"  -- | Strips unreachable branches from a given expr@@ -413,6 +408,7 @@           Unsat -> pure ([query], Nothing)           r -> error $ "Invalid solver result: " <> show r + -- | Evaluate the provided proposition down to its most concrete result evalProp :: Prop -> Prop evalProp = \case@@ -450,15 +446,9 @@ extractProps :: Expr End -> [Prop] extractProps = \case   ITE _ _ _ -> []-  Invalid asserts -> asserts-  SelfDestruct asserts -> asserts   Revert asserts _ -> asserts   Return asserts _ _ -> asserts-  EVM.Types.IllegalOverflow asserts -> asserts-  EVM.Types.StackLimitExceeded asserts -> asserts-  EVM.Types.InvalidMemoryAccess asserts -> asserts-  EVM.Types.BadJumpDestination asserts -> asserts-  TmpErr asserts _ -> asserts+  Failure asserts _ -> asserts   GVar _ -> error "cannot extract props from a GVar"  @@ -538,14 +528,13 @@             (Revert _ a, Revert _ b) -> if a==b then PBool False else a ./= b             (Revert _ _, _) -> PBool True             (_, Revert _ _) -> PBool True-            (Invalid _, Invalid _) -> PBool False-            (Invalid _, _ ) -> PBool True-            (_, Invalid _) -> PBool True-            (EVM.Types.StackLimitExceeded _, EVM.Types.StackLimitExceeded _ ) -> PBool False-            (EVM.Types.StackLimitExceeded _, _) -> PBool True-            (_, EVM.Types.StackLimitExceeded _) -> PBool True-            (a, b) -> if a == b then PBool False-                                else error $ "Unimplemented, see TODO about EVM failures and TmpExpr. Left: " <> show a <> " Right: " <> show b+            (Failure _ erra, Failure _ errb) -> if erra==errb then PBool False else PBool True+            (GVar _, _) -> error "Expressions cannot contain global vars"+            (_ , GVar _) -> error "Expressions cannot contain global vars"+            (Failure _ (TmpErr s), _) -> error $ "Unhandled error: " <> s+            (_, Failure _ (TmpErr s)) -> error $ "Unhandled error: " <> s+            (ITE _ _ _, _ ) -> error "Expressions must be flattened"+            (_, ITE _ _ _) -> error "Expressions must be flattened"          -- if the SMT solver can find a common input that satisfies BOTH sets of path conditions         -- AND the output differs, then we are in trouble. We do this for _every_ pair of paths, which

@@ -41,7 +41,7 @@  import Data.Aeson.Lens import Data.ByteString (ByteString)-import Data.Maybe (isJust, fromJust, fromMaybe)+import Data.Maybe (isJust, fromJust, fromMaybe, isNothing) import Data.Map (Map, insert, lookupLT, singleton, filter) import Data.Text (Text, pack) import Data.Text.Encoding (decodeUtf8)@@ -184,7 +184,7 @@          -- Stepper wants to make a query and wait for the results?         Stepper.IOAct q -> do-          zoom uiVm (StateT (runStateT q)) >>= interpret mode . k+          Brick.zoom uiVm (StateT (runStateT q)) >>= interpret mode . k          -- Stepper wants to modify the VM.         Stepper.EVM m -> do@@ -317,13 +317,13 @@      ,?maxIter :: Maybe Integer)   => UiVmState   -> StepMode-  -> EventM n (Next UiState)+  -> EventM n UiState () takeStep ui mode =   liftIO nxt >>= \case-    (Stopped (), ui') ->-      continue (ViewVm ui')-    (Continue steps, ui') -> do-      continue (ViewVm (ui' & set uiStepper steps))+    (Stopped (), _) ->+      pure ()+    (Continue steps, ui') ->+      put (ViewVm (ui' & set uiStepper steps))   where     m = interpret mode (view uiStepper ui)     nxt = runStateT m ui@@ -331,128 +331,140 @@ backstepUntil   :: (?fetcher :: Fetcher      ,?maxIter :: Maybe Integer)-  => (UiVmState -> Pred VM) -> UiVmState -> EventM n (Next UiState)-backstepUntil p s =-  case view uiStep s of-    0 -> continue (ViewVm s)-    n -> do-      s1 <- backstep s-      let-        -- find a previous vm that satisfies the predicate-        snapshots' = Data.Map.filter (p s1 . fst) (view uiSnapshots s1)-      case lookupLT n snapshots' of-        -- If no such vm exists, go to the beginning-        Nothing ->-          let-            (step', (vm', stepper')) = fromJust $ lookupLT (n - 1) (view uiSnapshots s)-            s2 = s1-              & set uiVm vm'-              & set (uiVm . cache) (view (uiVm . cache) s1)-              & set uiStep step'-              & set uiStepper stepper'-          in takeStep s2 (Step 0)-        -- step until the predicate doesn't hold-        Just (step', (vm', stepper')) ->-          let-            s2 = s1-              & set uiVm vm'-              & set (uiVm . cache) (view (uiVm . cache) s1)-              & set uiStep step'-              & set uiStepper stepper'-          in takeStep s2 (StepUntil (not . p s1))+  => (UiVmState -> Pred VM) -> EventM n UiState ()+backstepUntil p = get >>= \case+  ViewVm s ->+    case view uiStep s of+      0 -> pure ()+      n -> do+        s1 <- liftIO $ backstep s+        let+          -- find a previous vm that satisfies the predicate+          snapshots' = Data.Map.filter (p s1 . fst) (view uiSnapshots s1)+        case lookupLT n snapshots' of+          -- If no such vm exists, go to the beginning+          Nothing ->+            let+              (step', (vm', stepper')) = fromJust $ lookupLT (n - 1) (view uiSnapshots s)+              s2 = s1+                & set uiVm vm'+                & set (uiVm . cache) (view (uiVm . cache) s1)+                & set uiStep step'+                & set uiStepper stepper'+            in takeStep s2 (Step 0)+          -- step until the predicate doesn't hold+          Just (step', (vm', stepper')) ->+            let+              s2 = s1+                & set uiVm vm'+                & set (uiVm . cache) (view (uiVm . cache) s1)+                & set uiStep step'+                & set uiStepper stepper'+            in takeStep s2 (StepUntil (not . p s1))+  _ -> pure ()  backstep   :: (?fetcher :: Fetcher      ,?maxIter :: Maybe Integer)-  => UiVmState -> EventM n UiVmState-backstep s = case view uiStep s of-  -- We're already at the first step; ignore command.-  0 -> return s-  -- To step backwards, we revert to the previous snapshot-  -- and execute n - 1 `mod` snapshotInterval steps from there.+  => UiVmState -> IO UiVmState+backstep s =+  case view uiStep s of+    -- We're already at the first step; ignore command.+    0 -> pure s+    -- To step backwards, we revert to the previous snapshot+    -- and execute n - 1 `mod` snapshotInterval steps from there. -  -- We keep the current cache so we don't have to redo-  -- any blocking queries, and also the memory view.-  n ->-    let-      (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s)-      s1 = s-        & set uiVm vm-        & set (uiVm . cache) (view (uiVm . cache) s)-        & set uiStep step-        & set uiStepper stepper-      stepsToTake = n - step - 1+    -- We keep the current cache so we don't have to redo+    -- any blocking queries, and also the memory view.+    n ->+      let+        (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s)+        s1 = s+          & set uiVm vm+          & set (uiVm . cache) (view (uiVm . cache) s)+          & set uiStep step+          & set uiStepper stepper+        stepsToTake = n - step - 1 -    in-      liftIO $ runStateT (interpret (Step stepsToTake) stepper) s1 >>= \case-        (Continue steps, ui') -> return $ ui' & set uiStepper steps-        _ -> error "unexpected end"+      in+        runStateT (interpret (Step stepsToTake) stepper) s1 >>= \case+          (Continue steps, ui') -> pure $ ui' & set uiStepper steps+          _ -> error "unexpected end"  appEvent   :: (?fetcher::Fetcher, ?maxIter :: Maybe Integer) =>-  UiState ->   BrickEvent Name e ->-  EventM Name (Next UiState)+  EventM Name UiState ()  -- Contracts: Down - list down-appEvent (ViewContracts s) (VtyEvent e@(V.EvKey V.KDown [])) = do-  s' <- handleEventLensed s-    browserContractList-    handleListEvent-    e-  continue (ViewContracts s')+appEvent (VtyEvent e@(V.EvKey V.KDown [])) = get >>= \case+  ViewContracts _s -> do+    Brick.zoom+      (_ViewContracts . browserContractList)+      (handleListEvent e)+    pure ()+  _ -> pure ()  -- Contracts: Up - list up-appEvent (ViewContracts s) (VtyEvent e@(V.EvKey V.KUp [])) = do-  s' <- handleEventLensed s-    browserContractList-    handleListEvent-    e-  continue (ViewContracts s')+-- Page: Up - scroll+appEvent (VtyEvent e@(V.EvKey V.KUp [])) = get >>= \case+  ViewContracts _s -> do+    Brick.zoom+      (_ViewContracts . browserContractList)+      (handleListEvent e)+  _ -> pure ()  -- Vm Overview: Esc - return to test picker or exit-appEvent st@(ViewVm s) (VtyEvent (V.EvKey V.KEsc [])) =-  let opts = view uiTestOpts s-      dapp' = dapp (view uiTestOpts s)-      tests = concatMap-                (debuggableTests opts)-                (view dappUnitTests dapp')-  in case tests of-    [] -> halt st-    ts ->-      continue . ViewPicker $-      UiTestPickerState-        { _testPickerList =-            list-              TestPickerPane-              (Vec.fromList-              ts)-              1-        , _testPickerDapp = dapp'-        , _testOpts = opts-        }+-- Any: Esc - return to Vm Overview or Exit+appEvent (VtyEvent (V.EvKey V.KEsc [])) = get >>= \case+  ViewVm s -> do+    let opts = s ^. uiTestOpts+        dapp' = dapp opts+        tests = concatMap (debuggableTests opts) (dapp' ^. dappUnitTests)+    case tests of+      [] -> halt+      ts ->+        put $ ViewPicker $ UiTestPickerState+          { _testPickerList = list TestPickerPane (Vec.fromList ts) 1+          , _testPickerDapp = dapp'+          , _testOpts = opts+          }+  ViewHelp s -> put (ViewVm s)+  ViewContracts s -> put (ViewVm $ s ^. browserVm)+  _ -> halt  -- Vm Overview: Enter - open contracts view-appEvent (ViewVm s) (VtyEvent (V.EvKey V.KEnter [])) =-  continue . ViewContracts $ UiBrowserState-    { _browserContractList =-        list-          BrowserPane-          (Vec.fromList (Map.toList (view (uiVm . env . contracts) s)))-          2-    , _browserVm = s-    }+-- UnitTest Picker: Enter - select from list+appEvent (VtyEvent (V.EvKey V.KEnter [])) = get >>= \case+  ViewVm s ->+    put . ViewContracts $ UiBrowserState+      { _browserContractList =+          list+            BrowserPane+            (Vec.fromList (Map.toList (view (uiVm . env . contracts) s)))+            2+      , _browserVm = s+      }+  ViewPicker s ->+    case listSelectedElement (view testPickerList s) of+      Nothing -> error "nothing selected"+      Just (_, x) -> do+        let initVm  = initialUiVmStateForTest (view testOpts s) x+        put (ViewVm initVm)+  _ -> pure ()  -- Vm Overview: m - toggle memory pane-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'm') [])) =-  continue (ViewVm (over uiShowMemory not s))+appEvent (VtyEvent (V.EvKey (V.KChar 'm') [])) = get >>= \case+  ViewVm s -> put (ViewVm $ over uiShowMemory not s)+  _ -> pure ()  -- Vm Overview: h - open help view-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'h') []))-  = continue . ViewHelp $ s+appEvent (VtyEvent (V.EvKey (V.KChar 'h') [])) = get >>= \case+  ViewVm s -> put (ViewHelp s)+  _ -> pure ()  -- Vm Overview: spacebar - read input-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar ' ') [])) =+appEvent (VtyEvent (V.EvKey (V.KChar ' ') [])) =   let     loop = do       Readline.getInputLine "% " >>= \case@@ -461,153 +473,126 @@       Readline.getInputLine "% " >>= \case         Just hey' -> Readline.outputStrLn hey'         Nothing   -> pure ()-      return (ViewVm s)-  in-    suspendAndResume $+   in do+    s <- get+    suspendAndResume $ do       Readline.runInputT Readline.defaultSettings loop+      pure s  -- todo refactor to zipper step forward -- Vm Overview: n - step-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'n') [])) =-  if isJust $ view (uiVm . result) s-  then continue (ViewVm s)-  else takeStep s (Step 1)+appEvent (VtyEvent (V.EvKey (V.KChar 'n') [])) = get >>= \case+  ViewVm s ->+    when (isNothing (s ^. uiVm . result)) $+      takeStep s (Step 1)+  _ -> pure ()  -- Vm Overview: N - step-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'N') [])) =-  if isJust $ view (uiVm . result) s-  then continue (ViewVm s)-  else takeStep s-       (StepUntil (isNextSourcePosition s))+appEvent (VtyEvent (V.EvKey (V.KChar 'N') [])) = get >>= \case+  ViewVm s ->+    when (isNothing (s ^. uiVm . result)) $+      takeStep s (StepUntil (isNextSourcePosition s))+  _ -> pure ()  -- Vm Overview: C-n - step-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'n') [V.MCtrl])) =-  if isJust $ view (uiVm . result) s-  then continue (ViewVm s)-  else takeStep s-    (StepUntil (isNextSourcePositionWithoutEntering s))+appEvent (VtyEvent (V.EvKey (V.KChar 'n') [V.MCtrl])) = get >>= \case+  ViewVm s ->+    when (isNothing (s ^. uiVm . result)) $+      takeStep s (StepUntil (isNextSourcePositionWithoutEntering s))+  _ -> pure ()  -- Vm Overview: e - step-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'e') [])) =-  if isJust $ view (uiVm . result) s-  then continue (ViewVm s)-  else takeStep s-    (StepUntil (isExecutionHalted s))+appEvent (VtyEvent (V.EvKey (V.KChar 'e') [])) = get >>= \case+  ViewVm s ->+    when (isNothing (s ^. uiVm . result)) $+      takeStep s (StepUntil (isExecutionHalted s))+  _ -> pure ()  -- Vm Overview: a - step-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'a') [])) =-      -- We keep the current cache so we don't have to redo-      -- any blocking queries.-      let-        (vm, stepper) = fromJust (Map.lookup 0 (view uiSnapshots s))-        s' = s-          & set uiVm vm-          & set (uiVm . cache) (view (uiVm . cache) s)-          & set uiStep 0-          & set uiStepper stepper+appEvent (VtyEvent (V.EvKey (V.KChar 'a') [])) = get >>= \case+  ViewVm s ->+    -- We keep the current cache so we don't have to redo+    -- any blocking queries.+    let+      (vm, stepper) = fromJust (Map.lookup 0 (view uiSnapshots s))+      s' = s+        & set uiVm vm+        & set (uiVm . cache) (view (uiVm . cache) s)+        & set uiStep 0+        & set uiStepper stepper -      in takeStep s' (Step 0)+    in takeStep s' (Step 0)+  _ -> pure ()  -- Vm Overview: p - backstep-appEvent st@(ViewVm s) (VtyEvent (V.EvKey (V.KChar 'p') [])) =-  case view uiStep s of-    0 ->-      -- We're already at the first step; ignore command.-      continue st-    n -> do-      -- To step backwards, we revert to the previous snapshot-      -- and execute n - 1 `mod` snapshotInterval steps from there.+appEvent (VtyEvent (V.EvKey (V.KChar 'p') [])) = get >>= \case+  ViewVm s ->+    case view uiStep s of+      0 ->+        -- We're already at the first step; ignore command.+        pure ()+      n -> do+        -- To step backwards, we revert to the previous snapshot+        -- and execute n - 1 `mod` snapshotInterval steps from there. -      -- We keep the current cache so we don't have to redo-      -- any blocking queries, and also the memory view.-      let-        (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s)-        s1 = s-          & set uiVm vm -- set the vm to the one from the snapshot-          & set (uiVm . cache) (view (uiVm . cache) s) -- persist the cache-          & set uiStep step-          & set uiStepper stepper-        stepsToTake = n - step - 1+        -- We keep the current cache so we don't have to redo+        -- any blocking queries, and also the memory view.+        let+          (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s)+          s1 = s+            & set uiVm vm -- set the vm to the one from the snapshot+            & set (uiVm . cache) (view (uiVm . cache) s) -- persist the cache+            & set uiStep step+            & set uiStepper stepper+          stepsToTake = n - step - 1 -      takeStep s1 (Step stepsToTake)+        takeStep s1 (Step stepsToTake)+  _ -> pure ()  -- Vm Overview: P - backstep to previous source-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'P') [])) =-  backstepUntil isNextSourcePosition s+appEvent (VtyEvent (V.EvKey (V.KChar 'P') [])) =+  backstepUntil isNextSourcePosition  -- Vm Overview: c-p - backstep to previous source avoiding CALL and CREATE-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'p') [V.MCtrl])) =-  backstepUntil isNextSourcePositionWithoutEntering s+appEvent (VtyEvent (V.EvKey (V.KChar 'p') [V.MCtrl])) =+  backstepUntil isNextSourcePositionWithoutEntering  -- Vm Overview: 0 - choose no jump-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar '0') [])) =-  case view (uiVm . result) s of-    Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->-      takeStep (s & set uiStepper (Stepper.evm (contin True) >> (view uiStepper s)))-        (Step 1)-    _ -> continue (ViewVm s)+appEvent (VtyEvent (V.EvKey (V.KChar '0') [])) = get >>= \case+  ViewVm s ->+    case view (uiVm . result) s of+      Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->+        takeStep (s & set uiStepper (Stepper.evm (contin True) >> (view uiStepper s)))+          (Step 1)+      _ -> pure ()+  _ -> pure ()  -- Vm Overview: 1 - choose jump-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar '1') [])) =-  case view (uiVm . result) s of-    Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->-      takeStep (s & set uiStepper (Stepper.evm (contin False) >> (view uiStepper s)))-        (Step 1)-    _ -> continue (ViewVm s)----- Any: Esc - return to Vm Overview or Exit-appEvent s (VtyEvent (V.EvKey V.KEsc [])) =-  case s of-    (ViewHelp x) -> overview x-    (ViewContracts x) -> overview $ view browserVm x-    _ -> halt s-  where-    overview = continue . ViewVm---- UnitTest Picker: Enter - select from list-appEvent (ViewPicker s) (VtyEvent (V.EvKey V.KEnter [])) =-  case listSelectedElement (view testPickerList s) of-    Nothing -> error "nothing selected"-    Just (_, x) -> do-      let initVm  = initialUiVmStateForTest (view testOpts s) x-      continue . ViewVm $ initVm---- UnitTest Picker: (main) - render list-appEvent (ViewPicker s) (VtyEvent e) = do-  s' <- handleEventLensed s-    testPickerList-    handleListEvent-    e-  continue (ViewPicker s')---- Page: Down - scroll-appEvent (ViewVm s) (VtyEvent (V.EvKey V.KDown [])) =-  if view uiShowMemory s then-    vScrollBy (viewportScroll TracePane) 1 >> continue (ViewVm s)-  else-    if isJust $ view (uiVm . result) s-    then continue (ViewVm s)-    else takeStep s-         (StepUntil (isNewTraceAdded s))---- Page: Up - scroll-appEvent (ViewVm s) (VtyEvent (V.EvKey V.KUp [])) =-  if view uiShowMemory s then-    vScrollBy (viewportScroll TracePane) (-1) >> continue (ViewVm s)-  else-    backstepUntil isNewTraceAdded s+appEvent (VtyEvent (V.EvKey (V.KChar '1') [])) = get >>= \case+  ViewVm s ->+    case view (uiVm . result) s of+      Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->+        takeStep (s & set uiStepper (Stepper.evm (contin False) >> (view uiStepper s)))+          (Step 1)+      _ -> pure ()+  _ -> pure ()  -- Page: C-f - Page down-appEvent s (VtyEvent (V.EvKey (V.KChar 'f') [V.MCtrl])) =-  vScrollPage (viewportScroll TracePane) Down >> continue s+appEvent (VtyEvent (V.EvKey (V.KChar 'f') [V.MCtrl])) =+  vScrollPage (viewportScroll TracePane) Down  -- Page: C-b - Page up-appEvent s (VtyEvent (V.EvKey (V.KChar 'b') [V.MCtrl])) =-  vScrollPage (viewportScroll TracePane) Up >> continue s+appEvent (VtyEvent (V.EvKey (V.KChar 'b') [V.MCtrl])) =+  vScrollPage (viewportScroll TracePane) Up +-- UnitTest Picker: (main) - render list+appEvent (VtyEvent e) = do+  Brick.zoom+    (_ViewPicker . testPickerList)+    (handleListEvent e)+ -- Default-appEvent s _ = continue s+appEvent _ = pure ()  app :: UnitTestOptions -> App UiState () Name app UnitTestOptions{..} =@@ -617,7 +602,7 @@   { appDraw = drawUi   , appChooseCursor = neverShowCursor   , appHandleEvent = appEvent-  , appStartEvent = return+  , appStartEvent = pure ()   , appAttrMap = const (attrMap V.defAttr myTheme)   } @@ -630,9 +615,8 @@     cd = case test of       SymbolicTest _ -> symCalldata theTestName types [] (AbstractBuf "txdata")       _ -> (error "unreachable", error "unreachable")-    Just (test, types) = find (\(test',_) -> extractSig test' == theTestName) $ unitTestMethods testContract-    Just testContract =-      view (dappSolcByName . at theContractName) dapp+    (test, types) = fromJust $ find (\(test',_) -> extractSig test' == theTestName) $ unitTestMethods testContract+    testContract = fromJust $ view (dappSolcByName . at theContractName) dapp     vm0 =       initialUnitTestVm opts testContract     script = do@@ -763,7 +747,7 @@   ]   where     dapp' = dapp (view (browserVm . uiTestOpts) ui)-    Just (_, (_, c)) = listSelectedElement (view browserContractList ui)+    (_, (_, c)) = fromJust $ listSelectedElement (view browserContractList ui) --        currentContract  = view (dappSolcByHash . ix ) dapp     maybeHash ch = fromJust (error "Internal error: cannot find concrete codehash for partially symbolic code") (maybeLitWord (view codehash ch)) @@ -1051,8 +1035,8 @@ opWidget :: (Integral a, Show a) => (a, Op) -> Widget n opWidget = txt . pack . opString -selectedAttr :: AttrName; selectedAttr = "selected"-dimAttr :: AttrName; dimAttr = "dim"-wordAttr :: AttrName; wordAttr = "word"-boldAttr :: AttrName; boldAttr = "bold"-activeAttr :: AttrName; activeAttr = "active"+selectedAttr :: AttrName; selectedAttr = attrName "selected"+dimAttr :: AttrName; dimAttr = attrName "dim"+wordAttr :: AttrName; wordAttr = attrName "word"+boldAttr :: AttrName; boldAttr = attrName "bold"+activeAttr :: AttrName; activeAttr = attrName "active"

@@ -15,7 +15,7 @@ import Data.Aeson (FromJSON (..)) import Data.ByteString (ByteString) import Data.Map (Map)-import Data.Maybe (fromMaybe, isNothing)+import Data.Maybe (fromMaybe, isNothing, fromJust)  import qualified Data.Aeson        as JSON import qualified Data.Aeson.Types  as JSON@@ -78,9 +78,9 @@         to'        = case txToAddr tx of           Just a  -> BS $ word160Bytes a           Nothing -> BS mempty-        Just maxFee = txMaxFeePerGas tx-        Just maxPrio = txMaxPriorityFeeGas tx-        Just gasPrice = txGasPrice tx+        maxFee = fromJust $ txMaxFeePerGas tx+        maxPrio = fromJust $ txMaxPriorityFeeGas tx+        gasPrice = fromJust $ txGasPrice tx         accessList = txAccessList tx         rlpAccessList = EVM.RLP.List $ map (\accessEntry ->           EVM.RLP.List [BS $ word160Bytes (accessAddress accessEntry),@@ -163,7 +163,7 @@     toAddr   <- addrFieldMaybe val "to"     v        <- wordField val "v"     value    <- wordField val "value"-    txType   <- fmap read <$> (val JSON..:? "type")+    txType   <- fmap (read :: String -> Int) <$> (val JSON..:? "type")     case txType of       Just 0x00 -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing       Just 0x01 -> do@@ -184,7 +184,7 @@ touchAccount a = Map.insertWith (flip const) a newAccount  newAccount :: EVM.Contract-newAccount = initialContract $ EVM.RuntimeCode mempty+newAccount = initialContract $ EVM.RuntimeCode (EVM.ConcreteRuntimeCode "")  -- | Increments origin nonce and pays gas deposit setupTx :: Addr -> Addr -> W256 -> Word64 -> Map Addr EVM.Contract -> Map Addr EVM.Contract

@@ -66,16 +66,10 @@        -- control flow -      e@(Invalid a) -> f e <> (foldl (foldProp f) mempty a)-      e@(StackLimitExceeded a) -> f e <> (foldl (foldProp f) mempty a)-      e@(InvalidMemoryAccess a) -> f e <> (foldl (foldProp f) mempty a)-      e@(BadJumpDestination a) -> f e <> (foldl (foldProp f) mempty a)-      e@(SelfDestruct a) -> f e <> (foldl (foldProp f) mempty a)-      e@(IllegalOverflow a) -> f e <> (foldl (foldProp f) mempty a)       e@(Revert a b) -> f e <> (foldl (foldProp f) mempty a) <> (go b)       e@(Return a b c) -> f e <> (foldl (foldProp f) mempty a) <> (go b) <> (go c)       e@(ITE a b c) -> f e <> (go a) <> (go b) <> (go c)-      e@(TmpErr a _) -> f e <> (foldl (foldProp f) mempty a)+      e@(Failure a _) -> f e <> (foldl (foldProp f) mempty a)        -- integers @@ -314,24 +308,9 @@    -- control flow -  Invalid a -> do-    a' <- mapM (mapPropM f) a-    f (Invalid a')-  SelfDestruct a -> do-    a' <- mapM (mapPropM f) a-    f (SelfDestruct a')-  IllegalOverflow a -> do-    a' <- mapM (mapPropM f) a-    f (IllegalOverflow a')-  InvalidMemoryAccess a -> do-    a' <- mapM (mapPropM f) a-    f (InvalidMemoryAccess a')-  StackLimitExceeded a -> do-    a' <- mapM (mapPropM f) a-    f (StackLimitExceeded a')-  BadJumpDestination a -> do+  Failure a b -> do     a' <- mapM (mapPropM f) a-    f (BadJumpDestination a')+    f (Failure a' b)   Revert a b -> do     a' <- mapM (mapPropM f) a     b' <- mapExprM f b@@ -347,10 +326,6 @@     b' <- mapExprM f b     c' <- mapExprM f c     f (ITE a' b' c')--  TmpErr a b -> do-    a' <- mapM (mapPropM f) a-    f (TmpErr a' b)    -- integers 

@@ -5,6 +5,8 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} +{-# OPTIONS_GHC -Wno-error=inline-rule-shadowing #-}+ module EVM.Types where  import Prelude hiding  (Word, LT, GT)@@ -115,6 +117,17 @@   | End   deriving (Typeable) +-- EVM errors+data Error+  = Invalid+  | IllegalOverflow+  | StackLimitExceeded+  | InvalidMemoryAccess+  | BadJumpDestination+  | SelfDestruct+  | TmpErr String+  deriving (Show, Eq, Ord)+ -- Variables refering to a global environment data GVar (a :: EType) where   BufVar :: Int -> GVar Buf@@ -152,17 +165,11 @@                  -> Expr EWord   -- control flow -  Invalid             :: [Prop] -> Expr End-  IllegalOverflow     :: [Prop] -> Expr End-  SelfDestruct        :: [Prop] -> Expr End-  StackLimitExceeded  :: [Prop] -> Expr End-  InvalidMemoryAccess :: [Prop] -> Expr End-  BadJumpDestination  :: [Prop] -> Expr End   Revert              :: [Prop] -> Expr Buf -> Expr End+  Failure             :: [Prop] -> Error -> Expr End   Return              :: [Prop] -> Expr Buf -> Expr Storage -> Expr End   ITE                 :: Expr EWord -> Expr End -> Expr End -> Expr End-  TmpErr              :: [Prop] -> String -> Expr End -- TODO this is a crutch to help us not deal with all EVM failure modes in Expr-                                                      --      should be removed once EVM failure modes are handled in Expr+   -- integers    Add            :: Expr EWord -> Expr EWord -> Expr EWord@@ -657,6 +664,18 @@ packNibbles [] = mempty packNibbles (n1:n2:ns) = BS.singleton (toByte n1 n2) <> packNibbles ns packNibbles _ = error "can't pack odd number of nibbles"++toWord64 :: W256 -> Maybe Word64+toWord64 n =+  if n <= num (maxBound :: Word64)+    then let (W256 (Word256 _ (Word128 _ n'))) = n in Just n'+    else Nothing++toInt :: W256 -> Maybe Int+toInt n =+  if n <= num (maxBound :: Int)+    then let (W256 (Word256 _ (Word128 _ n'))) = n in Just (fromIntegral n')+    else Nothing  -- Keccak hashing 

@@ -17,7 +17,7 @@ import EVM.Solidity import qualified EVM.SymExec as SymExec import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, subModel, VeriOpts)-import EVM.Types+import EVM.Types hiding (Failure) import EVM.Transaction (initTx) import EVM.RLP import qualified EVM.Facts     as Facts@@ -244,7 +244,9 @@     res <- Stepper.execFully     case res of       Right (ConcreteBuf r) ->-        let AbiBool failed = decodeAbiValue AbiBoolType (BSLazy.fromStrict r)+        let failed = case decodeAbiValue AbiBoolType (BSLazy.fromStrict r) of+              AbiBool f -> f+              _ -> error "fix me with better types"         in pure (shouldFail == failed)       c -> error $ "internal error: unexpected failure code: " <> show c @@ -501,7 +503,11 @@ decodeCalls :: BSLazy.ByteString -> [ExploreTx] decodeCalls b = fromMaybe (error "could not decode replay data") $ do   List v <- rlpdecode $ BSLazy.toStrict b-  return $ flip fmap v $ \(List [BS caller', BS target, BS cd, BS ts]) -> (num (word caller'), num (word target), cd, word ts)+  pure $ unList <$> v+  where+    unList (List [BS caller', BS target, BS cd, BS ts]) =+      (num (word caller'), num (word target), cd, word ts)+    unList _ = error "fix me with better types"  -- | Runs an invariant test, calls the invariant before execution begins initialExplorationStepper :: UnitTestOptions -> ABIMethod -> [ExploreTx] -> [Addr] -> Int -> Stepper (Bool, RLP)@@ -523,7 +529,8 @@        vm <- get        let cs = view (env . contracts) vm            noCode c = case view contractcode c of-             RuntimeCode c' -> null c'+             RuntimeCode (ConcreteRuntimeCode "") -> True+             RuntimeCode (SymbolicRuntimeCode c') -> null c'              _ -> False            mutable m = view methodMutability m `elem` [NonPayable, Payable]            knownAbis :: Map Addr SolcContract@@ -585,7 +592,7 @@ getTargetContracts :: UnitTestOptions -> Stepper [Addr] getTargetContracts UnitTestOptions{..} = do   vm <- Stepper.evm get-  let Just contract' = currentContract vm+  let contract' = fromJust $ currentContract vm       theAbi = view abiMap $ fromJust $ lookupCode (view contractcode contract') dapp       setUp  = abiKeccak (encodeUtf8 "targetContracts()")   case Map.lookup setUp theAbi of@@ -595,9 +602,16 @@       res <- Stepper.execFully       case res of         Right (ConcreteBuf r) ->-          let AbiTuple vs = decodeAbiValue (AbiTupleType (Vector.fromList [AbiArrayDynamicType AbiAddressType])) (BSLazy.fromStrict r)-              [AbiArrayDynamic AbiAddressType targets] = Vector.toList vs-          in return $ fmap (\(AbiAddress a) -> a) (Vector.toList targets)+          let vs = case decodeAbiValue (AbiTupleType (Vector.fromList [AbiArrayDynamicType AbiAddressType])) (BSLazy.fromStrict r) of+                AbiTuple v -> v+                _ -> error "fix me with better types"+              targets = case Vector.toList vs of+                [AbiArrayDynamic AbiAddressType ts] ->+                  let unAbiAddress (AbiAddress a) = a+                      unAbiAddress _ = error "fix me with better types"+                  in unAbiAddress <$> Vector.toList ts+                _ -> error "fix me with better types"+          in pure targets         _ -> error "internal error: unexpected failure code"  exploreRun :: UnitTestOptions -> VM -> ABIMethod -> [ExploreTx] -> IO (Text, Either Text Text, VM)@@ -903,7 +917,9 @@           log_unnamed =             Just $ showValue (head ts) args           log_named =-            let [key, val] = take 2 (textValues ts args)+            let (key, val) = case take 2 (textValues ts args) of+                  [k, v] -> (k, v)+                  _ -> error "shouldn't happen"             in Just $ unquote key <> ": " <> val           showDecimal dec val =             pack $ show $ Decimal (num dec) val@@ -938,7 +954,7 @@   constraints %= (<> cdProps)   assign (state . caller) (litAddr testCaller)   assign (state . gas) testGasCall-  origin' <- fromMaybe (initialContract (RuntimeCode mempty)) <$> use (env . contracts . at testOrigin)+  origin' <- fromMaybe (initialContract (RuntimeCode (ConcreteRuntimeCode ""))) <$> use (env . contracts . at testOrigin)   let originBal = view balance origin'   when (originBal < testGasprice * (num testGasCall)) $ error "insufficient balance for gas cost"   vm <- get@@ -974,7 +990,7 @@            , vmoptAllowFFI = ffiAllowed            }     creator =-      initialContract (RuntimeCode mempty)+      initialContract (RuntimeCode (ConcreteRuntimeCode ""))         & set nonce 1         & set balance testBalanceCreate   in vm

@@ -1,374 +0,0 @@-{-# Language CPP #-}-{-# LANGUAGE TupleSections #-}--module EVM.VMTest-  ( Case-  , BlockchainCase--  , parseBCSuite--  , initTx-  , setupTx-  , vmForCase-  , checkExpectation-  ) where--import Prelude hiding (Word)--import qualified EVM-import EVM (contractcode, storage, origStorage, balance, nonce, initialContract, StorageBase(..))-import EVM.Expr (litCode, litAddr)-import qualified EVM.Concrete as EVM-import qualified EVM.FeeSchedule--import EVM.Transaction-import EVM.Types--import Control.Arrow ((***), (&&&))-import Control.Lens-import Control.Monad--import GHC.Stack--import Data.Aeson ((.:), (.:?), FromJSON (..))-import Data.Map (Map)-import Data.Maybe (fromMaybe, isNothing)-import Data.Witherable (Filterable, catMaybes)--import qualified Data.Map          as Map-import qualified Data.Aeson        as JSON-import qualified Data.Aeson.Types  as JSON-import qualified Data.ByteString.Lazy  as Lazy-import qualified Data.Vector as V-import Data.Word (Word64)--type Storage = Map W256 W256--data Which = Pre | Post--data Block = Block-  { blockCoinbase    :: Addr-  , blockDifficulty  :: W256-  , blockGasLimit    :: Word64-  , blockBaseFee     :: W256-  , blockNumber      :: W256-  , blockTimestamp   :: W256-  , blockTxs         :: [Transaction]-  } deriving Show--data Case = Case-  { testVmOpts      :: EVM.VMOpts-  , checkContracts  :: Map Addr (EVM.Contract, Storage)-  , testExpectation :: Map Addr (EVM.Contract, Storage)-  } deriving Show--data BlockchainCase = BlockchainCase-  { blockchainBlocks  :: [Block]-  , blockchainPre     :: Map Addr (EVM.Contract, Storage)-  , blockchainPost    :: Map Addr (EVM.Contract, Storage)-  , blockchainNetwork :: String-  } deriving Show--splitEithers :: (Filterable f) => f (Either a b) -> (f a, f b)-splitEithers =-  (catMaybes *** catMaybes)-  . (fmap fst &&& fmap snd)-  . (fmap (preview _Left &&& preview _Right))--checkStateFail :: Bool -> Case -> EVM.VM -> (Bool, Bool, Bool, Bool, Bool) -> IO Bool-checkStateFail diff x vm (okState, okMoney, okNonce, okData, okCode) = do-  let-    printContracts :: Map Addr (EVM.Contract, Storage) -> IO ()-    printContracts cs = putStrLn $ Map.foldrWithKey (\k (c, s) acc ->-      acc ++ show k ++ " : "-                   ++ (show . toInteger  $ (view nonce c)) ++ " "-                   ++ (show . toInteger  $ (view balance c)) ++ " "-                   ++ (printStorage s)-        ++ "\n") "" cs--    reason = map fst (filter (not . snd)-        [ ("bad-state",       okMoney || okNonce || okData  || okCode || okState)-        , ("bad-balance", not okMoney || okNonce || okData  || okCode || okState)-        , ("bad-nonce",   not okNonce || okMoney || okData  || okCode || okState)-        , ("bad-storage", not okData  || okMoney || okNonce || okCode || okState)-        , ("bad-code",    not okCode  || okMoney || okNonce || okData || okState)-        ])-    check = checkContracts x-    expected = testExpectation x-    actual = Map.map (,mempty) $ view (EVM.env . EVM.contracts) vm -- . to (fmap (clearZeroStorage.clearOrigStorage))) vm-    printStorage = show -- TODO: fixme--  putStr (unwords reason)-  when (diff && (not okState)) $ do-    putStrLn "\nPre balance/state: "-    printContracts check-    putStrLn "\nExpected balance/state: "-    printContracts expected-    putStrLn "\nActual balance/state: "-    printContracts actual-  return okState--checkExpectation :: HasCallStack => Bool -> Case -> EVM.VM -> IO Bool-checkExpectation diff x vm = do-  let expectation = testExpectation x-      (okState, b2, b3, b4, b5) = checkExpectedContracts vm expectation-  putStrLn $ show expectation-  unless okState $ void $ checkStateFail-    diff x vm (okState, b2, b3, b4, b5)-  return okState---- quotient account state by nullness-(~=) :: Map Addr (EVM.Contract, Storage) -> Map Addr (EVM.Contract, Storage) -> Bool-(~=) cs1 cs2 =-    let nullAccount = EVM.initialContract (EVM.RuntimeCode mempty)-        padNewAccounts cs ks = Map.union cs $ Map.fromList [(k, (nullAccount, mempty)) | k <- ks]-        padded_cs1 = padNewAccounts cs1 (Map.keys cs2)-        padded_cs2 = padNewAccounts cs2 (Map.keys cs1)-    in and $ zipWith (===) (Map.elems padded_cs1) (Map.elems padded_cs2)--(===) :: (EVM.Contract, Storage) -> (EVM.Contract, Storage) -> Bool-(c1, s1) === (c2, s2) =-  codeEqual && storageEqual && (c1 ^. balance == c2 ^. balance) && (c1 ^. nonce ==  c2 ^. nonce)-  where-    storageEqual = s1 == s2-    codeEqual = case (c1 ^. contractcode, c2 ^. contractcode) of-      (EVM.RuntimeCode a', EVM.RuntimeCode b') -> a' == b'-      _ -> error "unexpected code"--checkExpectedContracts :: HasCallStack => EVM.VM -> Map Addr (EVM.Contract, Storage) -> (Bool, Bool, Bool, Bool, Bool)-checkExpectedContracts vm expected =-  let cs = zipWithStorages $ vm ^. EVM.env . EVM.contracts -- . to (fmap (clearZeroStorage.clearOrigStorage))-      expectedCs = clearStorage <$> expected-  in ( (expectedCs ~= cs)-     , (clearBalance <$> expectedCs) ~= (clearBalance <$> cs)-     , (clearNonce   <$> expectedCs) ~= (clearNonce   <$> cs)-     , (clearStorage <$> expectedCs) ~= (clearStorage <$> cs)-     , (clearCode    <$> expectedCs) ~= (clearCode    <$> cs)-     )-  where-  zipWithStorages = Map.mapWithKey (\addr c -> (c, lookupStorage addr))-  lookupStorage _ =-    case vm ^. EVM.env . EVM.storage of-      ConcreteStore _ -> mempty -- clearZeroStorage $ fromMaybe mempty $ Map.lookup (num addr) s-      EmptyStore -> mempty-      AbstractStore -> mempty -- error "AbstractStore, should this be handled?"-      SStore {} -> mempty -- error "SStore, should this be handled?"-      GVar _ -> error "unexpected global variable"--clearStorage :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)-clearStorage (c, _) = (c, mempty)--clearBalance :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)-clearBalance (c, s) = (set balance 0 c, s)--clearNonce :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)-clearNonce (c, s) = (set nonce 0 c, s)--clearCode :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)-clearCode (c, s) = (set contractcode (EVM.RuntimeCode mempty) c, s)----newtype ContractWithStorage = ContractWithStorage { unContractWithStorage :: (EVM.Contract, Storage) }--instance FromJSON ContractWithStorage where-  parseJSON (JSON.Object v) = do-    code <- (EVM.RuntimeCode . V.fromList . litCode <$> (hexText <$> v .: "code"))-    storage' <- v .: "storage"-    balance' <- v .: "balance"-    nonce'   <- v .: "nonce"-    let c = EVM.initialContract code-              & balance .~ balance'-              & nonce   .~ nonce'-    return $ ContractWithStorage (c, storage')--  parseJSON invalid =-    JSON.typeMismatch "Contract" invalid--instance FromJSON BlockchainCase where-  parseJSON (JSON.Object v) = BlockchainCase-    <$> v .: "blocks"-    <*> parseContracts Pre v-    <*> parseContracts Post v-    <*> v .: "network"-  parseJSON invalid =-    JSON.typeMismatch "GeneralState test case" invalid--instance FromJSON Block where-  parseJSON (JSON.Object v) = do-    v'         <- v .: "blockHeader"-    txs        <- v .: "transactions"-    coinbase   <- addrField v' "coinbase"-    difficulty <- wordField v' "difficulty"-    gasLimit   <- word64Field v' "gasLimit"-    number     <- wordField v' "number"-    baseFee    <- fmap read <$> v' .:? "baseFeePerGas"-    timestamp  <- wordField v' "timestamp"-    return $ Block coinbase difficulty gasLimit (fromMaybe 0 baseFee) number timestamp txs-  parseJSON invalid =-    JSON.typeMismatch "Block" invalid--parseContracts ::-  Which -> JSON.Object -> JSON.Parser (Map Addr (EVM.Contract, Storage))-parseContracts w v =-  (Map.map unContractWithStorage) <$> (v .: which >>= parseJSON)-  where which = case w of-          Pre  -> "pre"-          Post -> "postState"--parseBCSuite ::-  Lazy.ByteString -> Either String (Map String Case)-parseBCSuite x = case (JSON.eitherDecode' x) :: Either String (Map String BlockchainCase) of-  Left e        -> Left e-  Right bcCases -> let allCases = fromBlockchainCase <$> bcCases-                       keepError (Left e) = errorFatal e-                       keepError _        = True-                       filteredCases = Map.filter keepError allCases-                       (erroredCases, parsedCases) = splitEithers filteredCases-    in if Map.size erroredCases > 0-    then Left ("errored case: " ++ (show erroredCases))-    else if Map.size parsedCases == 0-    then Left "No cases to check."-    else Right parsedCases---data BlockchainError-  = TooManyBlocks-  | TooManyTxs-  | NoTxs-  | SignatureUnverified-  | InvalidTx-  | OldNetwork-  | FailedCreate-  deriving Show--errorFatal :: BlockchainError -> Bool-errorFatal TooManyBlocks = True-errorFatal TooManyTxs = True-errorFatal SignatureUnverified = True-errorFatal InvalidTx = True-errorFatal _ = False--fromBlockchainCase :: BlockchainCase -> Either BlockchainError Case-fromBlockchainCase (BlockchainCase blocks preState postState network) =-  case (blocks, network) of-    ([block], "London") -> case blockTxs block of-      [tx] -> fromBlockchainCase' block tx preState postState-      []        -> Left NoTxs-      _         -> Left TooManyTxs-    ([_], _) -> Left OldNetwork-    (_, _)   -> Left TooManyBlocks--fromBlockchainCase' :: Block -> Transaction-                       -> Map Addr (EVM.Contract, Storage) -> Map Addr (EVM.Contract, Storage)-                       -> Either BlockchainError Case-fromBlockchainCase' block tx preState postState =-  let isCreate = isNothing (txToAddr tx) in-  case (sender 1 tx, checkTx tx block preState) of-      (Nothing, _) -> Left SignatureUnverified-      (_, Nothing) -> Left (if isCreate then FailedCreate else InvalidTx)-      (Just origin, Just checkState) -> Right $ Case-        (EVM.VMOpts-         { vmoptContract      = EVM.initialContract theCode-         , vmoptCalldata      = (cd, [])-         , vmoptValue         = Lit (txValue tx)-         , vmoptAddress       = toAddr-         , vmoptCaller        = litAddr origin-         , vmoptStorageBase   = Concrete-         , vmoptOrigin        = origin-         , vmoptGas           = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx)-         , vmoptBaseFee       = blockBaseFee block-         , vmoptPriorityFee   = priorityFee tx (blockBaseFee block)-         , vmoptGaslimit      = txGasLimit tx-         , vmoptNumber        = blockNumber block-         , vmoptTimestamp     = Lit $ blockTimestamp block-         , vmoptCoinbase      = blockCoinbase block-         , vmoptPrevRandao    = blockDifficulty block-         , vmoptMaxCodeSize   = 24576-         , vmoptBlockGaslimit = blockGasLimit block-         , vmoptGasprice      = effectiveGasPrice-         , vmoptSchedule      = feeSchedule-         , vmoptChainId       = 1-         , vmoptCreate        = isCreate-         , vmoptTxAccessList  = txAccessMap tx-         , vmoptAllowFFI      = False-         })-        checkState-        postState-          where-            toAddr = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)-            senderNonce = view (accountAt origin . nonce) (Map.map fst preState)-            feeSchedule = EVM.FeeSchedule.berlin-            toCode = Map.lookup toAddr preState-            theCode = if isCreate-                      then EVM.InitCode (txData tx) mempty-                      else maybe (EVM.RuntimeCode mempty) (view contractcode) (fst <$> toCode)-            effectiveGasPrice = effectiveprice tx (blockBaseFee block)-            cd = if isCreate-                 then mempty-                 else ConcreteBuf $ txData tx--effectiveprice :: Transaction -> W256 -> W256-effectiveprice tx baseFee = priorityFee tx baseFee + baseFee--priorityFee :: Transaction -> W256 -> W256-priorityFee tx baseFee = let-    (txPrioMax, txMaxFee) = case txType tx of-               EIP1559Transaction ->-                 let Just maxPrio = txMaxPriorityFeeGas tx-                     Just maxFee = txMaxFeePerGas tx-                 in (maxPrio, maxFee)-               _ ->-                 let Just gasPrice = txGasPrice tx-                 in (gasPrice, gasPrice)-  in min txPrioMax (txMaxFee - baseFee)--maxBaseFee :: Transaction -> W256-maxBaseFee tx =-  case txType tx of-     EIP1559Transaction ->-       let Just maxFee = txMaxFeePerGas tx-       in maxFee-     _ ->-       let Just gasPrice = txGasPrice tx-       in gasPrice---validateTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe ()-validateTx tx block cs = do-  let cs' = Map.map fst cs-  origin        <- sender 1 tx-  originBalance <- (view balance) <$> view (at origin) cs'-  originNonce   <- (view nonce)   <$> view (at origin) cs'-  let gasDeposit = (effectiveprice tx (blockBaseFee block)) * (num $ txGasLimit tx)-  if gasDeposit + (txValue tx) <= originBalance-    && txNonce tx == originNonce && blockBaseFee block <= maxBaseFee tx-  then Just ()-  else Nothing--checkTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe (Map Addr (EVM.Contract, Storage))-checkTx tx block prestate = do-  origin <- sender 1 tx-  validateTx tx block prestate-  let isCreate   = isNothing (txToAddr tx)-      senderNonce = view (accountAt origin . nonce) (Map.map fst prestate)-      toAddr      = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)-      prevCode    = view (accountAt toAddr . contractcode) (Map.map fst prestate)-      prevNonce   = view (accountAt toAddr . nonce) (Map.map fst prestate)-  if isCreate && ((case prevCode of {EVM.RuntimeCode b -> not (null b); _ -> True}) || (prevNonce /= 0))-  then mzero-  else-    return prestate--vmForCase :: Case -> EVM.VM-vmForCase x =-  let-    a = checkContracts x-    cs = Map.map fst a-    st = Map.mapKeys num $ Map.map snd a-    vm = EVM.makeVm (testVmOpts x)-      & set (EVM.env . EVM.contracts) cs-      & set (EVM.env . EVM.storage) (ConcreteStore st)-      & set (EVM.env . EVM.origStorage) st-  in-    initTx vm

@@ -0,0 +1,466 @@+{-# LANGUAGE ImportQualifiedPost #-}+{-# LANGUAGE TupleSections #-}++module Main where++import Prelude hiding (Word)++import EVM qualified+import EVM (contractcode, storage, origStorage, balance, nonce, initialContract, StorageBase(..))+import EVM.Concrete qualified as EVM+import EVM.Dapp (emptyDapp)+import EVM.Expr (litAddr)+import EVM.FeeSchedule qualified+import EVM.Fetch qualified+import EVM.Stepper qualified+import EVM.SMT (withSolvers, Solver(Z3))+import EVM.Transaction+import EVM.TTY qualified as TTY+import EVM.Types++import Control.Arrow ((***), (&&&))+import Control.Lens+import Control.Monad+import Control.Monad.State.Strict (execStateT)+import Data.Aeson ((.:), (.:?), FromJSON (..))+import Data.Aeson qualified as JSON+import Data.Aeson.Types qualified as JSON+import Data.ByteString qualified as BS+import Data.ByteString.Lazy qualified as Lazy+import Data.ByteString.Lazy qualified as LazyByteString+import Data.List (isInfixOf)+import Data.Map (Map)+import Data.Map qualified as Map+import Data.Maybe (fromJust, fromMaybe, isNothing, isJust)+import Data.Word (Word64)+import System.Environment (lookupEnv, getEnv)+import System.FilePath.Find qualified as Find+import System.FilePath.Posix (makeRelative, (</>))+import Witherable (Filterable, catMaybes)++import Test.Tasty+import Test.Tasty.ExpectedFailure+import Test.Tasty.HUnit++type Storage = Map W256 W256++data Which = Pre | Post++data Block = Block+  { blockCoinbase    :: Addr+  , blockDifficulty  :: W256+  , blockGasLimit    :: Word64+  , blockBaseFee     :: W256+  , blockNumber      :: W256+  , blockTimestamp   :: W256+  , blockTxs         :: [Transaction]+  } deriving Show++data Case = Case+  { testVmOpts      :: EVM.VMOpts+  , checkContracts  :: Map Addr (EVM.Contract, Storage)+  , testExpectation :: Map Addr (EVM.Contract, Storage)+  } deriving Show++data BlockchainCase = BlockchainCase+  { blockchainBlocks  :: [Block]+  , blockchainPre     :: Map Addr (EVM.Contract, Storage)+  , blockchainPost    :: Map Addr (EVM.Contract, Storage)+  , blockchainNetwork :: String+  } deriving Show++main :: IO ()+main = do+  tests <- prepareTests+  defaultMain tests++prepareTests :: IO TestTree+prepareTests = do+  repo <- getEnv "HEVM_ETHEREUM_TESTS_REPO"+  let testsDir = "BlockchainTests/GeneralStateTests"+  let dir = repo </> testsDir+  jsonFiles <- Find.find Find.always (Find.extension Find.==? ".json") dir+  putStrLn "Loading and parsing json files from ethereum-tests..."+  isCI <- isJust <$> lookupEnv "CI"+  let problematicTests = if isCI then commonProblematicTests <> ciProblematicTests else commonProblematicTests+  let ignoredFiles = if isCI then ciIgnoredFiles else []+  groups <- mapM (\f -> testGroup (makeRelative repo f) <$> (if any (`isInfixOf` f) ignoredFiles then pure [] else testsFromFile f problematicTests)) jsonFiles+  putStrLn "Loaded."+  pure $ testGroup "ethereum-tests" groups++testsFromFile :: String -> Map String (TestTree -> TestTree) -> IO [TestTree]+testsFromFile file problematicTests = do+  parsed <- parseBCSuite <$> LazyByteString.readFile file+  case parsed of+   Left "No cases to check." -> pure [] -- error "no-cases ok"+   Left _err -> pure [] -- error err+   Right allTests -> pure $+     (\(name, x) -> testCase' name $ runVMTest False (name, x)) <$> Map.toList allTests+  where+  testCase' name assertion =+    case Map.lookup name problematicTests of+      Just f -> f (testCase name assertion)+      Nothing -> testCase name assertion++-- CI has issues with some heaver tests, disable in bulk+ciIgnoredFiles :: [String]+ciIgnoredFiles =+  [ "BlockchainTests/GeneralStateTests/VMTests/vmPerformance"+  , "BlockchainTests/GeneralStateTests/stQuadraticComplexityTest"+  , "BlockchainTests/GeneralStateTests/stStaticCall"+  ]++commonProblematicTests :: Map String (TestTree -> TestTree)+commonProblematicTests = Map.fromList+  [ ("twoOps_d0g0v0_London", expectFailBecause "TODO: regression")+  , ("sar_2^256-1_0_d0g0v0_London", expectFailBecause "TODO: regression")+  , ("shiftCombinations_d0g0v0_London", expectFailBecause "TODO: regression")+  , ("shiftSignedCombinations_d0g0v0_London", expectFailBecause "TODO: regression")+  , ("bufferSrcOffset_d14g0v0_London", expectFailBecause "TODO: regression")+  , ("bufferSrcOffset_d38g0v0_London", expectFailBecause "TODO: regression")+  , ("loopMul_d0g0v0_London", ignoreTestBecause "hevm is too slow")+  , ("loopMul_d1g0v0_London", ignoreTestBecause "hevm is too slow")+  , ("loopMul_d2g0v0_London", ignoreTestBecause "hevm is too slow")+  , ("CALLBlake2f_MaxRounds_d0g0v0_London", ignoreTestBecause "very slow, bypasses timeout due time spent in FFI")+  ]++ciProblematicTests :: Map String (TestTree -> TestTree)+ciProblematicTests = Map.fromList+  [ ("Return50000_d0g1v0_London", ignoreTest)+  , ("Return50000_2_d0g1v0_London", ignoreTest)+  , ("randomStatetest177_d0g0v0_London", ignoreTest)+  , ("static_Call50000_d0g0v0_London", ignoreTest)+  , ("static_Call50000_d1g0v0_London", ignoreTest)+  , ("static_Call50000bytesContract50_1_d1g0v0_London", ignoreTest)+  , ("static_Call50000bytesContract50_2_d1g0v0_London", ignoreTest)+  , ("static_Return50000_2_d0g0v0_London", ignoreTest)+  , ("loopExp_d10g0v0_London", ignoreTest)+  , ("loopExp_d11g0v0_London", ignoreTest)+  , ("loopExp_d12g0v0_London", ignoreTest)+  , ("loopExp_d13g0v0_London", ignoreTest)+  , ("loopExp_d14g0v0_London", ignoreTest)+  , ("loopExp_d8g0v0_London", ignoreTest)+  , ("loopExp_d9g0v0_London", ignoreTest)+  ]++runVMTest :: Bool -> (String, Case) -> IO ()+runVMTest diffmode (_name, x) =+ do+  let vm0 = vmForCase x+  result <- execStateT (EVM.Stepper.interpret (EVM.Fetch.zero 0 (Just 0)) . void $ EVM.Stepper.execFully) vm0+  maybeReason <- checkExpectation diffmode x result+  case maybeReason of+    Just reason -> assertFailure reason+    Nothing -> pure ()++-- | Example usage:+-- | $ cabal new-repl ethereum-tests+-- | ghci> debugVMTest "BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/twoOps.json" "twoOps_d0g0v0_London"+debugVMTest :: String -> String -> IO ()+debugVMTest file test = do+  repo <- getEnv "HEVM_ETHEREUM_TESTS_REPO"+  Right allTests <- parseBCSuite <$> LazyByteString.readFile (repo </> file)+  let x = case filter (\(name, _) -> name == test) $ Map.toList allTests of+        [(_, x')] -> x'+        _ -> error "test not found"+  let vm0 = vmForCase x+  result <- withSolvers Z3 0 Nothing $ \solvers ->+    TTY.runFromVM solvers Nothing Nothing emptyDapp vm0+  void $ checkExpectation True x result++splitEithers :: (Filterable f) => f (Either a b) -> (f a, f b)+splitEithers =+  (catMaybes *** catMaybes)+  . (fmap fst &&& fmap snd)+  . (fmap (preview _Left &&& preview _Right))++checkStateFail :: Bool -> Case -> EVM.VM -> (Bool, Bool, Bool, Bool) -> IO String+checkStateFail diff x vm (okMoney, okNonce, okData, okCode) = do+  let+    printContracts :: Map Addr (EVM.Contract, Storage) -> IO ()+    printContracts cs = putStrLn $ Map.foldrWithKey (\k (c, s) acc ->+      acc ++ show k ++ " : "+                   ++ (show . toInteger  $ (view nonce c)) ++ " "+                   ++ (show . toInteger  $ (view balance c)) ++ " "+                   ++ (printStorage s)+        ++ "\n") "" cs++    reason = map fst (filter (not . snd)+        [ ("bad-state",       okMoney || okNonce || okData  || okCode)+        , ("bad-balance", not okMoney || okNonce || okData  || okCode)+        , ("bad-nonce",   not okNonce || okMoney || okData  || okCode)+        , ("bad-storage", not okData  || okMoney || okNonce || okCode)+        , ("bad-code",    not okCode  || okMoney || okNonce || okData)+        ])+    check = checkContracts x+    expected = testExpectation x+    actual = Map.map (,mempty) $ view (EVM.env . EVM.contracts) vm -- . to (fmap (clearZeroStorage.clearOrigStorage))) vm+    printStorage = show -- TODO: fixme++  when diff $ do+    putStr (unwords reason)+    putStrLn "\nPre balance/state: "+    printContracts check+    putStrLn "\nExpected balance/state: "+    printContracts expected+    putStrLn "\nActual balance/state: "+    printContracts actual+  pure (unwords reason)++checkExpectation :: Bool -> Case -> EVM.VM -> IO (Maybe String)+checkExpectation diff x vm = do+  let expectation = testExpectation x+      (okState, b2, b3, b4, b5) = checkExpectedContracts vm expectation+  if okState then+    pure Nothing+  else+    Just <$> checkStateFail diff x vm (b2, b3, b4, b5)++-- quotient account state by nullness+(~=) :: Map Addr (EVM.Contract, Storage) -> Map Addr (EVM.Contract, Storage) -> Bool+(~=) cs1 cs2 =+    let nullAccount = EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode ""))+        padNewAccounts cs ks = Map.union cs $ Map.fromList [(k, (nullAccount, mempty)) | k <- ks]+        padded_cs1 = padNewAccounts cs1 (Map.keys cs2)+        padded_cs2 = padNewAccounts cs2 (Map.keys cs1)+    in and $ zipWith (===) (Map.elems padded_cs1) (Map.elems padded_cs2)++(===) :: (EVM.Contract, Storage) -> (EVM.Contract, Storage) -> Bool+(c1, s1) === (c2, s2) =+  codeEqual && storageEqual && (c1 ^. balance == c2 ^. balance) && (c1 ^. nonce ==  c2 ^. nonce)+  where+    storageEqual = s1 == s2+    codeEqual = case (c1 ^. contractcode, c2 ^. contractcode) of+      (EVM.RuntimeCode a', EVM.RuntimeCode b') -> a' == b'+      _ -> error "unexpected code"++checkExpectedContracts :: EVM.VM -> Map Addr (EVM.Contract, Storage) -> (Bool, Bool, Bool, Bool, Bool)+checkExpectedContracts vm expected =+  let cs = zipWithStorages $ vm ^. EVM.env . EVM.contracts -- . to (fmap (clearZeroStorage.clearOrigStorage))+      expectedCs = clearStorage <$> expected+  in ( (expectedCs ~= cs)+     , (clearBalance <$> expectedCs) ~= (clearBalance <$> cs)+     , (clearNonce   <$> expectedCs) ~= (clearNonce   <$> cs)+     , (clearStorage <$> expectedCs) ~= (clearStorage <$> cs)+     , (clearCode    <$> expectedCs) ~= (clearCode    <$> cs)+     )+  where+  zipWithStorages = Map.mapWithKey (\addr c -> (c, lookupStorage addr))+  lookupStorage _ =+    case vm ^. EVM.env . EVM.storage of+      ConcreteStore _ -> mempty -- clearZeroStorage $ fromMaybe mempty $ Map.lookup (num addr) s+      EmptyStore -> mempty+      AbstractStore -> mempty -- error "AbstractStore, should this be handled?"+      SStore {} -> mempty -- error "SStore, should this be handled?"+      GVar _ -> error "unexpected global variable"++clearStorage :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)+clearStorage (c, _) = (c, mempty)++clearBalance :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)+clearBalance (c, s) = (set balance 0 c, s)++clearNonce :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)+clearNonce (c, s) = (set nonce 0 c, s)++clearCode :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)+clearCode (c, s) = (set contractcode (EVM.RuntimeCode (EVM.ConcreteRuntimeCode "")) c, s)++newtype ContractWithStorage = ContractWithStorage { unContractWithStorage :: (EVM.Contract, Storage) }++instance FromJSON ContractWithStorage where+  parseJSON (JSON.Object v) = do+    code <- (EVM.RuntimeCode . EVM.ConcreteRuntimeCode <$> (hexText <$> v .: "code"))+    storage' <- v .: "storage"+    balance' <- v .: "balance"+    nonce'   <- v .: "nonce"+    let c = EVM.initialContract code+              & balance .~ balance'+              & nonce   .~ nonce'+    return $ ContractWithStorage (c, storage')++  parseJSON invalid =+    JSON.typeMismatch "Contract" invalid++instance FromJSON BlockchainCase where+  parseJSON (JSON.Object v) = BlockchainCase+    <$> v .: "blocks"+    <*> parseContracts Pre v+    <*> parseContracts Post v+    <*> v .: "network"+  parseJSON invalid =+    JSON.typeMismatch "GeneralState test case" invalid++instance FromJSON Block where+  parseJSON (JSON.Object v) = do+    v'         <- v .: "blockHeader"+    txs        <- v .: "transactions"+    coinbase   <- addrField v' "coinbase"+    difficulty <- wordField v' "difficulty"+    gasLimit   <- word64Field v' "gasLimit"+    number     <- wordField v' "number"+    baseFee    <- fmap read <$> v' .:? "baseFeePerGas"+    timestamp  <- wordField v' "timestamp"+    return $ Block coinbase difficulty gasLimit (fromMaybe 0 baseFee) number timestamp txs+  parseJSON invalid =+    JSON.typeMismatch "Block" invalid++parseContracts ::+  Which -> JSON.Object -> JSON.Parser (Map Addr (EVM.Contract, Storage))+parseContracts w v =+  (Map.map unContractWithStorage) <$> (v .: which >>= parseJSON)+  where which = case w of+          Pre  -> "pre"+          Post -> "postState"++parseBCSuite ::+  Lazy.ByteString -> Either String (Map String Case)+parseBCSuite x = case (JSON.eitherDecode' x) :: Either String (Map String BlockchainCase) of+  Left e        -> Left e+  Right bcCases -> let allCases = fromBlockchainCase <$> bcCases+                       keepError (Left e) = errorFatal e+                       keepError _        = True+                       filteredCases = Map.filter keepError allCases+                       (erroredCases, parsedCases) = splitEithers filteredCases+    in if Map.size erroredCases > 0+    then Left ("errored case: " ++ (show erroredCases))+    else if Map.size parsedCases == 0+    then Left "No cases to check."+    else Right parsedCases+++data BlockchainError+  = TooManyBlocks+  | TooManyTxs+  | NoTxs+  | SignatureUnverified+  | InvalidTx+  | OldNetwork+  | FailedCreate+  deriving Show++errorFatal :: BlockchainError -> Bool+errorFatal TooManyBlocks = True+errorFatal TooManyTxs = True+errorFatal SignatureUnverified = True+errorFatal InvalidTx = True+errorFatal _ = False++fromBlockchainCase :: BlockchainCase -> Either BlockchainError Case+fromBlockchainCase (BlockchainCase blocks preState postState network) =+  case (blocks, network) of+    ([block], "London") -> case blockTxs block of+      [tx] -> fromBlockchainCase' block tx preState postState+      []        -> Left NoTxs+      _         -> Left TooManyTxs+    ([_], _) -> Left OldNetwork+    (_, _)   -> Left TooManyBlocks++fromBlockchainCase' :: Block -> Transaction+                       -> Map Addr (EVM.Contract, Storage) -> Map Addr (EVM.Contract, Storage)+                       -> Either BlockchainError Case+fromBlockchainCase' block tx preState postState =+  let isCreate = isNothing (txToAddr tx) in+  case (sender 1 tx, checkTx tx block preState) of+      (Nothing, _) -> Left SignatureUnverified+      (_, Nothing) -> Left (if isCreate then FailedCreate else InvalidTx)+      (Just origin, Just checkState) -> Right $ Case+        (EVM.VMOpts+         { vmoptContract      = EVM.initialContract theCode+         , vmoptCalldata      = (cd, [])+         , vmoptValue         = Lit (txValue tx)+         , vmoptAddress       = toAddr+         , vmoptCaller        = litAddr origin+         , vmoptStorageBase   = Concrete+         , vmoptOrigin        = origin+         , vmoptGas           = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx)+         , vmoptBaseFee       = blockBaseFee block+         , vmoptPriorityFee   = priorityFee tx (blockBaseFee block)+         , vmoptGaslimit      = txGasLimit tx+         , vmoptNumber        = blockNumber block+         , vmoptTimestamp     = Lit $ blockTimestamp block+         , vmoptCoinbase      = blockCoinbase block+         , vmoptPrevRandao    = blockDifficulty block+         , vmoptMaxCodeSize   = 24576+         , vmoptBlockGaslimit = blockGasLimit block+         , vmoptGasprice      = effectiveGasPrice+         , vmoptSchedule      = feeSchedule+         , vmoptChainId       = 1+         , vmoptCreate        = isCreate+         , vmoptTxAccessList  = txAccessMap tx+         , vmoptAllowFFI      = False+         })+        checkState+        postState+          where+            toAddr = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)+            senderNonce = view (accountAt origin . nonce) (Map.map fst preState)+            feeSchedule = EVM.FeeSchedule.berlin+            toCode = Map.lookup toAddr preState+            theCode = if isCreate+                      then EVM.InitCode (txData tx) mempty+                      else maybe (EVM.RuntimeCode (EVM.ConcreteRuntimeCode "")) (view contractcode . fst) toCode+            effectiveGasPrice = effectiveprice tx (blockBaseFee block)+            cd = if isCreate+                 then mempty+                 else ConcreteBuf $ txData tx++effectiveprice :: Transaction -> W256 -> W256+effectiveprice tx baseFee = priorityFee tx baseFee + baseFee++priorityFee :: Transaction -> W256 -> W256+priorityFee tx baseFee = let+    (txPrioMax, txMaxFee) = case txType tx of+               EIP1559Transaction ->+                 let maxPrio = fromJust $ txMaxPriorityFeeGas tx+                     maxFee = fromJust $ txMaxFeePerGas tx+                 in (maxPrio, maxFee)+               _ ->+                 let gasPrice = fromJust $ txGasPrice tx+                 in (gasPrice, gasPrice)+  in min txPrioMax (txMaxFee - baseFee)++maxBaseFee :: Transaction -> W256+maxBaseFee tx =+  case txType tx of+     EIP1559Transaction -> fromJust $ txMaxFeePerGas tx+     _ -> fromJust $ txGasPrice tx++validateTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe ()+validateTx tx block cs = do+  let cs' = Map.map fst cs+  origin        <- sender 1 tx+  originBalance <- (view balance) <$> view (at origin) cs'+  originNonce   <- (view nonce)   <$> view (at origin) cs'+  let gasDeposit = (effectiveprice tx (blockBaseFee block)) * (num $ txGasLimit tx)+  if gasDeposit + (txValue tx) <= originBalance+    && txNonce tx == originNonce && blockBaseFee block <= maxBaseFee tx+  then Just ()+  else Nothing++checkTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe (Map Addr (EVM.Contract, Storage))+checkTx tx block prestate = do+  origin <- sender 1 tx+  validateTx tx block prestate+  let isCreate   = isNothing (txToAddr tx)+      senderNonce = view (accountAt origin . nonce) (Map.map fst prestate)+      toAddr      = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)+      prevCode    = view (accountAt toAddr . contractcode) (Map.map fst prestate)+      prevNonce   = view (accountAt toAddr . nonce) (Map.map fst prestate)+  if isCreate && ((case prevCode of {EVM.RuntimeCode (EVM.ConcreteRuntimeCode b) -> not (BS.null b); _ -> True}) || (prevNonce /= 0))+  then mzero+  else+    return prestate++vmForCase :: Case -> EVM.VM+vmForCase x =+  let+    a = checkContracts x+    cs = Map.map fst a+    st = Map.mapKeys num $ Map.map snd a+    vm = EVM.makeVm (testVmOpts x)+      & set (EVM.env . EVM.contracts) cs+      & set (EVM.env . EVM.storage) (ConcreteStore st)+      & set (EVM.env . EVM.origStorage) st+  in+    initTx vm

@@ -75,10 +75,14 @@         postVm <- withSolvers Z3 1 Nothing $ \solvers ->           execStateT (Stepper.interpret (Fetch.oracle solvers (Just (BlockNumber blockNum, testRpc))) . void $ Stepper.execFully) vm         let-          (ConcreteStore postStore) = view (env . storage) postVm+          postStore = case view (env . storage) postVm of+            ConcreteStore s -> s+            _ -> error "ConcreteStore expected"           wethStore = fromJust $ Map.lookup 0xC02aaA39b223FE8D0A0e5C4F27eAD9083C756Cc2 postStore           receiverBal = fromJust $ Map.lookup (keccak' (word256Bytes 0xdead <> word256Bytes 0x3)) wethStore-          (Just (VMSuccess msg)) = view result postVm+          msg = case view result postVm of+            Just (VMSuccess m) -> m+            _ -> error "VMSuccess expected"         assertEqual "should succeed" msg (ConcreteBuf $ word256Bytes 0x1)         assertEqual "should revert" receiverBal (W256 $ 2595433725034301 + wad) 

@@ -7,7 +7,7 @@  import Data.Text (Text) import Data.ByteString (ByteString)-import Data.Bits+import Data.Bits hiding (And, Xor) import System.Directory import GHC.Natural import Control.Monad@@ -19,19 +19,18 @@ import Prelude hiding (fail, LT, GT)  import qualified Data.ByteString as BS-import qualified Data.ByteString.Lazy as BS (fromStrict) import qualified Data.ByteString.Base16 as Hex import Data.Maybe import Data.Typeable import Data.List (elemIndex) import Data.DoubleWord import Test.Tasty-import Test.Tasty.QuickCheck+import Test.Tasty.QuickCheck hiding (Failure) import Test.QuickCheck.Instances.Text() import Test.QuickCheck.Instances.Natural() import Test.QuickCheck.Instances.ByteString() import Test.Tasty.HUnit-import Test.Tasty.Runners+import Test.Tasty.Runners hiding (Failure) import Test.Tasty.ExpectedFailure  import Control.Monad.State.Strict (execState, runState)@@ -329,7 +328,9 @@           -- traceM ("encoding: " ++ (show y) ++ " : " ++ show (abiValueType y))           Just encoded <- runStatements [i| x = abi.encode(a);|]             [y] AbiBytesDynamicType-          let AbiTuple (Vector.toList -> [solidityEncoded]) = decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded)+          let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of+                AbiTuple (Vector.toList -> [e]) -> e+                _ -> error "AbiTuple expected"           let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [y])           -- traceM ("encoded (solidity): " ++ show solidityEncoded)           -- traceM ("encoded (hevm): " ++ show (AbiBytesDynamic hevmEncoded))@@ -340,7 +341,9 @@           -- traceM ("encoding: " ++ (show x') ++ ", " ++ (show y')  ++ " : " ++ show (abiValueType x') ++ ", " ++ show (abiValueType y'))           Just encoded <- runStatements [i| x = abi.encode(a, b);|]             [x', y'] AbiBytesDynamicType-          let AbiTuple (Vector.toList -> [solidityEncoded]) = decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded)+          let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of+                AbiTuple (Vector.toList -> [e]) -> e+                _ -> error "AbiTuple expected"           let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [x',y'])           -- traceM ("encoded (solidity): " ++ show solidityEncoded)           -- traceM ("encoded (hevm): " ++ show (AbiBytesDynamic hevmEncoded))@@ -421,9 +424,9 @@                 |]          (json, path') <- solidity' srccode-        let Just (solc', _, _) = readJSON json+        let (solc', _, _) = fromJust $ readJSON json             initCode :: ByteString-            Just initCode = solc' ^? ix (path' <> ":A") . creationCode+            initCode = fromJust $ solc' ^? ix (path' <> ":A") . creationCode         -- add constructor arguments         assertEqual "constructor args screwed up metadata stripping" (stripBytecodeMetadata (initCode <> encodeAbiValue (AbiUInt 256 1))) (stripBytecodeMetadata initCode)     ]@@ -1036,11 +1039,15 @@             }           }           |]-        let pre preVM = let [x, y] = getStaticAbiArgs 2 preVM+        let pre preVM = let (x, y) = case getStaticAbiArgs 2 preVM of+                                       [x', y'] -> (x', y')+                                       _ -> error "expected 2 args"                         in (x .<= Expr.add x y)                            .&& view (state . callvalue) preVM .== Lit 0             post prestate leaf =-              let [x, y] = getStaticAbiArgs 2 prestate+              let (x, y) = case getStaticAbiArgs 2 prestate of+                             [x', y'] -> (x', y')+                             _ -> error "expected 2 args"               in case leaf of                    Return _ b _ -> (ReadWord (Lit 0) b) .== (Add x y)                    _ -> PBool True@@ -1057,12 +1064,16 @@             }           }           |]-        let pre preVM = let [x, y] = getStaticAbiArgs  2 preVM+        let pre preVM = let (x, y) = case getStaticAbiArgs 2 preVM of+                                       [x', y'] -> (x', y')+                                       _ -> error "expected 2 args"                         in (x .<= Expr.add x y)                            .&& (x .== y)                            .&& view (state . callvalue) preVM .== Lit 0             post prestate leaf =-              let [_, y] = getStaticAbiArgs 2 prestate+              let (_, y) = case getStaticAbiArgs 2 prestate of+                             [x', y'] -> (x', y')+                             _ -> error "expected 2 args"               in case leaf of                    Return _ b _ -> (ReadWord (Lit 0) b) .== (Mul (Lit 2) y)                    _ -> PBool True@@ -1085,7 +1096,9 @@           |]         let pre vm = Lit 0 .== view (state . callvalue) vm             post prestate leaf =-              let [y] = getStaticAbiArgs 1 prestate+              let y = case getStaticAbiArgs 1 prestate of+                        [y'] -> y'+                        _ -> error "expected 1 arg"                   this = Expr.litAddr $ view (state . codeContract) prestate                   prex = Expr.readStorage' this (Lit 0) (view (env . storage) prestate)               in case leaf of@@ -1137,7 +1150,9 @@             |]           let pre vm = (Lit 0) .== view (state . callvalue) vm               post prestate poststate =-                let [x,y] = getStaticAbiArgs 2 prestate+                let (x,y) = case getStaticAbiArgs 2 prestate of+                        [x',y'] -> (x',y')+                        _ -> error "expected 2 args"                     this = Expr.litAddr $ view (state . codeContract) prestate                     prestore =  view (env . storage) prestate                     prex = Expr.readStorage' this x prestore@@ -1169,7 +1184,9 @@             |]           let pre vm = (Lit 0) .== view (state . callvalue) vm               post prestate poststate =-                let [x,y] = getStaticAbiArgs 2 prestate+                let (x,y) = case getStaticAbiArgs 2 prestate of+                        [x',y'] -> (x',y')+                        _ -> error "expected 2 args"                     this = Expr.litAddr $ view (state . codeContract) prestate                     prestore =  view (env . storage) prestate                     prex = Expr.readStorage' this x prestore@@ -1613,7 +1630,7 @@             let vm = vm0                   & set (state . callvalue) (Lit 0)                   & over (env . contracts)-                       (Map.insert aAddr (initialContract (RuntimeCode (fromJust $ Expr.toList $ ConcreteBuf a))))+                       (Map.insert aAddr (initialContract (RuntimeCode (ConcreteRuntimeCode a))))                   -- NOTE: this used to as follows, but there is no _storage field in Contract record                   -- (Map.insert aAddr (initialContract (RuntimeCode $ ConcreteBuffer a) &                   --                     set EVM.storage (EVM.Symbolic [] store)))@@ -2124,7 +2141,7 @@     case runState exec (vmForEthrunCreation x) of        (VMSuccess (ConcreteBuf targetCode), vm1) -> do          let target = view (state . contract) vm1-             vm2 = execState (replaceCodeOfSelf (RuntimeCode (fromJust $ Expr.toList $ ConcreteBuf targetCode))) vm1+             vm2 = execState (replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode targetCode))) vm1          return $ snd $ flip runState vm2                 (do resetState                     assign (state . gas) 0xffffffffffffffff -- kludge@@ -2188,7 +2205,9 @@ -- includes shaving off 4 byte function sig decodeAbiValues :: [AbiType] -> ByteString -> [AbiValue] decodeAbiValues types bs =-  let AbiTuple xy = decodeAbiValue (AbiTupleType $ Vector.fromList types) (BS.fromStrict (BS.drop 4 bs))+  let xy = case decodeAbiValue (AbiTupleType $ Vector.fromList types) (BS.fromStrict (BS.drop 4 bs)) of+        AbiTuple xy' -> xy'+        _ -> error "AbiTuple expected"   in Vector.toList xy  newtype Bytes = Bytes ByteString@@ -2270,13 +2289,14 @@ genNat = fmap fromIntegral (arbitrary :: Gen Natural)  genName :: Gen Text-genName = fmap T.pack $ listOf1 (oneof . (fmap pure) $ ['a'..'z'] <> ['A'..'Z'])+-- In order not to generate SMT reserved words, we prepend with "esc_"+genName = fmap (T.pack . ("esc_" <> )) $ listOf1 (oneof . (fmap pure) $ ['a'..'z'] <> ['A'..'Z'])  genEnd :: Int -> Gen (Expr End) genEnd 0 = oneof- [ pure $ Invalid []- , pure $ EVM.Types.IllegalOverflow []- , pure $ SelfDestruct []+ [ pure $ Failure [] Invalid+ , pure $ Failure [] EVM.Types.IllegalOverflow+ , pure $ Failure [] SelfDestruct  ] genEnd sz = oneof  [ fmap (EVM.Types.Revert []) subBuf