hevm 0.51.1 → 0.51.2

raw patch · 41 files changed

+1630/−1552 lines, 41 filesdep +githashdep +witchPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: githash, witch

API changes (from Hackage documentation)

Files

• CHANGELOG.md +18/−0
• hevm-cli/hevm-cli.hs +91/−88
• hevm.cabal +10/−4
• src/EVM.hs +136/−128
• src/EVM/ABI.hs +51/−53
• src/EVM/Assembler.hs +7/−8
• src/EVM/CSE.hs +4/−6
• src/EVM/Concrete.hs +14/−16
• src/EVM/Dapp.hs +5/−4
• src/EVM/Debug.hs +12/−15
• src/EVM/Dev.hs +19/−19
• src/EVM/Exec.hs +3/−5
• src/EVM/Expr.hs +61/−59
• src/EVM/Facts.hs +20/−26
• src/EVM/Facts/Git.hs +2/−3
• src/EVM/Fetch.hs +40/−47
• src/EVM/Format.hs +40/−43
• src/EVM/Keccak.hs +6/−11
• src/EVM/Op.hs +154/−153
• src/EVM/Patricia.hs +39/−39
• src/EVM/Precompiled.hs +1/−1
• src/EVM/RLP.hs +38/−33
• src/EVM/SMT.hs +81/−79
• src/EVM/Sign.hs +20/−21
• src/EVM/Solidity.hs +79/−34
• src/EVM/Solvers.hs +49/−24
• src/EVM/Stepper.hs +7/−8
• src/EVM/StorageLayout.hs +12/−11
• src/EVM/SymExec.hs +110/−105
• src/EVM/TTY.hs +17/−18
• src/EVM/TTYCenteredList.hs +36/−37
• src/EVM/Transaction.hs +24/−26
• src/EVM/Traversals.hs +87/−13
• src/EVM/Types.hs +82/−43
• src/EVM/UnitTest.hs +70/−79
• test/EVM/Test/BlockchainTests.hs +8/−9
• test/EVM/Test/Tracing.hs +64/−74
• test/EVM/Test/Utils.hs +9/−8
• test/contracts/pass/dsProvePass.sol +15/−14
• test/rpc.hs +8/−8
• test/test.hs +81/−180

@@ -5,6 +5,24 @@ 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.51.2] - 2023-07-11++## Fixed++- SMT encoding of Expr now has assertions for the range of environment values that are less than word size (256 bits).+- Trace now contains the cheat code calls+- More consistent error messages++## Changed++- SMT2 scripts are now being reprocessed to put one sexpr per line. Having sepxrs that span across multiple lines trigers a bug in CVC5.+- Removing long-running tests so we can finish all unit tests in approx 10 minutes on a current-gen laptop CPU+- Added git revision to `hevm version`++## Added++- execution traces are now shown for failed `prove_` tests+ ## [0.51.1] - 2023-06-02  ## Fixed

@@ -1,62 +1,57 @@ -- Main file of the hevm CLI program -{-# Language DataKinds #-}-{-# Language DeriveAnyClass #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE TemplateHaskell #-}  module Main where -import EVM.Concrete (createAddress)-import EVM (initialContract, makeVm)-import qualified EVM.FeeSchedule as FeeSchedule-import qualified EVM.Fetch-import qualified EVM.Stepper+import Control.Monad (void, when, forM_, unless)+import Control.Monad.State.Strict (liftIO)+import Data.Bifunctor (second)+import Data.ByteString (ByteString)+import Data.ByteString qualified as ByteString+import Data.ByteString.Char8 qualified as Char8+import Data.ByteString.Lazy qualified as LazyByteString+import Data.DoubleWord (Word256)+import Data.List (intersperse)+import Data.Map qualified as Map+import Data.Maybe (fromMaybe, mapMaybe)+import Data.Text (pack)+import Data.Text qualified as T+import Data.Text.IO qualified as T+import Data.Version (showVersion)+import Data.Word (Word64)+import GHC.Conc (getNumProcessors)+import Numeric.Natural (Natural)+import Optics.Core ((&), (%), set)+import Witch (unsafeInto)+import Options.Generic as Options+import Paths_hevm qualified as Paths+import System.IO (stderr)+import System.Directory (withCurrentDirectory, getCurrentDirectory, doesDirectoryExist)+import System.FilePath ((</>))+import System.Exit (exitFailure, exitWith, ExitCode(..)) -import EVM.SymExec-import EVM.Debug-import qualified EVM.Expr as Expr-import EVM.Solvers-import qualified EVM.TTY as TTY+import EVM (initialContract, makeVm)+import EVM.Concrete (createAddress)+import EVM.Dapp (findUnitTests, dappInfo, DappInfo, emptyDapp)+import EVM.Debug (Mode(..))+import EVM.Expr qualified as Expr+import EVM.Facts qualified as Facts+import EVM.Facts.Git qualified as Git+import GitHash+import EVM.FeeSchedule qualified as FeeSchedule+import EVM.Fetch qualified+import EVM.Format (hexByteString, strip0x, showTraceTree, formatExpr) import EVM.Solidity-import EVM.Expr (litAddr)+import EVM.Solvers+import EVM.Stepper qualified+import EVM.SymExec+import EVM.Transaction qualified+import EVM.TTY qualified as TTY import EVM.Types hiding (word)-import EVM.Format (hexByteString, strip0x)-import EVM.UnitTest (UnitTestOptions, coverageReport, coverageForUnitTestContract, getParametersFromEnvironmentVariables, unitTest)-import EVM.Dapp (findUnitTests, dappInfo, DappInfo, emptyDapp)-import GHC.Natural-import EVM.Format (showTraceTree, formatExpr)-import Data.Word (Word64)-import Data.Bifunctor (second)--import qualified Data.Map as Map-import qualified EVM.Facts     as Facts-import qualified EVM.Facts.Git as Git-import qualified EVM.UnitTest--import GHC.Conc-import Optics.Core hiding (pre, Empty)-import Control.Monad              (void, when, forM_, unless)-import Control.Monad.State.Strict (liftIO)-import Data.ByteString            (ByteString)-import Data.List                  (intersperse)-import Data.Text                  (pack)-import Data.Maybe                 (fromMaybe, mapMaybe)-import Data.Version               (showVersion)-import Data.DoubleWord            (Word256)-import System.IO                  (stderr)-import System.Directory           (withCurrentDirectory, getCurrentDirectory, doesDirectoryExist)-import System.FilePath            ((</>))-import System.Exit                (exitFailure, exitWith, ExitCode(..))--import qualified Data.ByteString        as ByteString-import qualified Data.ByteString.Char8  as Char8-import qualified Data.ByteString.Lazy   as LazyByteString-import qualified Data.Text              as T-import qualified Data.Text.IO           as T--import qualified Paths_hevm      as Paths--import Options.Generic as Options-import qualified EVM.Transaction+import EVM.UnitTest  -- This record defines the program's command-line options -- automatically via the `optparse-generic` package.@@ -237,7 +232,7 @@        then EVM.Fetch.Latest        else EVM.Fetch.BlockNumber testn -  pure EVM.UnitTest.UnitTestOptions+  pure UnitTestOptions     { solvers = solvers     , rpcInfo = case cmd.rpc of          Just url -> Just (block', url)@@ -254,18 +249,26 @@     , fuzzRuns = fromMaybe 100 cmd.fuzzRuns     , replay = do         arg' <- cmd.replay-        return (fst arg', LazyByteString.fromStrict (hexByteString "--replay" $ strip0x $ snd arg'))+        pure (fst arg', LazyByteString.fromStrict (hexByteString "--replay" $ strip0x $ snd arg'))     , vmModifier = vmModifier     , testParams = params     , dapp = srcInfo     , ffiAllowed = cmd.ffi     } +getFullVersion :: [Char]+getFullVersion = showVersion Paths.version <> " [" <> gitVersion <> "]"+  where+    gitInfo = $$tGitInfoCwdTry+    gitVersion = case gitInfo of+      Right val -> "git rev " <> giBranch val <>  "@" <> giHash val+      Left _ -> "no git revision present"+ main :: IO () main = do   cmd <- Options.unwrapRecord "hevm -- Ethereum evaluator"   case cmd of-    Version {} -> putStrLn (showVersion Paths.version)+    Version {} ->putStrLn getFullVersion     Symbolic {} -> do       root <- getRoot cmd       withCurrentDirectory root $ assert cmd@@ -275,7 +278,7 @@     Test {} -> do       root <- getRoot cmd       withCurrentDirectory root $ do-        cores <- num <$> getNumProcessors+        cores <- unsafeInto <$> getNumProcessors         solver <- getSolver cmd         withSolvers solver cores cmd.smttimeout $ \solvers -> do           buildOut <- readBuildOutput root (getProjectType cmd)@@ -291,7 +294,7 @@                   res <- unitTest testOpts out.contracts cmd.cache                   unless res exitFailure                 (False, Debug) -> liftIO $ TTY.main testOpts root (Just out)-                (False, JsonTrace) -> error "json traces not implemented for dappTest"+                (False, JsonTrace) -> internalError "json traces not implemented for dappTest"                 (True, _) -> liftIO $ dappCoverage testOpts (optsMode cmd) out  @@ -379,7 +382,7 @@   calldata <- buildCalldata cmd   preState <- symvmFromCommand cmd calldata   let errCodes = fromMaybe defaultPanicCodes cmd.assertions-  cores <- num <$> getNumProcessors+  cores <- unsafeInto <$> getNumProcessors   let solverCount = fromMaybe cores cmd.numSolvers   solver <- getSolver cmd   withSolvers solver solverCount cmd.smttimeout $ \solvers -> do@@ -521,11 +524,11 @@               Just path ->                 Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts vm'.cache)           _ ->-            error "Internal error: no EVM result"+            internalError "no EVM result"        Debug -> void $ TTY.runFromVM solvers rpcinfo Nothing dapp vm       --JsonTrace -> void $ execStateT (interpretWithTrace fetcher EVM.Stepper.runFully) vm-      _ -> error "TODO"+      _ -> internalError "TODO"      where block = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block            rpcinfo = (,) block <$> cmd.rpc @@ -535,25 +538,25 @@   withCache <- applyCache (cmd.state, cmd.cache)    (miner,ts,baseFee,blockNum,prevRan) <- case cmd.rpc of-    Nothing -> return (0,Lit 0,0,0,0)+    Nothing -> pure (0,Lit 0,0,0,0)     Just url -> EVM.Fetch.fetchBlockFrom block url >>= \case-      Nothing -> error "Could not fetch block"-      Just Block{..} -> return ( coinbase-                                   , timestamp-                                   , baseFee-                                   , number-                                   , prevRandao-                                   )+      Nothing -> error "Error: Could not fetch block"+      Just Block{..} -> pure ( coinbase+                             , timestamp+                             , baseFee+                             , number+                             , prevRandao+                             )    contract <- case (cmd.rpc, cmd.address, cmd.code) of     (Just url, Just addr', Just c) -> do       EVM.Fetch.fetchContractFrom block url addr' >>= \case         Nothing ->-          error $ "contract not found: " <> show address+          error $ "Error: contract not found: " <> show address         Just contract ->           -- if both code and url is given,           -- fetch the contract and overwrite the code-          return $+          pure $             initialContract  (mkCode $ hexByteString "--code" $ strip0x c)               & set #balance  (contract.balance)               & set #nonce    (contract.nonce)@@ -562,21 +565,21 @@     (Just url, Just addr', Nothing) ->       EVM.Fetch.fetchContractFrom block url addr' >>= \case         Nothing ->-          error $ "contract not found: " <> show address-        Just contract -> return contract+          error $ "Error: contract not found: " <> show address+        Just contract -> pure contract      (_, _, Just c)  ->-      return $+      pure $         initialContract (mkCode $ hexByteString "--code" $ strip0x c)      (_, _, Nothing) ->-      error "must provide at least (rpc + address) or code"+      error "Error: must provide at least (rpc + address) or code"    let ts' = case maybeLitWord ts of         Just t -> t-        Nothing -> error "unexpected symbolic timestamp when executing vm test"+        Nothing -> internalError "unexpected symbolic timestamp when executing vm test" -  return $ EVM.Transaction.initTx $ withCache (vm0 baseFee miner ts' blockNum prevRan contract)+  pure $ EVM.Transaction.initTx $ withCache (vm0 baseFee miner ts' blockNum prevRan contract)     where         block   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block         value   = word (.value) 0@@ -596,7 +599,7 @@           , calldata      = (calldata, [])           , value         = Lit value           , address       = address-          , caller        = litAddr caller+          , caller        = Expr.litAddr caller           , origin        = origin           , gas           = word64 (.gas) 0xffffffffffffffff           , baseFee       = baseFee@@ -624,14 +627,14 @@ symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM) symvmFromCommand cmd calldata = do   (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of-    Nothing -> return (0,0,0,0)+    Nothing -> pure (0,0,0,0)     Just url -> EVM.Fetch.fetchBlockFrom block url >>= \case-      Nothing -> error "Could not fetch block"-      Just Block{..} -> return ( coinbase-                                   , number-                                   , baseFee-                                   , prevRandao-                                   )+      Nothing -> error "Error: Could not fetch block"+      Just Block{..} -> pure ( coinbase+                             , number+                             , baseFee+                             , prevRandao+                             )    let     caller = Caller 0@@ -645,8 +648,8 @@     (Just url, Just addr', _) ->       EVM.Fetch.fetchContractFrom block url addr' >>= \case         Nothing ->-          error "contract not found."-        Just contract' -> return contract''+          error "Error: contract not found."+        Just contract' -> pure contract''           where             contract'' = case cmd.code of               Nothing -> contract'@@ -660,11 +663,11 @@                         & set #external    (contract'.external)      (_, _, Just c)  ->-      return (initialContract . mkCode $ decipher c)+      pure (initialContract . mkCode $ decipher c)     (_, _, Nothing) ->-      error "must provide at least (rpc + address) or code"+      error "Error: must provide at least (rpc + address) or code" -  return $ (EVM.Transaction.initTx $ withCache $ vm0 baseFee miner ts blockNum prevRan calldata callvalue caller contract)+  pure $ (EVM.Transaction.initTx $ withCache $ vm0 baseFee miner ts blockNum prevRan calldata callvalue caller contract)     & set (#env % #storage) store    where

@@ -2,7 +2,7 @@ name:   hevm version:-  0.51.1+  0.51.2 synopsis:   Ethereum virtual machine evaluator description:@@ -186,7 +186,8 @@     spool                             >= 0.1 && < 0.2,     stm                               >= 2.5.0 && < 2.6.0,     spawn                             >= 0.3 && < 0.4,-    filepattern                       >= 0.1.2 && < 0.2+    filepattern                       >= 0.1.2 && < 0.2,+    witch                             >= 1.1 && < 1.3   if !os(windows)     build-depends:       brick                           >= 1.4 && < 1.5,@@ -206,6 +207,7 @@   if os(darwin)     extra-libraries: c++     ld-options: -Wl,-keep_dwarf_unwind+    ghc-options: -fcompact-unwind   else     extra-libraries: stdc++   build-depends:@@ -240,7 +242,9 @@     vty,     stm,     spawn,-    optics-core+    optics-core,+    githash                       >= 0.1.6 && < 0.2,+    witch   if os(windows)     buildable: False @@ -292,7 +296,8 @@     smt2-parser >= 0.1.0.1,     operational,     optics-core,-    optics-extra+    optics-extra,+    witch  library test-utils   import:@@ -321,6 +326,7 @@     extra-libraries: c++     -- https://gitlab.haskell.org/ghc/ghc/-/issues/11829     ld-options: -Wl,-keep_dwarf_unwind+    ghc-options: -fcompact-unwind   else     extra-libraries: stdc++ 

@@ -1,15 +1,9 @@-{-# Language ImplicitParams #-}-{-# Language UndecidableInstances #-}-{-# Language ScopedTypeVariables #-}-{-# Language GADTs #-} {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DuplicateRecordFields #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE ImplicitParams #-}  module EVM where -import Prelude hiding (log, exponent, GT, LT)+import Prelude hiding (exponent)  import Optics.Core import Optics.State@@ -55,6 +49,7 @@ import Data.Vector.Storable qualified as SV import Data.Vector.Storable.Mutable qualified as SV import Data.Word (Word8, Word32, Word64)+import Witch (into, unsafeInto)  import Crypto.Hash (Digest, SHA256, RIPEMD160) import Crypto.Hash qualified as Crypto@@ -193,7 +188,7 @@     mem  = vm.state.memory     stk  = vm.state.stack     self = vm.state.contract-    this = fromMaybe (error "internal error: state contract") (Map.lookup self vm.env.contracts)+    this = fromMaybe (internalError "state contract") (Map.lookup self vm.env.contracts)      fees@FeeSchedule {..} = vm.block.schedule @@ -233,10 +228,10 @@                   InitCode conc _ -> BS.index conc vm.state.pc                   RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs vm.state.pc                   RuntimeCode (SymbolicRuntimeCode ops) ->-                    fromMaybe (error "could not analyze symbolic code") $+                    fromMaybe (internalError "could not analyze symbolic code") $                       maybeLitByte $ ops V.! vm.state.pc -      case getOp(?op) of+      case getOp (?op) of          OpPush0 -> do           limitStack 1 $@@ -245,7 +240,7 @@               pushSym (Lit 0)          OpPush n' -> do-          let n = fromIntegral n'+          let n = into n'               !xs = case vm.state.code of                 InitCode conc _ -> Lit $ word $ padRight n $ BS.take n (BS.drop (1 + vm.state.pc) conc)                 RuntimeCode (ConcreteRuntimeCode bs) -> Lit $ word $ BS.take n $ BS.drop (1 + vm.state.pc) bs@@ -258,7 +253,7 @@               pushSym xs          OpDup i ->-          case preview (ix (fromIntegral i - 1)) stk of+          case preview (ix (into i - 1)) stk of             Nothing -> underrun             Just y ->               limitStack 1 $@@ -267,27 +262,27 @@                   pushSym y          OpSwap i ->-          if length stk < (fromIntegral i) + 1+          if length stk < (into i) + 1             then underrun             else               burn g_verylow $ do                 next                 zoom (#state % #stack) $ do-                  assign (ix 0) (stk ^?! ix (fromIntegral i))-                  assign (ix (fromIntegral i)) (stk ^?! ix 0)+                  assign (ix 0) (stk ^?! ix (into i))+                  assign (ix (into i)) (stk ^?! ix 0)          OpLog n ->           notStatic $           case stk of             (xOffset':xSize':xs) ->-              if length xs < (fromIntegral n)+              if length xs < (into n)               then underrun               else                 forceConcrete2 (xOffset', xSize') "LOG" $ \(xOffset, xSize) -> do-                    let (topics, xs') = splitAt (fromIntegral n) xs+                    let (topics, xs') = splitAt (into n) xs                         bytes         = readMemory xOffset' xSize' vm                         logs'         = (LogEntry (litAddr self) bytes topics) : vm.logs-                    burn (g_log + g_logdata * (num xSize) + num n * g_logtopic) $+                    burn (g_log + g_logdata * (unsafeInto xSize) + into n * g_logtopic) $                       accessMemoryRange xOffset xSize $ do                         traceTopLog logs'                         next@@ -337,7 +332,7 @@             xOffset':xSize':xs ->               forceConcrete xOffset' "sha3 offset must be concrete" $                 \xOffset -> forceConcrete xSize' "sha3 size must be concrete" $ \xSize ->-                  burn (g_sha3 + g_sha3word * ceilDiv (num xSize) 32) $+                  burn (g_sha3 + g_sha3word * ceilDiv (unsafeInto xSize) 32) $                     accessMemoryRange xOffset xSize $ do                       (hash, invMap) <- case readMemory xOffset' xSize' vm of                                           ConcreteBuf bs -> do@@ -354,22 +349,22 @@          OpAddress ->           limitStack 1 $-            burn g_base (next >> push (num self))+            burn g_base (next >> push (into self))          OpBalance ->           case stk of             x':xs -> forceConcrete x' "BALANCE" $ \x ->-              accessAndBurn (num x) $-                fetchAccount (num x) $ \c -> do+              accessAndBurn (unsafeInto x) $+                fetchAccount (unsafeInto x) $ \c -> do                   next                   assign (#state % #stack) xs-                  push (num c.balance)+                  push c.balance             [] ->               underrun          OpOrigin ->           limitStack 1 . burn g_base $-            next >> push (num vm.tx.origin)+            next >> push (into vm.tx.origin)          OpCaller ->           limitStack 1 . burn g_base $@@ -391,7 +386,7 @@             xTo':xFrom:xSize':xs ->               forceConcrete2 (xTo', xSize') "CALLDATACOPY" $                 \(xTo, xSize) ->-                  burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $+                  burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) $                     accessMemoryRange xTo xSize $ do                       next                       assign (#state % #stack) xs@@ -411,7 +406,7 @@                     Nothing -> vmError IllegalOverflow                     Just n'' ->                       if n'' <= ( (maxBound :: Word64) - g_verylow ) `div` g_copy * 32 then-                        burn (g_verylow + g_copy * ceilDiv (num n) 32) $+                        burn (g_verylow + g_copy * ceilDiv (unsafeInto n) 32) $                           accessMemoryRange memOffset n $ do                             next                             assign (#state % #stack) xs@@ -426,14 +421,14 @@         OpExtcodesize ->           case stk of             x':xs -> case x' of-              Lit x -> if x == num cheatCode+              Lit x -> if x == into cheatCode                 then do                   next                   assign (#state % #stack) xs                   pushSym (Lit 1)                 else-                  accessAndBurn (num x) $-                    fetchAccount (num x) $ \c -> do+                  accessAndBurn (unsafeInto x) $+                    fetchAccount (unsafeInto x) $ \c -> do                       next                       assign (#state % #stack) xs                       pushSym (bufLength (view bytecode c))@@ -449,11 +444,11 @@             extAccount':memOffset':codeOffset:codeSize':xs ->               forceConcrete3 (extAccount', memOffset', codeSize') "EXTCODECOPY" $                 \(extAccount, memOffset, codeSize) -> do-                  acc <- accessAccountForGas (num extAccount)+                  acc <- accessAccountForGas (unsafeInto extAccount)                   let cost = if acc then g_warm_storage_read else g_cold_account_access-                  burn (cost + g_copy * ceilDiv (num codeSize) 32) $+                  burn (cost + g_copy * ceilDiv (unsafeInto codeSize) 32) $                     accessMemoryRange memOffset codeSize $-                      fetchAccount (num extAccount) $ \c -> do+                      fetchAccount (unsafeInto extAccount) $ \c -> do                         next                         assign (#state % #stack) xs                         copyBytesToMemory (view bytecode c) codeSize' codeOffset memOffset'@@ -467,7 +462,7 @@           case stk of             xTo':xFrom:xSize':xs -> forceConcrete2 (xTo', xSize') "RETURNDATACOPY" $               \(xTo, xSize) ->-                burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $+                burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) $                   accessMemoryRange xTo xSize $ do                     next                     assign (#state % #stack) xs@@ -488,12 +483,12 @@         OpExtcodehash ->           case stk of             x':xs -> forceConcrete x' "EXTCODEHASH" $ \x ->-              accessAndBurn (num x) $ do+              accessAndBurn (unsafeInto x) $ do                 next                 assign (#state % #stack) xs-                fetchAccount (num x) $ \c ->+                fetchAccount (unsafeInto x) $ \c ->                    if accountEmpty c-                     then push (num (0 :: Int))+                     then push 0                      else pushSym $ keccak (view bytecode c)             [] ->               underrun@@ -504,12 +499,12 @@           stackOp1 g_blockhash $ \case             Lit i -> if i + 256 < vm.block.number || i >= vm.block.number                      then Lit 0-                     else (num i :: Integer) & show & Char8.pack & keccak' & Lit+                     else (into i :: Integer) & show & Char8.pack & keccak' & Lit             i -> BlockHash i          OpCoinbase ->           limitStack 1 . burn g_base $-            next >> push (num vm.block.coinbase)+            next >> push (into vm.block.coinbase)          OpTimestamp ->           limitStack 1 . burn g_base $@@ -525,7 +520,7 @@          OpGaslimit ->           limitStack 1 . burn g_base $-            next >> push (num vm.block.gaslimit)+            next >> push (into vm.block.gaslimit)          OpChainid ->           limitStack 1 . burn g_base $@@ -592,8 +587,8 @@               accessStorage self x $ \current -> do                 availableGas <- use (#state % #gas) -                if num availableGas <= g_callstipend then-                  finishFrame (FrameErrored (OutOfGas availableGas (num g_callstipend)))+                if availableGas <= g_callstipend then+                  finishFrame (FrameErrored (OutOfGas availableGas g_callstipend))                 else do                   let                     original =@@ -664,15 +659,15 @@          OpPc ->           limitStack 1 . burn g_base $-            next >> push (num vm.state.pc)+            next >> push (unsafeInto vm.state.pc)          OpMsize ->           limitStack 1 . burn g_base $-            next >> push (num vm.state.memorySize)+            next >> push (into vm.state.memorySize)          OpGas ->           limitStack 1 . burn g_base $-            next >> push (num (vm.state.gas - g_base))+            next >> push (into (vm.state.gas - g_base))          OpJumpdest -> burn g_jumpdest next @@ -684,7 +679,7 @@             base:exponent':xs -> forceConcrete exponent' "EXP: symbolic exponent" $ \exponent ->               let cost = if exponent == 0                          then g_exp-                         else g_exp + g_expbyte * num (ceilDiv (1 + log2 exponent) 8)+                         else g_exp + g_expbyte * unsafeInto (ceilDiv (1 + log2 exponent) 8)               in burn cost $ do                 next                 (#state % #stack) .= Expr.exp base exponent' : xs@@ -705,7 +700,7 @@                   _ <- accessAccountForGas newAddr                   burn cost $ do                     let initCode = readMemory xOffset' xSize' vm-                    create self this xSize (num gas') xValue xs newAddr initCode+                    create self this xSize gas' xValue xs newAddr initCode             _ -> underrun          OpCall ->@@ -714,7 +709,7 @@               forceConcrete6 (xGas', xValue', xInOffset', xInSize', xOutOffset', xOutSize') "CALL" $               \(xGas, xValue, xInOffset, xInSize, xOutOffset, xOutSize) ->                 (if xValue > 0 then notStatic else id) $-                  delegateCall this (num xGas) xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do+                  delegateCall this (unsafeInto xGas) xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do                     let from' = fromMaybe self vm.overrideCaller                     zoom #state $ do                       assign #callvalue (Lit xValue)@@ -732,7 +727,7 @@             xGas':xTo:xValue':xInOffset':xInSize':xOutOffset':xOutSize':xs ->               forceConcrete6 (xGas', xValue', xInOffset', xInSize', xOutOffset', xOutSize') "CALLCODE" $               \(xGas, xValue, xInOffset, xInSize, xOutOffset, xOutSize) ->-                delegateCall this (num xGas) xTo (litAddr self) xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do+                delegateCall this (unsafeInto xGas) xTo (litAddr self) xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do                   zoom #state $ do                     assign #callvalue (Lit xValue)                     assign #caller $ litAddr $ fromMaybe self vm.overrideCaller@@ -747,7 +742,7 @@               accessMemoryRange xOffset xSize $ do                 let                   output = readMemory xOffset' xSize' vm-                  codesize = fromMaybe (error "RETURN: cannot return dynamically sized abstract data")+                  codesize = fromMaybe (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data")                                . maybeLitWord . bufLength $ output                   maxsize = vm.block.maxCodeSize                   creation = case vm.frames of@@ -761,7 +756,7 @@                   then                     finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))                   else do-                    let frameReturned = burn (g_codedeposit * num codesize) $+                    let frameReturned = burn (g_codedeposit * unsafeInto codesize) $                                           finishFrame (FrameReturned output)                         frameErrored = finishFrame $ FrameErrored InvalidFormat                     case readByte (Lit 0) output of@@ -781,7 +776,7 @@             xGas':xTo:xInOffset':xInSize':xOutOffset':xOutSize':xs ->               forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "DELEGATECALL" $               \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->-                delegateCall this (num xGas) xTo (litAddr self) 0 xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do+                delegateCall this (unsafeInto xGas) xTo (litAddr self) 0 xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do                   touchAccount self             _ -> underrun @@ -808,7 +803,7 @@             xGas':xTo:xInOffset':xInSize':xOutOffset':xOutSize':xs ->               forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "STATICCALL" $               \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) -> do-                delegateCall this (num xGas) xTo xTo 0 xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do+                delegateCall this (unsafeInto xGas) xTo xTo 0 xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do                   zoom #state $ do                     assign #callvalue (Lit 0)                     assign #caller $ litAddr $ fromMaybe self (vm.overrideCaller)@@ -824,8 +819,8 @@           notStatic $           case stk of             [] -> underrun-            (xTo':_) -> forceConcrete xTo' "SELFDESTRUCT" $ \(num -> xTo) -> do-              acc <- accessAccountForGas (num xTo)+            (xTo':_) -> forceConcrete xTo' "SELFDESTRUCT" $ \(unsafeInto -> xTo) -> do+              acc <- accessAccountForGas xTo               let cost = if acc then 0 else g_cold_account_access                   funds = this.balance                   recipientExists = accountExists xTo vm@@ -883,7 +878,7 @@       let recipientExists = accountExists xContext vm       (cost, gas') <- costOfCall fees recipientExists xValue availableGas xGas xTo       burn (cost - gas') $ do-        if xValue > num this.balance+        if xValue > this.balance         then do           assign (#state % #stack) (Lit 0 : xs)           assign (#state % #returndata) mempty@@ -939,7 +934,7 @@   let input = readMemory (Lit inOffset) (Lit inSize) vm       fees = vm.block.schedule       cost = costOfPrecompile fees preCompileAddr input-      notImplemented = error $ "precompile at address " <> show preCompileAddr <> " not yet implemented"+      notImplemented = internalError $ "precompile at address " <> show preCompileAddr <> " not yet implemented"       precompileFail = burn (gasCap - cost) $ do                          assign (#state % #stack) (Lit 0 : xs)                          pushTrace $ ErrorTrace PrecompileFailure@@ -1006,14 +1001,14 @@              output = ConcreteBuf $               if isZero (96 + lenb + lene) lenm input'-              then truncpadlit (num lenm) (asBE (0 :: Int))+              then truncpadlit (unsafeInto lenm) (asBE (0 :: Int))               else                 let                   b = asInteger $ lazySlice 96 lenb input'                   e = asInteger $ lazySlice (96 + lenb) lene input'                   m = asInteger $ lazySlice (96 + lenb + lene) lenm input'                 in-                  padLeft (num lenm) (asBE (expFast b e m))+                  padLeft (unsafeInto lenm) (asBE (expFast b e m))           assign (#state % #stack) (Lit 1 : xs)           assign (#state % #returndata) output           copyBytesToMemory output (Lit outSize) (Lit 0) (Lit outOffset)@@ -1082,8 +1077,8 @@  lazySlice :: W256 -> W256 -> ByteString -> LS.ByteString lazySlice offset size bs =-  let bs' = LS.take (num size) (LS.drop (num offset) (fromStrict bs))-  in bs' <> LS.replicate ((num size) - LS.length bs') 0+  let bs' = LS.take (unsafeInto size) (LS.drop (unsafeInto offset) (fromStrict bs))+  in bs' <> LS.replicate (unsafeInto size - LS.length bs') 0  parseModexpLength :: ByteString -> (W256, W256, W256) parseModexpLength input =@@ -1096,14 +1091,14 @@ isZero :: W256 -> W256 -> ByteString -> Bool isZero offset size bs =   LS.all (== 0) $-    LS.take (num size) $-      LS.drop (num offset) $+    LS.take (unsafeInto size) $+      LS.drop (unsafeInto offset) $         fromStrict bs  asInteger :: LS.ByteString -> Integer asInteger xs = if xs == mempty then 0   else 256 * asInteger (LS.init xs)-      + num (LS.last xs)+      + into (LS.last xs)  -- * Opcode helper actions @@ -1178,7 +1173,7 @@             forceConcrete slot "cannot read symbolic slots via RPC" $ \litSlot -> do               -- check if the slot is cached               cachedStore <- (.cache.fetchedStorage) <$> get-              case Map.lookup (num addr) cachedStore >>= Map.lookup litSlot of+              case Map.lookup (into addr) cachedStore >>= Map.lookup litSlot of                 Nothing -> mkQuery litSlot                 Just val -> continue (Lit val)           else do@@ -1192,7 +1187,7 @@       mkQuery s = query $                     PleaseFetchSlot addr s                       (\x -> do-                          modifying (#cache % #fetchedStorage % ix (num addr)) (Map.insert s x)+                          modifying (#cache % #fetchedStorage % ix (into addr)) (Map.insert s x)                           modifying (#env % #storage) (writeStorage (litAddr addr) slot (Lit x))                           assign #result Nothing                           continue (Lit x))@@ -1248,7 +1243,7 @@             Just ops ->               onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)     _ ->-      error "Finalising an unfinished tx."+      internalError "Finalising an unfinished tx."    -- compute and pay the refund to the caller and the   -- corresponding payment to the miner@@ -1259,9 +1254,9 @@   let     sumRefunds   = sum (snd <$> tx.substate.refunds)     gasUsed      = tx.gaslimit - gasRemaining-    cappedRefund = min (quot gasUsed 5) (num sumRefunds)-    originPay    = (num $ gasRemaining + cappedRefund) * tx.gasprice-    minerPay     = tx.priorityFee * (num gasUsed)+    cappedRefund = min (quot gasUsed 5) sumRefunds+    originPay    = (into $ gasRemaining + cappedRefund) * tx.gasprice+    minerPay     = tx.priorityFee * (into gasUsed)    modifying (#env % #contracts)      (Map.adjust (over #balance (+ originPay)) tx.origin)@@ -1292,7 +1287,7 @@   preuse (#env % #contracts % ix target % #contractcode) >>=     \case       Nothing ->-        error "Call target doesn't exist"+        internalError "Call target doesn't exist"       Just targetCode -> do         assign (#state % #contract) target         assign (#state % #code)     targetCode@@ -1426,7 +1421,7 @@ -- special things, e.g. changing the block timestamp. Beware that -- these are necessarily hevm specific. cheatCode :: Addr-cheatCode = num (keccak' "hevm cheat code")+cheatCode = unsafeInto (keccak' "hevm cheat code")  cheat   :: (?op :: Word8)@@ -1438,14 +1433,16 @@   let     abi = readBytes 4 (Lit inOffset) mem     input = readMemory (Lit $ inOffset + 4) (Lit $ inSize - 4) vm+  pushTrace $ FrameTrace (CallContext cheatCode cheatCode inOffset inSize (Lit 0) (maybeLitWord abi) input (vm.env.contracts, vm.env.storage) vm.tx.substate)   case maybeLitWord abi of     Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc "symbolic cheatcode selector" (wrap [abi])-    Just (fromIntegral -> abi') ->+    Just (unsafeInto -> abi') ->       case Map.lookup abi' cheatActions of         Nothing ->           vmError (BadCheatCode abi')         Just action -> do             action (Lit outOffset) (Lit outSize) input+            popTrace             next             push 1 @@ -1493,7 +1490,7 @@       action "store(address,bytes32,bytes32)" $         \sig _ _ input -> case decodeStaticArgs 0 3 input of           [a, slot, new] ->-            forceConcrete a "cannot store at a symbolic address" $ \(num -> a') ->+            forceConcrete a "cannot store at a symbolic address" $ \(unsafeInto -> a') ->               fetchAccount a' $ \_ -> do                 modifying (#env % #storage) (writeStorage (litAddr a') slot new)           _ -> vmError (BadCheatCode sig),@@ -1501,7 +1498,7 @@       action "load(address,bytes32)" $         \sig outOffset _ input -> case decodeStaticArgs 0 2 input of           [a, slot] ->-            forceConcrete a "cannot load from a symbolic address" $ \(num -> a') ->+            forceConcrete a "cannot load from a symbolic address" $ \(unsafeInto -> a') ->               accessStorage a' slot $ \res -> do                 assign (#state % #returndata % word256At (Lit 0)) res                 assign (#state % #memory % word256At outOffset) res@@ -1514,18 +1511,18 @@               let (v,r,s) = EVM.Sign.sign hash' (toInteger sk')                   encoded = encodeAbiValue $                     AbiTuple (V.fromList-                      [ AbiUInt 8 $ num v+                      [ AbiUInt 8 $ into v                       , AbiBytes 32 (word256Bytes r)                       , AbiBytes 32 (word256Bytes s)                       ])               assign (#state % #returndata) (ConcreteBuf encoded)-              copyBytesToMemory (ConcreteBuf encoded) (Lit . num . BS.length $ encoded) (Lit 0) outOffset+              copyBytesToMemory (ConcreteBuf encoded) (Lit . unsafeInto . BS.length $ encoded) (Lit 0) outOffset           _ -> vmError (BadCheatCode sig),        action "addr(uint256)" $         \sig outOffset _ input -> case decodeStaticArgs 0 1 input of           [sk] -> forceConcrete sk "cannot derive address for a symbolic key" $ \sk' -> do-            let a = EVM.Sign.deriveAddr $ num sk'+            let a = EVM.Sign.deriveAddr $ into sk'             case a of               Nothing -> vmError (BadCheatCode sig)               Just address -> do@@ -1553,7 +1550,7 @@   -> EVM () delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue =   forceConcrete2 (xTo, xContext) "cannot delegateCall with symbolic target or context" $-    \((num -> xTo'), (num -> xContext')) ->+    \((unsafeInto -> xTo'), (unsafeInto -> xContext')) ->       if xTo' > 0 && xTo' <= 9       then precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs       else if xTo' == cheatCode then@@ -1576,9 +1573,7 @@                                     , subState  = vm0.tx.substate                                     , abi =                                         if xInSize >= 4-                                        then case maybeLitWord $ readBytes 4 (Lit xInOffset) vm0.state.memory-                                             of Nothing -> Nothing-                                                Just abi -> Just $ num abi+                                        then (maybeLitWord $ readBytes 4 (Lit xInOffset) vm0.state.memory)                                         else Nothing                                     , calldata = (readMemory (Lit xInOffset) (Lit xInSize) vm0)                                     }@@ -1597,7 +1592,7 @@                         a -> a                    zoom #state $ do-                    assign #gas (num xGas)+                    assign #gas xGas                     assign #pc 0                     assign #code (clearInitCode target.contractcode)                     assign #codeContract xTo'@@ -1623,10 +1618,9 @@ create :: (?op :: Word8)   => Addr -> Contract   -> W256 -> Word64 -> W256 -> [Expr EWord] -> Addr -> Expr Buf -> EVM ()-create self this xSize xGas' xValue xs newAddr initCode = do+create self this xSize xGas xValue xs newAddr initCode = do   vm0 <- get-  let xGas = num xGas'-  if this.nonce == num (maxBound :: Word64)+  if this.nonce == into (maxBound :: Word64)   then do     assign (#state % #stack) (Lit 0 : xs)     assign (#state % #returndata) mempty@@ -1664,8 +1658,8 @@     -- from memory into a code and data section     let contract' = do           prefixLen <- Expr.concPrefix initCode-          prefix <- Expr.toList $ Expr.take (num prefixLen) initCode-          let sym = Expr.drop (num prefixLen) initCode+          prefix <- Expr.toList $ Expr.take (unsafeInto prefixLen) initCode+          let sym = Expr.drop (unsafeInto prefixLen) initCode           conc <- mapM maybeLitByte prefix           pure $ InitCode (BS.pack $ V.toList conc) sym     case contract' of@@ -1689,14 +1683,14 @@           modifying (ix self % #nonce) succ          let resetStorage = \case-              ConcreteStore s -> ConcreteStore (Map.delete (num newAddr) s)+              ConcreteStore s -> ConcreteStore (Map.delete (into newAddr) s)               AbstractStore -> AbstractStore               EmptyStore -> EmptyStore-              SStore {} -> error "trying to reset symbolic storage with writes in create"-              GVar _  -> error "unexpected global variable"+              SStore {} -> internalError "trying to reset symbolic storage with writes in create"+              GVar _  -> internalError "unexpected global variable"          modifying (#env % #storage) resetStorage-        modifying (#env % #origStorage) (Map.delete (num newAddr))+        modifying (#env % #origStorage) (Map.delete (into newAddr))          transfer self newAddr xValue @@ -1715,7 +1709,7 @@             & set #code         c             & set #callvalue    (Lit xValue)             & set #caller       (litAddr self)-            & set #gas          xGas'+            & set #gas          xGas  -- | Replace a contract's code, like when CREATE returns -- from the constructor code.@@ -1731,9 +1725,9 @@               , nonce = now.nonce               }         RuntimeCode _ ->-          error ("internal error: can't replace code of deployed contract " <> show target)+          internalError $ "can't replace code of deployed contract " <> show target       Nothing ->-        error "internal error: can't replace code of nonexistent contract"+        internalError "can't replace code of nonexistent contract"  replaceCodeOfSelf :: ContractCode -> EVM () replaceCodeOfSelf newCode = do@@ -1814,7 +1808,7 @@             modifying (#state % #gas) (+ remainingGas)        -- Now dispatch on whether we were creating or calling,-      -- and whether we shall return, revert, or error (six cases).+      -- and whether we shall return, revert, or internalError(six cases).       case nextFrame.context of          -- Were we calling?@@ -1879,7 +1873,7 @@                     replaceCode createe contractCode                     assign (#state % #returndata) mempty                     reclaimRemainingGasAllowance-                    push (num createe)+                    push (into createe)               case output of                 ConcreteBuf bs ->                   onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)@@ -1918,7 +1912,7 @@   -> EVM () accessUnboundedMemoryRange _ 0 continue = continue accessUnboundedMemoryRange f l continue = do-  m0 <- num <$> use (#state % #memorySize)+  m0 <- use (#state % #memorySize)   fees <- gets (.block.schedule)   let m1 = 32 * ceilDiv (max m0 (f + l)) 32   burn (memoryCost fees m1 - memoryCost fees m0) $ do@@ -1992,7 +1986,7 @@ popTrace =   modifying #traces $     \t -> case Zipper.parent t of-            Nothing -> error "internal error (trace root)"+            Nothing -> internalError "internal internalError(trace root)"             Just t' -> Zipper.nextSpace t'  zipperRootForest :: Zipper.TreePos Zipper.Empty a -> Forest a@@ -2004,13 +1998,27 @@ traceForest :: VM -> Forest Trace traceForest vm = zipperRootForest vm.traces +traceForest' :: Expr End -> Forest Trace+traceForest' (Success _ (Traces f _) _ _) = f+traceForest' (Partial _ (Traces f _) _) = f+traceForest' (Failure _ (Traces f _) _) = f+traceForest' (ITE {}) = internalError"Internal Error: ITE does not contain a trace"+traceForest' (GVar {}) = internalError"Internal Error: Unexpected GVar"++traceContext :: Expr End -> Map Addr Contract+traceContext (Success _ (Traces _ c) _ _) = c+traceContext (Partial _ (Traces _ c) _) = c+traceContext (Failure _ (Traces _ c) _) = c+traceContext (ITE {}) = internalError"Internal Error: ITE does not contain a trace"+traceContext (GVar {}) = internalError"Internal Error: Unexpected GVar"+ traceTopLog :: [Expr Log] -> EVM () traceTopLog [] = noop traceTopLog ((LogEntry addr bytes topics) : _) = do   trace <- withTraceLocation (EventTrace addr bytes topics)   modifying #traces $     \t -> Zipper.nextSpace (Zipper.insert (Node trace []) t)-traceTopLog ((GVar _) : _) = error "unexpected global variable"+traceTopLog ((GVar _) : _) = internalError "unexpected global variable"  -- * Stack manipulation @@ -2076,7 +2084,7 @@   case isValidJumpDest vm x of     True -> do       #state % #stack .= xs-      #state % #pc .= num x+      #state % #pc .= x     False -> vmError BadJumpDestination  isValidJumpDest :: VM -> Int -> Bool@@ -2084,7 +2092,7 @@     code = vm.state.code     self = vm.state.codeContract     contract = fromMaybe-      (error "Internal Error: self not found in current contracts")+      (internalError "self not found in current contracts")       (Map.lookup self vm.env.contracts)     op = case code of       InitCode ops _ -> BS.indexMaybe ops x@@ -2092,10 +2100,10 @@       RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByte   in case op of        Nothing -> False-       Just b -> 0x5b == b && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap SV.! num x))+       Just b -> 0x5b == b && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap SV.! x))  opSize :: Word8 -> Int-opSize x | x >= 0x60 && x <= 0x7f = num x - 0x60 + 2+opSize x | x >= 0x60 && x <= 0x7f = into x - 0x60 + 2 opSize _                          = 1  --  i of the resulting vector contains the operation index for@@ -2133,7 +2141,7 @@                      then (x' - 0x60 + 1, i + 1, j,     m >> SV.write v i j)             -- other data --                      else (0,             i + 1, j + 1, m >> SV.write v i j)-          _ -> error $ "cannot analyze symbolic code:\nx: " <> show x <> " i: " <> show i <> " j: " <> show j+          _ -> internalError $ "cannot analyze symbolic code:\nx: " <> show x <> " i: " <> show i <> " j: " <> show j          go v (1, !i, !j, !m) _ =           {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> SV.write v i j)@@ -2151,7 +2159,7 @@         RuntimeCode (ConcreteRuntimeCode xs') ->           (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')         RuntimeCode (SymbolicRuntimeCode xs') ->-          ( fromMaybe (error "unexpected symbolic code") . maybeLitByte $ xs' V.! i , V.toList $ V.drop i xs')+          ( fromMaybe (internalError "unexpected symbolic code") . maybeLitByte $ xs' V.! i , V.toList $ V.drop i xs')   in if (opslen code' < i)      then Nothing      else Just (readOp op pushdata)@@ -2178,7 +2186,7 @@         Nothing ->           mempty         Just (x, xs') ->-          let x' = fromMaybe (error "unexpected symbolic code argument") $ maybeLitByte x+          let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByte x               j = opSize x'           in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs) @@ -2195,7 +2203,7 @@       c_new = if not recipientExists && xValue /= 0             then g_newaccount             else 0-      c_xfer = if xValue /= 0  then num g_callvalue else 0+      c_xfer = if xValue /= 0  then g_callvalue else 0       c_extra = call_base_gas + c_xfer + c_new       c_gascap =  if availableGas >= c_extra                   then min xGas (allButOne64th (availableGas - c_extra))@@ -2211,14 +2219,14 @@   where     byteCost   = if hashNeeded then g_sha3word + g_initcodeword else g_initcodeword     createCost = g_create + codeCost-    codeCost   = byteCost * (ceilDiv (num size) 32)+    codeCost   = byteCost * (ceilDiv (unsafeInto size) 32)     initGas    = allButOne64th (availableGas - createCost)  concreteModexpGasFee :: ByteString -> Word64 concreteModexpGasFee input =-  if lenb < num (maxBound :: Word32) &&-     (lene < num (maxBound :: Word32) || (lenb == 0 && lenm == 0)) &&-     lenm < num (maxBound :: Word64)+  if lenb < into (maxBound :: Word32) &&+     (lene < into (maxBound :: Word32) || (lenb == 0 && lenm == 0)) &&+     lenm < into (maxBound :: Word64)   then     max 200 ((multiplicationComplexity * iterCount) `div` 3)   else@@ -2229,38 +2237,38 @@     e' = word $ LS.toStrict $       lazySlice (96 + lenb) (min 32 lene) input     nwords :: Word64-    nwords = ceilDiv (num $ max lenb lenm) 8+    nwords = ceilDiv (unsafeInto $ max lenb lenm) 8     multiplicationComplexity = nwords * nwords     iterCount' :: Word64     iterCount' | lene <= 32 && ez = 0-               | lene <= 32 = num (log2 e')-               | e' == 0 = 8 * (num lene - 32)-               | otherwise = num (log2 e') + 8 * (num lene - 32)+               | lene <= 32 = unsafeInto (log2 e')+               | e' == 0 = 8 * (unsafeInto lene - 32)+               | otherwise = unsafeInto (log2 e') + 8 * (unsafeInto lene - 32)     iterCount = max iterCount' 1  -- Gas cost of precompiles costOfPrecompile :: FeeSchedule Word64 -> Addr -> Expr Buf -> Word64 costOfPrecompile (FeeSchedule {..}) precompileAddr input =-  let errorDynamicSize = error "precompile input cannot have a dynamic size"+  let errorDynamicSize = internalError "precompile input cannot have a dynamic size"       inputLen = case input of-                   ConcreteBuf bs -> fromIntegral $ BS.length bs+                   ConcreteBuf bs -> unsafeInto $ BS.length bs                    AbstractBuf _ -> errorDynamicSize                    buf -> case bufLength buf of-                            Lit l -> num l -- TODO: overflow+                            Lit l -> unsafeInto l -- TODO: overflow                             _ -> errorDynamicSize   in case precompileAddr of     -- ECRECOVER     0x1 -> 3000     -- SHA2-256-    0x2 -> num $ (((inputLen + 31) `div` 32) * 12) + 60+    0x2 -> (((inputLen + 31) `div` 32) * 12) + 60     -- RIPEMD-160-    0x3 -> num $ (((inputLen + 31) `div` 32) * 120) + 600+    0x3 -> (((inputLen + 31) `div` 32) * 120) + 600     -- IDENTITY-    0x4 -> num $ (((inputLen + 31) `div` 32) * 3) + 15+    0x4 -> (((inputLen + 31) `div` 32) * 3) + 15     -- MODEXP     0x5 -> case input of              ConcreteBuf i -> concreteModexpGasFee i-             _ -> error "Unsupported symbolic modexp gas calc "+             _ -> internalError "Unsupported symbolic modexp gas calc "     -- ECADD     0x6 -> g_ecadd     -- ECMUL@@ -2269,9 +2277,9 @@     0x8 -> (inputLen `div` 192) * g_pairing_point + g_pairing_base     -- BLAKE2     0x9 -> case input of-             ConcreteBuf i -> g_fround * (num $ asInteger $ lazySlice 0 4 i)-             _ -> error "Unsupported symbolic blake2 gas calc"-    _ -> error ("unimplemented precompiled contract " ++ show precompileAddr)+             ConcreteBuf i -> g_fround * (unsafeInto $ asInteger $ lazySlice 0 4 i)+             _ -> internalError "Unsupported symbolic blake2 gas calc"+    _ -> internalError $ "unimplemented precompiled contract " ++ show precompileAddr  -- Gas cost of memory expansion memoryCost :: FeeSchedule Word64 -> Word64 -> Word64@@ -2299,8 +2307,8 @@ -- This can return an abstract value codelen :: ContractCode -> Expr EWord codelen c@(InitCode {}) = bufLength $ toBuf c-codelen (RuntimeCode (ConcreteRuntimeCode ops)) = Lit . num $ BS.length ops-codelen (RuntimeCode (SymbolicRuntimeCode ops)) = Lit . num $ length ops+codelen (RuntimeCode (ConcreteRuntimeCode ops)) = Lit . unsafeInto $ BS.length ops+codelen (RuntimeCode (SymbolicRuntimeCode ops)) = Lit . unsafeInto $ length ops  toBuf :: ContractCode -> Expr Buf toBuf (InitCode ops args) = ConcreteBuf ops <> args

@@ -1,3 +1,6 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE StrictData #-}+ {-    The ABI encoding is mostly straightforward.@@ -24,10 +27,6 @@   Calldata args are encoded as heterogenous sequences sans length prefix.  -}--{-# Language StrictData #-}-{-# Language DataKinds #-}- module EVM.ABI   ( AbiValue (..)   , AbiType (..)@@ -57,40 +56,38 @@   , selector   ) where -import EVM.Types import EVM.Expr (readWord, isLitWord)+import EVM.Types -import Control.Monad      (replicateM, replicateM_, forM_, void)-import Data.Binary.Get    (Get, runGet, runGetOrFail, label, getWord8, getWord32be, skip)-import Data.Binary.Put    (Put, runPut, putWord8, putWord32be)-import Data.Bits          (shiftL, shiftR, (.&.))-import Data.ByteString    (ByteString)-import Data.Char          (isHexDigit)-import Data.Data          (Data)-import Data.DoubleWord    (Word256, Int256, signedWord)-import Data.Functor       (($>))-import Data.Text          (Text)-import Data.List          (intercalate)+import Control.Applicative ((<|>))+import Control.Monad (replicateM, replicateM_, forM_, void)+import Data.Binary.Get (Get, runGet, runGetOrFail, label, getWord8, getWord32be, skip)+import Data.Binary.Put (Put, runPut, putWord8, putWord32be)+import Data.Bits (shiftL, shiftR, (.&.))+import Data.ByteString (ByteString)+import Data.ByteString qualified as BS+import Data.ByteString.Base16 qualified as BS16+import Data.ByteString.Char8 qualified as Char8+import Data.ByteString.Lazy qualified as BSLazy+import Data.Char (isHexDigit)+import Data.Data (Data)+import Data.DoubleWord (Word256, Int256, signedWord)+import Data.Functor (($>))+import Data.List (intercalate)+import Data.Maybe (mapMaybe)+import Data.Text (Text)+import Data.Text qualified as Text import Data.Text.Encoding (encodeUtf8)-import Data.Vector        (Vector, toList)-import Data.Word          (Word32)-import Data.Maybe         (mapMaybe)-import GHC.Generics+import Data.Vector (Vector, toList)+import Data.Vector qualified as Vector+import Data.Word (Word32)+import GHC.Generics (Generic)  import Test.QuickCheck hiding ((.&.), label)+import Text.Megaparsec qualified as P+import Text.Megaparsec.Char qualified as P import Text.ParserCombinators.ReadP-import Control.Applicative--import qualified Data.ByteString        as BS-import qualified Data.ByteString.Base16 as BS16-import qualified Data.ByteString.Char8  as Char8-import qualified Data.ByteString.Lazy   as BSLazy-import qualified Data.Text              as Text-import qualified Data.Vector            as Vector--import qualified Text.Megaparsec      as P-import qualified Text.Megaparsec.Char as P-+import Witch (unsafeInto, into)  data AbiValue   = AbiUInt         Int Word256@@ -220,7 +217,7 @@     AbiArrayDynamicType t' -> do       AbiUInt _ n <- label "array length" (getAbi (AbiUIntType 256))       AbiArrayDynamic t' <$>-        label "array body" (getAbiSeq (fromIntegral n) (repeat t'))+        label "array body" (getAbiSeq (unsafeInto n) (repeat t'))      AbiTupleType ts ->       AbiTuple <$> getAbiSeq (Vector.length ts) (Vector.toList ts)@@ -232,7 +229,7 @@ putAbi = \case   AbiUInt _ x ->     forM_ (reverse [0 .. 7]) $ \i ->-      putWord32be (fromIntegral (shiftR x (i * 32) .&. 0xffffffff))+      putWord32be (unsafeInto (shiftR x (i * 32) .&. 0xffffffff))    AbiInt n x   -> putAbi (AbiUInt n (fromIntegral x))   AbiAddress x -> putAbi (AbiUInt 160 (fromIntegral x))@@ -244,7 +241,7 @@    AbiBytesDynamic xs -> do     let n = BS.length xs-    putAbi (AbiUInt 256 (fromIntegral n))+    putAbi (AbiUInt 256 (unsafeInto n))     putAbi (AbiBytes n xs)    AbiString s ->@@ -300,7 +297,7 @@         AbiArrayDynamic _ xs -> 32 + sum ((abiHeadSize <$> xs) <> (abiTailSize <$> xs))         AbiArray _ _ xs -> sum ((abiHeadSize <$> xs) <> (abiTailSize <$> xs))         AbiTuple v -> sum ((abiHeadSize <$> v) <> (abiTailSize <$> v))-        _ -> error "impossible"+        _ -> internalError "impossible"  abiHeadSize :: AbiValue -> Int abiHeadSize x =@@ -316,7 +313,7 @@         AbiTuple v   -> sum (abiHeadSize <$> v)         AbiArray _ _ xs -> sum (abiHeadSize <$> xs)         AbiFunction _ -> 32-        _ -> error "impossible"+        _ -> internalError "impossible"  putAbiSeq :: Vector AbiValue -> Put putAbiSeq xs =@@ -329,7 +326,7 @@       case abiKind (abiValueType x) of         Static -> do putAbi x                      putHeads offset xs'-        Dynamic -> do putAbi (AbiUInt 256 (fromIntegral offset))+        Dynamic -> do putAbi (AbiUInt 256 (unsafeInto offset))                       putHeads (offset + abiTailSize x) xs'  encodeAbiValue :: AbiValue -> BS.ByteString@@ -391,12 +388,12 @@ pack32 :: Int -> [Word32] -> Word256 pack32 n xs =   sum [ shiftL x ((n - i) * 32)-      | (x, i) <- zip (map fromIntegral xs) [1..] ]+      | (x, i) <- zip (map into xs) [1..] ]  asUInt :: Integral i => Int -> (i -> a) -> Get a asUInt n f = y <$> getAbi (AbiUIntType n)   where y (AbiUInt _ x) = f (fromIntegral x)-        y _ = error "can't happen"+        y _ = internalError "can't happen"  getWord256 :: Get Word256 getWord256 = pack32 8 <$> replicateM 8 getWord32be@@ -502,7 +499,7 @@ makeAbiValue :: AbiType -> String -> AbiValue makeAbiValue typ str = case readP_to_S (parseAbiValue typ) (padStr str) of   [(val,"")] -> val-  _ -> error $  "could not parse abi argument: " ++ str ++ " : " ++ show typ+  _ -> internalError $ "could not parse abi argument: " ++ str ++ " : " ++ show typ   where     padStr = case typ of       (AbiBytesType n) -> padRight' (2 * n + 2) -- +2 is for the 0x prefix@@ -510,34 +507,34 @@  parseAbiValue :: AbiType -> ReadP AbiValue parseAbiValue (AbiUIntType n) = do W256 w <- readS_to_P reads-                                   return $ AbiUInt n w+                                   pure $ AbiUInt n w parseAbiValue (AbiIntType n) = do W256 w <- readS_to_P reads-                                  return $ AbiInt n (num w)+                                  pure $ AbiInt n (unsafeInto w) parseAbiValue AbiAddressType = AbiAddress <$> readS_to_P reads parseAbiValue AbiBoolType = (do W256 w <- readS_to_P reads-                                return $ AbiBool (w /= 0))+                                pure $ AbiBool (w /= 0))                             <|> (do Boolz b <- readS_to_P reads-                                    return $ AbiBool b)+                                    pure $ AbiBool b) parseAbiValue (AbiBytesType n) = AbiBytes n <$> do ByteStringS bytes <- bytesP-                                                   return bytes+                                                   pure bytes parseAbiValue AbiBytesDynamicType = AbiBytesDynamic <$> do ByteStringS bytes <- bytesP-                                                           return bytes+                                                           pure bytes parseAbiValue AbiStringType = AbiString <$> do Char8.pack <$> readS_to_P reads parseAbiValue (AbiArrayDynamicType typ) =   AbiArrayDynamic typ <$> do a <- listP (parseAbiValue typ)-                             return $ Vector.fromList a+                             pure $ Vector.fromList a parseAbiValue (AbiArrayType n typ) =   AbiArray n typ <$> do a <- listP (parseAbiValue typ)-                        return $ Vector.fromList a-parseAbiValue (AbiTupleType _) = error "tuple types not supported"+                        pure $ Vector.fromList a+parseAbiValue (AbiTupleType _) = internalError "tuple types not supported" parseAbiValue AbiFunctionType = AbiFunction <$> do ByteStringS bytes <- bytesP-                                                   return bytes+                                                   pure bytes  listP :: ReadP a -> ReadP [a] listP parser = between (char '[') (char ']') ((do skipSpaces                                                   a <- parser                                                   skipSpaces-                                                  return a) `sepBy` (char ','))+                                                  pure a) `sepBy` (char ','))  bytesP :: ReadP ByteStringS bytesP = do@@ -573,7 +570,8 @@     containsDynamic = or . fmap isDynamic  decodeStaticArgs :: Int -> Int -> Expr Buf -> [Expr EWord]-decodeStaticArgs offset numArgs b = [readWord (Lit . num $ i) b | i <- [offset,(offset+32) .. (offset + (numArgs-1)*32)]]+decodeStaticArgs offset numArgs b =+  [readWord (Lit . unsafeInto $ i) b | i <- [offset,(offset+32) .. (offset + (numArgs-1)*32)]]   -- A modification of 'arbitrarySizedBoundedIntegral' quickcheck library

@@ -1,18 +1,17 @@+{-# LANGUAGE DataKinds #-}+ {-| Module      : Assembler Description : Assembler for EVM opcodes used in the HEVM symbolic checker -}--{-# LANGUAGE DataKinds #-}- module EVM.Assembler where +import EVM.Expr qualified as Expr import EVM.Op import EVM.Types-import qualified EVM.Expr as Expr -import qualified Data.Vector as V import Data.Vector (Vector)+import Data.Vector qualified as V  assemble :: [Op] -> Vector (Expr Byte) assemble os = V.fromList $ concatMap go os@@ -95,15 +94,15 @@       OpDup n ->         if 1 <= n && n <= 16         then [LitByte (0x80 + (n - 1))]-        else error $ "Internal Error: invalid argument to OpDup: " <> show n+        else internalError $ "invalid argument to OpDup: " <> show n       OpSwap n ->         if 1 <= n && n <= 16         then [LitByte (0x90 + (n - 1))]-        else error $ "Internal Error: invalid argument to OpSwap: " <> show n+        else internalError $ "invalid argument to OpSwap: " <> show n       OpLog n ->         if 0 <= n && n <= 4         then [LitByte (0xA0 + n)]-        else error $ "Internal Error: invalid argument to OpLog: " <> show n+        else internalError $ "invalid argument to OpLog: " <> show n       -- we just always assemble OpPush into PUSH32       OpPush wrd -> (LitByte 0x7f) : [Expr.indexWord (Lit i) wrd | i <- [0..31]]       OpPush0 -> [LitByte 0x5f]

@@ -1,4 +1,4 @@-{-# Language DataKinds #-}+{-# LANGUAGE DataKinds #-}  {- |     Module: EVM.CSE@@ -7,14 +7,12 @@  module EVM.CSE (BufEnv, StoreEnv, eliminateExpr, eliminateProps) where -import Prelude hiding (Word, LT, GT)--import Data.Map (Map)-import qualified Data.Map as Map import Control.Monad.State+import Data.Map (Map)+import Data.Map qualified as Map -import EVM.Types import EVM.Traversals+import EVM.Types  -- maps expressions to variable names data BuilderState = BuilderState

@@ -1,16 +1,14 @@ module EVM.Concrete where -import Prelude hiding (Word)- import EVM.RLP import EVM.Types -import Data.Bits       (Bits (..), shiftR)+import Data.Bits (Bits(..), shiftR) import Data.ByteString (ByteString, (!?))-import Data.Maybe      (fromMaybe)-import Data.Word       (Word8)--import qualified Data.ByteString as BS+import Data.ByteString qualified as BS+import Data.Maybe (fromMaybe)+import Data.Word (Word8)+import Witch (unsafeInto)  wordAt :: Int -> ByteString -> W256 wordAt i bs =@@ -31,23 +29,23 @@     in bs' <> BS.replicate (size - BS.length bs') 0  -sliceMemory :: (Integral a, Integral b) => a -> b -> ByteString -> ByteString+sliceMemory :: W256 -> W256 -> ByteString -> ByteString sliceMemory o s =-  byteStringSliceWithDefaultZeroes (num o) (num s)+  byteStringSliceWithDefaultZeroes (unsafeInto o) (unsafeInto s)  writeMemory :: ByteString -> W256 -> W256 -> W256 -> ByteString -> ByteString writeMemory bs1 n src dst bs0 =   let-    (a, b) = BS.splitAt (num dst) bs0-    a'     = BS.replicate (num dst - BS.length a) 0+    (a, b) = BS.splitAt (unsafeInto dst) bs0+    a'     = BS.replicate (unsafeInto dst - BS.length a) 0     -- sliceMemory should work for both cases, but we are using 256 bit     -- words, whereas ByteString is only defined up to 64 bit. For large n,     -- src, dst this will cause problems (often in GeneralStateTests).     -- Later we could reimplement ByteString for 256 bit arguments.-    c      = if src > num (BS.length bs1)-             then BS.replicate (num n) 0+    c      = if src > unsafeInto (BS.length bs1)+             then BS.replicate (unsafeInto n) 0              else sliceMemory src n bs1-    b'     = BS.drop (num n) b+    b'     = BS.drop (unsafeInto n) b   in     a <> a' <> c <> b' @@ -67,8 +65,8 @@                   | otherwise   = g (x * x) ((y - 1) `shiftR` 1) (x * z)  createAddress :: Addr -> W256 -> Addr-createAddress a n = num $ keccak' $ rlpList [rlpAddrFull a, rlpWord256 n]+createAddress a n = unsafeInto $ keccak' $ rlpList [rlpAddrFull a, rlpWord256 n]  create2Address :: Addr -> W256 -> ByteString -> Addr-create2Address a s b = num $ keccak' $ mconcat+create2Address a s b = unsafeInto $ keccak' $ mconcat   [BS.singleton 0xff, word160Bytes a, word256Bytes s, word256Bytes $ keccak' b]

@@ -1,10 +1,10 @@ module EVM.Dapp where +import EVM.ABI import EVM.Concrete import EVM.Debug (srcMapCodePos) import EVM.Solidity import EVM.Types-import EVM.ABI  import Control.Arrow ((>>>)) import Data.Aeson (Value)@@ -19,6 +19,7 @@ import Data.Text (Text, isPrefixOf, pack, unpack) import Data.Text.Encoding (encodeUtf8) import Data.Vector qualified as V+import Witch (unsafeInto)  data DappInfo = DappInfo   { root       :: FilePath@@ -162,18 +163,18 @@   snd <$> Map.lookup (keccak' (stripBytecodeMetadata c)) a.solcByHash lookupCode (RuntimeCode (ConcreteRuntimeCode c)) a =   case snd <$> Map.lookup (keccak' (stripBytecodeMetadata c)) a.solcByHash of-    Just x -> return x+    Just x -> pure x     Nothing -> snd <$> find (compareCode c . fst) a.solcByCode lookupCode (RuntimeCode (SymbolicRuntimeCode c)) a = let     code = BS.pack $ mapMaybe maybeLitByte $ V.toList c   in case snd <$> Map.lookup (keccak' (stripBytecodeMetadata code)) a.solcByHash of-    Just x -> return x+    Just x -> pure x     Nothing -> snd <$> find (compareCode code . fst) a.solcByCode  compareCode :: ByteString -> Code -> Bool compareCode raw (Code template locs) =   let holes' = sort [(start, len) | (Reference start len) <- locs]-      insert at' len' bs = writeMemory (BS.replicate len' 0) (fromIntegral len') 0 (fromIntegral at') bs+      insert at' len' bs = writeMemory (BS.replicate len' 0) (unsafeInto len') 0 (unsafeInto at') bs       refined = foldr (\(start, len) acc -> insert start len acc) raw holes'   in BS.length raw == BS.length template && template == refined 

@@ -1,21 +1,18 @@-{-# Language DataKinds #-}- module EVM.Debug where -import EVM          (bytecode)+import EVM (bytecode)+import EVM.Expr (bufLength) import EVM.Solidity (SrcMap(..), SourceCache(..))-import EVM.Types    (Contract, Addr)-import EVM.Expr     (bufLength)+import EVM.Types (Contract(..), Addr) -import Control.Arrow   (second)-import Optics.Core+import Control.Arrow (second) import Data.ByteString (ByteString)-import Data.Map        (Map)--import qualified Data.ByteString       as ByteString-import qualified Data.Map              as Map-+import Data.ByteString qualified as ByteString+import Data.Map (Map)+import Data.Map qualified as Map+import Optics.Core import Text.PrettyPrint.ANSI.Leijen+import Witch (unsafeInto)  data Mode = Debug | Run | JsonTrace deriving (Eq, Show) @@ -31,9 +28,9 @@ prettyContract c =   object     [ (text "codesize", text . show $ (bufLength (c ^. bytecode)))-    , (text "codehash", text (show (c ^. #codehash)))-    , (text "balance", int (fromIntegral (c ^. #balance)))-    , (text "nonce", int (fromIntegral (c ^. #nonce)))+    , (text "codehash", text (show c.codehash))+    , (text "balance", int (unsafeInto c.balance))+    , (text "nonce", int (unsafeInto c.nonce))     ]  prettyContracts :: Map Addr Contract -> Doc

@@ -1,36 +1,36 @@-{-# Language DataKinds #-}-{-# Language QuasiQuotes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE QuasiQuotes #-} -{- |+{-| Module: EVM.Dev Description: Helpers for repl driven hevm hacking -} module EVM.Dev where -import Data.ByteString hiding (writeFile, zip) import Control.Monad.State.Strict hiding (state)+import Data.ByteString hiding (writeFile, zip) import Data.Maybe (fromJust)-import System.Directory-import Data.Typeable- import Data.String.Here-import qualified Data.Text.IO as T-import qualified Data.Text.Lazy.IO as TL+import Data.Text.IO qualified as T+import Data.Text.Lazy.IO qualified as TL+import Data.Typeable (Typeable)+import System.Directory (withCurrentDirectory)+import System.Exit (exitFailure)  import EVM+import EVM.Dapp (dappInfo)+import EVM.Expr (numBranches, simplify)+import EVM.Fetch qualified as Fetch+import EVM.FeeSchedule qualified as FeeSchedule+import EVM.Format (formatExpr) import EVM.SMT import EVM.Solvers-import EVM.Types-import EVM.Expr (numBranches, simplify)-import EVM.SymExec import EVM.Solidity+import EVM.SymExec+import EVM.Types import EVM.UnitTest-import EVM.Format (formatExpr)-import EVM.Dapp (dappInfo) import GHC.Conc-import System.Exit (exitFailure)-import qualified EVM.Fetch as Fetch-import qualified EVM.FeeSchedule as FeeSchedule+import Witch (unsafeInto)  checkEquiv :: (Typeable a) => Expr a -> Expr a -> IO () checkEquiv a b = withSolvers Z3 1 Nothing $ \s -> do@@ -41,7 +41,7 @@ runDappTest :: FilePath -> IO () runDappTest root =   withCurrentDirectory root $ do-    cores <- num <$> getNumProcessors+    cores <- unsafeInto <$> getNumProcessors     let testFile = root <> "/out/dapp.sol.json"     Right (BuildOutput contracts _) <- readSolc DappTools root testFile     withSolvers Z3 cores Nothing $ \solvers -> do@@ -52,7 +52,7 @@ testOpts :: SolverGroup -> FilePath -> FilePath -> IO UnitTestOptions testOpts solvers root testFile = do   srcInfo <- readSolc DappTools root testFile >>= \case-    Left e -> error e+    Left e -> internalError e     Right out ->       pure $ dappInfo root out 

@@ -2,16 +2,14 @@  import EVM import EVM.Concrete (createAddress)-import EVM.Types+import EVM.FeeSchedule qualified as FeeSchedule import EVM.Expr (litAddr)--import qualified EVM.FeeSchedule as FeeSchedule+import EVM.Types -import Optics.Core import Control.Monad.Trans.State.Strict (get, State) import Data.ByteString (ByteString) import Data.Maybe (isNothing)-+import Optics.Core  ethrunAddress :: Addr ethrunAddress = Addr 0x00a329c0648769a73afac7f9381e08fb43dbea72

@@ -1,5 +1,4 @@-{-# Language DataKinds #-}-{-# Language PatternGuards #-}+{-# LANGUAGE DataKinds #-}  {-|    Helper functions for working with Expr instances.@@ -9,23 +8,23 @@  import Prelude hiding (LT, GT) import Data.Bits hiding (And, Xor)+import Data.ByteString (ByteString)+import Data.ByteString qualified as BS import Data.DoubleWord (Int256, Word256(Word256), Word128(Word128))-import Data.Int (Int32)-import Data.Word-import Data.Maybe import Data.List+import Data.Map.Strict qualified as Map+import Data.Maybe (mapMaybe)+import Data.Semigroup (Any, Any(..), getAny)+import Data.Vector qualified as V+import Data.Vector.Storable qualified as VS+import Data.Vector.Storable.ByteString+import Data.Word (Word8, Word32)+import Witch (unsafeInto, into)  import Optics.Core -import EVM.Types import EVM.Traversals-import Data.ByteString (ByteString)-import qualified Data.ByteString as BS-import qualified Data.Map.Strict as Map-import qualified Data.Vector as V-import qualified Data.Vector.Storable as VS-import Data.Vector.Storable.ByteString-import Data.Semigroup (Any, Any(..), getAny)+import EVM.Types   -- ** Stack Ops ** ---------------------------------------------------------------------------------@@ -110,7 +109,7 @@ sex :: Expr EWord -> Expr EWord -> Expr EWord sex = op2 SEx (\bytes x ->   if bytes >= 32 then x-  else let n = num bytes * 8 + 7 in+  else let n = unsafeInto bytes * 8 + 7 in     if testBit x n     then x .|. complement (bit n - 1)     else x .&. (bit n - 1))@@ -202,13 +201,13 @@ -- fuly concrete reads readByte :: Expr EWord -> Expr Buf -> Expr Byte readByte (Lit x) (ConcreteBuf b)-  = if x <= num (maxBound :: Int) && i < BS.length b+  = if x <= unsafeInto (maxBound :: Int) && i < BS.length b     then LitByte (BS.index b i)     else LitByte 0x0   where     i :: Int     i = case x of-          (W256 (Word256 _ (Word128 _ x'))) -> num x'+          (W256 (Word256 _ (Word128 _ x'))) -> unsafeInto x'  readByte i@(Lit x) (WriteByte (Lit idx) val src)   = if x == idx@@ -239,7 +238,7 @@ -- If n is >= 32 this is the same as readWord readBytes :: Int -> Expr EWord -> Expr Buf -> Expr EWord readBytes (Prelude.min 32 -> n) idx buf-  = joinBytes [readByte (add idx (Lit . num $ i)) buf | i <- [0 .. n - 1]]+  = joinBytes [readByte (add idx (Lit . unsafeInto $ i)) buf | i <- [0 .. n - 1]]  -- | Reads the word starting at idx from the given buf readWord :: Expr EWord -> Expr Buf -> Expr EWord@@ -297,36 +296,36 @@ --     note that things can still stack up, e.g. N such rewrites could eventually eat --     N*1GB. maxBytes :: W256-maxBytes = num (maxBound :: Int32) `Prelude.div` 4+maxBytes = into (maxBound :: Word32) `Prelude.div` 8  copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf -> Expr Buf  -- Copies from empty buffers copySlice _ _ (Lit 0) (ConcreteBuf "") dst = dst copySlice a b c@(Lit size) d@(ConcreteBuf "") e@(ConcreteBuf "")-  | size < maxBytes = ConcreteBuf $ BS.replicate (num size) 0+  | size < maxBytes = ConcreteBuf $ BS.replicate (unsafeInto size) 0   | otherwise = CopySlice a b c d e copySlice srcOffset dstOffset sz@(Lit size) src@(ConcreteBuf "") dst-  | size < maxBytes = copySlice srcOffset dstOffset (Lit size) (ConcreteBuf $ BS.replicate (num size) 0) dst+  | size < maxBytes = copySlice srcOffset dstOffset (Lit size) (ConcreteBuf $ BS.replicate (unsafeInto size) 0) dst   | otherwise = CopySlice srcOffset dstOffset sz src dst  -- Fully concrete copies copySlice a@(Lit srcOffset) b@(Lit dstOffset) c@(Lit size) d@(ConcreteBuf src) e@(ConcreteBuf "")-  | srcOffset > num (BS.length src), size < maxBytes = ConcreteBuf $ BS.replicate (num size) 0-  | srcOffset <= num (BS.length src), dstOffset < maxBytes, size < maxBytes = let-    hd = BS.replicate (num dstOffset) 0-    sl = padRight (num size) $ BS.take (num size) (BS.drop (num srcOffset) src)+  | srcOffset > unsafeInto (BS.length src), size < maxBytes = ConcreteBuf $ BS.replicate (unsafeInto size) 0+  | srcOffset <= unsafeInto (BS.length src), dstOffset < maxBytes, size < maxBytes = let+    hd = BS.replicate (unsafeInto dstOffset) 0+    sl = padRight (unsafeInto size) $ BS.take (unsafeInto size) (BS.drop (unsafeInto srcOffset) src)     in ConcreteBuf $ hd <> sl   | otherwise = CopySlice a b c d e  copySlice a@(Lit srcOffset) b@(Lit dstOffset) c@(Lit size) d@(ConcreteBuf src) e@(ConcreteBuf dst)   | dstOffset < maxBytes   , size < maxBytes =-      let hd = padRight (num dstOffset) $ BS.take (num dstOffset) dst-          sl = if srcOffset > num (BS.length src)-            then BS.replicate (num size) 0-            else padRight (num size) $ BS.take (num size) (BS.drop (num srcOffset) src)-          tl = BS.drop (num dstOffset + num size) dst+      let hd = padRight (unsafeInto dstOffset) $ BS.take (unsafeInto dstOffset) dst+          sl = if srcOffset > unsafeInto (BS.length src)+            then BS.replicate (unsafeInto size) 0+            else padRight (unsafeInto size) $ BS.take (unsafeInto size) (BS.drop (unsafeInto srcOffset) src)+          tl = BS.drop (unsafeInto dstOffset + unsafeInto size) dst       in ConcreteBuf $ hd <> sl <> tl   | otherwise = CopySlice a b c d e @@ -337,9 +336,9 @@ -- copying from a concrete region of src) copySlice s@(Lit srcOffset) d@(Lit dstOffset) sz@(Lit size) src ds@(ConcreteBuf dst)   | dstOffset < maxBytes, size < maxBytes = let-    hd = padRight (num dstOffset) $ BS.take (num dstOffset) dst+    hd = padRight (unsafeInto dstOffset) $ BS.take (unsafeInto dstOffset) dst     sl = [readByte (Lit i) src | i <- [srcOffset .. srcOffset + (size - 1)]]-    tl = BS.drop (num dstOffset + num size) dst+    tl = BS.drop (unsafeInto dstOffset + unsafeInto size) dst     in if Prelude.and . (fmap isLitByte) $ sl        then ConcreteBuf $ hd <> (BS.pack . (mapMaybe maybeLitByte) $ sl) <> tl        else CopySlice s d sz src ds@@ -352,12 +351,12 @@ writeByte :: Expr EWord -> Expr Byte -> Expr Buf -> Expr Buf writeByte (Lit offset) (LitByte val) (ConcreteBuf "")   | offset < maxBytes-  = ConcreteBuf $ BS.replicate (num offset) 0 <> BS.singleton val+  = ConcreteBuf $ BS.replicate (unsafeInto offset) 0 <> BS.singleton val writeByte o@(Lit offset) b@(LitByte byte) buf@(ConcreteBuf src)   | offset < maxBytes-    = ConcreteBuf $ (padRight (num offset) $ BS.take (num offset) src)+    = ConcreteBuf $ (padRight (unsafeInto offset) $ BS.take (unsafeInto offset) src)                  <> BS.pack [byte]-                 <> BS.drop (num offset + 1) src+                 <> BS.drop (unsafeInto offset + 1) src   | otherwise = WriteByte o b buf writeByte offset byte src = WriteByte offset byte src @@ -365,12 +364,12 @@ writeWord :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf writeWord (Lit offset) (Lit val) (ConcreteBuf "")   | offset + 32 < maxBytes-  = ConcreteBuf $ BS.replicate (num offset) 0 <> word256Bytes val+  = ConcreteBuf $ BS.replicate (unsafeInto offset) 0 <> word256Bytes val writeWord o@(Lit offset) v@(Lit val) buf@(ConcreteBuf src)   | offset + 32 < maxBytes-    = ConcreteBuf $ (padRight (num offset) $ BS.take (num offset) src)+    = ConcreteBuf $ (padRight (unsafeInto offset) $ BS.take (unsafeInto offset) src)                  <> word256Bytes val-                 <> BS.drop ((num offset) + 32) src+                 <> BS.drop ((unsafeInto offset) + 32) src   | otherwise = WriteWord o v buf writeWord idx val b@(WriteWord idx' val' buf)   -- if the indices match exactly then we just replace the value in the current write and return@@ -407,7 +406,7 @@ bufLengthEnv env useEnv buf = go (Lit 0) buf   where     go :: Expr EWord -> Expr Buf -> Expr EWord-    go l (ConcreteBuf b) = EVM.Expr.max l (Lit (num . BS.length $ b))+    go l (ConcreteBuf b) = EVM.Expr.max l (Lit (unsafeInto . BS.length $ b))     go l (AbstractBuf b) = Max l (BufLength (AbstractBuf b))     go l (WriteWord idx _ b) = go (EVM.Expr.max l (add idx (Lit 32))) b     go l (WriteByte idx _ b) = go (EVM.Expr.max l (add idx (Lit 1))) b@@ -416,19 +415,19 @@     go l (GVar (BufVar a)) | useEnv =       case Map.lookup a env of         Just b -> go l b-        Nothing -> error "Internal error: cannot compute length of open expression"+        Nothing -> internalError "cannot compute length of open expression"     go l (GVar (BufVar a)) = EVM.Expr.max l (BufLength (GVar (BufVar a)))  -- | If a buffer has a concrete prefix, we return it's length here concPrefix :: Expr Buf -> Maybe Integer concPrefix (CopySlice (Lit srcOff) (Lit _) (Lit _) src (ConcreteBuf "")) = do   sz <- go 0 src-  pure . num $ (num sz) - srcOff+  pure . into $ (unsafeInto sz) - srcOff   where     go :: W256 -> Expr Buf -> Maybe Integer     -- base cases     go _ (AbstractBuf _) = Nothing-    go l (ConcreteBuf b) = Just . num $ Prelude.max (num . BS.length $ b) l+    go l (ConcreteBuf b) = Just . into $ Prelude.max (unsafeInto . BS.length $ b) l      -- writes to a concrete index     go l (WriteWord (Lit idx) (Lit _) b) = go (Prelude.max l (idx + 32)) b@@ -438,10 +437,10 @@     -- writes to an abstract index are ignored     go l (WriteWord _ _ b) = go l b     go l (WriteByte _ _ b) = go l b-    go _ (CopySlice _ _ _ _ _) = error "Internal Error: cannot compute a concrete prefix length for nested copySlice expressions"-    go _ (GVar _) = error "Internal error: cannot calculate a concrete prefix of an open expression"-concPrefix (ConcreteBuf b) = Just (num . BS.length $ b)-concPrefix e = error $ "Internal error: cannot compute a concrete prefix length for: " <> show e+    go _ (CopySlice _ _ _ _ _) = internalError "cannot compute a concrete prefix length for nested copySlice expressions"+    go _ (GVar _) = internalError "cannot calculate a concrete prefix of an open expression"+concPrefix (ConcreteBuf b) = Just (into . BS.length $ b)+concPrefix e = internalError $ "cannot compute a concrete prefix length for: " <> show e   -- | Return the minimum possible length of a buffer. In the case of an@@ -452,8 +451,8 @@   where     go :: W256 -> Expr Buf -> Maybe Integer     -- base cases-    go l (AbstractBuf _) = if l == 0 then Nothing else Just $ num l-    go l (ConcreteBuf b) = Just . num $ Prelude.max (num . BS.length $ b) l+    go l (AbstractBuf _) = if l == 0 then Nothing else Just $ into l+    go l (ConcreteBuf b) = Just . into $ Prelude.max (unsafeInto . BS.length $ b) l     -- writes to a concrete index     go l (WriteWord (Lit idx) _ b) = go (Prelude.max l (idx + 32)) b     go l (WriteByte (Lit idx) _ b) = go (Prelude.max l (idx + 1)) b@@ -488,9 +487,9 @@ toList (AbstractBuf _) = Nothing toList (ConcreteBuf bs) = Just $ V.fromList $ LitByte <$> BS.unpack bs toList buf = case bufLength buf of-  Lit l -> if l <= num (maxBound :: Int)-              then Just $ V.generate (num l) (\i -> readByte (Lit $ num i) buf)-              else error "Internal Error: overflow when converting buffer to list"+  Lit l -> if l <= unsafeInto (maxBound :: Int)+              then Just $ V.generate (unsafeInto l) (\i -> readByte (Lit $ unsafeInto i) buf)+              else internalError "overflow when converting buffer to list"   _ -> Nothing  fromList :: V.Vector (Expr Byte) -> Expr Buf@@ -512,7 +511,7 @@        applySymWrites :: Expr Buf -> Int -> Expr Byte -> Expr Buf       applySymWrites buf _ (LitByte _) = buf-      applySymWrites buf idx by = WriteByte (Lit $ num idx) by buf+      applySymWrites buf idx by = WriteByte (Lit $ unsafeInto idx) by buf  instance Semigroup (Expr Buf) where   (ConcreteBuf a) <> (ConcreteBuf b) = ConcreteBuf $ a <> b@@ -534,7 +533,7 @@ stripWrites off size = \case   AbstractBuf s -> AbstractBuf s   ConcreteBuf b -> ConcreteBuf $ if off <= off + size-                                 then BS.take (num $ off+size) b+                                 then BS.take (unsafeInto $ off+size) b                                  else b   WriteByte (Lit idx) v prev     -> if idx - off >= size@@ -554,7 +553,7 @@   WriteByte i v prev -> WriteByte i v (stripWrites off size prev)   WriteWord i v prev -> WriteWord i v (stripWrites off size prev)   CopySlice srcOff dstOff size' src dst -> CopySlice srcOff dstOff size' src dst-  GVar _ ->  error "unexpected GVar in stripWrites"+  GVar _ ->  internalError "unexpected GVar in stripWrites"   -- ** Storage ** -----------------------------------------------------------------------------------@@ -591,7 +590,7 @@     (Lit _, Lit _) -> readStorage addr' slot' prev     -- if the the addresses don't match syntactically and are abstract then we can't skip this write     _ -> Just $ SLoad addr' slot' s-readStorage _ _ (GVar _) = error "Can't read from a GVar"+readStorage _ _ (GVar _) = internalError "Can't read from a GVar"  readStorage' :: Expr EWord -> Expr EWord -> Expr Storage -> Expr EWord readStorage' addr loc store = case readStorage addr loc store of@@ -665,9 +664,9 @@       | idx < maxBytes         = (writeWord (Lit idx) val (             ConcreteBuf $-              (BS.take (num idx) (padRight (num idx) b))+              (BS.take (unsafeInto idx) (padRight (unsafeInto idx) b))               <> (BS.replicate 32 0)-              <> (BS.drop (num idx + 32) b)))+              <> (BS.drop (unsafeInto idx + 32) b)))       | otherwise = o     go (WriteWord a b c) = writeWord a b c @@ -812,10 +811,10 @@   litAddr :: Addr -> Expr EWord-litAddr = Lit . num+litAddr = Lit . into  exprToAddr :: Expr EWord -> Maybe Addr-exprToAddr (Lit x) = Just (num x)+exprToAddr (Lit x) = Just (unsafeInto x) exprToAddr _ = Nothing  litCode :: BS.ByteString -> [Expr Byte]@@ -892,7 +891,7 @@     unmaskedBytes = fromIntegral $ (countLeadingZeros mask) `Prelude.div` 8     isByteAligned m = (countLeadingZeros m) `Prelude.mod` 8 == 0 indexWord (Lit idx) (Lit w)-  | idx <= 31 = LitByte . fromIntegral $ shiftR w (248 - num idx * 8)+  | idx <= 31 = LitByte . fromIntegral $ shiftR w (248 - unsafeInto idx * 8)   | otherwise = LitByte 0 indexWord (Lit idx) (JoinBytes zero        one        two       three                                four        five       six       seven@@ -993,3 +992,6 @@     go :: Expr a -> Any     go node | p node  = Any True     go _ = Any False++inRange :: Int -> Expr EWord -> Prop+inRange sz e = PAnd (PGEq e (Lit 0)) (PLEq e (Lit $ 2 ^ sz - 1))

@@ -1,7 +1,4 @@-{-# Language PartialTypeSignatures #-}-{-# Language DataKinds #-}-{-# Language ExtendedDefaultRules #-}-{-# Language PatternSynonyms #-}+{-# LANGUAGE PatternSynonyms #-}  -- Converts between Ethereum contract states and simple trees of -- texts.  Dumps and loads such trees as Git repositories (the state@@ -32,29 +29,26 @@   , fileToFact   ) where -import EVM          (bytecode)-import EVM.Expr     (writeStorage, litAddr)+import EVM (bytecode)+import EVM qualified+import EVM.Expr (writeStorage, litAddr) import EVM.Types -import qualified EVM--import Prelude hiding (Word)- import Optics.Core import Optics.State  import Control.Monad.State.Strict (execState, when) import Data.ByteString (ByteString)-import Data.Ord        (comparing)-import Data.Set        (Set)-import Data.Map        (Map)-import Text.Read       (readMaybe)--import qualified Data.ByteString.Base16 as BS16-import qualified Data.ByteString as BS-import qualified Data.ByteString.Char8 as Char8-import qualified Data.Map as Map-import qualified Data.Set as Set+import Data.ByteString.Base16 qualified as BS16+import Data.ByteString qualified as BS+import Data.ByteString.Char8 qualified as Char8+import Data.Map (Map)+import Data.Map qualified as Map+import Data.Set (Set)+import Data.Set qualified as Set+import Data.Ord (comparing)+import Text.Read (readMaybe)+import Witch (into)  -- We treat everything as ASCII byte strings because -- we only use hex digits (and the letter 'x').@@ -126,13 +120,13 @@   storageFacts :: Addr -> Map W256 (Map W256 W256) -> [Fact]-storageFacts a store = map f (Map.toList (Map.findWithDefault Map.empty (num a) store))+storageFacts a store = map f (Map.toList (Map.findWithDefault Map.empty (into a) store))   where     f :: (W256, W256) -> Fact     f (k, v) = StorageFact       { addr  = a-      , what  = fromIntegral v-      , which = fromIntegral k+      , what  = v+      , which = k       }  cacheFacts :: Cache -> Set Fact@@ -146,7 +140,7 @@   case vm.env.storage of     EmptyStore -> contractFacts k v Map.empty     ConcreteStore s -> contractFacts k v s-    _ -> error "cannot serialize an abstract store"+    _ -> internalError "cannot serialize an abstract store"  -- Somewhat stupidly, this function demands that for each contract, -- the code fact for that contract comes before the other facts for@@ -176,9 +170,9 @@       when (vm.state.contract == addr) $ EVM.loadContract addr     StorageFact {..} -> let         store = vm.cache.fetchedStorage-        ctrct = Map.findWithDefault Map.empty (num addr) store+        ctrct = Map.findWithDefault Map.empty (into addr) store       in-        vm & set (#cache % #fetchedStorage) (Map.insert (num addr) (Map.insert which what ctrct) store)+        vm & set (#cache % #fetchedStorage) (Map.insert (into addr) (Map.insert which what ctrct) store)     BalanceFact {..} ->       vm & set (#cache % #fetchedContracts % ix addr % #balance) what     NonceFact   {..} ->

@@ -12,10 +12,9 @@  import Optics.Core import Data.Set   (Set)+import Data.Set qualified as Set import Data.Maybe (catMaybes)--import qualified Data.Set         as Set-import qualified Restless.Git     as Git+import Restless.Git qualified as Git  newtype RepoAt = RepoAt String   deriving (Eq, Ord, Show)

@@ -1,36 +1,31 @@-{-# Language GADTs #-}-{-# Language DataKinds #-}+{-# LANGUAGE DataKinds #-}  module EVM.Fetch where -import Prelude hiding (Word)-+import EVM (initialContract) import EVM.ABI+import EVM.FeeSchedule qualified as FeeSchedule+import EVM.Format (hexText) import EVM.SMT import EVM.Solvers import EVM.Types-import EVM.Format (hexText)-import EVM        (initialContract)-import qualified EVM.FeeSchedule as FeeSchedule  import Optics.Core  import Control.Monad.Trans.Maybe import Data.Aeson hiding (Error) import Data.Aeson.Optics-import qualified Data.ByteString as BS+import Data.ByteString qualified as BS import Data.Text (Text, unpack, pack) import Data.Maybe (fromMaybe) import Data.List (foldl')-import qualified Data.Text as T--import qualified Data.Vector as RegularVector+import Data.Text qualified as T+import Data.Vector qualified as RegularVector import Network.Wreq import Network.Wreq.Session (Session)-import System.Process--import qualified Network.Wreq.Session as Session+import Network.Wreq.Session qualified as Session import Numeric.Natural (Natural)+import System.Process  -- | Abstract representation of an RPC fetch request data RpcQuery a where@@ -81,8 +76,8 @@   -> (Value -> IO (Maybe Value))   -> RpcQuery a   -> IO (Maybe a)-fetchQuery n f q = do-  x <- case q of+fetchQuery n f q =+  case q of     QueryCode addr -> do         m <- f (rpc "eth_getCode" [toRPC addr, toRPC n])         pure $ do@@ -95,7 +90,7 @@           readText <$> t     QueryBlock -> do       m <- f (rpc "eth_getBlockByNumber" [toRPC n, toRPC False])-      return $ m >>= parseBlock+      pure $ m >>= parseBlock     QueryBalance addr -> do         m <- f (rpc "eth_getBalance" [toRPC addr, toRPC n])         pure $ do@@ -111,9 +106,7 @@         pure $ do           t <- preview _String <$> m           readText <$> t-  return x - parseBlock :: (AsValue s, Show s) => s -> Maybe Block parseBlock j = do   coinbase   <- readText <$> j ^? key "miner" % _String@@ -132,14 +125,14 @@      (Just p, _, _) -> p      (Nothing, Just mh, Just 0x0) -> mh      (Nothing, Just _, Just d) -> d-     _ -> error "Internal Error: block contains both difficulty and prevRandao"+     _ -> internalError "block contains both difficulty and prevRandao"   -- default codesize, default gas limit, default feescedule-  return $ Block coinbase timestamp number prd gasLimit (fromMaybe 0 baseFee) 0xffffffff FeeSchedule.berlin+  pure $ Block coinbase timestamp number prd gasLimit (fromMaybe 0 baseFee) 0xffffffff FeeSchedule.berlin  fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value) fetchWithSession url sess x = do   r <- asValue =<< Session.post sess (unpack url) x-  return (r ^? (lensVL responseBody) % key "result")+  pure (r ^? (lensVL responseBody) % key "result")  fetchContractWithSession   :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)@@ -152,7 +145,7 @@   theNonce   <- MaybeT $ fetch (QueryNonce addr)   theBalance <- MaybeT $ fetch (QueryBalance addr) -  return $+  pure $     initialContract (RuntimeCode (ConcreteRuntimeCode theCode))       & set #nonce    theNonce       & set #balance  theBalance@@ -207,7 +200,7 @@           (_, stdout', _) <- readProcessWithExitCode cmd args ""           pure . continue . encodeAbiValue $             AbiTuple (RegularVector.fromList [ AbiBytesDynamic . hexText . pack $ stdout'])-       _ -> error (show vals)+       _ -> internalError (show vals)      PleaseAskSMT branchcondition pathconditions continue -> do          let pathconds = foldl' PAnd (PBool True) pathconditions@@ -218,20 +211,20 @@     -- we generate a new array to the fetched contract here     PleaseFetchContract addr continue -> do       contract <- case info of-                    Nothing -> return $ Just $ initialContract (RuntimeCode (ConcreteRuntimeCode ""))+                    Nothing -> pure $ Just $ initialContract (RuntimeCode (ConcreteRuntimeCode ""))                     Just (n, url) -> fetchContractFrom n url addr       case contract of-        Just x -> return $ continue x-        Nothing -> error ("oracle error: " ++ show q)+        Just x -> pure $ continue x+        Nothing -> internalError $ "oracle error: " ++ show q      PleaseFetchSlot addr slot continue ->       case info of-        Nothing -> return (continue 0)+        Nothing -> pure (continue 0)         Just (n, url) ->-         fetchSlotFrom n url addr (fromIntegral slot) >>= \case-           Just x  -> return (continue x)+         fetchSlotFrom n url addr slot >>= \case+           Just x  -> pure (continue x)            Nothing ->-             error ("oracle error: " ++ show q)+             internalError $ "oracle error: " ++ show q  type Fetcher = Query -> IO (EVM ()) @@ -243,19 +236,19 @@ checkBranch :: SolverGroup -> Prop -> Prop -> IO BranchCondition checkBranch solvers branchcondition pathconditions = do   checkSat solvers (assertProps [(branchcondition .&& pathconditions)]) >>= \case-     -- the condition is unsatisfiable-     Unsat -> -- if pathconditions are consistent then the condition must be false-            return $ Case False-     -- Sat means its possible for condition to hold-     Sat _ -> -- is its negation also possible?-            checkSat solvers (assertProps [(pathconditions .&& (PNeg branchcondition))]) >>= \case-               -- No. The condition must hold-               Unsat -> return $ Case True-               -- Yes. Both branches possible-               Sat _ -> return EVM.Types.Unknown-               -- Explore both branches in case of timeout-               EVM.Solvers.Unknown -> return EVM.Types.Unknown-               Error e -> error $ "Internal Error: SMT Solver returned with an error: " <> T.unpack e-     -- If the query times out, we simply explore both paths-     EVM.Solvers.Unknown -> return EVM.Types.Unknown-     Error e -> error $ "Internal Error: SMT Solver returned with an error: " <> T.unpack e+    -- the condition is unsatisfiable+    Unsat -> -- if pathconditions are consistent then the condition must be false+      pure $ Case False+    -- Sat means its possible for condition to hold+    Sat _ -> -- is its negation also possible?+      checkSat solvers (assertProps [(pathconditions .&& (PNeg branchcondition))]) >>= \case+        -- No. The condition must hold+        Unsat -> pure $ Case True+        -- Yes. Both branches possible+        Sat _ -> pure EVM.Types.Unknown+        -- Explore both branches in case of timeout+        EVM.Solvers.Unknown -> pure EVM.Types.Unknown+        Error e -> error $ "Internal Error: SMT Solver pureed with an error: " <> T.unpack e+    -- If the query times out, we simply explore both paths+    EVM.Solvers.Unknown -> pure EVM.Types.Unknown+    Error e -> internalError $ "SMT Solver pureed with an error: " <> T.unpack e

@@ -1,5 +1,5 @@-{-# Language DataKinds #-}-{-# Language ImplicitParams #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ImplicitParams #-}  module EVM.Format   ( formatExpr@@ -10,6 +10,7 @@   , showError   , showTree   , showTraceTree+  , showTraceTree'   , showValues   , prettyvmresult   , showCall@@ -31,10 +32,8 @@   , bsToHex   ) where -import Prelude hiding (Word)- import EVM.Types-import EVM (cheatCode, traceForest)+import EVM (cheatCode, traceForest, traceForest', traceContext) import EVM.ABI (getAbiSeq, parseTypeName, AbiValue(..), AbiType(..), SolError(..), Indexed(..), Event(..)) import EVM.Dapp (DappContext(..), DappInfo(..), showTraceLocation) import EVM.Expr qualified as Expr@@ -53,6 +52,7 @@ import Data.DoubleWord (signedWord) import Data.Foldable (toList) import Data.List (isPrefixOf)+import Data.Map (Map) import Data.Map qualified as Map import Data.Maybe (catMaybes, fromMaybe, fromJust) import Data.Text (Text, pack, unpack, intercalate, dropEnd, splitOn)@@ -63,19 +63,20 @@ import Numeric (showHex) import Data.ByteString.Char8 qualified as Char8 import Data.ByteString.Base16 qualified as BS16+import Witch (into, unsafeInto)  data Signedness = Signed | Unsigned   deriving (Show)  showDec :: Signedness -> W256 -> Text showDec signed (W256 w)-  | i == num cheatCode = "<hevm cheat address>"+  | i == into cheatCode = "<hevm cheat address>"   | (i :: Integer) == 2 ^ (256 :: Integer) - 1 = "MAX_UINT256"   | otherwise = T.pack (show (i :: Integer))   where     i = case signed of-          Signed   -> num (signedWord w)-          Unsigned -> num w+          Signed   -> into (signedWord w)+          Unsigned -> into w  showWordExact :: W256 -> Text showWordExact w = humanizeInteger (toInteger w)@@ -83,7 +84,7 @@ showWordExplanation :: W256 -> DappInfo -> Text showWordExplanation w _ | w > 0xffffffff = showDec Unsigned w showWordExplanation w dapp =-  case Map.lookup (fromIntegral w) dapp.abiMap of+  case Map.lookup (unsafeInto w) dapp.abiMap of     Nothing -> showDec Unsigned w     Just x  -> "keccak(\"" <> x.methodSignature <> "\")" @@ -184,20 +185,27 @@ formatSBinary :: Expr Buf -> Text formatSBinary (ConcreteBuf bs) = formatBinary bs formatSBinary (AbstractBuf t) = "<" <> t <> " abstract buf>"-formatSBinary _ = error "formatSBinary: implement me"+formatSBinary _ = internalError "formatSBinary: implement me"  showTraceTree :: DappInfo -> VM -> Text showTraceTree dapp vm =   let forest = traceForest vm-      traces = fmap (fmap (unpack . showTrace dapp vm)) forest+      traces = fmap (fmap (unpack . showTrace dapp (vm.env.contracts))) forest   in pack $ concatMap showTree traces +showTraceTree' :: DappInfo -> Expr End -> Text+showTraceTree' _ (ITE {}) = error "Internal Error: ITE does not contain a trace"+showTraceTree' dapp leaf =+  let forest = traceForest' leaf+      traces = fmap (fmap (unpack . showTrace dapp (traceContext leaf))) forest+  in pack $ concatMap showTree traces+ unindexed :: [(Text, AbiType, Indexed)] -> [AbiType] unindexed ts = [t | (_, t, NotIndexed) <- ts] -showTrace :: DappInfo -> VM -> Trace -> Text-showTrace dapp vm trace =-  let ?context = DappContext { info = dapp, env = vm.env.contracts }+showTrace :: DappInfo -> Map Addr Contract -> Trace -> Text+showTrace dapp env trace =+  let ?context = DappContext { info = dapp, env = env }   in let     pos =       case showTraceLocation dapp trace of@@ -246,10 +254,10 @@                       --     bytes             data                       -- ) anonymous;                       let-                        sig = fromIntegral $ shiftR topic 224 :: FunctionSelector+                        sig = unsafeInto $ shiftR topic 224 :: FunctionSelector                         usr = case maybeLitWord t2 of                           Just w ->-                            pack $ show (fromIntegral w :: Addr)+                            pack $ show (unsafeInto w :: Addr)                           Nothing  ->                             "<symbolic>"                       in@@ -263,19 +271,6 @@             Nothing ->               logn -    QueryTrace q ->-      case q of-        PleaseFetchContract addr _ ->-          "fetch contract " <> pack (show addr) <> pos-        PleaseFetchSlot addr slot _ ->-          "fetch storage slot " <> pack (show slot) <> " from " <> pack (show addr) <> pos-        PleaseAskSMT {} ->-          "ask smt" <> pos-        --PleaseMakeUnique {} ->-          --"make unique value" <> pos-        PleaseDoFFI cmd _ ->-          "execute ffi " <> pack (show cmd) <> pos-     ErrorTrace e ->       case e of         Revert out ->@@ -285,7 +280,7 @@      ReturnTrace out (CallContext _ _ _ _ _ (Just abi) _ _ _) ->       "← " <>-        case Map.lookup (fromIntegral abi) fullAbiMap of+        case Map.lookup (unsafeInto abi) fullAbiMap of           Just m  ->             case unzip m.output of               ([], []) ->@@ -319,9 +314,11 @@       in case preview (ix hash' % _2) dapp.solcByHash of         Nothing ->           calltype-            <> pack (show target)+            <> case target of+                 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D -> "HEVM"+                 _ -> pack (show target)             <> pack "::"-            <> case Map.lookup (fromIntegral (fromMaybe 0x00 abi)) fullAbiMap of+            <> case Map.lookup (unsafeInto (fromMaybe 0x00 abi)) fullAbiMap of                  Just m  ->                    "\x1b[1m"                    <> m.name@@ -361,7 +358,7 @@   maybe "" (contractNamePart . (.contractName))  maybeAbiName :: SolcContract -> W256 -> Maybe Text-maybeAbiName solc abi = Map.lookup (fromIntegral abi) solc.abiMap <&> (.methodSignature)+maybeAbiName solc abi = Map.lookup (unsafeInto abi) solc.abiMap <&> (.methodSignature)  contractNamePart :: Text -> Text contractNamePart x = T.split (== ':') x !! 1@@ -393,16 +390,16 @@   BadCheatCode a -> "Bad cheat code: sig: " <> show a  prettyvmresult :: Expr End -> String-prettyvmresult (Failure _ (Revert (ConcreteBuf ""))) = "Revert"-prettyvmresult (Success _ (ConcreteBuf msg) _) =+prettyvmresult (Failure _ _ (Revert (ConcreteBuf ""))) = "Revert"+prettyvmresult (Success _ _ (ConcreteBuf msg) _) =   if BS.null msg   then "Stop"   else "Return: " <> show (ByteStringS msg)-prettyvmresult (Success _ _ _) =+prettyvmresult (Success _ _ _ _) =   "Return: <symbolic>"-prettyvmresult (Failure _ err) = prettyError err-prettyvmresult (Partial _ p) = T.unpack $ formatPartial p-prettyvmresult r = error $ "Internal Error: Invalid result: " <> show r+prettyvmresult (Failure _ _ err) = prettyError err+prettyvmresult (Partial _ _ p) = T.unpack $ formatPartial p+prettyvmresult r = internalError $ "Invalid result: " <> show r  indent :: Int -> Text -> Text indent n = rstrip . T.unlines . fmap (T.replicate n (T.pack [' ']) <>) . T.lines@@ -448,7 +445,7 @@         , indent 2 (formatExpr t)         , indent 2 (formatExpr f)         , ")"]-      Success asserts buf store -> T.unlines+      Success asserts _ buf store -> T.unlines         [ "(Return"         , indent 2 $ T.unlines           [ "Data:"@@ -461,7 +458,7 @@           ]         , ")"         ]-      Failure asserts err -> T.unlines+      Failure asserts _ err -> T.unlines         [ "(Failure"         , indent 2 $ T.unlines           [ "Error:"@@ -596,13 +593,13 @@ hexByteString msg bs =   case BS16.decodeBase16 bs of     Right x -> x-    _ -> error ("invalid hex bytestring for " ++ msg)+    _ -> internalError $ "invalid hex bytestring for " ++ msg  hexText :: Text -> ByteString hexText t =   case BS16.decodeBase16 (T.encodeUtf8 (T.drop 2 t)) of     Right x -> x-    _ -> error ("invalid hex bytestring " ++ show t)+    _ -> internalError $ "invalid hex bytestring " ++ show t  bsToHex :: ByteString -> String bsToHex bs = concatMap (paddedShowHex 2) (BS.unpack bs)

@@ -1,20 +1,17 @@ {-# LANGUAGE DataKinds #-}+ {- |     Module: EVM.Keccak     Description: Expr passes to determine Keccak assumptions -}- module EVM.Keccak (keccakAssumptions) where -import Prelude hiding (Word, LT, GT)--import Data.Set (Set)-import qualified Data.Set as Set import Control.Monad.State+import Data.Set (Set)+import Data.Set qualified as Set -import EVM.Types import EVM.Traversals-+import EVM.Types  data BuilderState = BuilderState   { keccaks :: Set (Expr EWord) }@@ -54,12 +51,12 @@  minProp :: Expr EWord -> Prop minProp k@(Keccak _) = PGT k (Lit 50)-minProp _ = error "Internal error: expected keccak expression"+minProp _ = internalError "expected keccak expression"  injProp :: (Expr EWord, Expr EWord) -> Prop injProp (k1@(Keccak b1), k2@(Keccak b2)) =   POr (PEq b1 b2) (PNeg (PEq k1 k2))-injProp _ = error "Internal error: expected keccak expression"+injProp _ = internalError "expected keccak expression"  -- Takes a list of props, find all keccak occurences and generates two kinds of assumptions: --   1. Minimum output value: That the output of the invocation is greater than@@ -75,5 +72,3 @@      injectivity = fmap injProp $ combine (Set.toList st.keccaks)     minValue = fmap minProp (Set.toList st.keccaks)--

@@ -15,162 +15,163 @@ import Data.Vector qualified as V import Data.Word (Word8) import Numeric (showHex)+import Witch (into)  intToOpName:: Int -> String intToOpName a =   case a of-   0x00-> "STOP"-   0x01-> "ADD"-   0x02-> "MUL"-   0x03-> "SUB"-   0x04-> "DIV"-   0x05-> "SDIV"-   0x06-> "MOD"-   0x07-> "SMOD"-   0x08-> "ADDMOD"-   0x09-> "MULMOD"-   0x0a-> "EXP"-   0x0b-> "SIGNEXTEND"-   ---   0x10 -> "LT"-   0x11 -> "GT"-   0x12 -> "SLT"-   0x13 -> "SGT"-   0x14 -> "EQ"-   0x15 -> "ISZERO"-   0x16 -> "AND"-   0x17 -> "OR"-   0x18 -> "XOR"-   0x19 -> "NOT"-   0x1a -> "BYTE"-   0x1b -> "SHL"-   0x1c -> "SHR"-   0x1d -> "SAR"-   0x20 -> "SHA3"-   0x30 -> "ADDRESS"-   ---   0x31 -> "BALANCE"-   0x32 -> "ORIGIN"-   0x33 -> "CALLER"-   0x34 -> "CALLVALUE"-   0x35 -> "CALLDATALOAD"-   0x36 -> "CALLDATASIZE"-   0x37 -> "CALLDATACOPY"-   0x38 -> "CODESIZE"-   0x39 -> "CODECOPY"-   0x3a -> "GASPRICE"-   0x3b -> "EXTCODESIZE"-   0x3c -> "EXTCODECOPY"-   0x3d -> "RETURNDATASIZE"-   0x3e -> "RETURNDATACOPY"-   0x3f -> "EXTCODEHASH"-   0x40 -> "BLOCKHASH"-   0x41 -> "COINBASE"-   0x42 -> "TIMESTAMP"-   0x43 -> "NUMBER"-   0x44 -> "PREVRANDAO"-   0x45 -> "GASLIMIT"-   0x46 -> "CHAINID"-   0x47 -> "SELFBALANCE"-   0x48 -> "BASEFEE"-   0x50 -> "POP"-   0x51 -> "MLOAD"-   0x52 -> "MSTORE"-   0x53 -> "MSTORE8"-   0x54 -> "SLOAD"-   0x55 -> "SSTORE"-   0x56 -> "JUMP"-   0x57 -> "JUMPI"-   0x58 -> "PC"-   0x59 -> "MSIZE"-   0x5a -> "GAS"-   0x5b -> "JUMPDEST"-   ---   0x5f -> "PUSH0"-   0x60 -> "PUSH1"-   0x61 -> "PUSH2"-   0x62 -> "PUSH3"-   0x63 -> "PUSH4"-   0x64 -> "PUSH5"-   0x65 -> "PUSH6"-   0x66 -> "PUSH7"-   0x67 -> "PUSH8"-   0x68 -> "PUSH9"-   0x69 -> "PUSH10"-   0x6a -> "PUSH11"-   0x6b -> "PUSH12"-   0x6c -> "PUSH13"-   0x6d -> "PUSH14"-   0x6e -> "PUSH15"-   0x6f -> "PUSH16"-   0x70 -> "PUSH17"-   0x71 -> "PUSH18"-   0x72 -> "PUSH19"-   0x73 -> "PUSH20"-   0x74 -> "PUSH21"-   0x75 -> "PUSH22"-   0x76 -> "PUSH23"-   0x77 -> "PUSH24"-   0x78 -> "PUSH25"-   0x79 -> "PUSH26"-   0x7a -> "PUSH27"-   0x7b -> "PUSH28"-   0x7c -> "PUSH29"-   0x7d -> "PUSH30"-   0x7e -> "PUSH31"-   0x7f -> "PUSH32"-   ---   0x80 -> "DUP1"-   0x81 -> "DUP2"-   0x82 -> "DUP3"-   0x83 -> "DUP4"-   0x84 -> "DUP5"-   0x85 -> "DUP6"-   0x86 -> "DUP7"-   0x87 -> "DUP8"-   0x88 -> "DUP9"-   0x89 -> "DUP10"-   0x8a -> "DUP11"-   0x8b -> "DUP12"-   0x8c -> "DUP13"-   0x8d -> "DUP14"-   0x8e -> "DUP15"-   0x8f -> "DUP16"-   ---   0x90 -> "SWAP1"-   0x91 -> "SWAP2"-   0x92 -> "SWAP3"-   0x93 -> "SWAP4"-   0x94 -> "SWAP5"-   0x95 -> "SWAP6"-   0x96 -> "SWAP7"-   0x97 -> "SWAP8"-   0x98 -> "SWAP9"-   0x99 -> "SWAP10"-   0x9a -> "SWAP11"-   0x9b -> "SWAP12"-   0x9c -> "SWAP13"-   0x9d -> "SWAP14"-   0x9e -> "SWAP15"-   0x9f -> "SWAP16"-   ---   0xa0 -> "LOG0"-   0xa1 -> "LOG1"-   0xa2 -> "LOG2"-   0xa3 -> "LOG3"-   0xa4 -> "LOG4"-   ---   0xf0 -> "CREATE"-   0xf1 -> "CALL"-   0xf2 -> "CALLCODE"-   0xf3 -> "RETURN"-   0xf4 -> "DELEGATECALL"-   0xf5 -> "CREATE2"-   0xfa -> "STATICCALL"-   0xfd -> "REVERT"-   0xfe -> "INVALID"-   0xff -> "SELFDESTRUCT"-   _ -> "UNKNOWN "+    0x00 -> "STOP"+    0x01 -> "ADD"+    0x02 -> "MUL"+    0x03 -> "SUB"+    0x04 -> "DIV"+    0x05 -> "SDIV"+    0x06 -> "MOD"+    0x07 -> "SMOD"+    0x08 -> "ADDMOD"+    0x09 -> "MULMOD"+    0x0a -> "EXP"+    0x0b -> "SIGNEXTEND"+    --+    0x10 -> "LT"+    0x11 -> "GT"+    0x12 -> "SLT"+    0x13 -> "SGT"+    0x14 -> "EQ"+    0x15 -> "ISZERO"+    0x16 -> "AND"+    0x17 -> "OR"+    0x18 -> "XOR"+    0x19 -> "NOT"+    0x1a -> "BYTE"+    0x1b -> "SHL"+    0x1c -> "SHR"+    0x1d -> "SAR"+    0x20 -> "SHA3"+    0x30 -> "ADDRESS"+    --+    0x31 -> "BALANCE"+    0x32 -> "ORIGIN"+    0x33 -> "CALLER"+    0x34 -> "CALLVALUE"+    0x35 -> "CALLDATALOAD"+    0x36 -> "CALLDATASIZE"+    0x37 -> "CALLDATACOPY"+    0x38 -> "CODESIZE"+    0x39 -> "CODECOPY"+    0x3a -> "GASPRICE"+    0x3b -> "EXTCODESIZE"+    0x3c -> "EXTCODECOPY"+    0x3d -> "RETURNDATASIZE"+    0x3e -> "RETURNDATACOPY"+    0x3f -> "EXTCODEHASH"+    0x40 -> "BLOCKHASH"+    0x41 -> "COINBASE"+    0x42 -> "TIMESTAMP"+    0x43 -> "NUMBER"+    0x44 -> "PREVRANDAO"+    0x45 -> "GASLIMIT"+    0x46 -> "CHAINID"+    0x47 -> "SELFBALANCE"+    0x48 -> "BASEFEE"+    0x50 -> "POP"+    0x51 -> "MLOAD"+    0x52 -> "MSTORE"+    0x53 -> "MSTORE8"+    0x54 -> "SLOAD"+    0x55 -> "SSTORE"+    0x56 -> "JUMP"+    0x57 -> "JUMPI"+    0x58 -> "PC"+    0x59 -> "MSIZE"+    0x5a -> "GAS"+    0x5b -> "JUMPDEST"+    --+    0x5f -> "PUSH0"+    0x60 -> "PUSH1"+    0x61 -> "PUSH2"+    0x62 -> "PUSH3"+    0x63 -> "PUSH4"+    0x64 -> "PUSH5"+    0x65 -> "PUSH6"+    0x66 -> "PUSH7"+    0x67 -> "PUSH8"+    0x68 -> "PUSH9"+    0x69 -> "PUSH10"+    0x6a -> "PUSH11"+    0x6b -> "PUSH12"+    0x6c -> "PUSH13"+    0x6d -> "PUSH14"+    0x6e -> "PUSH15"+    0x6f -> "PUSH16"+    0x70 -> "PUSH17"+    0x71 -> "PUSH18"+    0x72 -> "PUSH19"+    0x73 -> "PUSH20"+    0x74 -> "PUSH21"+    0x75 -> "PUSH22"+    0x76 -> "PUSH23"+    0x77 -> "PUSH24"+    0x78 -> "PUSH25"+    0x79 -> "PUSH26"+    0x7a -> "PUSH27"+    0x7b -> "PUSH28"+    0x7c -> "PUSH29"+    0x7d -> "PUSH30"+    0x7e -> "PUSH31"+    0x7f -> "PUSH32"+    --+    0x80 -> "DUP1"+    0x81 -> "DUP2"+    0x82 -> "DUP3"+    0x83 -> "DUP4"+    0x84 -> "DUP5"+    0x85 -> "DUP6"+    0x86 -> "DUP7"+    0x87 -> "DUP8"+    0x88 -> "DUP9"+    0x89 -> "DUP10"+    0x8a -> "DUP11"+    0x8b -> "DUP12"+    0x8c -> "DUP13"+    0x8d -> "DUP14"+    0x8e -> "DUP15"+    0x8f -> "DUP16"+    --+    0x90 -> "SWAP1"+    0x91 -> "SWAP2"+    0x92 -> "SWAP3"+    0x93 -> "SWAP4"+    0x94 -> "SWAP5"+    0x95 -> "SWAP6"+    0x96 -> "SWAP7"+    0x97 -> "SWAP8"+    0x98 -> "SWAP9"+    0x99 -> "SWAP10"+    0x9a -> "SWAP11"+    0x9b -> "SWAP12"+    0x9c -> "SWAP13"+    0x9d -> "SWAP14"+    0x9e -> "SWAP15"+    0x9f -> "SWAP16"+    --+    0xa0 -> "LOG0"+    0xa1 -> "LOG1"+    0xa2 -> "LOG2"+    0xa3 -> "LOG3"+    0xa4 -> "LOG4"+    --+    0xf0 -> "CREATE"+    0xf1 -> "CALL"+    0xf2 -> "CALLCODE"+    0xf3 -> "RETURN"+    0xf4 -> "DELEGATECALL"+    0xf5 -> "CREATE2"+    0xfa -> "STATICCALL"+    0xfd -> "REVERT"+    0xfe -> "INVALID"+    0xff -> "SELFDESTRUCT"+    _ -> "UNKNOWN "  opString :: (Integral a, Show a) => (a, Op) -> String opString (i, o) = let showPc x | x < 0x10 = '0' : showHex x ""@@ -262,7 +263,7 @@  readOp :: Word8 -> [Expr Byte] -> Op readOp x xs =-  (\n -> Expr.readBytes (fromIntegral n) (Lit 0) (Expr.fromList $ V.fromList xs)) <$> getOp x+  (\n -> Expr.readBytes (into n) (Lit 0) (Expr.fromList $ V.fromList xs)) <$> getOp x  getOp :: Word8 -> GenericOp Word8 getOp x | x >= 0x80 && x <= 0x8f = OpDup (x - 0x80 + 1)

@@ -6,13 +6,13 @@ import Control.Monad.Free import Control.Monad.State import Data.ByteString (ByteString)+import Data.ByteString qualified as BS import Data.Foldable (toList) import Data.List (stripPrefix)+import Data.Map qualified as Map import Data.Sequence (Seq)--import qualified Data.ByteString as BS-import qualified Data.Map as Map-import qualified Data.Sequence as Seq+import Data.Sequence qualified as Seq+import Witch (into)  data KV k v a   = Put k v a@@ -36,7 +36,7 @@       -> m a runDB putt gett (DB ops) = go ops   where-    go (Pure a) = return a+    go (Pure a) = pure a     go (Free (Put k v next)) = putt k v >> go next     go (Free (Get k handler)) = gett k >>= go . handler @@ -82,28 +82,28 @@   let bytes = rlpencode $ rlpNode node       digest = word256Bytes $ keccak' bytes   in if BS.length bytes < 32-    then return $ Literal node+    then pure $ Literal node     else do       insertDB digest node-      return $ Hash digest+      pure $ Hash digest  getNode :: Ref -> NodeDB Node getNode (Hash d) = lookupDB d-getNode (Literal n) = return n+getNode (Literal n) = pure n  lookupPath :: Ref -> Path -> NodeDB ByteString lookupPath root path = getNode root >>= getVal path  getVal :: Path -> Node -> NodeDB ByteString-getVal _ Empty = return BS.empty+getVal _ Empty = pure BS.empty getVal path (Shortcut nodePath ref) =   case (stripPrefix nodePath path, ref) of-    (Just [], Right value) -> return value+    (Just [], Right value) -> pure value     (Just remaining, Left key) -> lookupPath key remaining-    _ -> return BS.empty+    _ -> pure BS.empty -getVal [] (Full _ val) = return val-getVal (p:ps) (Full refs _) = lookupPath (refs `Seq.index` (num p)) ps+getVal [] (Full _ val) = pure val+getVal (p:ps) (Full refs _) = lookupPath (refs `Seq.index` (into p)) ps  emptyRef :: Ref emptyRef = Literal Empty@@ -112,9 +112,9 @@ emptyRefs = Seq.replicate 16 emptyRef  addPrefix :: Path -> Node -> NodeDB Node-addPrefix _ Empty = return Empty-addPrefix [] node = return node-addPrefix path (Shortcut p v) = return $ Shortcut (path <> p) v+addPrefix _ Empty = pure Empty+addPrefix [] node = pure node+addPrefix path (Shortcut p v) = pure $ Shortcut (path <> p) v addPrefix path n = Shortcut path . Left <$> putNode n  insertRef :: Ref -> Path -> ByteString -> NodeDB Ref@@ -125,19 +125,19 @@                          putNode newNode  update :: Node -> Path -> ByteString -> NodeDB Node-update Empty p new  = return $ Shortcut p (Right new)-update (Full refs _) [] new = return (Full refs new)+update Empty p new  = pure $ Shortcut p (Right new)+update (Full refs _) [] new = pure (Full refs new) update (Full refs old) (p:ps) new = do-  newRef <- insertRef (refs `Seq.index` (num p)) ps new-  return $ Full (Seq.update (num p) newRef refs) old+  newRef <- insertRef (refs `Seq.index` (into p)) ps new+  pure $ Full (Seq.update (into p) newRef refs) old update (Shortcut (o:os) (Right old)) [] new = do   newRef <- insertRef emptyRef os old-  return $ Full (Seq.update (num o) newRef emptyRefs) new+  pure $ Full (Seq.update (into o) newRef emptyRefs) new update (Shortcut [] (Right old)) (p:ps) new = do   newRef <- insertRef emptyRef ps new-  return $ Full (Seq.update (num p) newRef emptyRefs) old+  pure $ Full (Seq.update (into p) newRef emptyRefs) old update (Shortcut [] (Right _)) [] new =-  return $ Shortcut [] (Right new)+  pure $ Shortcut [] (Right new) update (Shortcut (o:os) to) (p:ps) new | o == p   = update (Shortcut os to) ps new >>= addPrefix [o]                                        | otherwise = do@@ -145,38 +145,38 @@               (Left ref)  -> getNode ref >>= addPrefix os >>= putNode               (Right val) -> insertRef emptyRef os val   newRef <- insertRef emptyRef ps new-  let refs = Seq.update (num p) newRef $ Seq.update (num o) oldRef emptyRefs-  return $ Full refs BS.empty+  let refs = Seq.update (into p) newRef $ Seq.update (into o) oldRef emptyRefs+  pure $ Full refs BS.empty update (Shortcut (o:os) (Left ref)) [] new = do   newRef <- getNode ref >>= addPrefix os >>= putNode-  return $ Full (Seq.update (num o) newRef emptyRefs) new+  pure $ Full (Seq.update (into o) newRef emptyRefs) new update (Shortcut cut (Left ref)) ps new = do   newRef <- insertRef ref ps new-  return $ Shortcut cut (Left newRef)+  pure $ Shortcut cut (Left newRef)  delete :: Node -> Path -> NodeDB Node-delete Empty _ = return Empty-delete (Shortcut [] (Right _)) [] = return Empty-delete n@(Shortcut [] (Right _)) _ = return n+delete Empty _ = pure Empty+delete (Shortcut [] (Right _)) [] = pure Empty+delete n@(Shortcut [] (Right _)) _ = pure n delete (Shortcut [] (Left ref)) p = do node <- getNode ref                                        delete node p-delete n@(Shortcut _ _) [] = return n+delete n@(Shortcut _ _) [] = pure n delete n@(Shortcut (o:os) to) (p:ps) | p == o   = delete (Shortcut os to) ps >>= addPrefix [o]                                      | otherwise-  = return n+  = pure n delete (Full refs _) [] | refs == emptyRefs-  = return Empty+  = pure Empty                         | otherwise-  = return (Full refs BS.empty)+  = pure (Full refs BS.empty) delete (Full refs val) (p:ps) = do-  newRef <- insertRef (refs `Seq.index` (num p)) ps BS.empty-  let newRefs = Seq.update (num p) newRef refs+  newRef <- insertRef (refs `Seq.index` (into p)) ps BS.empty+  let newRefs = Seq.update (into p) newRef refs       nonEmpties = filter (\(_, ref) -> ref /= emptyRef) $ zip [0..15] $ toList newRefs   case (nonEmpties, BS.null val) of-    ([], True)         -> return Empty-    ([(n, ref)], True)  -> getNode ref >>= addPrefix [Nibble n]-    _                    -> return $ Full newRefs val+    ([], True)         -> pure Empty+    ([(n, ref)], True) -> getNode ref >>= addPrefix [Nibble n]+    _                  -> pure $ Full newRefs val  insert :: Ref -> ByteString -> ByteString -> NodeDB Ref insert ref key = insertRef ref (unpackNibbles key)

@@ -1,7 +1,7 @@ module EVM.Precompiled (execute) where  import Data.ByteString (ByteString)-import qualified Data.ByteString as BS+import Data.ByteString qualified as BS  import Foreign.C import Foreign.Ptr

@@ -1,10 +1,10 @@ module EVM.RLP where -import Prelude hiding (drop, head) import EVM.Types-import Data.Bits       (shiftR)-import Data.ByteString (ByteString, drop, head)-import qualified Data.ByteString   as BS+import Data.Bits (shiftR)+import Data.ByteString (ByteString)+import Data.ByteString qualified as BS+import Witch (into, unsafeInto)  data RLP = BS ByteString | List [RLP] deriving Eq @@ -18,46 +18,51 @@ -- helper function returning (the length of the prefix, the length of the content, isList boolean, optimal boolean) itemInfo :: ByteString -> (Int, Int, Bool, Bool) itemInfo bs | bs == mempty = (0, 0, False, False)-            | otherwise = case head bs of+            | otherwise = case BS.head bs of   x | 0 <= x && x < 128   -> (0, 1, False, True) -- directly encoded byte-  x | 128 <= x && x < 184 -> (1, num x - 128, False, (BS.length bs /= 2) || (127 < (head $ drop 1 bs))) -- short string-  x | 184 <= x && x < 192 -> (1 + pre, len, False, (len > 55) && head (drop 1 bs) /= 0) -- long string-    where pre = num $ x - 183-          len = num $ word $ slice 1 pre bs-  x | 192 <= x && x < 248 -> (1, num $ x - 192, True, True) -- short list-  x                       -> (1 + pre, len, True, (len > 55) && head (drop 1 bs) /= 0) -- long list-    where pre = num $ x - 247-          len = num $ word $ slice 1 pre bs+  x | 128 <= x && x < 184 -> (1, into x - 128, False, (BS.length bs /= 2) || (127 < (BS.head $ BS.drop 1 bs))) -- short string+  x | 184 <= x && x < 192 -> (1 + pre, len, False, (len > 55) && BS.head (BS.drop 1 bs) /= 0) -- long string+    where pre = into $ x - 183+          -- TODO: unsafeInto fails: cabal run test -- -p 'rlp' --quickcheck-replay=413899+          len = fromIntegral $ word $ slice 1 pre bs+  x | 192 <= x && x < 248 -> (1, into $ x - 192, True, True) -- short list+  x                       -> (1 + pre, len, True, (len > 55) && BS.head (BS.drop 1 bs) /= 0) -- long list+    where pre = into $ x - 247+          -- TODO: unsafeInto fails: cabal run test -- -p 'rlp' --quickcheck-replay=146332+          len = fromIntegral $ word $ slice 1 pre bs  rlpdecode :: ByteString -> Maybe RLP-rlpdecode bs | optimal && pre + len == BS.length bs = if isList-                                                   then do-                                                      items <- mapM-                                                        (\(s, e) -> rlpdecode $ slice s e content) $-                                                        rlplengths content 0 len-                                                      Just (List items)-                                                   else Just (BS content)-             | otherwise = Nothing+rlpdecode bs =+  if optimal && pre + len == BS.length bs then+    if isList then do+      items <- mapM (\(s, e) -> rlpdecode $ slice s e content) (rlplengths content 0 len)+      Just (List items)+    else+      Just (BS content)+  else Nothing   where (pre, len, isList, optimal) = itemInfo bs-        content = drop pre bs+        content = BS.drop pre bs  rlplengths :: ByteString -> Int -> Int -> [(Int,Int)]-rlplengths bs acc top | acc < top = let (pre, len, _, _) = itemInfo bs-                                    in (acc, pre + len) : rlplengths (drop (pre + len) bs) (acc + pre + len) top-                      | otherwise = []+rlplengths bs acc top =+  if acc < top then+    let (pre, len, _, _) = itemInfo bs+    in (acc, pre + len) : rlplengths (BS.drop (pre + len) bs) (acc + pre + len) top+  else []  rlpencode :: RLP -> ByteString-rlpencode (BS bs) = if BS.length bs == 1 && head bs < 128 then bs+rlpencode (BS bs) = if BS.length bs == 1 && BS.head bs < 128 then bs                     else encodeLen 128 bs rlpencode (List items) = encodeLen 192 (mconcat $ map rlpencode items)  encodeLen :: Int -> ByteString -> ByteString-encodeLen offset bs | BS.length bs <= 55 = prefix (BS.length bs) <> bs-                    | otherwise = prefix lenLen <> lenBytes <> bs-          where-            lenBytes = asBE $ BS.length bs-            prefix n = BS.singleton $ num $ offset + n-            lenLen = BS.length lenBytes + 55+encodeLen offset bs =+  if BS.length bs <= 55 then prefix (BS.length bs) <> bs+  else prefix lenLen <> lenBytes <> bs+  where+    lenBytes = asBE $ BS.length bs+    prefix n = BS.singleton $ unsafeInto $ offset + n+    lenLen = BS.length lenBytes + 55  rlpList :: [RLP] -> ByteString rlpList n = rlpencode $ List n@@ -82,7 +87,7 @@ rlpWordFull = BS . octetsFull 31  rlpAddrFull :: Addr -> RLP-rlpAddrFull = BS . octetsFull 19 . num+rlpAddrFull = BS . octetsFull 19 . into  rlpWord160 :: Addr -> RLP rlpWord160 0 = BS mempty

@@ -1,9 +1,5 @@-{-# Language DataKinds #-}-{-# Language GADTs #-}-{-# Language PolyKinds #-}-{-# Language ScopedTypeVariables #-}-{-# Language TypeApplications #-}-{-# Language QuasiQuotes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE QuasiQuotes #-}  {- |     Module: EVM.SMT@@ -15,32 +11,32 @@  import Control.Monad import Data.Containers.ListUtils (nubOrd)-import Language.SMT2.Parser (getValueRes, parseCommentFreeFileMsg)-import Language.SMT2.Syntax (Symbol, SpecConstant(..), GeneralRes(..), Term(..), QualIdentifier(..), Identifier(..), Sort(..), Index(..), VarBinding(..))-import Data.Word-import Numeric (readHex, readBin) import Data.ByteString (ByteString)--import qualified Data.ByteString as BS-import qualified Data.List as List+import Data.Bifunctor (second)+import Data.ByteString qualified as BS+import Data.List qualified as List import Data.List.NonEmpty (NonEmpty((:|)))-import qualified Data.List.NonEmpty as NonEmpty+import Data.List.NonEmpty qualified as NonEmpty import Data.String.Here import Data.Maybe (fromJust) import Data.Map (Map)-import qualified Data.Map as Map+import Data.Map qualified as Map+import Data.Word (Word8) import Data.Text.Lazy (Text)-import qualified Data.Text as TS-import qualified Data.Text.Lazy as T+import Data.Text qualified as TS+import Data.Text.Lazy qualified as T import Data.Text.Lazy.Builder-import Data.Bifunctor (second)+import Language.SMT2.Parser (getValueRes, parseCommentFreeFileMsg)+import Language.SMT2.Syntax (Symbol, SpecConstant(..), GeneralRes(..), Term(..), QualIdentifier(..), Identifier(..), Sort(..), Index(..), VarBinding(..))+import Numeric (readHex, readBin)+import Witch (into, unsafeInto) -import EVM.Types-import EVM.Traversals import EVM.CSE-import EVM.Keccak-import EVM.Expr (writeByte, bufLengthEnv, containsNode, bufLength, minLength)-import qualified EVM.Expr as Expr+import EVM.Expr (writeByte, bufLengthEnv, containsNode, bufLength, minLength, inRange)+import EVM.Expr qualified as Expr+import EVM.Keccak (keccakAssumptions)+import EVM.Traversals+import EVM.Types   -- ** Encoding ** ----------------------------------------------------------------------------------@@ -105,7 +101,7 @@   Just (ConcreteBuf b) -> Just $ Flat b   _ -> Nothing   where-    toBuf (Comp (Base b sz)) | sz <= 120_000_000 = Just . ConcreteBuf $ BS.replicate (num sz) b+    toBuf (Comp (Base b sz)) | sz <= 120_000_000 = Just . ConcreteBuf $ BS.replicate (unsafeInto sz) b     toBuf (Comp (Write b idx next)) = fmap (writeByte (Lit idx) (LitByte b)) (toBuf $ Comp next)     toBuf (Flat b) = Just . ConcreteBuf $ b     toBuf _ = Nothing@@ -205,39 +201,39 @@ referencedVars' :: Prop -> [Builder] referencedVars' prop = nubOrd $ foldProp referencedVarsGo [] prop -referencedFrameContextGo :: Expr a -> [Builder]+referencedFrameContextGo :: Expr a -> [(Builder, [Prop])] referencedFrameContextGo = \case-  CallValue a -> [fromLazyText $ T.append "callvalue_" (T.pack . show $ a)]-  Caller a -> [fromLazyText $ T.append "caller_" (T.pack . show $ a)]-  Address a -> [fromLazyText $ T.append "address_" (T.pack . show $ a)]-  Balance {} -> error "TODO: BALANCE"-  SelfBalance {} -> error "TODO: SELFBALANCE"-  Gas {} -> error "TODO: GAS"+  CallValue a -> [(fromLazyText $ T.append "callvalue_" (T.pack . show $ a), [])]+  Caller a -> [(fromLazyText $ T.append "caller_" (T.pack . show $ a), [inRange 160 (Caller a)])]+  Address a -> [(fromLazyText $ T.append "address_" (T.pack . show $ a), [inRange 160 (Address a)])]+  Balance {} -> internalError "TODO: BALANCE"+  SelfBalance {} -> internalError "TODO: SELFBALANCE"+  Gas {} -> internalError "TODO: GAS"   _ -> [] -referencedFrameContext :: Expr a -> [Builder]+referencedFrameContext :: Expr a -> [(Builder, [Prop])] referencedFrameContext expr = nubOrd $ foldExpr referencedFrameContextGo [] expr -referencedFrameContext' :: Prop -> [Builder]+referencedFrameContext' :: Prop -> [(Builder, [Prop])] referencedFrameContext' prop = nubOrd $ foldProp referencedFrameContextGo [] prop  -referencedBlockContextGo :: Expr a -> [Builder]+referencedBlockContextGo :: Expr a -> [(Builder, [Prop])] referencedBlockContextGo = \case-  Origin -> ["origin"]-  Coinbase -> ["coinbase"]-  Timestamp -> ["timestamp"]-  BlockNumber -> ["blocknumber"]-  PrevRandao -> ["prevrandao"]-  GasLimit -> ["gaslimit"]-  ChainId -> ["chainid"]-  BaseFee -> ["basefee"]+  Origin -> [("origin", [inRange 160 Origin])]+  Coinbase -> [("coinbase", [inRange 160 Coinbase])]+  Timestamp -> [("timestamp", [])]+  BlockNumber -> [("blocknumber", [])]+  PrevRandao -> [("prevrandao", [])]+  GasLimit -> [("gaslimit", [])]+  ChainId -> [("chainid", [])]+  BaseFee -> [("basefee", [])]   _ -> [] -referencedBlockContext :: Expr a -> [Builder]+referencedBlockContext :: Expr a -> [(Builder, [Prop])] referencedBlockContext expr = nubOrd $ foldExpr referencedBlockContextGo [] expr -referencedBlockContext' :: Prop -> [Builder]+referencedBlockContext' :: Prop -> [(Builder, [Prop])] referencedBlockContext' prop = nubOrd $ foldProp referencedBlockContextGo [] prop  -- | This function overapproximates the reads from the abstract@@ -276,15 +272,19 @@   where     assertRead :: (Expr EWord, Expr EWord, Expr Buf) -> [Prop]     assertRead (idx, Lit 32, buf) = [PImpl (PGEq idx (bufLength buf)) (PEq (ReadWord idx buf) (Lit 0))]-    assertRead (idx, Lit sz, buf) = fmap (\s -> PImpl (PGEq idx (bufLength buf)) (PEq (ReadByte idx buf) (LitByte (num s)))) [(0::Int)..num sz-1]-    assertRead (_, _, _) = error "Cannot generate assertions for accesses of symbolic size"+    assertRead (idx, Lit sz, buf) =+      fmap+        -- TODO: unsafeInto instead fromIntegral here makes symbolic tests fail+        (PImpl (PGEq idx (bufLength buf)) . PEq (ReadByte idx buf) . LitByte . fromIntegral)+        [(0::Int)..unsafeInto sz-1]+    assertRead (_, _, _) = internalError "Cannot generate assertions for accesses of symbolic size"      allReads = filter keepRead $ nubOrd $ findBufferAccess props <> findBufferAccess (Map.elems benv) <> findBufferAccess (Map.elems senv)      -- discard constraints if we can statically determine that read is less than the buffer length     keepRead (Lit idx, Lit size, buf) =       case minLength benv buf of-        Just l | num (idx + size) <= l -> False+        Just l | into (idx + size) <= l -> False         _ -> True     keepRead _ = True @@ -310,7 +310,7 @@     baseBuf (GVar (BufVar a)) =       case Map.lookup a benv of         Just b -> baseBuf b-        Nothing -> error "Internal error: could not find buffer variable"+        Nothing -> internalError "could not find buffer variable"     baseBuf (WriteByte _ _ b) = baseBuf b     baseBuf (WriteWord _ _ b) = baseBuf b     baseBuf (CopySlice _ _ _ _ dst)= baseBuf dst@@ -332,18 +332,20 @@     cexvars = (mempty :: CexVars){ calldata = fmap toLazyText names }  -declareFrameContext :: [Builder] -> SMT2-declareFrameContext names = SMT2 (["; frame context"] <> fmap declare names) cexvars+declareFrameContext :: [(Builder, [Prop])] -> SMT2+declareFrameContext names = SMT2 (["; frame context"] <> concatMap declare names) cexvars   where-    declare n = "(declare-const " <> n <> " (_ BitVec 256))"-    cexvars = (mempty :: CexVars){ txContext = fmap toLazyText names }+    declare (n,props) = [ "(declare-const " <> n <> " (_ BitVec 256))" ]+                        <> fmap (\p -> "(assert " <> propToSMT p <> ")") props+    cexvars = (mempty :: CexVars){ txContext = fmap (toLazyText . fst) names }  -declareBlockContext :: [Builder] -> SMT2-declareBlockContext names = SMT2 (["; block context"] <> fmap declare names) cexvars+declareBlockContext :: [(Builder, [Prop])] -> SMT2+declareBlockContext names = SMT2 (["; block context"] <> concatMap declare names) cexvars   where-    declare n = "(declare-const " <> n <> " (_ BitVec 256))"-    cexvars = (mempty :: CexVars){ blockContext = fmap toLazyText names }+    declare (n, props) = [ "(declare-const " <> n <> " (_ BitVec 256))" ]+                         <> fmap (\p -> "(assert " <> propToSMT p <> ")") props+    cexvars = (mempty :: CexVars){ blockContext = fmap (toLazyText . fst) names }   prelude :: SMT2@@ -566,7 +568,7 @@  exprToSMT :: Expr a -> Builder exprToSMT = \case-  Lit w -> fromLazyText $ "(_ bv" <> (T.pack $ show (num w :: Integer)) <> " 256)"+  Lit w -> fromLazyText $ "(_ bv" <> (T.pack $ show (into w :: Integer)) <> " 256)"   Var s -> fromText s   GVar (BufVar n) -> fromLazyText $ "buf" <> (T.pack . show $ n)   GVar (StoreVar n) -> fromLazyText $ "store" <> (T.pack . show $ n)@@ -586,7 +588,7 @@   Mul a b -> op2 "bvmul" a b   Exp a b -> case b of                Lit b' -> expandExp a b'-               _ -> error "cannot encode symbolic exponentation into SMT"+               _ -> internalError "cannot encode symbolic exponentation into SMT"   Min a b ->     let aenc = exprToSMT a         benc = exprToSMT b in@@ -674,12 +676,12 @@   ChainId -> "chainid"   BaseFee -> "basefee" -  LitByte b -> fromLazyText $ "(_ bv" <> T.pack (show (num b :: Integer)) <> " 8)"+  LitByte b -> fromLazyText $ "(_ bv" <> T.pack (show (into b :: Integer)) <> " 8)"   IndexWord idx w -> case idx of     Lit n -> if n >= 0 && n < 32              then                let enc = exprToSMT w in-               fromLazyText ("(indexWord" <> T.pack (show (num n :: Integer))) `sp` enc <> ")"+               fromLazyText ("(indexWord" <> T.pack (show (into n :: Integer))) `sp` enc <> ")"              else exprToSMT (LitByte 0)     _ -> op2 "indexWord" idx w   ReadByte idx src -> op2 "select" src idx@@ -714,7 +716,7 @@     "(sstore" `sp` encAddr `sp` encIdx `sp` encVal `sp` encPrev <> ")"   SLoad addr idx store -> op3 "sload" addr idx store -  a -> error $ "TODO: implement: " <> show a+  a -> internalError $ "TODO: implement: " <> show a   where     op1 op a =       let enc =  exprToSMT a in@@ -786,7 +788,7 @@         encSrcOff = exprToSMT (Expr.add srcOffset size')         child = copySlice srcOffset dstOffset size' src dst in     "(store " <> child `sp` encDstOff `sp` "(select " <> src `sp` encSrcOff <> "))"-copySlice _ _ _ _ _ = error "TODO: implement copySlice with a symbolically sized region"+copySlice _ _ _ _ _ = internalError "TODO: implement copySlice with a symbolically sized region"  -- | Unrolls an exponentiation into a series of multiplications expandExp :: Expr EWord -> W256 -> Builder@@ -820,7 +822,7 @@       then (idx + 1, inner)       else let           byteSMT = exprToSMT (LitByte byte)-          idxSMT = exprToSMT . Lit . num $ idx+          idxSMT = exprToSMT . Lit . unsafeInto $ idx         in (idx + 1, "(store " <> inner `sp` idxSMT `sp` byteSMT <> ")")  encodeConcreteStore :: Map W256 (Map W256 W256) -> Builder@@ -850,10 +852,10 @@ parseSC :: (Num a, Eq a) => SpecConstant -> a parseSC (SCHexadecimal a) = fst . head . Numeric.readHex . T.unpack . T.fromStrict $ a parseSC (SCBinary a) = fst . head . Numeric.readBin . T.unpack . T.fromStrict $ a-parseSC sc = error $ "Internal Error: cannot parse: " <> show sc+parseSC sc = internalError $ "cannot parse: " <> show sc  parseErr :: (Show a) => a -> b-parseErr res = error $ "Internal Error: cannot parse solver response: " <> show res+parseErr res = internalError $ "cannot parse solver response: " <> show res  parseVar :: TS.Text -> Expr EWord parseVar = Var@@ -867,14 +869,14 @@ parseBlockCtx "gaslimit" = GasLimit parseBlockCtx "chainid" = ChainId parseBlockCtx "basefee" = BaseFee-parseBlockCtx t = error $ "Internal Error: cannot parse " <> (TS.unpack t) <> " into an Expr"+parseBlockCtx t = internalError $ "cannot parse " <> (TS.unpack t) <> " into an Expr"  parseFrameCtx :: TS.Text -> Expr EWord parseFrameCtx name = case TS.unpack name of   ('c':'a':'l':'l':'v':'a':'l':'u':'e':'_':frame) -> CallValue (read frame)   ('c':'a':'l':'l':'e':'r':'_':frame) -> Caller (read frame)   ('a':'d':'d':'r':'e':'s':'s':'_':frame) -> Address (read frame)-  t -> error $ "Internal Error: cannot parse " <> t <> " into an Expr"+  t -> internalError $ "cannot parse " <> t <> " into an Expr"  getVars :: (TS.Text -> Expr EWord) -> (Text -> IO Text) -> [TS.Text] -> IO (Map (Expr EWord) W256) getVars parseFn getVal names = Map.mapKeys parseFn <$> foldM getOne mempty names@@ -892,7 +894,7 @@             TermSpecConstant sc)               -> if symbol == name                  then parseW256 sc-                 else error "Internal Error: solver did not return model for requested value"+                 else internalError "solver did not return model for requested value"           r -> parseErr r       pure $ Map.insert name val acc @@ -913,7 +915,7 @@           (TermQualIdentifier (Unqualified (IdSymbol symbol)), (TermSpecConstant sc))             -> if symbol == (T.toStrict $ name <> "_length")                then parseW256 sc-               else error "Internal Error: solver did not return model for requested value"+               else internalError "solver did not return model for requested value"           res -> parseErr res         res -> parseErr res @@ -927,9 +929,9 @@           (TermQualIdentifier (Unqualified (IdSymbol symbol)), term)             -> if (T.fromStrict symbol) == name                then pure $ parseBuf len term-               else error "Internal Error: solver did not return model for requested value"-          res -> error $ "Internal Error: cannot parse solver response: " <> show res-        res -> error $ "Internal Error: cannot parse solver response: " <> show res+               else internalError "solver did not return model for requested value"+          res -> internalError $ "cannot parse solver response: " <> show res+        res -> internalError $ "cannot parse solver response: " <> show res       pure $ Map.insert (AbstractBuf $ T.toStrict name) buf acc      parseBuf :: W256 -> Term -> BufModel@@ -966,7 +968,7 @@           -- looking up a bound name           (TermQualIdentifier (Unqualified (IdSymbol name))) -> case Map.lookup name env of             Just t -> t-            Nothing -> error $ "Internal error: could not find "+            Nothing -> internalError $ "could not find "                             <> (TS.unpack name)                             <> " in environment mapping"           p -> parseErr p@@ -982,7 +984,7 @@               (TermQualIdentifier (Unqualified (IdSymbol symbol)), term) ->                 if symbol == "abstractStore"                 then interpret2DArray Map.empty term-                else error "Internal Error: solver did not return model for requested value"+                else internalError "solver did not return model for requested value"               r -> parseErr r    -- then create a map by adding only the locations that are read by the program@@ -1009,7 +1011,7 @@     Right (ResSpecific (valParsed :| [])) ->       case valParsed of         (_, TermSpecConstant sc) -> pure $ parseW256 sc-        _ -> error $ "Internal Error: cannot parse model for: " <> show w+        _ -> internalError $ "cannot parse model for: " <> show w     r -> parseErr r  @@ -1022,7 +1024,7 @@   TermQualIdentifier (Unqualified (IdSymbol s)) ->     case Map.lookup s env of       Just t -> interpretNDArray interp env t-      Nothing -> error "Internal error: unknown identifier, cannot parse array"+      Nothing -> internalError "unknown identifier, cannot parse array"   -- (let (x t') t)   TermLet (VarBinding x t' :| []) t -> interpretNDArray interp (Map.insert x t' env) t   TermLet (VarBinding x t' :| lets) t -> interpretNDArray interp (Map.insert x t' env) (TermLet (NonEmpty.fromList lets) t)@@ -1032,7 +1034,7 @@   -- (store arr ind val)   TermApplication store (arr :| [TermSpecConstant ind, val]) | isStore store ->     \x -> if x == parseW256 ind then interp env val else interpretNDArray interp env arr x-  t -> error $ "Internal error: cannot parse array value. Unexpected term: " <> (show t)+  t -> internalError $ "cannot parse array value. Unexpected term: " <> (show t)    where     isArrConst :: QualIdentifier -> Bool@@ -1053,8 +1055,8 @@     interpretW256 env (TermQualIdentifier (Unqualified (IdSymbol s))) =       case Map.lookup s env of         Just t -> interpretW256 env t-        Nothing -> error "Internal error: unknown identifier, cannot parse array"-    interpretW256 _ t = error $ "Internal error: cannot parse array value. Unexpected term: " <> (show t)+        Nothing -> internalError "unknown identifier, cannot parse array"+    interpretW256 _ t = internalError $ "cannot parse array value. Unexpected term: " <> (show t)  -- | Interpret an 2-dimensional array as a function interpret2DArray :: (Map Symbol Term) -> Term -> (W256 -> W256 -> W256)

@@ -2,36 +2,36 @@ Module      : Helper functions to sign a transaction and derive address from Description :        for the EVM given a secret key -}- module EVM.Sign where -import qualified Crypto.Hash as Crypto+import Data.ByteString qualified as BS import Data.Maybe (fromMaybe)+import Data.Word+import Crypto.Hash qualified as Crypto import Crypto.PubKey.ECC.ECDSA (signDigestWith, PrivateKey(..), Signature(..)) import Crypto.PubKey.ECC.Types (getCurveByName, CurveName(..), Point(..)) import Crypto.PubKey.ECC.Generate (generateQ)+import Witch (unsafeInto)  import EVM.ABI (encodeAbiValue, AbiValue(..))-import qualified Data.ByteString   as BS import EVM.Types import EVM.Expr (exprToAddr) import EVM.Precompiled-import Data.Word - -- Given a secret key, generates the address deriveAddr :: Integer -> Maybe Addr-deriveAddr sk = case pubPoint of-           PointO -> Nothing-           Point x y ->-             -- See yellow paper #286-               let pub = BS.concat [ encodeInt x, encodeInt y ]-                   addr = Lit . W256 . word256 . BS.drop 12 . BS.take 32 . keccakBytes $ pub-                in exprToAddr addr-         where-          curve = getCurveByName SEC_p256k1-          pubPoint = generateQ curve (num sk)-          encodeInt = encodeAbiValue . AbiUInt 256 . fromInteger+deriveAddr sk =+  case pubPoint of+    PointO -> Nothing+    Point x y ->+      -- See yellow paper #286+      let pub = BS.concat [ encodeInt x, encodeInt y ]+          addr = Lit . W256 . word256 . BS.drop 12 . BS.take 32 . keccakBytes $ pub+      in exprToAddr addr+  where+    curve = getCurveByName SEC_p256k1+    pubPoint = generateQ curve sk+    encodeInt = encodeAbiValue . AbiUInt 256 . fromInteger  sign :: W256 -> Integer -> (Word8, W256, W256) sign hash sk = (v, r, s)@@ -40,13 +40,13 @@     curve = getCurveByName SEC_p256k1     priv = PrivateKey curve sk     digest = fromMaybe-      (error $ "Internal Error: could produce a digest from " <> show hash)+      (internalError $ "could produce a digest from " <> show hash)       (Crypto.digestFromByteString (word256Bytes hash))      -- sign message     sig = ethsign priv digest-    r = num $ sign_r sig-    s = num lowS+    r = unsafeInto $ sign_r sig+    s = unsafeInto lowS      -- this is a little bit sad, but cryptonite doesn't give us back a v value     -- so we compute it by guessing one, and then seeing if that gives us the right answer from ecrecover@@ -72,6 +72,5 @@        Just sig -> sig  ecrec :: W256 -> W256 -> W256 -> W256 -> Maybe Addr-ecrec v r s e = num . word <$> EVM.Precompiled.execute 1 input 32+ecrec v r s e = unsafeInto . word <$> EVM.Precompiled.execute 1 input 32   where input = BS.concat (word256Bytes <$> [e, v, r, s])-

@@ -1,8 +1,7 @@-{-# Language DeriveAnyClass #-}-{-# Language DerivingStrategies #-}-{-# Language GeneralisedNewtypeDeriving #-}-{-# Language DataKinds #-}-{-# Language QuasiQuotes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE QuasiQuotes #-}  module EVM.Solidity   ( solidity@@ -89,6 +88,7 @@ import System.IO.Temp import System.Process import Text.Read (readMaybe)+import Witch (unsafeInto)   data StorageItem = StorageItem@@ -121,12 +121,12 @@   readsPrec _ t@('m':'a':'p':'p':'i':'n':'g':'(':s) =     let (lhs,rhs) = case T.splitOn " => " (pack s) of           (l:r) -> (l,r)-          _ -> error $ "could not parse storage item: " <> t+          _ -> internalError $ "could not parse storage item: " <> t         first = fromJust $ parseTypeName mempty lhs         target = fromJust $ parseTypeName mempty (T.replace ")" "" (last rhs))         rest = fmap (fromJust . (parseTypeName mempty . (T.replace "mapping(" ""))) (take (length rhs - 1) rhs)     in [(StorageMapping (first NonEmpty.:| rest) target, "")]-  readsPrec _ s = [(StorageValue $ fromMaybe (error $ "could not parse storage item: " <> s) (parseTypeName mempty (pack s)),"")]+  readsPrec _ s = [(StorageValue $ fromMaybe (internalError $ "could not parse storage item: " <> s) (parseTypeName mempty (pack s)),"")]  data SolcContract = SolcContract   { runtimeCodehash  :: W256@@ -190,7 +190,7 @@   mempty = BuildOutput mempty mempty  -- | The various project types understood by hevm-data ProjectType = DappTools | Foundry+data ProjectType = DappTools | CombinedJSON | Foundry   deriving (Eq, Show, Read, ParseField)  data SourceCache = SourceCache@@ -286,7 +286,7 @@     go ';' (xs, F5 a b c j ds, _)              = let p' = SM a b c j (readR ds) in -- solc >=0.6                                                  (xs |> p', F1 [] 1, p') -    go c (xs, state, p)                        = (xs, error ("srcmap: y u " ++ show c ++ " in state" ++ show state ++ "?!?"), p)+    go c (xs, state, p)                        = (xs, internalError ("srcmap: y u " ++ show c ++ " in state" ++ show state ++ "?!?"), p)  -- | Reads all solc ouput json files found under the provided filepath and returns them merged into a BuildOutput readBuildOutput :: FilePath -> ProjectType -> IO (Either String BuildOutput)@@ -297,6 +297,13 @@     [x] -> readSolc DappTools root (outDir <> x)     [] -> pure . Left $ "no json files found in: " <> outDir     _ -> pure . Left $ "multiple json files found in: " <> outDir+readBuildOutput root CombinedJSON = do+  let outDir = root <> "/out/"+  jsons <- findJsonFiles outDir+  case jsons of+    [x] -> readSolc CombinedJSON root (outDir <> x)+    [] -> pure . Left $ "no json files found in: " <> outDir+    _ -> pure . Left $ "multiple json files found in: " <> outDir readBuildOutput root Foundry = do   let outDir = root <> "/out/"   jsons <- findJsonFiles (root <> "/out")@@ -318,11 +325,11 @@ makeSourceCache root (Sources sources) (Asts asts) = do   files <- Map.fromList <$> forM (Map.toList sources) (\x@(SrcFile id' fp, _) -> do       contents <- case x of-        (_,  Just content) -> return content+        (_,  Just content) -> pure content         (SrcFile _ _, Nothing) -> BS.readFile (root <> "/" <> fp)       pure (id', (fp, contents))     )-  return $! SourceCache+  pure $! SourceCache     { files = files     , lines = fmap (Vector.fromList . BS.split 0xa . snd) files     , asts  = asts@@ -347,7 +354,7 @@       Nothing -> pure . Left $ "unable to parse: " <> fp       Just (contracts, asts, sources) -> do         sourceCache <- makeSourceCache root sources asts-        return (Right (BuildOutput contracts sourceCache))+        pure (Right (BuildOutput contracts sourceCache))  yul :: Text -> Text -> IO (Maybe ByteString) yul contract src = do@@ -382,14 +389,15 @@   (json, path) <- solidity' ("contract ABI { function " <> f <> " public {}}")   let (Contracts sol, _, _) = fromJust $ readStdJSON json   case Map.toList $ (fromJust (Map.lookup (path <> ":ABI") sol)).abiMap of-     [(_,b)] -> return b-     _ -> error "hevm internal error: unexpected abi format"+     [(_,b)] -> pure b+     _ -> internalError "unexpected abi format"  force :: String -> Maybe a -> a-force s = fromMaybe (error s)+force s = fromMaybe (internalError s)  readJSON :: ProjectType -> Text -> Text -> Maybe (Contracts, Asts, Sources) readJSON DappTools _ json = readStdJSON json+readJSON CombinedJSON _ json = readCombinedJSON json readJSON Foundry contractName json = readFoundryJSON contractName json  -- | Reads a foundry json output@@ -408,7 +416,7 @@    abi <- toList <$> json ^? key "abi" % _Array -  id' <- num <$> json ^? key "id" % _Integer+  id' <- unsafeInto <$> json ^? key "id" % _Integer    let contract = SolcContract         { runtimeCodehash     = keccak' (stripBytecodeMetadata runtimeCode)@@ -425,7 +433,7 @@         , storageLayout       = mempty -- TODO: foundry doesn't expose this?         , immutableReferences = mempty -- TODO: foundry doesn't expose this?         }-  return ( Contracts $ Map.singleton (path <> ":" <> contractName) contract+  pure ( Contracts $ Map.singleton (path <> ":" <> contractName) contract          , Asts      $ Map.singleton path ast          , Sources   $ Map.singleton (SrcFile id' (T.unpack path)) Nothing          )@@ -438,16 +446,16 @@   sources <- KeyMap.toHashMapText <$>  json ^? key "sources" % _Object   let asts = force "JSON lacks abstract syntax trees." . preview (key "ast") <$> sources       contractMap = f contracts-      getId src = num $ (force "" $ HMap.lookup src sources) ^?! key "id" % _Integer+      getId src = unsafeInto $ (force "" $ HMap.lookup src sources) ^?! key "id" % _Integer       contents src = (SrcFile (getId src) (T.unpack src), encodeUtf8 <$> HMap.lookup src (mconcat $ Map.elems $ snd <$> contractMap))-  return ( Contracts $ fst <$> contractMap+  pure ( Contracts $ fst <$> contractMap          , Asts      $ Map.fromList (HMap.toList asts)          , Sources   $ Map.fromList $ contents <$> (sort $ HMap.keys sources)          )   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 (KeyMap.toHashMapText (fromMaybe (error "Could not parse json object") (preview _Object x)))+    g (s, x) = h s <$> HMap.toList (KeyMap.toHashMapText (fromMaybe (internalError "Could not parse json object") (preview _Object x)))     h :: Text -> (Text, Value) -> (Text, (SolcContract, HMap.HashMap Text Text))     h s (c, x) =       let@@ -459,8 +467,8 @@         srcContents :: Maybe (HMap.HashMap Text Text)         srcContents = do metadata <- x ^? key "metadata" % _String                          srcs <- KeyMap.toHashMapText <$> metadata ^? key "sources" % _Object-                         return $ fmap-                           (fromMaybe (error "Internal Error: could not parse contents field into a string") . preview (key "content" % _String))+                         pure $ fmap+                           (fromMaybe (internalError "could not parse contents field into a string") . preview (key "content" % _String))                            (HMap.filter (isJust . preview (key "content")) srcs)         abis = force ("abi key not found in " <> show x) $           toList <$> x ^? key "abi" % _Array@@ -469,8 +477,8 @@         creationCode     = theCreationCode,         runtimeCodehash  = keccak' (stripBytecodeMetadata theRuntimeCode),         creationCodehash = keccak' (stripBytecodeMetadata theCreationCode),-        runtimeSrcmap    = force "internal error: srcmap-runtime" (makeSrcMaps (runtime ^?! key "sourceMap" % _String)),-        creationSrcmap   = force "internal error: srcmap" (makeSrcMaps (creation ^?! key "sourceMap" % _String)),+        runtimeSrcmap    = force "srcmap-runtime" (makeSrcMaps (runtime ^?! key "sourceMap" % _String)),+        creationSrcmap   = force "srcmap" (makeSrcMaps (creation ^?! key "sourceMap" % _String)),         contractName = s <> ":" <> c,         constructorInputs = mkConstructor abis,         abiMap        = mkAbiMap abis,@@ -480,10 +488,47 @@         immutableReferences = fromMaybe mempty $           do x' <- runtime ^? key "immutableReferences"              case fromJSON x' of-               Success a -> return a+               Success a -> pure a                _ -> Nothing       }, fromMaybe mempty srcContents)) +-- deprecate me soon+readCombinedJSON :: Text -> Maybe (Contracts, Asts, Sources)+readCombinedJSON json = do+  contracts <- f . KeyMap.toHashMapText <$> (json ^? key "contracts" % _Object)+  sources <- toList . fmap (preview _String) <$> json ^? key "sourceList" % _Array+  pure ( Contracts contracts+       , Asts (Map.fromList (HMap.toList asts))+       , Sources $ Map.fromList $+           (\(path, id') -> (SrcFile id' (T.unpack path), Nothing)) <$>+             zip (catMaybes sources) [0..]+       )+  where+    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+        theRuntimeCode = toCode (x ^?! key "bin-runtime" % _String)+        theCreationCode = toCode (x ^?! key "bin" % _String)+        abis = toList $ case (x ^?! key "abi") ^? _Array of+                 Just v -> v                                       -- solc >= 0.8+                 Nothing -> (x ^?! key "abi" % _String) ^?! _Array -- solc <  0.8+      in SolcContract {+        runtimeCode      = theRuntimeCode,+        creationCode     = theCreationCode,+        runtimeCodehash  = keccak' (stripBytecodeMetadata theRuntimeCode),+        creationCodehash = keccak' (stripBytecodeMetadata theCreationCode),+        runtimeSrcmap    = force "internal error: srcmap-runtime" (makeSrcMaps (x ^?! key "srcmap-runtime" % _String)),+        creationSrcmap   = force "internal error: srcmap" (makeSrcMaps (x ^?! key "srcmap" % _String)),+        contractName = s,+        constructorInputs = mkConstructor abis,+        abiMap       = mkAbiMap abis,+        eventMap     = mkEventMap abis,+        errorMap     = mkErrorMap abis,+        storageLayout = mkStorageLayout $ x ^? key "storage-layout",+        immutableReferences = mempty -- TODO: deprecate combined-json+      }+ mkAbiMap :: [Value] -> Map FunctionSelector Method mkAbiMap abis = Map.fromList $   let@@ -514,7 +559,7 @@          False -> NotAnonymous)        (map (\y ->         ( y ^?! key "name" % _String-        , force "internal error: type" (parseTypeName' y)+        , force "type" (parseTypeName' y)         , if y ^?! key "indexed" % _Bool           then Indexed           else NotIndexed@@ -548,7 +593,7 @@     case filter isConstructor abis of       [abi] -> map parseMethodInput (toList (abi ^?! key "inputs" % _Array))       [] -> [] -- default constructor has zero inputs-      _  -> error "strange: contract has multiple constructors"+      _  -> internalError "strange: contract has multiple constructors"  mkStorageLayout :: Maybe Value -> Maybe (Map Text StorageItem) mkStorageLayout Nothing = Nothing@@ -561,7 +606,7 @@        slot <- item ^? key "slot" % _String        typ <- Key.fromText <$> item ^? key "type" % _String        slotType <- types ^?! key typ ^? key "label" % _String-       return (name, StorageItem (read $ T.unpack slotType) offset (read $ T.unpack slot)))+       pure (name, StorageItem (read $ T.unpack slotType) offset (read $ T.unpack slot)))  signature :: AsValue s => s -> Text signature abi =@@ -589,13 +634,13 @@ parseMutability "pure" = Pure parseMutability "nonpayable" = NonPayable parseMutability "payable" = Payable-parseMutability _ = error "unknown function mutability"+parseMutability _ = internalError "unknown function mutability"  -- This actually can also parse a method output! :O parseMethodInput :: AsValue s => s -> (Text, AbiType) parseMethodInput x =   ( x ^?! key "name" % _String-  , force "internal error: method type" (parseTypeName' x)+  , force "method type" (parseTypeName' x)   )  containsLinkerHole :: Text -> Bool@@ -605,7 +650,7 @@ toCode t = case BS16.decodeBase16 (encodeUtf8 t) of   Right d -> d   Left e -> if containsLinkerHole t-            then error "unlinked libraries detected in bytecode"+            then error "Error: unlinked libraries detected in bytecode"             else error $ T.unpack e  solidity' :: Text -> IO (Text, Text)@@ -652,7 +697,7 @@       "solc"       ["--allow-paths", path, "--standard-json", (path <> ".json")]       ""-  return (x, pack path)+  pure (x, pack path)  yul' :: Text -> IO (Text, Text) yul' src = withSystemTempFile "hevm.yul" $ \path handle -> do@@ -671,7 +716,7 @@       "solc"       ["--allow-paths", path, "--standard-json", (path <> ".json")]       ""-  return (x, pack path)+  pure (x, pack path)  solc :: Language -> Text -> IO Text solc lang src =@@ -794,7 +839,7 @@         (\v -> do           src <- preview (key "src" % _String) v           [i, n, f] <- mapM (readMaybe . T.unpack) (T.split (== ':') src)-          return ((i, n, f), v)+          pure ((i, n, f), v)         )       . Map.elems       $ astIds

@@ -1,8 +1,3 @@-{-# Language DataKinds #-}-{-# Language GADTs #-}-{-# Language PolyKinds #-}-{-# Language ScopedTypeVariables #-}- {- |     Module: EVM.Solvers     Description: Solver orchestration@@ -12,25 +7,25 @@ import Prelude hiding (LT, GT)  import GHC.Natural-import Control.Monad import GHC.IO.Handle (Handle, hFlush, hSetBuffering, BufferMode(..)) import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan) import Control.Concurrent (forkIO, killThread)+import Control.Monad import Control.Monad.State.Strict import Data.Char (isSpace)+import Data.Map (Map)+import Data.Map qualified as Map import Data.Maybe (fromMaybe)-+import Data.Text qualified as TS import Data.Text.Lazy (Text)-import Data.Map (Map)-import qualified Data.Map as Map-import qualified Data.Text as TS-import qualified Data.Text.Lazy as T-import qualified Data.Text.Lazy.IO as T+import Data.Text.Lazy qualified as T+import Data.Text.Lazy.IO qualified as T import Data.Text.Lazy.Builder import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..))+import Witch (into)  import EVM.SMT-import EVM.Types hiding (Unknown)+import EVM.Types (W256, Expr(AbstractBuf), internalError)  -- | Supported solvers data Solver@@ -88,10 +83,8 @@ checkSat (SolverGroup taskQueue) script = do   -- prepare result channel   resChan <- newChan-   -- send task to solver group   writeChan taskQueue (Task script resChan)-   -- collect result   readChan resChan @@ -99,7 +92,6 @@ withSolvers solver count timeout cont = do   -- spawn solvers   instances <- mapM (const $ spawnSolver solver timeout) [1..count]-   -- spawn orchestration thread   taskQueue <- newChan   availableInstances <- newChan@@ -176,10 +168,10 @@         AbstractBuf b -> do           let name = T.fromStrict b               hint = fromMaybe-                       (error $ "Internal Error: Could not find hint for buffer: " <> T.unpack name)+                       (internalError $ "Could not find hint for buffer: " <> T.unpack name)                        (Map.lookup name hints)           shrinkBuf name hint-        _ -> error "Internal Error: Received model from solver for non AbstractBuf"+        _ -> internalError "Received model from solver for non AbstractBuf"      -- starting with some guess at the max useful size for a buffer, cap     -- it's size to that value, and ask the solver to check satisfiability. If@@ -188,7 +180,7 @@     -- and try again.     shrinkBuf :: Text -> W256 -> StateT SMTCex IO ()     shrinkBuf buf hint = do-      let encBound = "(_ bv" <> (T.pack $ show (num hint :: Integer)) <> " 256)"+      let encBound = "(_ bv" <> (T.pack $ show (into hint :: Integer)) <> " 256)"       sat <- liftIO $ do         sendLine' inst "(push)"         sendLine' inst $ "(assert (bvule " <> buf <> "_length " <> encBound <> "))"@@ -200,12 +192,12 @@         "unsat" -> do           liftIO $ sendLine' inst "(pop)"           shrinkBuf buf (if hint == 0 then hint + 1 else hint * 2)-        _ -> error "TODO: HANDLE ERRORS"+        _ -> internalError "SMT solver returned unexpected result (neither sat/unsat), which HEVM currently cannot handle"      -- Collapses the abstract description of a models buffers down to a bytestring     mkConcrete :: SMTCex -> SMTCex     mkConcrete c = fromMaybe-      (error $ "Internal Error: counterexample contains buffers that are too large to be represented as a ByteString: " <> show c)+      (internalError $ "counterexample contains buffers that are too large to be represented as a ByteString: " <> show c)       (flattenBufs c)      -- we set a pretty arbitrary upper limit (of 1024) to decide if we need to do some shrinking@@ -226,12 +218,11 @@ -- | Arguments used when spawing a solver instance solverArgs :: Solver -> Maybe Natural -> [Text] solverArgs solver timeout = case solver of-  Bitwuzla -> error "TODO: Bitwuzla args"+  Bitwuzla -> internalError "TODO: Bitwuzla args"   Z3 ->     [ "-in" ]   CVC5 ->     [ "--lang=smt"-    , "--no-interactive"     , "--produce-models"     , "--tlimit-per=" <> mkTimeout timeout     ]@@ -257,7 +248,7 @@ -- | Sends a list of commands to the solver. Returns the first error, if there was one. sendScript :: SolverInstance -> SMT2 -> IO (Either Text ()) sendScript solver (SMT2 cmds _) = do-  sendLine' solver (T.unlines $ fmap toLazyText cmds)+  sendLine' solver (splitSExpr $ fmap toLazyText cmds)   pure $ Right()  -- | Sends a single command to the solver, returns the first available line from the output buffer@@ -308,3 +299,37 @@       if (ls + ls') == (rs + rs')          then pure $ line : prev          else go (ls + ls') (rs + rs') (line : prev)++-- From a list of lines, take each separate SExpression and put it in+-- its own list, after removing comments.+splitSExpr :: [Text] -> Text+splitSExpr ls =+  -- split lines, strip comments, and append everything to a single line+  let text = T.intercalate " " $ T.takeWhile (/= ';') <$> concatMap T.lines ls in+  T.unlines $ filter (/= "") $ go text []+  where+    go "" acc = reverse acc+    go text acc =+      let (sexpr, text') = getSExpr text in+      let (sexpr', rest) = T.breakOnEnd ")" sexpr in+      go text' ((T.strip rest):(T.strip sexpr'):acc)++data Par = LPar | RPar++-- take the first SExpression and return the rest of the text+getSExpr :: Text -> (Text, Text)+getSExpr l = go LPar l 0 []+  where+    go _ text 0 prev@(_:_) = (T.intercalate "" (reverse prev), text)+    go _ _ r _ | r < 0 = internalError "Unbalanced SExpression"+    go _ "" _ _  = internalError "Unbalanced SExpression"+    -- find the next left parenthesis+    go LPar line r prev = -- r is how many right parentheses we are missing+      let (before, after) = T.breakOn "(" line in+      let rp = T.length $ T.filter (== ')') before in+      go RPar after (r - rp) (if before == "" then prev else before : prev)+    -- find the next right parenthesis+    go RPar line r prev =+      let (before, after) = T.breakOn ")" line in+      let lp = T.length $ T.filter (== '(') before in+      go LPar after (r + lp) (if before == "" then prev else before : prev)

@@ -1,4 +1,4 @@-{-# Language DataKinds #-}+{-# LANGUAGE DataKinds #-}  module EVM.Stepper   ( Action (..)@@ -26,12 +26,11 @@ import Control.Monad.Operational (Program, ProgramViewT(..), ProgramView, singleton, view) import Control.Monad.State.Strict (StateT, execState, runState, runStateT) import Data.Text (Text)-import EVM.Types -import qualified EVM--import qualified EVM.Fetch as Fetch+import EVM qualified import EVM.Exec qualified+import EVM.Fetch qualified as Fetch+import EVM.Types  -- | The instruction type of the operational monad data Action a where@@ -90,14 +89,14 @@     VMSuccess x ->       pure (Right x)     Unfinished x-      -> error $ "Internal Error: partial execution encountered during concrete execution: " <> show x+      -> internalError $ "partial execution encountered during concrete execution: " <> show x  -- | Run the VM until its final state runFully :: Stepper VM runFully = do   vm <- run   case vm.result of-    Nothing -> error "should not occur"+    Nothing -> internalError "should not occur"     Just (HandleEffect (Query q)) ->       wait q >> runFully     Just (HandleEffect (Choose q)) ->@@ -136,7 +135,7 @@           let vm' = execState m vm           interpret fetcher vm' (k ())         Ask _ ->-          error "cannot make choices with this interpreter"+          internalError "cannot make choices with this interpreter"         IOAct m -> do           (r, vm') <- runStateT m vm           interpret fetcher vm' (k r)

@@ -15,6 +15,7 @@ import Data.Maybe (fromMaybe, isJust) import Data.Sequence qualified as Seq import Data.Text (Text, unpack, pack, words)+import EVM.Types (internalError)  import Prelude hiding (words) @@ -52,11 +53,11 @@       Just ((reverse . toList) -> linearizedBaseContracts) ->         flip concatMap linearizedBaseContracts           (\case-             Number i -> fromMaybe (error "malformed AST JSON") $+             Number i -> fromMaybe (internalError "malformed AST JSON") $                storageVariablesForContract =<<                  Map.lookup (floor i) dapp.astIdMap              _ ->-               error "malformed AST JSON")+               internalError "malformed AST JSON")  storageVariablesForContract :: Value -> Maybe [Text] storageVariablesForContract node = do@@ -77,7 +78,7 @@             , pack $ show (slotTypeForDeclaration x)             ]         Nothing ->-          error "malformed variable declaration"+          internalError "malformed variable declaration"  nodeIs :: Text -> Value -> Bool nodeIs t x = isSourceNode && hasRightName@@ -98,7 +99,7 @@     Just (x:_) ->       grokDeclarationType x     _ ->-      error "malformed AST"+      internalError "malformed AST"  grokDeclarationType :: Value -> SlotType grokDeclarationType x =@@ -108,11 +109,11 @@         Just (toList -> xs) ->           grokMappingType xs         _ ->-          error "malformed AST"+          internalError "malformed AST"     Just _ ->       StorageValue (grokValueType x)     _ ->-      error ("malformed AST " ++ show x)+      internalError ("malformed AST " ++ show x)  grokMappingType :: [Value] -> SlotType grokMappingType [s, t] =@@ -122,9 +123,9 @@     (StorageValue s', StorageValue t') ->       StorageMapping (pure s') t'     (StorageMapping _ _, _) ->-      error "unexpected mapping as mapping key"+      internalError "unexpected mapping as mapping key" grokMappingType _ =-  error "unexpected AST child count for mapping"+  internalError "unexpected AST child count for mapping"  grokValueType :: Value -> AbiType grokValueType x =@@ -133,7 +134,7 @@        , preview (key "attributes" % key "type" % _String) x        ) of     (Just "ElementaryTypeName", _, Just typeName) ->-      fromMaybe (error ("ungrokked value type: " ++ show typeName))+      fromMaybe (internalError $ "ungrokked value type: " ++ show typeName)         (parseTypeName mempty (head (words typeName)))     (Just "UserDefinedTypeName", _, _) ->       AbiAddressType@@ -146,6 +147,6 @@         (Just "Literal", Just ((read . unpack) -> i)) ->           AbiArrayType i (grokValueType t)         _ ->-          error "malformed AST"+          internalError "malformed AST"     _ ->-      error ("unknown value type " ++ show x)+      internalError ("unknown value type " ++ show x)

@@ -1,52 +1,52 @@-{-# Language TupleSections #-}-{-# Language DeriveAnyClass #-}-{-# Language DataKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}  module EVM.SymExec where -import Prelude hiding (Word)-+import Control.Concurrent.Async (concurrently, mapConcurrently)+import Control.Concurrent.Spawn (parMapIO, pool)+import Control.Concurrent.STM (atomically, TVar, readTVarIO, readTVar, newTVarIO, writeTVar)+import Control.Monad.Operational qualified as Operational+import Control.Monad.State.Strict+import Data.Bifunctor (second)+import Data.ByteString (ByteString)+import Data.ByteString qualified as BS+import Data.Containers.ListUtils (nubOrd)+import Data.DoubleWord (Word256)+import Data.List (foldl', sortBy)+import Data.Maybe (fromMaybe, mapMaybe)+import Data.Map (Map)+import Data.Map qualified as Map+import Data.Set (Set, isSubsetOf, size)+import Data.Set qualified as Set+import Data.Text (Text)+import Data.Text qualified as T+import Data.Text.IO qualified as T+import Data.Text.Lazy qualified as TL+import Data.Text.Lazy.IO qualified as TL+import Data.Tree.Zipper qualified as Zipper import Data.Tuple (swap)-import Optics.Core-import EVM hiding (push, bytecode, query, wrap)+import EVM (makeVm, initialContract, getCodeLocation, isValidJumpDest) import EVM.Exec-import qualified EVM.Fetch as Fetch+import EVM.Fetch qualified as Fetch import EVM.ABI+import EVM.Expr qualified as Expr+import EVM.Format (formatExpr, formatPartial) import EVM.SMT (SMTCex(..), SMT2(..), assertProps, formatSMT2)-import qualified EVM.SMT as SMT+import EVM.SMT qualified as SMT import EVM.Solvers-import EVM.Traversals-import qualified EVM.Expr as Expr import EVM.Stepper (Stepper)-import qualified EVM.Stepper as Stepper-import qualified Control.Monad.Operational as Operational-import Control.Monad.State.Strict hiding (state)+import EVM.Stepper qualified as Stepper+import EVM.Traversals import EVM.Types import EVM.Concrete (createAddress)-import qualified EVM.FeeSchedule as FeeSchedule-import Data.DoubleWord (Word256)-import Control.Concurrent.Async-import Data.Maybe-import Data.Containers.ListUtils-import Data.List (foldl', sortBy)-import Data.ByteString (ByteString)-import qualified Data.ByteString as BS-import Data.Bifunctor (second)-import Data.Map (Map)-import qualified Data.Map as Map-import qualified Data.Text as T-import qualified Data.Text.IO as T-import qualified Data.Text.Lazy as TL-import qualified Data.Text.Lazy.IO as TL-import EVM.Format (formatExpr, formatPartial)-import Data.Set (Set, isSubsetOf, size)-import qualified Data.Set as Set-import Control.Concurrent.Spawn (parMapIO, pool)-import Control.Concurrent.STM (atomically, TVar, readTVarIO, readTVar, newTVarIO, writeTVar)-import GHC.Conc (getNumProcessors)+import EVM.FeeSchedule qualified as FeeSchedule import EVM.Format (indent, formatBinary)-import Options.Generic as Options-+import GHC.Conc (getNumProcessors)+import GHC.Generics (Generic)+import Optics.Core+import Options.Generic (ParseField, ParseFields, ParseRecord)+import Witch (into, unsafeInto)  -- | A method name, and the (ordered) types of it's arguments data Sig = Sig Text [AbiType]@@ -103,9 +103,6 @@ extractCex (Cex c) = Just c extractCex _ = Nothing -inRange :: Int -> Expr EWord -> Prop-inRange sz e = PAnd (PGEq e (Lit 0)) (PLEq e (Lit $ 2 ^ sz - 1))- bool :: Expr EWord -> Prop bool e = POr (PEq e (Lit 1)) (PEq e (Lit 0)) @@ -114,22 +111,22 @@ symAbiArg name = \case   AbiUIntType n ->     if n `mod` 8 == 0 && n <= 256-    then let v = Var name in St [inRange n v] v-    else error "bad type"+    then let v = Var name in St [Expr.inRange n v] v+    else internalError "bad type"   AbiIntType n ->     if n `mod` 8 == 0 && n <= 256     -- TODO: is this correct?-    then let v = Var name in St [inRange n v] v-    else error "bad type"+    then let v = Var name in St [Expr.inRange n v] v+    else internalError "bad type"   AbiBoolType -> let v = Var name in St [bool v] v-  AbiAddressType -> let v = Var name in St [inRange 160 v] v+  AbiAddressType -> let v = Var name in St [Expr.inRange 160 v] v   AbiBytesType n ->     if n > 0 && n <= 32-    then let v = Var name in St [inRange (n * 8) v] v-    else error "bad type"+    then let v = Var name in St [Expr.inRange (n * 8) v] v+    else internalError "bad type"   AbiArrayType sz tp ->     Comp $ fmap (\n -> symAbiArg (name <> n) tp) [T.pack (show n) | n <- [0..sz-1]]-  t -> error $ "TODO: symbolic abi encoding for " <> show t+  t -> internalError $ "TODO: symbolic abi encoding for " <> show t  data CalldataFragment   = St [Prop] (Expr EWord)@@ -149,11 +146,11 @@     mkArg typ "<symbolic>" n = symAbiArg (T.pack $ "arg" <> show n) typ     mkArg typ arg _ =       case makeAbiValue typ arg of-        AbiUInt _ w -> St [] . Lit . num $ w-        AbiInt _ w -> St [] . Lit . num $ w-        AbiAddress w -> St [] . Lit . num $ w+        AbiUInt _ w -> St [] . Lit . into $ w+        AbiInt _ w -> St [] . Lit . unsafeInto $ w+        AbiAddress w -> St [] . Lit . into $ w         AbiBool w -> St [] . Lit $ if w then 1 else 0-        _ -> error "TODO"+        _ -> internalError "TODO"     calldatas = zipWith3 mkArg typesignature args [1..]     (cdBuf, props) = combineFragments calldatas base     withSelector = writeSelector cdBuf sig@@ -169,7 +166,7 @@       [] -> acc       (hd:tl) -> case hd of                    St _ _ -> go (Expr.add acc (Lit 32)) tl-                   _ -> error "unsupported"+                   _ -> internalError "unsupported"  writeSelector :: Expr Buf -> Text -> Expr Buf writeSelector buf sig =@@ -186,7 +183,7 @@     go idx (f:rest) (buf, ps) =       case f of         St p w -> go (Expr.add idx (Lit 32)) rest (Expr.writeWord idx w buf, p <> ps)-        s -> error $ "unsupported cd fragment: " <> show s+        s -> internalError $ "unsupported cd fragment: " <> show s   abstractVM@@ -277,7 +274,6 @@            in interpret fetcher maxIter askSmtIters heuristic vma (k ra))           (let (rb, vmb) = runState (continue False) vm { result = Nothing }            in interpret fetcher maxIter askSmtIters heuristic vmb (k rb))-         pure $ ITE cond a b       Stepper.Wait q -> do         let performQuery = do@@ -294,7 +290,7 @@                 case (maxIterationsReached vm maxIter, isLoopHead heuristic vm) of                   -- Yes. return a partial leaf                   (Just _, Just True) ->-                    pure $ Partial vm.keccakEqs $ MaxIterationsReached vm.state.pc vm.state.contract+                    pure $ Partial vm.keccakEqs (Traces (Zipper.toForest vm.traces) vm.env.contracts) $ MaxIterationsReached vm.state.pc vm.state.contract                   -- No. keep executing                   _ ->                     let (r, vm') = runState (continue (Case (c > 0))) vm@@ -310,7 +306,7 @@                     -- got us to this point and return a partial leaf for the other side                     let (r, vm') = runState (continue (Case $ not n)) vm                     a <- interpret fetcher maxIter askSmtIters heuristic vm' (k r)-                    pure $ ITE cond a (Partial vm.keccakEqs (MaxIterationsReached vm.state.pc vm.state.contract))+                    pure $ ITE cond a (Partial vm.keccakEqs (Traces (Zipper.toForest vm.traces) vm.env.contracts) (MaxIterationsReached vm.state.pc vm.state.contract))                   -- we're in a loop and askSmtIters has been reached                   (Just True, True, _) ->                     -- ask the smt solver about the loop condition@@ -331,7 +327,7 @@ maxIterationsReached vm (Just maxIter) =   let codelocation = getCodeLocation vm       (iters, _) = view (at codelocation % non (0, [])) vm.iterations-  in if num maxIter <= iters+  in if unsafeInto maxIter <= iters      then Map.lookup (codelocation, iters - 1) vm.cache.path      else Nothing @@ -339,7 +335,7 @@ askSmtItersReached vm askSmtIters = let     codelocation = getCodeLocation vm     (iters, _) = view (at codelocation % non (0, [])) vm.iterations-  in askSmtIters <= num iters+  in askSmtIters <= into iters  {- | Loop head detection heuristic @@ -354,7 +350,7 @@ isLoopHead StackBased vm = let     loc = getCodeLocation vm     oldIters = Map.lookup loc vm.iterations-    isValid (Lit wrd) = wrd <= num (maxBound :: Int) && isValidJumpDest vm (num wrd)+    isValid (Lit wrd) = wrd <= unsafeInto (maxBound :: Int) && isValidJumpDest vm (unsafeInto wrd)     isValid _ = False   in case oldIters of        Just (_, oldStack) -> Just $ filter isValid oldStack == filter isValid vm.state.stack@@ -395,8 +391,8 @@ -} checkAssertions :: [Word256] -> Postcondition checkAssertions errs _ = \case-  Failure _ (Revert (ConcreteBuf msg)) -> PBool $ msg `notElem` (fmap panicMsg errs)-  Failure _ (Revert b) -> foldl' PAnd (PBool True) (fmap (PNeg . PEq b . ConcreteBuf . panicMsg) errs)+  Failure _ _ (Revert (ConcreteBuf msg)) -> PBool $ msg `notElem` (fmap panicMsg errs)+  Failure _ _ (Revert b) -> foldl' PAnd (PBool True) (fmap (PNeg . PEq b . ConcreteBuf . panicMsg) errs)   _ -> PBool True  -- | By default hevm only checks for user-defined assertions@@ -444,10 +440,10 @@   vm <- Stepper.runFully   let asserts = vm.keccakEqs <> vm.constraints   pure $ case vm.result of-    Just (VMSuccess buf) -> Success asserts buf vm.env.storage-    Just (VMFailure e) -> Failure asserts e-    Just (Unfinished p) -> Partial asserts p-    _ -> error "Internal Error: vm in intermediate state after call to runFully"+    Just (VMSuccess buf) -> Success asserts (Traces (Zipper.toForest vm.traces) vm.env.contracts) buf vm.env.storage+    Just (VMFailure e) -> Failure asserts (Traces (Zipper.toForest vm.traces) vm.env.contracts) e+    Just (Unfinished p) -> Partial asserts (Traces (Zipper.toForest vm.traces) vm.env.contracts) p+    _ -> internalError "vm in intermediate state after call to runFully"  -- | Converts a given top level expr into a list of final states and the -- associated path conditions for each state.@@ -457,10 +453,10 @@     go :: [Prop] -> Expr End -> [Expr End]     go pcs = \case       ITE c t f -> go (PNeg ((PEq c (Lit 0))) : pcs) t <> go (PEq c (Lit 0) : pcs) f-      Success ps msg store -> [Success (ps <> pcs) msg store]-      Failure ps e -> [Failure (ps <> pcs) e]-      Partial ps p -> [Partial (ps <> pcs) p]-      GVar _ -> error "cannot flatten an Expr containing a GVar"+      Success ps trace msg store -> [Success (ps <> pcs) trace msg store]+      Failure ps trace e -> [Failure (ps <> pcs) trace e]+      Partial ps trace p -> [Partial (ps <> pcs) trace p]+      GVar _ -> internalError "cannot flatten an Expr containing a GVar"  -- | Strips unreachable branches from a given expr -- Returns a list of executed SMT queries alongside the reduced expression for debugging purposes@@ -474,7 +470,7 @@ reachable :: SolverGroup -> Expr End -> IO ([SMT2], Expr End) reachable solvers e = do   res <- go [] e-  pure $ second (fromMaybe (error "Internal Error: no reachable paths found")) res+  pure $ second (fromMaybe (internalError "no reachable paths found")) res   where     {-        Walk down the tree and collect pcs.@@ -500,7 +496,7 @@         case res of           Sat _ -> pure ([query], Just leaf)           Unsat -> pure ([query], Nothing)-          r -> error $ "Invalid solver result: " <> show r+          r -> internalError $ "Invalid solver result: " <> show r   -- | Evaluate the provided proposition down to its most concrete result@@ -540,13 +536,13 @@ extractProps :: Expr End -> [Prop] extractProps = \case   ITE _ _ _ -> []-  Success asserts _ _ -> asserts-  Failure asserts _ -> asserts-  Partial asserts _ -> asserts-  GVar _ -> error "cannot extract props from a GVar"+  Success asserts _ _ _ -> asserts+  Failure asserts _ _ -> asserts+  Partial asserts _ _ -> asserts+  GVar _ -> internalError "cannot extract props from a GVar"  isPartial :: Expr a -> Bool-isPartial (Partial _ _) = True+isPartial (Partial _ _ _) = True isPartial _ = False  getPartials :: [Expr End] -> [PartialExec]@@ -554,7 +550,7 @@   where     go :: Expr End -> Maybe PartialExec     go = \case-      Partial _ p -> Just p+      Partial _ _ p -> Just p       _ -> Nothing  -- | Symbolically execute the VM and check all endstates against the@@ -617,7 +613,7 @@       Sat model -> Cex (leaf, model)       EVM.Solvers.Unknown -> Timeout leaf       Unsat -> Qed ()-      Error e -> error $ "Internal Error: solver responded with error: " <> show e+      Error e -> internalError $ "solver responded with error: " <> show e  type UnsatCache = TVar [Set Prop] @@ -632,7 +628,7 @@ equivalenceCheck   :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> (Expr Buf, [Prop])   -> IO [EquivResult]-equivalenceCheck solvers bytecodeA bytecodeB opts calldata' = do+equivalenceCheck solvers bytecodeA bytecodeB opts calldata = do   case bytecodeA == bytecodeB of     True -> do       putStrLn "bytecodeA and bytecodeB are identical"@@ -640,7 +636,21 @@     False -> do       branchesA <- getBranches bytecodeA       branchesB <- getBranches bytecodeB+      equivalenceCheck' solvers branchesA branchesB opts+  where+    -- decompiles the given bytecode into a list of branches+    getBranches :: ByteString -> IO [Expr End]+    getBranches bs = do+      let+        bytecode = if BS.null bs then BS.pack [0] else bs+        prestate = abstractVM calldata bytecode Nothing AbstractStore+      expr <- interpret (Fetch.oracle solvers Nothing) opts.maxIter opts.askSmtIters opts.loopHeuristic prestate runExpr+      let simpl = if opts.simp then (Expr.simplify expr) else expr+      pure $ flattenExpr simpl ++equivalenceCheck' :: SolverGroup -> [Expr End] -> [Expr End] -> VeriOpts -> IO [EquivResult]+equivalenceCheck' solvers branchesA branchesB opts = do       when (any isPartial branchesA || any isPartial branchesB) $ do         putStrLn ""         putStrLn "WARNING: hevm was only able to partially explore the given contract due to the following issues:"@@ -678,23 +688,17 @@     subsetAny :: Set Prop -> [Set Prop] -> Bool     subsetAny a b = foldr (\bp acc -> acc || isSubsetOf a bp) False b -    -- decompiles the given bytecode into a list of branches-    getBranches :: ByteString -> IO [Expr End]-    getBranches bs = do-      let-        bytecode = if BS.null bs then BS.pack [0] else bs-        prestate = abstractVM calldata' bytecode Nothing AbstractStore-      expr <- interpret (Fetch.oracle solvers Nothing) opts.maxIter opts.askSmtIters opts.loopHeuristic prestate runExpr-      let simpl = if opts.simp then (Expr.simplify expr) else expr-      pure $ flattenExpr simpl-     -- checks for satisfiability of all the props in the provided set. skips     -- the solver if we can determine unsatisfiability from the cache already     -- the last element of the returned tuple indicates whether the cache was     -- used or not-    check :: UnsatCache -> Set Prop -> IO (EquivResult, Bool)-    check knownUnsat props = do+    check :: UnsatCache -> (Set Prop) -> Int -> IO (EquivResult, Bool)+    check knownUnsat props idx = do       let smt = assertProps $ Set.toList props+      -- if debug is on, write the query to a file+      when opts.debug $ TL.writeFile+        ("equiv-query-" <> show idx <> ".smt2") (formatSMT2 smt <> "\n\n(check-sat)")+       ku <- readTVarIO knownUnsat       res <- if subsetAny props ku              then pure (True, Unsat)@@ -710,7 +714,7 @@               atomically $ readTVar knownUnsat >>= writeTVar knownUnsat . (props :)               pure (Qed (), False)         (_, EVM.Solvers.Unknown) -> pure (Timeout (), False)-        (_, Error txt) -> error $ "Error while running solver: `" <> T.unpack txt -- <> "` SMT file was: `" <> filename <> "`"+        (_, Error txt) -> internalError $ "issue while running solver: `" <> T.unpack txt -- <> "` SMT file was: `" <> filename <> "`"      -- Allows us to run it in parallel. Note that this (seems to) run it     -- from left-to-right, and with a max of K threads. This is in contrast to@@ -719,8 +723,9 @@     checkAll :: [(Set Prop)] -> UnsatCache -> Int -> IO [(EquivResult, Bool)]     checkAll input cache numproc = do        wrap <- pool numproc-       parMapIO (wrap . (check cache)) input+       parMapIO (wrap . (uncurry $ check cache)) $ zip input [1..] +     -- Takes two branches and returns a set of props that will need to be     -- satisfied for the two branches to violate the equivalence check. i.e.     -- for a given pair of branches, equivalence is violated if there exists an@@ -730,17 +735,17 @@     distinct aEnd bEnd =       let         differingResults = case (aEnd, bEnd) of-          (Success _ aOut aStore, Success _ bOut bStore) ->+          (Success _ _ aOut aStore, Success _ _ bOut bStore) ->             if aOut == bOut && aStore == bStore             then PBool False             else aStore ./= bStore .|| aOut ./= bOut-          (Failure _ (Revert a), Failure _ (Revert b)) -> if a == b then PBool False else a ./= b-          (Failure _ a, Failure _ b) -> if a == b then PBool False else PBool True+          (Failure _ _ (Revert a), Failure _ _ (Revert b)) -> if a == b then PBool False else a ./= b+          (Failure _ _ a, Failure _ _ b) -> if a == b then PBool False else PBool True           -- partial end states can't be compared to actual end states, so we always ignore them           (Partial {}, _) -> PBool False           (_, Partial {}) -> PBool False-          (ITE _ _ _, _) -> error "Expressions must be flattened"-          (_, ITE _ _ _) -> error "Expressions must be flattened"+          (ITE _ _ _, _) -> internalError "Expressions must be flattened"+          (_, ITE _ _ _) -> internalError "Expressions must be flattened"           (a, b) -> if a == b                     then PBool False                     else PBool True@@ -773,7 +778,7 @@ showModel cd (expr, res) = do   case res of     Unsat -> pure () -- ignore unreachable branches-    Error e -> error $ "Internal error: smt solver returned an error: " <> show e+    Error e -> internalError $ "smt solver returned an error: " <> show e     EVM.Solvers.Unknown -> do       putStrLn "--- Branch ---"       putStrLn ""@@ -819,7 +824,7 @@       | otherwise =           [ "Storage:"           , indent 2 $ T.unlines $ Map.foldrWithKey (\key val acc ->-              ("Addr " <> (T.pack . show . Addr . num $ key)+              ("Addr " <> (T.pack $ show (unsafeInto key :: Addr))                 <> ": " <> (T.pack $ show (Map.toList val))) : acc             ) mempty store           , ""@@ -851,9 +856,9 @@         go (CallValue x) _ = x == 0         go (Caller x) _ = x == 0         go (Address x) _ = x == 0-        go (Balance {}) _ = error "TODO: BALANCE"-        go (SelfBalance {}) _ = error "TODO: SELFBALANCE"-        go (Gas {}) _ = error "TODO: Gas"+        go (Balance {}) _ = internalError "TODO: BALANCE"+        go (SelfBalance {}) _ = internalError "TODO: SELFBALANCE"+        go (Gas {}) _ = internalError "TODO: Gas"         go _ _ = False      blockCtx :: [Text]@@ -881,7 +886,7 @@   where     forceFlattened (SMT.Flat bs) = bs     forceFlattened b@(SMT.Comp _) = forceFlattened $-      fromMaybe (error $ "Internal Error: cannot flatten buffer: " <> show b)+      fromMaybe (internalError $ "cannot flatten buffer: " <> show b)                 (SMT.collapse b)      subVars model b = Map.foldlWithKey subVar b model

@@ -1,12 +1,10 @@-{-# Language TemplateHaskell #-}-{-# Language UndecidableInstances #-}-{-# Language ImplicitParams #-}-{-# Language DataKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}  module EVM.TTY where -import Prelude hiding (lookup, Word)- import Brick import Brick.Widgets.Border import Brick.Widgets.Center@@ -57,6 +55,7 @@ import System.Console.Haskeline qualified as Readline import Paths_hevm qualified as Paths import Text.Wrap+import Witch (into)  data Name   = AbiPane@@ -227,7 +226,7 @@ mkVty = do   vty <- V.mkVty V.defaultConfig   V.setMode (V.outputIface vty) V.BracketedPaste True-  return vty+  pure vty  runFromVM :: SolverGroup -> Fetch.RpcInfo -> Maybe Integer -> DappInfo -> VM -> IO VM runFromVM solvers rpcInfo maxIter' dappinfo vm = do@@ -245,9 +244,9 @@       , maxDepth      = Nothing       , match         = ""       , fuzzRuns      = 1-      , replay        = error "irrelevant"+      , replay        = internalError "irrelevant"       , vmModifier    = id-      , testParams    = error "irrelevant"+      , testParams    = internalError "irrelevant"       , dapp          = dappinfo       , ffiAllowed    = False       , covMatch       = Nothing@@ -257,8 +256,8 @@   v <- mkVty   ui2 <- customMain v mkVty Nothing (app opts) (ViewVm ui0)   case ui2 of-    ViewVm ui -> return ui.vm-    _ -> error "internal error: customMain returned prematurely"+    ViewVm ui -> pure ui.vm+    _ -> internalError "customMain returned prematurely"   initUiVmState :: VM -> UnitTestOptions -> Stepper () -> UiVmState@@ -304,7 +303,7 @@       }   v <- mkVty   _ <- customMain v mkVty Nothing (app opts) (ui :: UiState)-  return ()+  pure ()  takeStep   :: (?fetcher :: Fetcher@@ -383,7 +382,7 @@       in         runStateT (interpret (Step stepsToTake) stepper) s1 >>= \case           (Continue steps, ui') -> pure $ ui' & set #stepper steps-          _ -> error "unexpected end"+          _ -> internalError "unexpected end"  appEvent   :: (?fetcher::Fetcher, ?maxIter :: Maybe Integer) =>@@ -451,7 +450,7 @@       }   ViewPicker s ->     case listSelectedElement s.tests of-      Nothing -> error "nothing selected"+      Nothing -> internalError "nothing selected"       Just (_, x) -> do         let initVm  = initialUiVmStateForTest s.opts x         put (ViewVm initVm)@@ -617,7 +616,7 @@   where     cd = case test of       SymbolicTest _ -> symCalldata theTestName types [] (AbstractBuf "txdata")-      _ -> (error "unreachable", error "unreachable")+      _ -> (internalError "unreachable", error $ internalError "unreachable")     (test, types) = fromJust $ find (\(test',_) -> extractSig test' == theTestName) $ unitTestMethods testContract     testContract = fromJust $ Map.lookup theContractName dapp.solcByName     vm0 =@@ -751,7 +750,7 @@     dapp = ui.vm.testOpts.dapp     (_, (_, c)) = fromJust $ listSelectedElement ui.contracts --        currentContract  = view (dappSolcByHash . ix ) dapp-    maybeHash ch = fromJust (error "Internal error: cannot find concrete codehash for partially symbolic code") (maybeLitWord ch.codehash)+    maybeHash ch = fromJust (internalError "cannot find concrete codehash for partially symbolic code") (maybeLitWord ch.codehash)  drawVm :: UiVmState -> [UiWidget] drawVm ui =@@ -863,7 +862,7 @@ drawStackPane :: UiVmState -> UiWidget drawStackPane ui =   let-    gasText = showWordExact (num ui.vm.state.gas)+    gasText = showWordExact (into ui.vm.state.gas)     labelText = txt ("Gas available: " <> gasText <> "; stack:")     stackList = list StackPane (Vec.fromList $ zip [(1 :: Int)..] (simplify <$> ui.vm.state.stack)) 2   in hBorderWithLabel labelText <=>@@ -977,7 +976,7 @@         Nothing -> mempty         Just x ->           fromMaybe-            (error "Internal Error: unable to find line for source map")+            (internalError "unable to find line for source map")             (preview (               ix x.file               % to (Vec.imap (,)))

@@ -4,13 +4,12 @@  import Optics.Core import Data.Maybe (fromMaybe)+import Data.Vector qualified as V  import Brick.Types import Brick.Widgets.Core import Brick.Widgets.List -import qualified Data.Vector as V- -- | Turn a list state value into a widget given an item drawing -- function. renderList :: (Ord n, Show n)@@ -28,44 +27,44 @@  drawListElements :: (Ord n, Show n) => Bool -> List n e -> (Bool -> e -> Widget n) -> Widget n drawListElements foc l drawElem =-    Widget Greedy Greedy $ do-        c <- getContext+  Widget Greedy Greedy $ do+    c <- getContext -        let es = V.slice start num (l ^. (lensVL listElementsL))-            idx = fromMaybe 0 (l ^. (lensVL listSelectedL))+    let es = V.slice start num (l ^. (lensVL listElementsL))+        idx = fromMaybe 0 (l ^. (lensVL listSelectedL)) -            start = max 0 $ idx - (initialNumPerHeight `div` 2)-            num = min (numPerHeight * 2) (V.length (l ^. (lensVL listElementsL)) - start)+        start = max 0 $ idx - (initialNumPerHeight `div` 2)+        num = min (numPerHeight * 2) (V.length (l ^. (lensVL listElementsL)) - start) -            -- The number of items to show is the available height divided by-            -- the item height...-            initialNumPerHeight = (c ^. (lensVL availHeightL)) `div` (l ^. (lensVL listItemHeightL))-            -- ... but if the available height leaves a remainder of-            -- an item height then we need to ensure that we render an-            -- extra item to show a partial item at the top or bottom to-            -- give the expected result when an item is more than one-            -- row high. (Example: 5 rows available with item height-            -- of 3 yields two items: one fully rendered, the other-            -- rendered with only its top 2 or bottom 2 rows visible,-            -- depending on how the viewport state changes.)-            numPerHeight = initialNumPerHeight +-                           if initialNumPerHeight * (l ^. (lensVL listItemHeightL)) == c ^. (lensVL availHeightL)-                           then 0-                           else 1+        -- The number of items to show is the available height divided by+        -- the item height...+        initialNumPerHeight = (c ^. (lensVL availHeightL)) `div` (l ^. (lensVL listItemHeightL))+        -- ... but if the available height leaves a remainder of+        -- an item height then we need to ensure that we render an+        -- extra item to show a partial item at the top or bottom to+        -- give the expected result when an item is more than one+        -- row high. (Example: 5 rows available with item height+        -- of 3 yields two items: one fully rendered, the other+        -- rendered with only its top 2 or bottom 2 rows visible,+        -- depending on how the viewport state changes.)+        numPerHeight = initialNumPerHeight ++                       if initialNumPerHeight * (l ^. (lensVL listItemHeightL)) == c ^. (lensVL availHeightL)+                       then 0+                       else 1 -            -- off = start * (l^.listItemHeightL)+        -- off = start * (l^.listItemHeightL) -            drawnElements = flip V.imap es $ \i e ->-                let isSelected = i == (if start == 0 then idx else div initialNumPerHeight 2)-                    elemWidget = drawElem isSelected e-                    selItemAttr = if foc-                                  then withDefAttr listSelectedFocusedAttr-                                  else withDefAttr listSelectedAttr-                    makeVisible = if isSelected-                                  then visible . selItemAttr-                                  else id-                in makeVisible elemWidget+        drawnElements = flip V.imap es $ \i e ->+            let isSelected = i == (if start == 0 then idx else div initialNumPerHeight 2)+                elemWidget = drawElem isSelected e+                selItemAttr = if foc+                              then withDefAttr listSelectedFocusedAttr+                              else withDefAttr listSelectedAttr+                makeVisible = if isSelected+                              then visible . selItemAttr+                              else id+            in makeVisible elemWidget -        render $ viewport (l ^. (lensVL listNameL)) Vertical $-                 -- translateBy (Location (0, off)) $-                 vBox $ V.toList drawnElements+    render $ viewport (l ^. (lensVL listNameL)) Vertical $+             -- translateBy (Location (0, off)) $+             vBox $ V.toList drawnElements

@@ -1,7 +1,5 @@ module EVM.Transaction where -import Prelude hiding (Word)- import EVM (initialContract, ceilDiv) import EVM.FeeSchedule import EVM.RLP@@ -12,18 +10,18 @@  import Optics.Core hiding (cons) +import Data.Aeson (FromJSON (..))+import Data.Aeson qualified as JSON+import Data.Aeson.Types qualified as JSON import Data.ByteString (ByteString, cons)+import Data.ByteString qualified as BS import Data.Map (Map)+import Data.Map qualified as Map import Data.Maybe (fromMaybe, isNothing, fromJust)-import GHC.Generics (Generic)--import Data.Aeson (FromJSON (..))-import qualified Data.Aeson        as JSON-import qualified Data.Aeson.Types  as JSON-import qualified Data.ByteString   as BS-import qualified Data.Map          as Map import Data.Word (Word64)+import GHC.Generics (Generic) import Numeric (showHex)+import Witch (into, unsafeInto)  data AccessListEntry = AccessListEntry {   address :: Addr,@@ -110,7 +108,7 @@                else 27 + v  sign :: Integer -> Transaction -> Transaction-sign sk tx = tx { v = num v, r = r, s = s}+sign sk tx = tx { v = into v, r = r, s = s}   where     hash = keccak' $ signingData tx     (v, r, s) = EVM.Sign.sign hash sk@@ -123,7 +121,7 @@       else normalData     AccessListTransaction -> eip2930Data     EIP1559Transaction -> eip1559Data-  where v          = fromIntegral tx.v+  where v          = tx.v         to'        = case tx.toAddr of           Just a  -> BS $ word160Bytes a           Nothing -> BS mempty@@ -137,13 +135,13 @@           ) accessList         normalData = rlpList [rlpWord256 tx.nonce,                               rlpWord256 gasPrice,-                              rlpWord256 (num tx.gasLimit),+                              rlpWord256 (into tx.gasLimit),                               to',                               rlpWord256 tx.value,                               BS tx.txdata]         eip155Data = rlpList [rlpWord256 tx.nonce,                               rlpWord256 gasPrice,-                              rlpWord256 (num tx.gasLimit),+                              rlpWord256 (into tx.gasLimit),                               to',                               rlpWord256 tx.value,                               BS tx.txdata,@@ -155,7 +153,7 @@           rlpWord256 tx.nonce,           rlpWord256 maxPrio,           rlpWord256 maxFee,-          rlpWord256 (num tx.gasLimit),+          rlpWord256 (into tx.gasLimit),           to',           rlpWord256 tx.value,           BS tx.txdata,@@ -165,7 +163,7 @@           rlpWord256 tx.chainId,           rlpWord256 tx.nonce,           rlpWord256 gasPrice,-          rlpWord256 (num tx.gasLimit),+          rlpWord256 (into tx.gasLimit),           to',           rlpWord256 tx.value,           BS tx.txdata,@@ -176,7 +174,7 @@     sum (map       (\ale ->         fs.g_access_list_address  +-        (fs.g_access_list_storage_key  * (fromIntegral . length) ale.storageKeys))+        (fs.g_access_list_storage_key  * (unsafeInto . length) ale.storageKeys))         al)  txGasCost :: FeeSchedule Word64 -> Transaction -> Word64@@ -189,14 +187,14 @@         + (accessListPrice fs tx.accessList )       zeroCost     = fs.g_txdatazero       nonZeroCost  = fs.g_txdatanonzero-      initcodeCost = fs.g_initcodeword * num (ceilDiv (BS.length calldata) 32)-  in baseCost + zeroCost * (fromIntegral zeroBytes) + nonZeroCost * (fromIntegral nonZeroBytes)+      initcodeCost = fs.g_initcodeword * unsafeInto (ceilDiv (BS.length calldata) 32)+  in baseCost + zeroCost * (unsafeInto zeroBytes) + nonZeroCost * (unsafeInto nonZeroBytes)  instance FromJSON AccessListEntry where   parseJSON (JSON.Object val) = do     accessAddress_ <- addrField val "address"     accessStorageKeys_ <- (val JSON..: "storageKeys") >>= parseJSONList-    return $ AccessListEntry accessAddress_ accessStorageKeys_+    pure $ AccessListEntry accessAddress_ accessStorageKeys_   parseJSON invalid =     JSON.typeMismatch "AccessListEntry" invalid @@ -215,15 +213,15 @@     value    <- wordField val "value"     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 1+      Just 0x00 -> pure $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing 1       Just 0x01 -> do         accessListEntries <- (val JSON..: "accessList") >>= parseJSONList-        return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value AccessListTransaction accessListEntries Nothing Nothing 1+        pure $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value AccessListTransaction accessListEntries Nothing Nothing 1       Just 0x02 -> do         accessListEntries <- (val JSON..: "accessList") >>= parseJSONList-        return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value EIP1559Transaction accessListEntries maxPrio maxFee 1+        pure $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value EIP1559Transaction accessListEntries maxPrio maxFee 1       Just _ -> fail "unrecognized custom transaction type"-      Nothing -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing 1+      Nothing -> pure $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing 1   parseJSON invalid =     JSON.typeMismatch "Transaction" invalid @@ -239,7 +237,7 @@ -- | Increments origin nonce and pays gas deposit setupTx :: Addr -> Addr -> W256 -> Word64 -> Map Addr Contract -> Map Addr Contract setupTx origin coinbase gasPrice gasLimit prestate =-  let gasCost = gasPrice * (num gasLimit)+  let gasCost = gasPrice * (into gasLimit)   in (Map.adjust ((over #nonce   (+ 1))                . (over #balance (subtract gasCost))) origin)     . touchAccount origin@@ -269,11 +267,11 @@          else touchAccount toAddr)       $ preState -    resetConcreteStore s = if creation then Map.insert (num toAddr) mempty s else s+    resetConcreteStore s = if creation then Map.insert (into toAddr) mempty s else s      resetStore (ConcreteStore s) = ConcreteStore (resetConcreteStore s)     resetStore (SStore a@(Lit _) k v s) = if creation && a == (litAddr toAddr) then resetStore s else (SStore a k v (resetStore s))-    resetStore (SStore {}) = error "cannot reset storage if it contains symbolic addresses"+    resetStore (SStore {}) = internalError "cannot reset storage if it contains symbolic addresses"     resetStore s = s     in       vm & #env % #contracts .~ initState

@@ -1,12 +1,10 @@-{-# Language DataKinds #-}- {- |     Module: EVM.Traversals     Description: Generic traversal functions for Expr datatypes -} module EVM.Traversals where -import Prelude hiding (Word, LT, GT)+import Prelude hiding (LT, GT)  import Control.Monad.Identity @@ -28,6 +26,27 @@       POr a b -> go a <> go b       PImpl a b -> go a <> go b +foldTrace :: forall b . Monoid b => (forall a . Expr a -> b) -> b -> Trace -> b+foldTrace f acc t = acc <> (go t)+  where+    go :: Trace -> b+    go (Trace _ _ d) = case d of+      EventTrace a b c -> foldExpr f mempty a <> foldExpr f mempty b <> (foldl (foldExpr f) mempty c)+      FrameTrace a -> go' a+      ErrorTrace _ -> mempty+      EntryTrace _ -> mempty+      ReturnTrace a b -> foldExpr f mempty a <> go' b++    go' :: FrameContext -> b+    go' = \case+      CreationContext _ b _ _ -> foldExpr f mempty b+      CallContext _ _ _ _ e _ g (_, h) _ -> foldExpr f mempty e <> foldExpr f mempty g <> foldExpr f mempty h++foldTraces :: forall b . Monoid b => (forall a . Expr a -> b) -> b -> Traces -> b+foldTraces f acc (Traces a _) = acc <> foldl (foldl (foldTrace f)) mempty a+++ -- | Recursively folds a given function over a given expression -- Recursion schemes do this & a lot more, but defining them over GADT's isn't worth the hassle foldExpr :: forall b c . Monoid b => (forall a . Expr a -> b) -> b -> Expr c -> b@@ -67,9 +86,9 @@        -- control flow -      e@(Success a b c) -> f e <> (foldl (foldProp f) mempty a) <> (go b) <> (go c)-      e@(Failure a _) -> f e <> (foldl (foldProp f) mempty a)-      e@(Partial a _) -> f e <> (foldl (foldProp f) mempty a)+      e@(Success a b c d) -> f e <> (foldl (foldProp f) mempty a) <> foldTraces f mempty b <> (go c) <> (go d)+      e@(Failure a b _) -> f e <> (foldl (foldProp f) mempty a) <> foldTraces f mempty b+      e@(Partial a b _) -> f e <> (foldl (foldProp f) mempty a) <> foldTraces f mempty b       e@(ITE a b c) -> f e <> (go a) <> (go b) <> (go c)        -- integers@@ -241,6 +260,22 @@   POr a b -> POr (mapProp f a) (mapProp f b)   PImpl a b -> PImpl (mapProp f a) (mapProp f b) +mapTrace :: (forall a . Expr a -> Expr a) -> Trace -> Trace+mapTrace f (Trace x y z) = Trace x y (go z)+  where+    go :: TraceData -> TraceData+    go = \case+      EventTrace a b c -> EventTrace (f a) (f b) (fmap (mapExpr f) c)+      FrameTrace a -> FrameTrace (go' a)+      ErrorTrace a -> ErrorTrace a+      EntryTrace a -> EntryTrace a+      ReturnTrace a b -> ReturnTrace (f a) (go' b)++    go' :: FrameContext -> FrameContext+    go' = \case+      CreationContext a b c d -> CreationContext a (f b) c d+      CallContext a b c d e g h (i,j) k -> CallContext a b c d (f e) g (f h) (i,f j) k+ -- | Recursively applies a given function to every node in a given expr instance -- Recursion schemes do this & a lot more, but defining them over GADT's isn't worth the hassle mapExpr :: (forall a . Expr a -> Expr a) -> Expr b -> Expr b@@ -311,17 +346,20 @@    -- control flow -  Failure a b -> do+  Failure a b c -> do     a' <- mapM (mapPropM f) a-    f (Failure a' b)-  Partial a b -> do+    b' <- mapTracesM f b+    f (Failure a' b' c)+  Partial a b c -> do     a' <- mapM (mapPropM f) a-    f (Partial a' b)-  Success a b c -> do+    b' <- mapTracesM f b+    f (Partial a' b' c)+  Success a b c d -> do     a' <- mapM (mapPropM f) a-    b' <- mapExprM f b+    b' <- mapTracesM f b     c' <- mapExprM f c-    f (Success a' b' c')+    d' <- mapExprM f d+    f (Success a' b' c' d')    ITE a b c -> do     a' <- mapExprM f a@@ -653,6 +691,42 @@     b' <- mapPropM f b     pure $ PImpl a' b' +mapTracesM :: forall m . Monad m => (forall a . Expr a -> m (Expr a)) -> Traces -> m Traces+mapTracesM f (Traces a b) = do+  a' <- mapM (mapM (mapTraceM f)) a+  pure $ Traces a' b++mapTraceM :: forall m . Monad m => (forall a . Expr a -> m (Expr a)) -> Trace -> m Trace+mapTraceM f (Trace x y z) = do+  z' <- go z+  pure $ Trace x y z'+  where+    go :: TraceData -> m TraceData+    go = \case+      EventTrace a b c -> do+        a' <- mapExprM f a+        b' <- mapExprM f b+        c' <- mapM (mapExprM f) c+        pure $ EventTrace a' b' c'+      FrameTrace a -> do+        a' <- go' a+        pure $ FrameTrace a'+      ReturnTrace a b -> do+        a' <- mapExprM f a+        b' <- go' b+        pure $ ReturnTrace a' b'+      a -> pure a++    go' :: FrameContext -> m FrameContext+    go' = \case+      CreationContext a b c d -> do+        b' <- mapExprM f b+        pure $ CreationContext a b' c d+      CallContext a b c d e g h (i,j) k -> do+        e' <- mapExprM f e+        h' <- mapExprM f h+        j' <- mapExprM f j+        pure $ CallContext a b c d e' g h' (i,j') k  -- | Generic operations over AST terms class TraversableTerm a where

@@ -1,25 +1,20 @@-{-# Language CPP #-}-{-# Language UndecidableInstances #-}-{-# Language TemplateHaskell #-}-{-# Language TypeApplications #-}-{-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}  {-# OPTIONS_GHC -Wno-inline-rule-shadowing #-}  module EVM.Types where -import Prelude hiding  (Word, LT, GT)-+import GHC.Stack (HasCallStack, prettyCallStack, callStack) import Control.Arrow ((>>>))-import Control.Monad.State.Strict hiding (state)-import Crypto.Hash hiding (SHA256)+import Control.Monad.State.Strict (State, mzero)+import Crypto.Hash (hash, Keccak_256, Digest) import Data.Aeson import Data.Aeson qualified as JSON import Data.Aeson.Types qualified as JSON import Data.Bifunctor (first)-import Data.Bits (Bits, FiniteBits, shiftR, shift, shiftL, (.&.), (.|.))+import Data.Bits (Bits, FiniteBits, shiftR, shift, shiftL, (.&.), (.|.), toIntegralSized) import Data.ByteArray qualified as BA import Data.Char import Data.List (foldl')@@ -30,17 +25,20 @@ import Data.ByteString.Char8 qualified as Char8 import Data.ByteString.Lazy (toStrict) import Data.Data+import Data.Int (Int64) import Data.Word (Word8, Word32, Word64) import Data.DoubleWord import Data.DoubleWord.TH import Data.Map (Map)-import qualified Data.Map as Map+import Data.Map qualified as Map import Data.Maybe (fromMaybe) import Data.Set (Set) import Data.Sequence qualified as Seq import Data.Serialize qualified as Cereal import Data.Text qualified as T import Data.Text.Encoding qualified as T+import Data.Tree (Forest)+import Data.Tree.Zipper qualified as Zipper import Data.Vector qualified as V import Data.Vector.Storable qualified as SV import Numeric (readHex, showHex)@@ -48,10 +46,10 @@ import Optics.TH import EVM.Hexdump (paddedShowHex) import EVM.FeeSchedule (FeeSchedule (..))-import Data.Tree.Zipper qualified as Zipper -import qualified Text.Regex.TDFA      as Regex-import qualified Text.Read+import Text.Regex.TDFA qualified as Regex+import Text.Read qualified+import Witch   -- Template Haskell --------------------------------------------------------------------------@@ -61,7 +59,40 @@ mkUnpackedDoubleWord "Word512" ''Word256 "Int512" ''Int256 ''Word256   [''Typeable, ''Data, ''Generic] +instance From Addr Integer where from = fromIntegral+instance From Addr W256 where from = fromIntegral+instance From Int256 Integer where from = fromIntegral+instance From Nibble Int where from = fromIntegral+instance From W256 Integer where from = fromIntegral+instance From Word8 W256 where from = fromIntegral+instance From Word8 Word256 where from = fromIntegral+instance From Word32 W256 where from = fromIntegral+instance From Word32 Word256 where from = fromIntegral+instance From Word64 W256 where from = fromIntegral+instance From Word256 Integer where from = fromIntegral+instance From Word256 W256 where from = fromIntegral +instance TryFrom Int W256 where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom Int Word256 where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom Int256 W256 where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom Integer W256 where tryFrom = maybeTryFrom toIntegralSized+-- TODO: hevm relies on this behavior+instance TryFrom W256 Addr where tryFrom = Right . fromIntegral+instance TryFrom W256 FunctionSelector where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom W256 Int where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom W256 Int64 where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom W256 Int256 where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom W256 Word8 where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom W256 Word32 where tryFrom = maybeTryFrom toIntegralSized+-- TODO: hevm relies on this behavior+instance TryFrom W256 Word64 where tryFrom = Right . fromIntegral+instance TryFrom Word160 Word8 where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom Word256 Int where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom Word256 Int256 where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom Word256 Word8 where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom Word256 Word32 where tryFrom = maybeTryFrom toIntegralSized+instance TryFrom Word512 W256 where tryFrom = maybeTryFrom toIntegralSized+ -- Symbolic IR -------------------------------------------------------------------------------------  -- phantom type tags for AST construction@@ -84,7 +115,6 @@ deriving instance Eq (GVar a) deriving instance Ord (GVar a) - {- |   Expr implements an abstract respresentation of an EVM program @@ -160,9 +190,9 @@    -- control flow -  Partial        :: [Prop] -> PartialExec -> Expr End-  Failure        :: [Prop] -> EvmError -> Expr End-  Success        :: [Prop] -> Expr Buf -> Expr Storage -> Expr End+  Partial        :: [Prop] -> Traces -> PartialExec -> Expr End+  Failure        :: [Prop] -> Traces -> EvmError -> Expr End+  Success        :: [Prop] -> Traces -> Expr Buf -> Expr Storage -> Expr End   ITE            :: Expr EWord -> Expr End -> Expr End -> Expr End    -- integers@@ -619,7 +649,7 @@     , callreversion :: (Map Addr Contract, Expr Storage)     , subState      :: SubState     }-  deriving (Show, Generic)+  deriving (Eq, Ord, Show, Generic)  -- | The "accrued substate" across a transaction data SubState = SubState@@ -630,7 +660,7 @@   , refunds             :: [(Addr, Word64)]   -- in principle we should include logs here, but do not for now   }-  deriving (Show)+  deriving (Eq, Ord, Show)  -- | The "registers" of the VM along with memory and data stack data FrameState = FrameState@@ -714,7 +744,7 @@   , codeOps      :: V.Vector (Int, Op)   , external     :: Bool   }-  deriving (Show)+  deriving (Eq, Ord, Show)   -- Bytecode Representations ------------------------------------------------------------------------@@ -807,18 +837,29 @@   , contract  :: Contract   , tracedata :: TraceData   }-  deriving (Show, Generic)+  deriving (Eq, Ord, Show, Generic)  data TraceData   = EventTrace (Expr EWord) (Expr Buf) [Expr EWord]   | FrameTrace FrameContext-  | QueryTrace Query   | ErrorTrace EvmError   | EntryTrace Text   | ReturnTrace (Expr Buf) FrameContext-  deriving (Show, Generic)+  deriving (Eq, Ord, Show, Generic) +-- | Wrapper type containing vm traces and the context needed to pretty print them properly+data Traces = Traces+  { traces :: Forest Trace+  , contracts :: Map Addr Contract+  }+  deriving (Eq, Ord, Show, Generic) +instance Semigroup Traces where+  (Traces a b) <> (Traces c d) = Traces (a <> c) (b <> d)+instance Monoid Traces where+  mempty = Traces mempty mempty++ -- VM Initialization -------------------------------------------------------------------------------  @@ -935,7 +976,7 @@   | OpPush0   | OpPush a   | OpUnknown Word8-  deriving (Show, Eq, Functor)+  deriving (Show, Eq, Ord, Functor)   -- Function Selectors ------------------------------------------------------------------------------@@ -943,7 +984,7 @@  -- | https://docs.soliditylang.org/en/v0.8.19/abi-spec.html#function-selector newtype FunctionSelector = FunctionSelector { unFunctionSelector :: Word32 }-  deriving (Num, Eq, Ord, Real, Enum, Integral)+  deriving (Bits, Num, Eq, Ord, Real, Enum, Integral) instance Show FunctionSelector where show s = "0x" <> showHex s ""  @@ -996,13 +1037,13 @@   parseJSON v = do     s <- T.unpack <$> parseJSON v     case reads s of-      [(x, "")]  -> return x+      [(x, "")]  -> pure x       _          -> fail $ "invalid hex word (" ++ s ++ ")"  instance FromJSONKey W256 where   fromJSONKey = FromJSONKeyTextParser $ \s ->     case reads (T.unpack s) of-      [(x, "")]  -> return x+      [(x, "")]  -> pure x       _          -> fail $ "invalid word (" ++ T.unpack s ++ ")"  wordField :: JSON.Object -> Key -> JSON.Parser W256@@ -1073,7 +1114,7 @@   parseJSON v = do     s <- T.unpack <$> parseJSON v     case reads s of-      [(x, "")] -> return x+      [(x, "")] -> pure x       _         -> fail $ "invalid address (" ++ s ++ ")"  instance JSON.ToJSONKey Addr where@@ -1087,7 +1128,7 @@ instance FromJSONKey Addr where   fromJSONKey = FromJSONKeyTextParser $ \s ->     case reads (T.unpack s) of-      [(x, "")] -> return x+      [(x, "")] -> pure x       _         -> fail $ "invalid word (" ++ T.unpack s ++ ")"  addrField :: JSON.Object -> Key -> JSON.Parser Addr@@ -1107,10 +1148,10 @@  -- | A four bit value newtype Nibble = Nibble Word8-  deriving ( Num, Integral, Real, Ord, Enum, Eq, Bounded, Generic)+  deriving (Num, Integral, Real, Ord, Enum, Eq, Bounded, Generic)  instance Show Nibble where-  show = (:[]) . intToDigit . num+  show = (:[]) . intToDigit . fromIntegral   -- Conversions -------------------------------------------------------------------------------------@@ -1135,7 +1176,7 @@   -- optimize one byte pushes   Word256 (Word128 0 0) (Word128 0 (fromIntegral $ BS.head xs)) word256 xs = case Cereal.runGet m (padLeft 32 xs) of-               Left _ -> error "internal error"+               Left _ -> internalError "should not happen"                Right x -> x   where     m = do a <- Cereal.getWord64be@@ -1150,12 +1191,12 @@ fromBE :: (Integral a) => ByteString -> a fromBE xs = if xs == mempty then 0   else 256 * fromBE (BS.init xs)-       + (num $ BS.last xs)+       + (fromIntegral $ BS.last xs)  asBE :: (Integral a) => a -> ByteString asBE 0 = mempty asBE x = asBE (x `div` 256)-  <> BS.pack [num $ x `mod` 256]+  <> BS.pack [fromIntegral $ x `mod` 256]  word256Bytes :: W256 -> ByteString word256Bytes (W256 (Word256 (Word128 a b) (Word128 c d))) =@@ -1181,28 +1222,24 @@ packNibbles :: [Nibble] -> ByteString packNibbles [] = mempty packNibbles (n1:n2:ns) = BS.singleton (toByte n1 n2) <> packNibbles ns-packNibbles _ = error "can't pack odd number of nibbles"+packNibbles _ = internalError "can't pack odd number of nibbles"  toWord64 :: W256 -> Maybe Word64 toWord64 n =-  if n <= num (maxBound :: Word64)+  if n <= into (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)+  if n <= unsafeInto (maxBound :: Int)     then let (W256 (Word256 _ (Word128 _ n'))) = n in Just (fromIntegral n')     else Nothing  bssToBs :: ByteStringS -> ByteString bssToBs (ByteStringS bs) = bs --- | This just overflows silently, and is generally a terrible footgun, should be removed-num :: (Integral a, Num b) => a -> b-num = fromIntegral - -- Keccak hashing ----------------------------------------------------------------------------------  @@ -1233,6 +1270,8 @@  -- Utils ------------------------------------------------------------------------------------------- +internalError:: HasCallStack => [Char] -> a+internalError m = error $ "Internal error: " ++ m ++ " -- " ++ (prettyCallStack callStack)  concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] concatMapM f xs = fmap concat (mapM f xs)

@@ -1,5 +1,5 @@-{-# Language DataKinds #-}-{-# Language ImplicitParams #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ImplicitParams #-}  module EVM.UnitTest where @@ -64,6 +64,7 @@ import System.IO (hFlush, stdout) import Test.QuickCheck hiding (verbose, Success, Failure) import qualified Test.QuickCheck as QC+import Witch (unsafeInto, into)  data UnitTestOptions = UnitTestOptions   { rpcInfo     :: Fetch.RpcInfo@@ -144,7 +145,7 @@       in         liftIO $ Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts evmcache) -  return $ and passing+  pure $ and passing   -- | Assuming a constructor is loaded, this stepper will run the constructor@@ -206,10 +207,10 @@   Stepper.evm $ do     cs <- use (#env % #contracts)     abiCall testParams (Right bs)-    let (Method _ inputs sig _ _) = fromMaybe (error "unknown abi call") $ Map.lookup (num $ word $ BS.take 4 bs) dapp.abiMap+    let Method _ inputs sig _ _ = fromMaybe (internalError "unknown abi call") $ Map.lookup (unsafeInto $ word $ BS.take 4 bs) dapp.abiMap         types = snd <$> inputs     let ?context = DappContext dapp cs-    this <- fromMaybe (error "unknown target") <$> (use (#env % #contracts % at testParams.address))+    this <- fromMaybe (internalError "unknown target") <$> (use (#env % #contracts % at testParams.address))     let name = maybe "" (contractNamePart . (.contractName)) $ lookupCode this.contractcode dapp     pushTrace (EntryTrace (name <> "." <> sig <> "(" <> intercalate "," ((pack . show) <$> types) <> ")" <> showCall types (ConcreteBuf bs)))   -- Try running the test method@@ -234,9 +235,9 @@       Right (ConcreteBuf r) ->         let failed = case decodeAbiValue AbiBoolType (BSLazy.fromStrict r) of               AbiBool f -> f-              _ -> error "fix me with better types"+              _ -> internalError "fix me with better types"         in pure (shouldFail == failed)-      c -> error $ "internal error: unexpected failure code: " <> show c+      c -> internalError $ "unexpected failure code: " <> show c  -- | Randomly generates the calldata arguments and runs the test fuzzTest :: UnitTestOptions -> Text -> [AbiType] -> VM -> Property@@ -268,11 +269,11 @@ currentOpLocation vm =   case currentContract vm of     Nothing ->-      error "internal error: why no contract?"+      internalError "why no contract?"     Just c ->       OpLocation         c-        (fromMaybe (error "internal error: op ix") (vmOpIx vm))+        (fromMaybe (internalError "op ix") (vmOpIx vm))  execWithCoverage :: StateT CoverageState IO VMResult execWithCoverage = do _ <- runWithCoverage@@ -318,7 +319,7 @@           do m <- liftIO ((Fetch.oracle solvers rpcInfo) q)              zoom _1 (State.state (runState m)) >> interpretWithCoverage opts (k ())         Stepper.Ask _ ->-          error "cannot make choice in this interpreter"+          internalError "cannot make choice in this interpreter"         Stepper.IOAct q ->           zoom _1 (StateT (runStateT q)) >>= interpretWithCoverage opts . k         Stepper.EVM m ->@@ -381,7 +382,7 @@   case Map.lookup name contractMap of     Nothing ->       -- Fail if there's no such contract-      error $ "Contract " ++ unpack name ++ " not found"+      internalError $ "Contract " ++ unpack name ++ " not found"      Just theContract -> do       -- Construct the initial VM and begin the contract's constructor@@ -425,7 +426,7 @@   case Map.lookup name contractMap of     Nothing ->       -- Fail if there's no such contract-      error $ "Contract " ++ unpack name ++ " not found"+      internalError $ "Contract " ++ unpack name ++ " not found"      Just theContract -> do       -- Construct the initial VM and begin the contract's constructor@@ -465,7 +466,7 @@             tick (Text.unlines bailing)            pure [(isRight r, vm) | (r, vm) <- details]-        _ -> error "internal error: setUp() did not end with a result"+        _ -> internalError "setUp() did not end with a result"   runTest :: UnitTestOptions -> VM -> (Test, [AbiType]) -> IO (Text, Either Text Text, VM)@@ -484,19 +485,19 @@     if sig == testName     then exploreRun opts vm testName (decodeCalls cds)     else exploreRun opts vm testName []-runTest _ _ (InvariantTest _, types) = error $ "invariant testing with arguments: " <> show types <> " is not implemented (yet!)"+runTest _ _ (InvariantTest _, types) = internalError $ "invariant testing with arguments: " <> show types <> " is not implemented (yet!)" runTest opts vm (SymbolicTest testName, types) = symRun opts vm testName types  type ExploreTx = (Addr, Addr, ByteString, W256)  decodeCalls :: BSLazy.ByteString -> [ExploreTx]-decodeCalls b = fromMaybe (error "could not decode replay data") $ do+decodeCalls b = fromMaybe (internalError "could not decode replay data") $ do   List v <- rlpdecode $ BSLazy.toStrict b   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"+      (unsafeInto (word caller'), unsafeInto (word target), cd, word ts)+    unList _ = internalError "fix me with better types"  -- | Runs an invariant test, calls the invariant before execution begins initialExplorationStepper :: UnitTestOptions -> ABIMethod -> [ExploreTx] -> [Addr] -> Int -> Stepper (Bool, RLP)@@ -508,11 +509,11 @@   else pure (False, history)  explorationStepper :: UnitTestOptions -> ABIMethod -> [ExploreTx] -> [Addr] -> RLP -> Int -> Stepper (Bool, RLP)-explorationStepper _ _ _ _ history 0  = return (True, history)+explorationStepper _ _ _ _ history 0  = pure (True, history) explorationStepper opts@UnitTestOptions{..} testName replayData targets (List history) i = do  (caller', target, cd, timestamp') <-    case preview (ix (i - 1)) replayData of-     Just v -> return v+     Just v -> pure v      Nothing ->       Stepper.evmIO $ do        vm <- get@@ -533,8 +534,8 @@              -- pick all contracts with known compiler artifacts              fmap fromJust (Map.filter isJust $ Map.fromList [(addr, lookupCode c.contractcode dapp) | (addr, c)  <- Map.toList cs])            selected = [(addr,-                        fromMaybe (error ("no src found for: " <> show addr)) $-                          lookupCode (fromMaybe (error $ "contract not found: " <> show addr) $+                        fromMaybe (internalError $ "no src found for: " <> show addr) $+                          lookupCode (fromMaybe (internalError $ "contract not found: " <> show addr) $                             Map.lookup addr cs).contractcode dapp)                        | addr  <- targets]        -- go to IO and generate a random valid call to any known contract@@ -557,9 +558,9 @@          args <- generate $ genAbiValue (AbiTupleType $ Vector.fromList types)          let cd = abiMethod (sig <> "(" <> intercalate "," ((pack . show) <$> types) <> ")") args          -- increment timestamp with random amount-         timepassed <- num <$> generate (arbitrarySizedNatural :: Gen Word32)-         let ts = fromMaybe (error "symbolic timestamp not supported here") $ maybeLitWord vm.block.timestamp-         return (caller', target, cd, num ts + timepassed)+         timepassed <- into <$> generate (arbitrarySizedNatural :: Gen Word32)+         let ts = fromMaybe (internalError "symbolic timestamp not supported here") $ maybeLitWord vm.block.timestamp+         pure (caller', target, cd, into ts + timepassed)  let opts' = opts { testParams = testParams {address = target, caller = caller', timestamp = timestamp'}}      thisCallRLP = List [BS $ word160Bytes caller', BS $ word160Bytes target, BS cd, BS $ word256Bytes timestamp']  -- set the timestamp@@ -578,7 +579,7 @@       if x       then carryOn       else pure (False, List (thisCallRLP:history))-explorationStepper _ _ _ _ _ _  = error "malformed rlp"+explorationStepper _ _ _ _ _ _  = internalError "malformed rlp"  getTargetContracts :: UnitTestOptions -> Stepper [Addr] getTargetContracts UnitTestOptions{..} = do@@ -587,7 +588,7 @@       theAbi = (fromJust $ lookupCode contract'.contractcode dapp).abiMap       setUp  = abiKeccak (encodeUtf8 "targetContracts()")   case Map.lookup setUp theAbi of-    Nothing -> return []+    Nothing -> pure []     Just _ -> do       Stepper.evm $ abiCall testParams (Left ("targetContracts()", emptyAbi))       res <- Stepper.execFully@@ -595,15 +596,15 @@         Right (ConcreteBuf r) ->           let vs = case decodeAbiValue (AbiTupleType (Vector.fromList [AbiArrayDynamicType AbiAddressType])) (BSLazy.fromStrict r) of                 AbiTuple v -> v-                _ -> error "fix me with better types"+                _ -> internalError "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"+                      unAbiAddress _ = internalError "fix me with better types"                   in unAbiAddress <$> Vector.toList ts-                _ -> error "fix me with better types"+                _ -> internalError "fix me with better types"           in pure targets-        _ -> error "internal error: unexpected failure code"+        _ -> internalError "internal error: unexpected failure code"  exploreRun :: UnitTestOptions -> VM -> ABIMethod -> [ExploreTx] -> IO (Text, Either Text Text, VM) exploreRun opts@UnitTestOptions{..} initialVm testName replayTxs = do@@ -624,12 +625,12 @@       (,) <$> initialExplorationStepper opts testName replayTxs targets (length replayTxs)           <*> Stepper.evm get   if x-  then return ("\x1b[32m[PASS]\x1b[0m " <> testName <>  " (runs: " <> (pack $ show fuzzRuns) <>", depth: " <> pack (show depth) <> ")",+  then pure ("\x1b[32m[PASS]\x1b[0m " <> testName <>  " (runs: " <> (pack $ show fuzzRuns) <>", depth: " <> pack (show depth) <> ")",                Right (passOutput vm' opts testName), vm') -- no canonical "post vm"   else let replayText = if null replayTxs                         then "\nReplay data: '(" <> pack (show testName) <> "," <> pack (show (show (ByteStringS $ rlpencode counterex))) <> ")'"                         else " (replayed)"-       in return ("\x1b[31m[FAIL]\x1b[0m " <> testName <> replayText, Left  (failOutput vm' opts testName), vm')+       in pure ("\x1b[31m[FAIL]\x1b[0m " <> testName <> replayText, Left  (failOutput vm' opts testName), vm')  execTest :: UnitTestOptions -> VM -> ABIMethod -> AbiValue -> IO (Bool, VM) execTest opts@UnitTestOptions{..} vm testName args =@@ -647,8 +648,8 @@         <*> Stepper.evm get   if success   then-     let gasSpent = num testParams.gasCall - vm'.state.gas-         gasText = pack $ show (fromIntegral gasSpent :: Integer)+     let gasSpent = testParams.gasCall - vm'.state.gas+         gasText = pack $ show (into gasSpent :: Integer)      in         pure           ("\x1b[32m[PASS]\x1b[0m "@@ -726,17 +727,17 @@                    .|| (readStorage' (litAddr cheatCode) (Lit 0x6661696c65640000000000000000000000000000000000000000000000000000) store .== Lit 1)         postcondition = curry $ case shouldFail of           True -> \(_, post) -> case post of-                                  Success _ _ store -> failed store+                                  Success _ _ _ store -> failed store                                   _ -> PBool True           False -> \(_, post) -> case post of-                                   Success _ _ store -> PNeg (failed store)-                                   Failure _ _ -> PBool False-                                   Partial _ _ -> PBool True-                                   _ -> error "Internal Error: Invalid leaf node"+                                   Success _ _ _ store -> PNeg (failed store)+                                   Failure _ _ _ -> PBool False+                                   Partial _ _ _ -> PBool True+                                   _ -> internalError "Invalid leaf node"      vm' <- EVM.Stepper.interpret (Fetch.oracle solvers rpcInfo) vm $       Stepper.evm $ do-        popTrace+        pushTrace (EntryTrace testName)         makeTxCall testParams cd         get @@ -746,11 +747,11 @@     -- display results     if all isQed results     then do-      return ("\x1b[32m[PASS]\x1b[0m " <> testName, Right "", vm)+      pure ("\x1b[32m[PASS]\x1b[0m " <> testName, Right "", vm)     else do       let x = mapMaybe extractCex results       let y = symFailure opts testName (fst cd) types x-      return ("\x1b[31m[FAIL]\x1b[0m " <> testName, Left y, vm)+      pure ("\x1b[31m[FAIL]\x1b[0m " <> testName, Left y, vm)  symFailure :: UnitTestOptions -> Text -> Expr Buf -> [AbiType] -> [(Expr End, SMTCex)] -> Text symFailure UnitTestOptions {..} testName cd types failures' =@@ -761,25 +762,24 @@     , intercalate "\n" $ indentLines 2 . mkMsg <$> failures'     ]     where-      ctx = DappContext { info = dapp, env = mempty }       showRes = \case-                       Success _ _ _ -> if "proveFail" `isPrefixOf` testName-                                      then "Successful execution"-                                      else "Failed: DSTest Assertion Violation"-                       res ->-                         --let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env . EVM.contracts}-                         let ?context = ctx-                         in Text.pack $ prettyvmresult res+        Success _ _ _ _ -> if "proveFail" `isPrefixOf` testName+                       then "Successful execution"+                       else "Failed: DSTest Assertion Violation"+        res ->+          let ?context = DappContext { info = dapp, env = traceContext res}+          in Text.pack $ prettyvmresult res       mkMsg (leaf, cex) = Text.unlines         ["Counterexample:"         ,""         ,"  result:   " <> showRes leaf-        ,"  calldata: " <> let ?context = ctx in prettyCalldata cex cd testName types+        ,"  calldata: " <> let ?context =  DappContext dapp (traceContext leaf)+                           in prettyCalldata cex cd testName types         , case verbose of-            --Just _ -> unlines-              --[ ""-              --, unpack $ indentLines 2 (showTraceTree dapp vm)-              --]+            Just _ -> Text.unlines+              [ ""+              , indentLines 2 (showTraceTree' dapp leaf)+              ]             _ -> ""         ] @@ -792,22 +792,13 @@     argdata = Expr.drop 4 $ simplify $ subModel cex buf     vals = case decodeBuf tps argdata of              CAbi v -> v-             _ -> error $ "Internal Error: unable to abi decode function arguments:\n" <> (Text.unpack $ formatExpr argdata)+             _ -> internalError $ "unable to abi decode function arguments:\n" <> (Text.unpack $ formatExpr argdata)  showVal :: AbiValue -> Text showVal (AbiBytes _ bs) = formatBytes bs showVal (AbiAddress addr) = Text.pack  . show $ addr showVal v = Text.pack . show $ v ---- prettyCalldata :: (?context :: DappContext) => Expr Buf -> Text -> [AbiType]-> IO Text--- prettyCalldata buf sig types = do---   cdlen' <- num <$> SBV.getValue cdlen---   cd <- case buf of---     ConcreteBuf cd -> return $ BS.take cdlen' cd---     cd -> mapM (SBV.getValue . fromSized) (take cdlen' cd) <&> BS.pack---   pure $ (head (Text.splitOn "(" sig)) <> showCall types (ConcreteBuffer cd)- execSymTest :: UnitTestOptions -> ABIMethod -> (Expr Buf, [Prop]) -> Stepper (Expr End) execSymTest UnitTestOptions{ .. } method cd = do   -- Set up the call to the test method@@ -871,7 +862,7 @@ -- regular trace output. formatTestLog :: (?context :: DappContext) => Map W256 Event -> Expr Log -> Maybe Text formatTestLog _ (LogEntry _ _ []) = Nothing-formatTestLog _ (GVar _) = error "unexpected global variable"+formatTestLog _ (GVar _) = internalError "unexpected global variable" formatTestLog events (LogEntry _ args (topic:_)) =   case maybeLitWord topic >>= \t1 -> (Map.lookup t1 events) of     Nothing -> Nothing@@ -916,10 +907,10 @@           log_named =             let (key, val) = case take 2 (textValues ts args) of                   [k, v] -> (k, v)-                  _ -> error "shouldn't happen"+                  _ -> internalError "shouldn't happen"             in Just $ unquote key <> ": " <> val           showDecimal dec val =-            pack $ show $ Decimal (num dec) val+            pack $ show $ Decimal (unsafeInto dec) val           log_named_decimal =             case args of               (ConcreteBuf b) ->@@ -949,7 +940,7 @@   assign (#state % #gas) params.gasCall   origin' <- fromMaybe (initialContract (RuntimeCode (ConcreteRuntimeCode ""))) <$> use (#env % #contracts % at params.origin)   let originBal = origin'.balance-  when (originBal < params.gasprice * (num params.gasCall)) $ error "insufficient balance for gas cost"+  when (originBal < params.gasprice * (into params.gasCall)) $ internalError "insufficient balance for gas cost"   vm <- get   put $ initTx vm @@ -995,20 +986,20 @@    (miner,ts,blockNum,ran,limit,base) <-     case rpc of-      Nothing  -> return (0,Lit 0,0,0,0,0)+      Nothing  -> pure (0,Lit 0,0,0,0,0)       Just url -> Fetch.fetchBlockFrom block' url >>= \case-        Nothing -> error "Could not fetch block"-        Just Block{..} -> return (  coinbase-                                      , timestamp-                                      , number-                                      , prevRandao-                                      , gaslimit-                                      , baseFee-                                      )+        Nothing -> internalError "Could not fetch block"+        Just Block{..} -> pure ( coinbase+                               , timestamp+                               , number+                               , prevRandao+                               , gaslimit+                               , baseFee+                               )   let     getWord s def = maybe def read <$> lookupEnv s     getAddr s def = maybe def read <$> lookupEnv s-    ts' = fromMaybe (error "Internal Error: received unexpected symbolic timestamp via rpc") (maybeLitWord ts)+    ts' = fromMaybe (internalError "received unexpected symbolic timestamp via rpc") (maybeLitWord ts)    TestVMParams     <$> getAddr "DAPP_TEST_ADDRESS" (createAddress ethrunAddress 1)

@@ -1,7 +1,5 @@ module EVM.Test.BlockchainTests where -import Prelude hiding (Word)- import EVM (initialContract, makeVm) import EVM.Concrete qualified as EVM import EVM.Dapp (emptyDapp)@@ -37,6 +35,7 @@ import Test.Tasty import Test.Tasty.ExpectedFailure import Test.Tasty.HUnit+import Witch (into, unsafeInto)  type Storage = Map W256 W256 @@ -146,7 +145,7 @@   Right allTests <- parseBCSuite <$> LazyByteString.readFile (repo </> file)   let x = case filter (\(name, _) -> name == test) $ Map.toList allTests of         [(_, x')] -> x'-        _ -> error "test not found"+        _ -> internalError "test not found"   let vm0 = vmForCase x   result <- withSolvers Z3 0 Nothing $ \solvers ->     TTY.runFromVM solvers Nothing Nothing emptyDapp vm0@@ -216,7 +215,7 @@     storageEqual = s1 == s2     codeEqual = case (c1 ^. #contractcode, c2 ^. #contractcode) of       (RuntimeCode a', RuntimeCode b') -> a' == b'-      _ -> error "unexpected code"+      _ -> internalError "unexpected code"  checkExpectedContracts :: VM -> Map Addr (Contract, Storage) -> (Bool, Bool, Bool, Bool, Bool) checkExpectedContracts vm expected =@@ -236,7 +235,7 @@       EmptyStore -> mempty       AbstractStore -> mempty -- error "AbstractStore, should this be handled?"       SStore {} -> mempty -- error "SStore, should this be handled?"-      GVar _ -> error "unexpected global variable"+      GVar _ -> internalError "unexpected global variable"  clearStorage :: (Contract, Storage) -> (Contract, Storage) clearStorage (c, _) = (c, mempty)@@ -360,7 +359,7 @@          , caller        = litAddr origin          , initialStorage = EmptyStore          , origin        = origin-         , gas           = tx.gasLimit  - fromIntegral (txGasCost feeSchedule tx)+         , gas           = tx.gasLimit - txGasCost feeSchedule tx          , baseFee       = block.baseFee          , priorityFee   = priorityFee tx block.baseFee          , gaslimit      = tx.gasLimit@@ -419,7 +418,7 @@   origin        <- sender tx   originBalance <- (view #balance) <$> view (at origin) cs'   originNonce   <- (view #nonce)   <$> view (at origin) cs'-  let gasDeposit = (effectiveprice tx block.baseFee) * (num tx.gasLimit)+  let gasDeposit = (effectiveprice tx block.baseFee) * (into tx.gasLimit)   if gasDeposit + tx.value <= originBalance     && tx.nonce == originNonce && block.baseFee <= maxBaseFee tx   then Just ()@@ -439,7 +438,7 @@                         RuntimeCode (ConcreteRuntimeCode b) -> not (BS.null b)                         _ -> True       badNonce = prevNonce /= 0-      initCodeSizeExceeded = BS.length tx.txdata > (num maxCodeSize * 2)+      initCodeSizeExceeded = BS.length tx.txdata > (unsafeInto maxCodeSize * 2)   if isCreate && (badNonce || nonEmptyAccount || initCodeSizeExceeded)   then mzero   else@@ -450,7 +449,7 @@   let     a = x.checkContracts     cs = Map.map fst a-    st = Map.mapKeys num $ Map.map snd a+    st = Map.mapKeys into $ Map.map snd a     vm = makeVm x.vmOpts       & set (#env % #contracts) cs       & set (#env % #storage) (ConcreteStore st)

@@ -1,3 +1,5 @@+{-# LANGUAGE DataKinds #-}+ {-| Module      : Tracing Description : Tests to fuzz concrete tracing, and symbolic execution@@ -7,77 +9,66 @@ of this code, we also generate a symbolic expression then evaluate it concretely through Expr.simplify, then check that against evmtool's output. -}--{-# Language DataKinds #-}-{-# Language DuplicateRecordFields #-}-{-# LANGUAGE DeriveGeneric #-}- module EVM.Test.Tracing where +import Control.Monad (when)+import Control.Monad.Operational qualified as Operational+import Control.Monad.State.Strict (StateT(..), liftIO, runState)+import Control.Monad.State.Strict qualified as State+import Data.Aeson ((.:), (.:?))+import Data.Aeson qualified as JSON import Data.ByteString (ByteString)-import System.Directory-import System.IO-import qualified Data.Word-import GHC.Generics+import Data.ByteString qualified as BS+import Data.ByteString.Char8 qualified as Char8+import Data.Maybe (fromJust, isJust, isNothing)+import Data.Map.Strict qualified as Map+import Data.Text.IO qualified as T+import Data.Vector qualified as Vector+import Data.Word (Word8, Word64)+import GHC.Generics (Generic)+import GHC.IO.Exception (ExitCode(ExitSuccess)) import Numeric (showHex)-import qualified Paths_hevm as Paths--import Prelude hiding (fail, LT, GT)--import qualified Data.ByteString as BS-import Data.Maybe-import Data.List qualified (length)-import Test.Tasty-import Test.Tasty.QuickCheck hiding (Failure, Success)+import Paths_hevm qualified as Paths+import System.Directory (removeFile)+import System.Process (readProcessWithExitCode)+import Test.QuickCheck (elements) import Test.QuickCheck.Instances.Text() import Test.QuickCheck.Instances.Natural() import Test.QuickCheck.Instances.ByteString()-import Test.QuickCheck (elements)-import Test.Tasty.HUnit-import qualified Data.Aeson as JSON-import Data.Aeson ((.:), (.:?))-import Data.ByteString.Char8 qualified as Char8+import Test.Tasty (testGroup, TestTree)+import Test.Tasty.HUnit (assertEqual)+import Test.Tasty.QuickCheck hiding (Failure, Success)+import Witch (into) -import qualified Control.Monad (when)-import qualified Control.Monad.Operational as Operational (view, ProgramViewT(..), ProgramView)-import Control.Monad.State.Strict hiding (state)-import Control.Monad.State.Strict qualified as State import Optics.Core hiding (pre) import Optics.State import Optics.Zoom -import qualified Data.Vector as Vector-import qualified Data.Map.Strict as Map--import EVM-import EVM.SymExec-import EVM.Assembler-import EVM.Op hiding (getOp)-import EVM.Exec-import EVM.Types-import EVM.Format (bsToHex)-import EVM.Traversals+import EVM (makeVm, initialContract, exec1)+import EVM.Assembler (assemble)+import EVM.Expr qualified as Expr+import EVM.Exec (ethrunAddress)+import EVM.Fetch qualified as Fetch+import EVM.Format (bsToHex, formatBinary) import EVM.Concrete (createAddress)-import qualified EVM.FeeSchedule as FeeSchedule-import EVM.Solvers-import qualified EVM.Expr as Expr-import qualified Data.Text.IO as T-import qualified EVM.Stepper as Stepper-import qualified EVM.Fetch as Fetch-import System.Process-import qualified EVM.Transaction-import EVM.Format (formatBinary)+import EVM.FeeSchedule qualified as FeeSchedule+import EVM.Op (intToOpName) import EVM.Sign (deriveAddr)-import GHC.IO.Exception (ExitCode(ExitSuccess))+import EVM.Solvers+import EVM.Stepper qualified as Stepper+import EVM.SymExec+import EVM.Traversals (mapExpr)+import EVM.Transaction qualified+import EVM.Types  data VMTrace =   VMTrace   { tracePc      :: Int   , traceOp      :: Int   , traceStack   :: [W256]-  , traceMemSize :: Data.Word.Word64+  , traceMemSize :: Word64   , traceDepth   :: Int-  , traceGas     :: Data.Word.Word64+  , traceGas     :: Word64   , traceError   :: Maybe String   } deriving (Generic, Show) @@ -120,7 +111,7 @@     <*> v .:? "error"  mkBlockHash:: Int -> Expr 'EWord-mkBlockHash x = (num x :: Integer) & show & Char8.pack & EVM.Types.keccak' & Lit+mkBlockHash x = (into x :: Integer) & show & Char8.pack & EVM.Types.keccak' & Lit  blockHashesDefault :: Map.Map Int W256 blockHashesDefault = Map.fromList [(x, forceLit $ mkBlockHash x) | x<- [1..256]]@@ -129,7 +120,6 @@   EVMToolOutput     { output :: ByteStringS     , gasUsed :: W256-    , time :: Integer     } deriving (Generic, Show)  instance JSON.FromJSON EVMToolOutput@@ -167,7 +157,7 @@                 tstamp :: W256                 tstamp = case (b.timestamp) of                               Lit a -> a-                              _ -> error "Timestamp needs to be a Lit"+                              _ -> internalError "Timestamp needs to be a Lit"  emptyEvmToolEnv :: EVMToolEnv emptyEvmToolEnv = EVMToolEnv { coinbase = 0@@ -262,9 +252,9 @@ evmSetup contr txData gaslimitExec = (txn, evmEnv, contrAlloc, fromAddress, toAddress, sk)   where     contrLits = assemble $ getOpData contr-    toW8fromLitB :: Expr 'Byte -> Data.Word.Word8+    toW8fromLitB :: Expr 'Byte -> Word8     toW8fromLitB (LitByte a) = a-    toW8fromLitB _ = error "Cannot convert non-litB"+    toW8fromLitB _ = internalError "Cannot convert non-litB"      bitcode = BS.pack . Vector.toList $ toW8fromLitB <$> contrLits     contrAlloc = EVMToolAlloc{ balance = 0xa493d65e20984bc@@ -331,10 +321,10 @@                                , "--trace" , "trace.json"                                , "--output.result", "result.json"                                ] ""-  Control.Monad.when (exitCode /= ExitSuccess) $ do-                   putStrLn $ "evmtool exited with code " <> show exitCode-                   putStrLn $ "evmtool stderr output:" <> show evmtoolStderr-                   putStrLn $ "evmtool stdout output:" <> show evmtoolStdout+  when (exitCode /= ExitSuccess) $ do+    putStrLn $ "evmtool exited with code " <> show exitCode+    putStrLn $ "evmtool stderr output:" <> show evmtoolStderr+    putStrLn $ "evmtool stdout output:" <> show evmtoolStdout   evmtoolResult <- JSON.decodeFileStrict "result.json" :: IO (Maybe EVMToolResult)   return evmtoolResult @@ -366,14 +356,14 @@                           -- putStrLn $ "trace element match. " <> (intToOpName aOp) <> " pc: " <> (show aPc)                           return () -      Control.Monad.when (isJust b.error) $ do-                           putStrLn $ "Error by evmtool: " <> (show b.error)-                           putStrLn $ "Error by HEVM   : " <> (show a.traceError)+      when (isJust b.error) $ do+        putStrLn $ "Error by evmtool: " <> (show b.error)+        putStrLn $ "Error by HEVM   : " <> (show a.traceError) -      Control.Monad.when (aStack /= bStack) $ do-                          putStrLn "stacks don't match:"-                          putStrLn $ "HEVM's stack   : " <> (show aStack)-                          putStrLn $ "evmtool's stack: " <> (show bStack)+      when (aStack /= bStack) $ do+        putStrLn "stacks don't match:"+        putStrLn $ "HEVM's stack   : " <> (show aStack)+        putStrLn $ "evmtool's stack: " <> (show bStack)       if aOp == bOp && aStack == bStack && aPc == bPc && aGas == bGas then go ax bx       else pure False @@ -485,7 +475,7 @@   let     memsize = vm.state.memorySize   in VMTrace { tracePc = vm.state.pc-             , traceOp = num $ getOp vm+             , traceOp = into $ getOp vm              , traceGas = vm.state.gas              , traceMemSize = memsize              -- increment to match geth format@@ -524,7 +514,7 @@     gasUsed' = vm.tx.gaslimit - vm.state.gas     res = case vm.result of       Just (VMSuccess (ConcreteBuf b)) -> (ByteStringS b)-      Just (VMSuccess x) -> error $ "unhandled: " <> (show x)+      Just (VMSuccess x) -> internalError $ "unhandled: " <> (show x)       Just (VMFailure (Revert (ConcreteBuf b))) -> (ByteStringS b)       Just (VMFailure _) -> ByteStringS mempty       _ -> ByteStringS mempty@@ -554,7 +544,7 @@       -- Update error text for last trace element       (a, b) <- State.get       let updatedElem = (last b) {traceError = (vmtrace vm0).traceError}-          updatedTraces = take ((Data.List.length b)-1) b ++ [updatedElem]+          updatedTraces = take (length b - 1) b ++ [updatedElem]       State.put (a, updatedTraces)       pure vm0     Just _ -> pure vm0@@ -587,7 +577,7 @@             m <- liftIO (fetcher q)             zoom _1 (State.state (runState m)) >> interpretWithTrace fetcher (k ())         Stepper.Ask _ ->-          error "cannot make choice in this interpreter"+          internalError "cannot make choice in this interpreter"         Stepper.IOAct q ->           zoom _1 (StateT (runStateT q)) >>= interpretWithTrace fetcher . k         Stepper.EVM m ->@@ -805,14 +795,14 @@ randItem :: [a] -> IO a randItem = generate . Test.QuickCheck.elements -getOp :: VM -> Data.Word.Word8+getOp :: VM -> Word8 getOp vm =   let pcpos  = vm ^. #state % #pc       code' = vm ^. #state % #code       xs = case code' of-        InitCode _ _ -> error "InitCode instead of RuntimeCode"+        InitCode _ _ -> internalError "InitCode instead of RuntimeCode"         RuntimeCode (ConcreteRuntimeCode xs') -> BS.drop pcpos xs'-        RuntimeCode (SymbolicRuntimeCode _) -> error "RuntimeCode is symbolic"+        RuntimeCode (SymbolicRuntimeCode _) -> internalError "RuntimeCode is symbolic"   in if xs == BS.empty then 0                        else BS.head xs @@ -841,7 +831,7 @@               concretizedExpr = concretize expr (ConcreteBuf txData)               simplConcExpr = Expr.simplify concretizedExpr               getReturnVal :: Expr End -> Maybe ByteString-              getReturnVal (Success _ (ConcreteBuf bs) _) = Just bs+              getReturnVal (Success _ _ (ConcreteBuf bs) _) = Just bs               getReturnVal _ = Nothing               simplConcrExprRetval = getReturnVal simplConcExpr             traceOK <- compareTraces hevmTrace (evmtoolTraceOutput.trace)

@@ -1,24 +1,24 @@-{-# Language QuasiQuotes #-}+{-# LANGUAGE QuasiQuotes #-}  module EVM.Test.Utils where  import Data.String.Here-import Data.Text+import Data.Text (Text)+import Data.Text qualified as T+import Data.Text.IO qualified as T import GHC.IO.Handle (hClose)-import qualified Paths_hevm as Paths+import Paths_hevm qualified as Paths import System.Directory import System.IO.Temp import System.Process import System.Exit-import qualified Data.Text as T-import qualified Data.Text.IO as T +import EVM.Dapp (dappInfo, emptyDapp)+import EVM.Fetch (RpcInfo) import EVM.Solidity import EVM.Solvers-import EVM.Dapp+import EVM.TTY qualified as TTY import EVM.UnitTest-import EVM.Fetch (RpcInfo)-import qualified EVM.TTY as TTY  runSolidityTestCustom :: FilePath -> Text -> Maybe Integer -> Bool -> RpcInfo -> ProjectType -> IO Bool runSolidityTestCustom testFile match maxIter ffiAllowed rpcinfo projectType = do@@ -75,6 +75,7 @@   createDirectory (root <> "/out")   T.writeFile (root <> "/out/dapp.sol.json") json   readBuildOutput root DappTools+compile CombinedJSON _root _src = error "unsupported" compile Foundry root src = do   createDirectory (root <> "/src")   writeFile (root <> "/src/unit-tests.t.sol") =<< readFile =<< Paths.getDataFileName src

@@ -56,20 +56,21 @@         assertTrue(false);     } -    function prove_transfer(uint supply, address usr, uint amt) public {-        if (amt > supply) return; // no underflow--        token.mint(address(this), supply);--        uint prebal = token.balanceOf(usr);-        token.transfer(usr, amt);-        uint postbal = token.balanceOf(usr);--        uint expected = usr == address(this)-                        ? 0    // self transfer is a noop-                        : amt; // otherwise `amt` has been transfered to `usr`-        assertEq(expected, postbal - prebal);-    }+    // Takes too long, disabling here, moving to benchmarks+    // function prove_transfer(uint supply, address usr, uint amt) public {+    //     if (amt > supply) return; // no underflow+    //+    //     token.mint(address(this), supply);+    //+    //     uint prebal = token.balanceOf(usr);+    //     token.transfer(usr, amt);+    //     uint postbal = token.balanceOf(usr);+    //+    //     uint expected = usr == address(this)+    //                     ? 0    // self transfer is a noop+    //                     : amt; // otherwise `amt` has been transfered to `usr`+    //     assertEq(expected, postbal - prebal);+    // }      function prove_burn(uint supply, uint amt) public {         if (amt > supply) return; // no undeflow

@@ -1,4 +1,4 @@-{-# Language DataKinds #-}+{-# LANGUAGE DataKinds #-}  module Main where @@ -30,7 +30,7 @@     [ testCase "pre-merge-block" $ do         let block = BlockNumber 15537392         (cb, numb, basefee, prevRan) <- fetchBlockFrom block testRpc >>= \case-                      Nothing -> error "Could not fetch block"+                      Nothing -> internalError "Could not fetch block"                       Just Block{..} -> return ( coinbase                                                    , number                                                    , baseFee@@ -44,7 +44,7 @@     , testCase "post-merge-block" $ do         let block = BlockNumber 16184420         (cb, numb, basefee, prevRan) <- fetchBlockFrom block testRpc >>= \case-                      Nothing -> error "Could not fetch block"+                      Nothing -> internalError "Could not fetch block"                       Just Block{..} -> return ( coinbase                                                    , number                                                    , baseFee@@ -75,12 +75,12 @@         let           postStore = case postVm.env.storage of             ConcreteStore s -> s-            _ -> error "ConcreteStore expected"+            _ -> internalError "ConcreteStore expected"           wethStore = fromJust $ Map.lookup 0xC02aaA39b223FE8D0A0e5C4F27eAD9083C756Cc2 postStore           receiverBal = fromJust $ Map.lookup (keccak' (word256Bytes 0xdead <> word256Bytes 0x3)) wethStore           msg = case postVm.result of             Just (VMSuccess m) -> m-            _ -> error "VMSuccess expected"+            _ -> internalError "VMSuccess expected"         assertEqual "should succeed" msg (ConcreteBuf $ word256Bytes 0x1)         assertEqual "should revert" receiverBal (W256 $ 2595433725034301 + wad) @@ -90,7 +90,7 @@         let           blockNum = 16198552           calldata' = symCalldata "transfer(address,uint256)" [AbiAddressType, AbiUIntType 256] ["0xdead"] (AbstractBuf "txdata")-          postc _ (Failure _ (Revert _)) = PBool False+          postc _ (Failure _ _ (Revert _)) = PBool False           postc _ _ = PBool True         vm <- weth9VM blockNum calldata'         (_, [Cex (_, model)]) <- withSolvers Z3 1 Nothing $ \solvers ->@@ -111,11 +111,11 @@ vmFromRpc :: W256 -> (Expr Buf, [Prop]) -> Expr EWord -> Expr EWord -> Addr -> IO VM vmFromRpc blockNum calldata' callvalue' caller' address' = do   ctrct <- fetchContractFrom (BlockNumber blockNum) testRpc address' >>= \case-        Nothing -> error $ "contract not found: " <> show address'+        Nothing -> internalError $ "contract not found: " <> show address'         Just contract' -> return contract'    blk <- fetchBlockFrom (BlockNumber blockNum) testRpc >>= \case-    Nothing -> error "could not fetch block"+    Nothing -> internalError "could not fetch block"     Just b -> pure b    pure $ makeVm $ VMOpts

@@ -1,29 +1,31 @@-{-# Language QuasiQuotes #-}-{-# Language DataKinds #-}-{-# Language DuplicateRecordFields #-}-{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE QuasiQuotes #-}  module Main where -import Data.Text (Text)-import Data.ByteString (ByteString)-import Data.Bits hiding (And, Xor)-import System.Directory-import System.IO-import GHC.Natural-import Text.RE.TDFA.String-import Text.RE.Replace-import Data.Time-import System.Environment--import Prelude hiding (fail, LT, GT)+import Prelude hiding (LT, GT) -import qualified Data.ByteString as BS-import qualified Data.ByteString.Base16 as BS16+import Control.Monad.State.Strict+import Data.Bits hiding (And, Xor)+import Data.ByteString (ByteString)+import Data.ByteString qualified as BS+import Data.ByteString.Base16 qualified as BS16+import Data.Binary.Put (runPut)+import Data.Binary.Get (runGetOrFail)+import Data.DoubleWord+import Data.List qualified as List+import Data.Map.Strict qualified as Map import Data.Maybe+import Data.String.Here+import Data.Text (Text)+import Data.Text qualified as T+import Data.Time (diffUTCTime, getCurrentTime) import Data.Typeable-import Data.List qualified (elemIndex)-import Data.DoubleWord+import Data.Vector qualified as Vector+import GHC.Conc (getNumProcessors)+import Numeric.Natural (Natural)+import System.Directory+import System.Environment import Test.Tasty import Test.Tasty.QuickCheck hiding (Failure, Success) import Test.QuickCheck.Instances.Text()@@ -32,41 +34,33 @@ import Test.Tasty.HUnit import Test.Tasty.Runners hiding (Failure, Success) import Test.Tasty.ExpectedFailure-import EVM.Test.Tracing qualified as Tracing+import Text.RE.TDFA.String+import Text.RE.Replace+import Witch (into, unsafeInto) -import Control.Monad.State.Strict hiding (state) import Optics.Core hiding (pre, re) import Optics.State import Optics.Operators.Unsafe -import qualified Data.Vector as Vector-import Data.String.Here-import qualified Data.Map.Strict as Map--import Data.Binary.Put (runPut)-import Data.Binary.Get (runGetOrFail)- import EVM hiding (choose)-import EVM.SymExec import EVM.ABI+import EVM.Concrete (createAddress) import EVM.Exec-import qualified EVM.Patricia as Patricia+import EVM.Expr qualified as Expr+import EVM.Fetch qualified as Fetch+import EVM.Format (hexText)+import EVM.Patricia qualified as Patricia import EVM.Precompiled import EVM.RLP-import EVM.Solidity-import EVM.Types-import EVM.Format (hexText)-import EVM.Traversals-import EVM.Concrete (createAddress) import EVM.SMT hiding (one)+import EVM.Solidity import EVM.Solvers-import qualified EVM.Expr as Expr-import qualified EVM.Stepper as Stepper-import qualified EVM.Fetch as Fetch-import qualified Data.Text as T-import Data.List (isSubsequenceOf)+import EVM.Stepper qualified as Stepper+import EVM.SymExec+import EVM.Test.Tracing qualified as Tracing import EVM.Test.Utils-import GHC.Conc (getNumProcessors)+import EVM.Traversals+import EVM.Types  main :: IO () main = defaultMain tests@@ -109,12 +103,12 @@             vm2 = case vm1.result of                     Just (HandleEffect (Query (PleaseFetchContract _addr continue))) ->                       execState (continue dummyContract) vm1-                    _ -> error "unexpected result"+                    _ -> internalError "unexpected result"             -- then it should fetch the slow             vm3 = case vm2.result of                     Just (HandleEffect (Query (PleaseFetchSlot _addr _slot continue))) ->                       execState (continue 1337) vm2-                    _ -> error "unexpected result"+                    _ -> internalError "unexpected result"             -- perform the same access as for vm1             vm4 = execState (EVM.accessStorage 0 (Lit 0) (pure . pure ())) vm3 @@ -136,8 +130,8 @@   -- applying some simplification rules, and then using the smt encoding to   -- check that the simplified version is semantically equivalent to the   -- unsimplified one-  , testGroup "SimplifierTests"-    [ testProperty "buffer-simplification" $ \(expr :: Expr Buf) -> ioProperty $ do+  , adjustOption (\(Test.Tasty.QuickCheck.QuickCheckTests n) -> Test.Tasty.QuickCheck.QuickCheckTests (min n 50)) $ testGroup "SimplifierTests"+    [ testProperty  "buffer-simplification" $ \(expr :: Expr Buf) -> ioProperty $ do         let simplified = Expr.simplify expr         checkEquiv expr simplified     , testProperty "store-simplification" $ \(expr :: Expr Storage) -> ioProperty $ do@@ -377,7 +371,7 @@             [y] AbiBytesDynamicType           let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of                 AbiTuple (Vector.toList -> [e]) -> e-                _ -> error "AbiTuple expected"+                _ -> internalError "AbiTuple expected"           let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [y])           assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded) @@ -387,7 +381,7 @@             [x', y'] AbiBytesDynamicType           let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of                 AbiTuple (Vector.toList -> [e]) -> e-                _ -> error "AbiTuple expected"+                _ -> internalError "AbiTuple expected"           let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [x',y'])           assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded) @@ -401,7 +395,7 @@             |] (abiMethod "foo(function)" (AbiTuple (Vector.singleton y)))           let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of                 AbiTuple (Vector.toList -> [e]) -> e-                _ -> error "AbiTuple expected"+                _ -> internalError "AbiTuple expected"           let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [y])           assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded)     ]@@ -693,10 +687,8 @@         runSolidityTest testFile "prove_add" >>= assertEqual "test result" False         --runSolidityTest testFile "prove_smtTimeout" >>= assertEqual "test result" False         runSolidityTest testFile "prove_multi" >>= assertEqual "test result" False-        runSolidityTest testFile "prove_mul" >>= assertEqual "test result" False         -- TODO: implement overflow checking optimizations and enable, currently this runs forever         --runSolidityTest testFile "prove_distributivity" >>= assertEqual "test result" False-        runSolidityTest testFile "prove_transfer" >>= assertEqual "test result" False     , testCase "Loop-Tests" $ do         let testFile = "test/contracts/pass/loops.sol"         runSolidityTestCustom testFile "prove_loop" (Just 10) False Nothing Foundry >>= assertEqual "test result" True@@ -715,6 +707,9 @@         let testFile = "test/contracts/fail/cheatCodes.sol"         runSolidityTestCustom testFile "testBadFFI" Nothing False Nothing Foundry >>= assertEqual "test result" False         runSolidityTestCustom testFile "test_prank_underflow" Nothing False Nothing Foundry >>= assertEqual "test result" False+    , testCase "Unwind" $ do+        let testFile = "test/contracts/pass/unwind.sol"+        runSolidityTest testFile ".*" >>= assertEqual "test result" True     ]   , testGroup "max-iterations"     [ testCase "concrete-loops-reached" $ do@@ -971,23 +966,6 @@         (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts         putStrLn "sdiv works as expected"       ,-     testCase "opcode-div-zero-2" $ do-        Just c <- solcRuntime "MyContract"-            [i|-            contract MyContract {-              function fun(uint256 val) external pure {-                uint out;-                assembly {-                  out := div(0, val)-                }-                assert(out == 0);--              }-            }-            |]-        (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts-        putStrLn "sdiv works as expected"-     ,      testCase "opcode-sdiv-zero-1" $ do         Just c <- solcRuntime "MyContract"             [i|@@ -1162,52 +1140,6 @@         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts         putStrLn "XOR works as expected"       ,-      testCase "opcode-addmod-no-overflow" $ do-        Just c <- solcRuntime "MyContract"-            [i|-            contract MyContract {-              function fun(uint8 a, uint8 b, uint8 c) external pure {-                require(a < 4);-                require(b < 4);-                require(c < 4);-                uint16 r1;-                uint16 r2;-                uint16 g2;-                assembly {-                  r1 := add(a,b)-                  r2 := mod(r1, c)-                  g2 := addmod (a, b, c)-                }-                assert (r2 == g2);-              }-            }-            |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint8,uint8,uint8)" [AbiUIntType 8, AbiUIntType 8, AbiUIntType 8])) [] defaultVeriOpts-        putStrLn "ADDMOD is fine on NON overflow values"-      ,-      testCase "opcode-mulmod-no-overflow" $ do-        Just c <- solcRuntime "MyContract"-            [i|-            contract MyContract {-              function fun(uint8 a, uint8 b, uint8 c) external pure {-                require(a < 4);-                require(b < 4);-                require(c < 4);-                uint16 r1;-                uint16 r2;-                uint16 g2;-                assembly {-                  r1 := mul(a,b)-                  r2 := mod(r1, c)-                  g2 := mulmod (a, b, c)-                }-                assert (r2 == g2);-              }-            }-            |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint8,uint8,uint8)" [AbiUIntType 8, AbiUIntType 8, AbiUIntType 8])) [] defaultVeriOpts-        putStrLn "MULMOD is fine on NON overflow values"-      ,       testCase "opcode-div-res-zero-on-div-by-zero" $ do         Just c <- solcRuntime "MyContract"             [i|@@ -1238,16 +1170,16 @@           |]         let pre preVM = let (x, y) = case getStaticAbiArgs 2 preVM of                                        [x', y'] -> (x', y')-                                       _ -> error "expected 2 args"+                                       _ -> internalError "expected 2 args"                         in (x .<= Expr.add x y)                         -- TODO check if it's needed                            .&& preVM.state.callvalue .== Lit 0             post prestate leaf =               let (x, y) = case getStaticAbiArgs 2 prestate of                              [x', y'] -> (x', y')-                             _ -> error "expected 2 args"+                             _ -> internalError "expected 2 args"               in case leaf of-                   Success _ b _ -> (ReadWord (Lit 0) b) .== (Add x y)+                   Success _ _ b _ -> (ReadWord (Lit 0) b) .== (Add x y)                    _ -> PBool True         (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s safeAdd (Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts AbstractStore (Just pre) (Just post)         putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"@@ -1264,16 +1196,16 @@           |]         let pre preVM = let (x, y) = case getStaticAbiArgs 2 preVM of                                        [x', y'] -> (x', y')-                                       _ -> error "expected 2 args"+                                       _ -> internalError "expected 2 args"                         in (x .<= Expr.add x y)                            .&& (x .== y)                            .&& preVM.state.callvalue .== Lit 0             post prestate leaf =               let (_, y) = case getStaticAbiArgs 2 prestate of                              [x', y'] -> (x', y')-                             _ -> error "expected 2 args"+                             _ -> internalError "expected 2 args"               in case leaf of-                   Success _ b _ -> (ReadWord (Lit 0) b) .== (Mul (Lit 2) y)+                   Success _ _ b _ -> (ReadWord (Lit 0) b) .== (Mul (Lit 2) y)                    _ -> PBool True         (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->           verifyContract s safeAdd (Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts AbstractStore (Just pre) (Just post)@@ -1296,11 +1228,11 @@             post prestate leaf =               let y = case getStaticAbiArgs 1 prestate of                         [y'] -> y'-                        _ -> error "expected 1 arg"+                        _ -> internalError "expected 1 arg"                   this = Expr.litAddr $ prestate.state.codeContract                   prex = Expr.readStorage' this (Lit 0) prestate.env.storage               in case leaf of-                Success _ _ postStore -> Expr.add prex (Expr.mul (Lit 2) y) .== (Expr.readStorage' this (Lit 0) postStore)+                Success _ _ _ postStore -> Expr.add prex (Expr.mul (Lit 2) y) .== (Expr.readStorage' this (Lit 0) postStore)                 _ -> PBool True         (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts AbstractStore (Just pre) (Just post)         putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"@@ -1350,13 +1282,13 @@               post prestate poststate =                 let (x,y) = case getStaticAbiArgs 2 prestate of                         [x',y'] -> (x',y')-                        _ -> error "expected 2 args"+                        _ -> internalError "expected 2 args"                     this = Expr.litAddr $ prestate.state.codeContract                     prestore = prestate.env.storage                     prex = Expr.readStorage' this x prestore                     prey = Expr.readStorage' this y prestore                 in case poststate of-                     Success _ _ poststore -> let+                     Success _ _ _ poststore -> let                            postx = Expr.readStorage' this x poststore                            posty = Expr.readStorage' this y poststore                        in Expr.add prex prey .== Expr.add postx posty@@ -1384,13 +1316,13 @@               post prestate poststate =                 let (x,y) = case getStaticAbiArgs 2 prestate of                         [x',y'] -> (x',y')-                        _ -> error "expected 2 args"+                        _ -> internalError "expected 2 args"                     this = Expr.litAddr $ prestate.state.codeContract                     prestore =  prestate.env.storage                     prex = Expr.readStorage' this x prestore                     prey = Expr.readStorage' this y prestore                 in case poststate of-                     Success _ _ poststore -> let+                     Success _ _ _ poststore -> let                            postx = Expr.readStorage' this x poststore                            posty = Expr.readStorage' this y poststore                        in Expr.add prex prey .== Expr.add postx posty@@ -1412,7 +1344,7 @@               }              }             |]-          (_, [Cex (Failure _ (Revert msg), _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo()" [])) [] defaultVeriOpts+          (_, [Cex (Failure _ _ (Revert msg), _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo()" [])) [] defaultVeriOpts           assertEqual "incorrect revert msg" msg (ConcreteBuf $ panicMsg 0x01)         ,         testCase "simple-assert-2" $ do@@ -1440,7 +1372,7 @@             |]           (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           let ints = map (flip getVar "arg1") [a,b]-          assertBool "0 must be one of the Cex-es" $ isJust $ Data.List.elemIndex 0 ints+          assertBool "0 must be one of the Cex-es" $ isJust $ List.elemIndex 0 ints           putStrLn "expected 2 counterexamples found, one Cex is the 0 value"         ,         testCase "assert-fail-notequal" $ do@@ -1721,24 +1653,6 @@           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts           putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,-        testCase "injectivity of keccak all pairs (32 bytes)" $ do-          Just c <- solcRuntime "A"-            [i|-            contract A {-              function f(uint x, uint y, uint z) public pure {-                bytes32 w; bytes32 u; bytes32 v;-                w = keccak256(abi.encode(x));-                u = keccak256(abi.encode(y));-                v = keccak256(abi.encode(z));-                if (w == u) assert(x==y);-                if (w == v) assert(x==z);-                if (u == v) assert(y==z);-              }-            }-            |]-          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"-        ,         testCase "injectivity of keccak contrapositive (32 bytes)" $ do           Just c <- solcRuntime "A"             [i|@@ -1824,22 +1738,6 @@           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,-        testCase "keccak soundness" $ do-          Just c <- solcRuntime "C"-            [i|-              contract C {-                mapping (uint => mapping (uint => uint)) maps;--                  function f(uint x, uint y) public view {-                  assert(maps[y][0] == maps[x][0]);-                }-              }-            |]--          -- should find a counterexample-          (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts-          putStrLn "expected counterexample found"-        ,         testCase "multiple-contracts" $ do           let code' =                 [i|@@ -1868,7 +1766,7 @@             verify s defaultVeriOpts vm (Just $ checkAssertions defaultPanicCodes)            let storeCex = cex.store-              addrC = W256 $ num $ createAddress ethrunAddress 1+              addrC = into $ createAddress ethrunAddress 1               addrA = W256 0x35D1b3F3D7966A1DFe207aa4514C12a259A0492B               testCex = Map.size storeCex == 2 &&                         case (Map.lookup addrC storeCex, Map.lookup addrA storeCex) of@@ -1969,7 +1867,7 @@             }             |]           (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts-          let addr =  W256 $ num $ createAddress ethrunAddress 1+          let addr = into $ createAddress ethrunAddress 1               testCex = Map.size cex.store == 1 &&                         case Map.lookup addr cex.store of                           Just s -> Map.size s == 2 &&@@ -1992,7 +1890,7 @@             }             |]           (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts-          let addr = W256 $ num $ createAddress ethrunAddress 1+          let addr = into $ createAddress ethrunAddress 1               a = getVar cex "arg1"               testCex = Map.size cex.store == 1 &&                         case Map.lookup addr cex.store of@@ -2296,13 +2194,16 @@                     -- Takes too long, would timeout on most test setups.                     -- We could probably fix these by "bunching together" queries                     , "reasoningBasedSimplifier/mulmod.yul"+                    , "loadResolver/multi_sload_loop.yul"+                    , "reasoningBasedSimplifier/mulcheck.yul"+                    , "reasoningBasedSimplifier/smod.yul"                      -- TODO check what's wrong with these!                     , "loadResolver/keccak_short.yul" -- ACTUAL bug -- keccak                     , "reasoningBasedSimplifier/signed_division.yul" -- ACTUAL bug, SDIV                     ] -        solcRepo <- fromMaybe (error "cannot find solidity repo") <$> (lookupEnv "HEVM_SOLIDITY_REPO")+        solcRepo <- fromMaybe (internalError "cannot find solidity repo") <$> (lookupEnv "HEVM_SOLIDITY_REPO")         let testDir = solcRepo <> "/test/libyul/yulOptimizerTests"         dircontents <- System.Directory.listDirectory testDir         let@@ -2318,7 +2219,7 @@                 False -> recursiveList ax (a:b)           recursiveList [] b = pure b         files <- recursiveList fullpaths []-        let filesFiltered = filter (\file -> not $ any (`isSubsequenceOf` file) ignoredTests) files+        let filesFiltered = filter (\file -> not $ any (`List.isSubsequenceOf` file) ignoredTests) files          -- Takes one file which follows the Solidity Yul optimizer unit tests format,         -- extracts both the nonoptimized and the optimized versions, and checks equivalence.@@ -2340,7 +2241,7 @@                                       let a2 = replaceAll "a calldatacopy(0,0,1024)" $ a *=~ [re|code {|]                                       in (a2:ax)                                     else replaceOnce [re|^ *{|] "{\ncalldatacopy(0,0,1024)" $ onlyAfter [re|^ *{|] (a:ax)-            symbolicMem _ = error "Program too short"+            symbolicMem _ = internalError "Program too short"              unfiltered = lines origcont             filteredASym = symbolicMem [ x | x <- unfiltered, (not $ x =~ [re|^//|]) && (not $ x =~ [re|^$|]) ]@@ -2358,7 +2259,7 @@           Just aPrgm <- yul "" $ T.pack $ unlines filteredASym           Just bPrgm <- yul "" $ T.pack $ unlines filteredBSym           procs <- getNumProcessors-          withSolvers CVC5 (num procs) (Just 100) $ \s -> do+          withSolvers CVC5 (unsafeInto procs) (Just 100) $ \s -> do             res <- equivalenceCheck s aPrgm bPrgm opts (mkCalldata Nothing [])             end <- getCurrentTime             case any isCex res of@@ -2367,10 +2268,10 @@                 let timeouts = filter isTimeout res                 unless (null timeouts) $ do                   putStrLn $ "But " <> (show $ length timeouts) <> " timeout(s) occurred"-                  error "Encountered timeouts, error"+                  internalError "Encountered timeouts"               True -> do                 putStrLn $ "Not OK: " <> show f <> " Got: " <> show res-                error "Was NOT equivalent, error"+                internalError "Was NOT equivalent"            )     ]   ]@@ -2379,7 +2280,7 @@   checkEquiv :: (Typeable a) => Expr a -> Expr a -> IO Bool-checkEquiv l r = withSolvers Z3 1 (Just 100) $ \solvers -> do+checkEquiv l r = withSolvers Z3 1 (Just 10) $ \solvers -> do   if l == r      then do        putStrLn "skip"@@ -2407,7 +2308,7 @@      res <- Stepper.interpret (Fetch.zero 0 Nothing) vm' Stepper.execFully      case res of        (Right (ConcreteBuf bs)) -> pure $ Just bs-       s -> error $ show s+       s -> internalError $ show s  -- | Takes a creation code and returns a vm with the result of executing the creation code loadVM :: ByteString -> IO (Maybe VM)@@ -2430,7 +2331,7 @@ hex s =   case BS16.decodeBase16 s of     Right x -> x-    Left e -> error $ T.unpack e+    Left e -> internalError $ T.unpack e  singleContract :: Text -> Text -> IO (Maybe ByteString) singleContract x s =@@ -2485,7 +2386,7 @@ decodeAbiValues types bs =   let xy = case decodeAbiValue (AbiTupleType $ Vector.fromList types) (BS.fromStrict (BS.drop 4 bs)) of         AbiTuple xy' -> xy'-        _ -> error "AbiTuple expected"+        _ -> internalError "AbiTuple expected"   in Vector.toList xy  newtype Bytes = Bytes ByteString@@ -2572,13 +2473,13 @@  genEnd :: Int -> Gen (Expr End) genEnd 0 = oneof- [ fmap (Failure [] . UnrecognizedOpcode) arbitrary- , pure $ Failure [] IllegalOverflow- , pure $ Failure [] SelfDestruction+ [ fmap (Failure mempty mempty . UnrecognizedOpcode) arbitrary+ , pure $ Failure mempty mempty IllegalOverflow+ , pure $ Failure mempty mempty SelfDestruction  ] genEnd sz = oneof- [ fmap (Failure [] . Revert) subBuf- , liftM3 Success (return []) subBuf subStore+ [ fmap (Failure mempty mempty . Revert) subBuf+ , liftM4 Success (return mempty) (return mempty) subBuf subStore  , liftM3 ITE subWord subEnd subEnd  ]  where