hevm 0.50.4 → 0.50.5

raw patch · 37 files changed

+5506/−5417 lines, 37 filesdep +aeson-opticsdep +optics-coredep +optics-extradep −lensdep −lens-aesondep ~containersdep ~filepathdep ~mtlPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: aeson-optics, optics-core, optics-extra, optics-th

Dependencies removed: lens, lens-aeson

Dependency ranges changed: containers, filepath, mtl

API changes (from Hackage documentation)

Files

• CHANGELOG.md +15/−1
• bench/bench.hs +78/−18
• hevm-cli/hevm-cli.hs +140/−132
• hevm.cabal +31/−16
• src/EVM.hs +2650/−2762
• src/EVM/ABI.hs +3/−2
• src/EVM/Concrete.hs +2/−3
• src/EVM/Dapp.hs +7/−8
• src/EVM/Debug.hs +10/−10
• src/EVM/Demand.hs +0/−13
• src/EVM/Dev.hs +31/−31
• src/EVM/Exec.hs +28/−28
• src/EVM/Expr.hs +37/−35
• src/EVM/Facts.hs +23/−21
• src/EVM/Facts/Git.hs +2/−2
• src/EVM/Fetch.hs +45/−29
• src/EVM/Format.hs +9/−11
• src/EVM/SMT.hs +16/−16
• src/EVM/Solidity.hs +65/−61
• src/EVM/Solvers.hs +22/−20
• src/EVM/Stepper.hs +33/−41
• src/EVM/StorageLayout.hs +17/−17
• src/EVM/SymExec.hs +284/−224
• src/EVM/TTY.hs +142/−137
• src/EVM/TTYCenteredList.hs +7/−7
• src/EVM/Transaction.hs +106/−105
• src/EVM/Types.hs +8/−4
• src/EVM/UnitTest.hs +123/−118
• test/BlockchainTests.hs +1/−449
• test/EVM/Test/BlockchainTests.hs +448/−0
• test/EVM/Test/Tracing.hs +868/−0
• test/EVM/Test/Utils.hs +136/−0
• test/EVM/TestUtils.hs +0/−136
• test/EVM/Tracing.hs +0/−870
• test/contracts/pass/cheatCodes.sol +21/−0
• test/rpc.hs +47/−51
• test/test.hs +51/−39

@@ -5,6 +5,20 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.50.5] - 2023-03-18++## Changed++- The `--storage-model` parameter has been replaced with `--initial-storage`+- The `--smttimeout` argument now expects a value in seconds not milliseconds+- The default smt timeout has been set to 5 minutes+- `hevm symbolic` now searches only for user defined assertions by default++### Fixed++- The `prank` cheatcode now transfers value from the correct address+- Fixed an off-by-one error in `EVM.Debug.srcMapCodePos`+ ## [0.50.4] - 2023-03-17  ### Fixed@@ -23,8 +37,8 @@ - Implemented a shrinking algorithm for counterexamples - A new differential fuzzing test harness that compares the concrete semantics, as well as parts of the symbolic semantics against the geth evm implementation - The `hevm` library can now be built on Windows systems.-- Support for function pointers in ABI - `equivalence` can now be checked for fully or partially concrete calldata+- Support for function pointers in ABI  ## [0.50.3] - 2023-02-17 

@@ -1,15 +1,23 @@ module Main where  import GHC.Natural+import Control.Monad+import Data.Maybe+import System.Environment (lookupEnv, getEnv)  import qualified Paths_hevm as Paths -import Test.Tasty (localOption)+import Test.Tasty (localOption, withResource) import Test.Tasty.Bench import Data.Functor import Data.String.Here import Data.ByteString (ByteString)+import System.FilePath.Posix+import Control.Monad.State.Strict+import qualified Data.Map.Strict as Map import qualified Data.Text as T+import qualified System.FilePath.Find as Find+import qualified Data.ByteString.Lazy as LazyByteString  import EVM (StorageModel(..)) import EVM.SymExec@@ -19,7 +27,76 @@ import EVM.Dapp import EVM.Types import qualified EVM.TTY as TTY+import qualified EVM.Stepper as Stepper+import qualified EVM.Fetch as Fetch +import EVM.Test.BlockchainTests qualified as BCTests++main :: IO ()+main = defaultMain+  [ mkbench erc20 "erc20" Nothing [1]+  , mkbench (pure vat) "vat" Nothing [4]+  , mkbench (pure deposit) "deposit" (Just 32) [4]+  , mkbench (pure uniV2Pair) "uniV2" (Just 10) [4]+  , withResource bcjsons (pure . const ()) blockchainTests+  ]+++--- General State Tests ----------------------------------------------------------------------------+++-- | loads and parses all blockchain test files+-- We pull this out into a separate stage to ensure that we only benchmark the+-- actual time spent executing tests, and not the IO & parsing overhead+bcjsons :: IO (Map.Map FilePath (Map.Map String BCTests.Case))+bcjsons = do+  repo <- getEnv "HEVM_ETHEREUM_TESTS_REPO"+  let testsDir = "BlockchainTests/GeneralStateTests"+      dir = repo </> testsDir+  jsons <- Find.find Find.always (Find.extension Find.==? ".json") dir+  Map.fromList <$> mapM parseSuite jsons+  where+    parseSuite path = do+      contents <- LazyByteString.readFile path+      case BCTests.parseBCSuite contents of+        Left e -> pure (path, mempty)+        Right tests -> pure (path, tests)++-- | executes all provided bc tests in sequence and accumulates a boolean value representing their success.+-- the accumulated value ensures that we actually have to execute all the tests as a part of this benchmark+blockchainTests :: IO (Map.Map FilePath (Map.Map String BCTests.Case)) -> Benchmark+blockchainTests ts = bench "blockchain-tests" $ nfIO $ do+  tests <- ts+  putStrLn "\n    executing tests:"+  let cases = concat . Map.elems . (fmap Map.toList) $ tests+      ignored = Map.keys BCTests.commonProblematicTests+  foldM (\acc (n, c) ->+      if n `elem` ignored+      then pure True+      else do+        res <- runBCTest c+        putStrLn $ "      " <> n+        pure $ acc && res+    ) True cases++-- | executes a single test case and returns a boolean value representing its success+runBCTest :: BCTests.Case -> IO Bool+runBCTest x =+ do+  let vm0 = BCTests.vmForCase x+  result <- execStateT (Stepper.interpret (Fetch.zero 0 (Just 0)) . void $ Stepper.execFully) vm0+  maybeReason <- BCTests.checkExpectation False x result+  pure $ isNothing maybeReason+++--- Helpers ----------------------------------------------------------------------------------------+++debugContract :: ByteString -> IO ()+debugContract c = withSolvers CVC5 4 Nothing $ \solvers -> do+  let prestate = abstractVM (mkCalldata Nothing []) c Nothing SymbolicS+  void $ TTY.runFromVM solvers Nothing Nothing emptyDapp prestate+ findPanics :: Solver -> Natural -> Maybe Integer -> ByteString -> IO () findPanics solver count iters c = do   (_, res) <- withSolvers solver count Nothing $ \s -> do@@ -44,23 +121,6 @@        ]        | i <- counts      ]--main :: IO ()-main = defaultMain-  [ mkbench erc20 "erc20" Nothing [1]-  , mkbench (pure vat) "vat" Nothing [4]-  , mkbench (pure deposit) "deposit" (Just 32) [4]-  , mkbench (pure uniV2Pair) "uniV2" (Just 10) [4]-  ]------ Helpers -------------------------------------------------------------------------------------------debugContract :: ByteString -> IO ()-debugContract c = withSolvers CVC5 4 Nothing $ \solvers -> do-  let prestate = abstractVM (mkCalldata Nothing []) c Nothing SymbolicS-  void $ TTY.runFromVM solvers Nothing Nothing emptyDapp prestate   --- Bytecodes --------------------------------------------------------------------------------------

@@ -5,7 +5,6 @@  module Main where -import EVM (StorageModel(..)) import qualified EVM import EVM.Concrete (createAddress) import qualified EVM.FeeSchedule as FeeSchedule@@ -20,20 +19,22 @@ import EVM.Solidity import EVM.Expr (litAddr) import EVM.Types hiding (word)-import EVM.UnitTest (UnitTestOptions, coverageReport, coverageForUnitTestContract, getParametersFromEnvironmentVariables, testNumber, dappTest)+import EVM.UnitTest (UnitTestOptions, coverageReport, coverageForUnitTestContract, getParametersFromEnvironmentVariables, dappTest) 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 Control.Lens hiding (pre, passing)+import Optics.Core hiding (pre, Empty) import Control.Monad              (void, when, forM_, unless)-import Control.Monad.State.Strict (execStateT, liftIO)+import Control.Monad.State.Strict (liftIO) import Data.ByteString            (ByteString) import Data.List                  (intercalate, isSuffixOf, intersperse) import Data.Text                  (unpack, pack)@@ -47,7 +48,6 @@ import qualified Data.ByteString        as ByteString import qualified Data.ByteString.Char8  as Char8 import qualified Data.ByteString.Lazy   as LazyByteString-import qualified Data.Map               as Map import qualified Data.Text              as T import qualified Data.Text.IO           as T @@ -89,14 +89,14 @@   -- symbolic execution opts       , jsonFile      :: w ::: Maybe String       <?> "Filename or path to dapp build output (default: out/*.solc.json)"       , dappRoot      :: w ::: Maybe String       <?> "Path to dapp project root directory (default: . )"-      , storageModel  :: w ::: Maybe StorageModel <?> "Select storage model: ConcreteS, SymbolicS (default) or InitialS"+      , initialStorage :: w ::: Maybe (InitialStorage) <?> "Starting state for storage: Empty, Abstract, Concrete <STORE> (default Abstract)"       , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"       , arg           :: w ::: [String]           <?> "Values to encode"       , debug         :: w ::: Bool               <?> "Run interactively"       , getModels     :: w ::: Bool               <?> "Print example testcase for each execution path"       , showTree      :: w ::: Bool               <?> "Print branches explored in tree view"       , showReachableTree :: w ::: Bool           <?> "Print only reachable branches explored in tree view"-      , smttimeout    :: w ::: Maybe Natural      <?> "Timeout given to SMT solver in milliseconds (default: 60000)"+      , smttimeout    :: w ::: Maybe Natural      <?> "Timeout given to SMT solver in seconds (default: 300)"       , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"       , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc5"       , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"@@ -110,7 +110,7 @@       , sig           :: w ::: Maybe Text       <?> "Signature of types to decode / encode"       , arg           :: w ::: [String]         <?> "Values to encode"       , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"-      , smttimeout    :: w ::: Maybe Natural    <?> "Timeout given to SMT solver in milliseconds (default: 60000)"+      , smttimeout    :: w ::: Maybe Natural    <?> "Timeout given to SMT solver in seconds (default: 300)"       , maxIterations :: w ::: Maybe Integer    <?> "Number of times we may revisit a particular branching point"       , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default) or cvc5"       , smtoutput     :: w ::: Bool             <?> "Print verbose smt output"@@ -165,7 +165,7 @@       , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default) or cvc5"       , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"       , ffi           :: w ::: Bool                     <?> "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)"-      , smttimeout    :: w ::: Maybe Natural            <?> "Timeout given to SMT solver in milliseconds (default: 60000)"+      , smttimeout    :: w ::: Maybe Natural            <?> "Timeout given to SMT solver in seconds (default: 300)"       , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point"       , askSmtIterations :: w ::: Maybe Integer         <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)"       }@@ -187,6 +187,12 @@   parseRecord =     Options.parseRecordWithModifiers Options.lispCaseModifiers +data InitialStorage+  = Empty+  | Concrete [(W256, [(W256, W256)])]+  | Abstract+  deriving (Show, Read, Options.ParseField)+ optsMode :: Command Options.Unwrapped -> Mode optsMode x   | x.debug = Debug@@ -224,7 +230,7 @@   params <- getParametersFromEnvironmentVariables cmd.rpc    let-    testn = params.testNumber+    testn = params.number     block' = if 0 == testn        then EVM.Fetch.Latest        else EVM.Fetch.BlockNumber testn@@ -262,8 +268,7 @@     Version {} -> putStrLn (showVersion Paths.version)     Symbolic {} -> withCurrentDirectory root $ assert cmd     Equivalence {} -> equivalence cmd-    Exec {} ->-      launchExec cmd+    Exec {} -> launchExec cmd     DappTest {} ->       withCurrentDirectory root $ do         cores <- num <$> getNumProcessors@@ -372,8 +377,8 @@ assert cmd = do   let block'  = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block       rpcinfo = (,) block' <$> cmd.rpc-  calldata' <- buildCalldata cmd-  preState <- symvmFromCommand cmd calldata'+  calldata <- buildCalldata cmd+  preState <- symvmFromCommand cmd calldata   let errCodes = fromMaybe defaultPanicCodes cmd.assertions   cores <- num <$> getNumProcessors   let solverCount = fromMaybe cores cmd.numSolvers@@ -391,7 +396,9 @@       let opts = VeriOpts { simp = True, debug = cmd.smtdebug, maxIter = cmd.maxIterations, askSmtIters = cmd.askSmtIterations, rpcInfo = rpcinfo}       (expr, res) <- verify solvers opts preState (Just $ checkAssertions errCodes)       case res of-        [Qed _] -> putStrLn "\nQED: No reachable property violations discovered\n"+        [Qed _] -> do+          putStrLn "\nQED: No reachable property violations discovered\n"+          showExtras solvers cmd calldata expr         _ -> do           let cexs = snd <$> mapMaybe getCex res               timeouts = mapMaybe getTimeout res@@ -401,7 +408,7 @@                    [ ""                    , "Discovered the following counterexamples:"                    , ""-                   ] <> fmap (formatCex (fst calldata')) cexs+                   ] <> fmap (formatCex (fst calldata)) cexs               unknowns                 | null timeouts = []                 | otherwise =@@ -410,21 +417,25 @@                    , ""                    ] <> fmap (formatExpr) timeouts           T.putStrLn $ T.unlines (counterexamples <> unknowns)+          showExtras solvers cmd calldata expr           exitFailure-      when cmd.showTree $ do-        putStrLn "=== Expression ===\n"-        T.putStrLn $ formatExpr expr-        putStrLn ""-      when cmd.showReachableTree $ do-        reached <- reachable solvers expr-        putStrLn "=== Reachable Expression ===\n"-        T.putStrLn (formatExpr . snd $ reached)-        putStrLn ""-      when cmd.getModels $ do-        putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ===\n"-        ms <- produceModels solvers expr-        forM_ ms (showModel (fst calldata')) +showExtras :: SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> IO ()+showExtras solvers cmd calldata expr = do+  when cmd.showTree $ do+    putStrLn "=== Expression ===\n"+    T.putStrLn $ formatExpr expr+    putStrLn ""+  when cmd.showReachableTree $ do+    reached <- reachable solvers expr+    putStrLn "=== Reachable Expression ===\n"+    T.putStrLn (formatExpr . snd $ reached)+    putStrLn ""+  when cmd.getModels $ do+    putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ===\n"+    ms <- produceModels solvers expr+    forM_ ms (showModel (fst calldata))+ getCex :: ProofResult a b c -> Maybe b getCex (Cex c) = Just c getCex _ = Nothing@@ -480,9 +491,9 @@   withSolvers Z3 0 Nothing $ \solvers -> do     case optsMode cmd of       Run -> do-        vm' <- execStateT (EVM.Stepper.interpret (EVM.Fetch.oracle solvers rpcinfo) . void $ EVM.Stepper.execFully) vm+        vm' <- EVM.Stepper.interpret (EVM.Fetch.oracle solvers rpcinfo) vm EVM.Stepper.runFully         when cmd.trace $ T.hPutStr stderr (showTraceTree dapp vm')-        case view EVM.result vm' of+        case vm'.result of           Nothing ->             error "internal error; no EVM result"           Just (EVM.VMFailure (EVM.Revert msg)) -> do@@ -506,13 +517,13 @@             case cmd.cache of               Nothing -> pure ()               Just path ->-                Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts (view EVM.cache vm'))+                Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts vm'.cache)        Debug -> void $ TTY.runFromVM solvers rpcinfo Nothing dapp vm       --JsonTrace -> void $ execStateT (interpretWithTrace fetcher EVM.Stepper.runFully) vm       _ -> error "TODO"-     where block' = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block-           rpcinfo = (,) block' <$> cmd.rpc+     where block = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block+           rpcinfo = (,) block <$> cmd.rpc  -- | Creates a (concrete) VM from command line options vmFromCommand :: Command Options.Unwrapped -> IO EVM.VM@@ -521,34 +532,34 @@    (miner,ts,baseFee,blockNum,prevRan) <- case cmd.rpc of     Nothing -> return (0,Lit 0,0,0,0)-    Just url -> EVM.Fetch.fetchBlockFrom block' url >>= \case+    Just url -> EVM.Fetch.fetchBlockFrom block url >>= \case       Nothing -> error "Could not fetch block"-      Just EVM.Block{..} -> return (_coinbase-                                   , _timestamp-                                   , _baseFee-                                   , _number-                                   , _prevRandao+      Just EVM.Block{..} -> return ( 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+      EVM.Fetch.fetchContractFrom block url addr' >>= \case         Nothing ->-          error $ "contract not found: " <> show address'-        Just contract' ->+          error $ "contract not found: " <> show address+        Just contract ->           -- if both code and url is given,           -- fetch the contract and overwrite the code           return $             EVM.initialContract  (mkCode $ hexByteString "--code" $ strip0x c)-              & set EVM.balance  (view EVM.balance  contract')-              & set EVM.nonce    (view EVM.nonce    contract')-              & set EVM.external (view EVM.external contract')+              & set #balance  (contract.balance)+              & set #nonce    (contract.nonce)+              & set #external (contract.external)      (Just url, Just addr', Nothing) ->-      EVM.Fetch.fetchContractFrom block' url addr' >>= \case+      EVM.Fetch.fetchContractFrom block url addr' >>= \case         Nothing ->-          error $ "contract not found: " <> show address'-        Just contract' -> return contract'+          error $ "contract not found: " <> show address+        Just contract -> return contract      (_, _, Just c)  ->       return $@@ -563,43 +574,43 @@    return $ 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-        caller'  = addr (.caller) 0-        origin'  = addr (.origin) 0-        calldata' = ConcreteBuf $ bytes (.calldata) ""+        block   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block+        value   = word (.value) 0+        caller  = addr (.caller) 0+        origin  = addr (.origin) 0+        calldata = ConcreteBuf $ bytes (.calldata) ""         decipher = hexByteString "bytes" . strip0x         mkCode bs = if cmd.create                     then EVM.InitCode bs mempty                     else EVM.RuntimeCode (EVM.ConcreteRuntimeCode bs)-        address' = if cmd.create-              then addr (.address) (createAddress origin' (word (.nonce) 0))+        address = if cmd.create+              then addr (.address) (createAddress origin (word (.nonce) 0))               else addr (.address) 0xacab          vm0 baseFee miner ts blockNum prevRan c = EVM.makeVm $ EVM.VMOpts-          { vmoptContract      = c-          , vmoptCalldata      = (calldata', [])-          , vmoptValue         = Lit value'-          , vmoptAddress       = address'-          , vmoptCaller        = litAddr caller'-          , vmoptOrigin        = origin'-          , vmoptGas           = word64 (.gas) 0xffffffffffffffff-          , vmoptBaseFee       = baseFee-          , vmoptPriorityFee   = word (.priorityFee) 0-          , vmoptGaslimit      = word64 (.gaslimit) 0xffffffffffffffff-          , vmoptCoinbase      = addr (.coinbase) miner-          , vmoptNumber        = word (.number) blockNum-          , vmoptTimestamp     = Lit $ word (.timestamp) ts-          , vmoptBlockGaslimit = word64 (.gaslimit) 0xffffffffffffffff-          , vmoptGasprice      = word (.gasprice) 0-          , vmoptMaxCodeSize   = word (.maxcodesize) 0xffffffff-          , vmoptPrevRandao    = word (.prevRandao) prevRan-          , vmoptSchedule      = FeeSchedule.berlin-          , vmoptChainId       = word (.chainid) 1-          , vmoptCreate        = (.create) cmd-          , vmoptStorageBase   = EVM.Concrete-          , vmoptTxAccessList  = mempty -- TODO: support me soon-          , vmoptAllowFFI      = False+          { contract       = c+          , calldata       = (calldata, [])+          , value          = Lit value+          , address        = address+          , caller         = litAddr caller+          , origin         = origin+          , gas            = word64 (.gas) 0xffffffffffffffff+          , baseFee        = baseFee+          , priorityFee    = word (.priorityFee) 0+          , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff+          , coinbase       = addr (.coinbase) miner+          , number         = word (.number) blockNum+          , timestamp      = Lit $ word (.timestamp) ts+          , blockGaslimit  = word64 (.gaslimit) 0xffffffffffffffff+          , gasprice       = word (.gasprice) 0+          , maxCodeSize    = word (.maxcodesize) 0xffffffff+          , prevRandao     = word (.prevRandao) prevRan+          , schedule       = FeeSchedule.berlin+          , chainId        = word (.chainid) 1+          , create         = (.create) cmd+          , initialStorage = EmptyStore+          , txAccessList   = mempty -- TODO: support me soon+          , allowFFI       = False           }         word f def = fromMaybe def (f cmd)         word64 f def = fromMaybe def (f cmd)@@ -607,37 +618,28 @@         bytes f def = maybe def decipher (f cmd)  symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (EVM.VM)-symvmFromCommand cmd calldata' = do+symvmFromCommand cmd calldata = do   (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of     Nothing -> return (0,0,0,0)-    Just url -> EVM.Fetch.fetchBlockFrom block' url >>= \case+    Just url -> EVM.Fetch.fetchBlockFrom block url >>= \case       Nothing -> error "Could not fetch block"-      Just EVM.Block{..} -> return (_coinbase-                                   , _number-                                   , _baseFee-                                   , _prevRandao+      Just EVM.Block{..} -> return ( coinbase+                                   , number+                                   , baseFee+                                   , prevRandao                                    )    let-    caller' = Caller 0+    caller = Caller 0     ts = maybe Timestamp Lit cmd.timestamp-    callvalue' = maybe (CallValue 0) Lit cmd.value+    callvalue = maybe (CallValue 0) Lit cmd.value   -- TODO: rework this, ConcreteS not needed anymore-  let store = case cmd.storageModel of-                -- InitialS and SymbolicS can read and write to symbolic locations-                -- ConcreteS cannot (instead values can be fetched from rpc!)-                -- Initial defaults to 0 for uninitialized storage slots,-                -- whereas the values of SymbolicS are unconstrained.-                Just InitialS  -> EmptyStore-                Just ConcreteS -> ConcreteStore mempty-                Just SymbolicS -> AbstractStore-                Nothing -> if cmd.create then EmptyStore else AbstractStore-+  let store = maybe AbstractStore parseInitialStorage (cmd.initialStorage)   withCache <- applyCache (cmd.state, cmd.cache) -  contract' <- case (cmd.rpc, cmd.address, cmd.code) of+  contract <- case (cmd.rpc, cmd.address, cmd.code) of     (Just url, Just addr', _) ->-      EVM.Fetch.fetchContractFrom block' url addr' >>= \case+      EVM.Fetch.fetchContractFrom block url addr' >>= \case         Nothing ->           error "contract not found."         Just contract' -> return contract''@@ -649,53 +651,59 @@               Just c -> EVM.initialContract (mkCode $ decipher c)                         -- TODO: fix this                         -- & set EVM.origStorage (view EVM.origStorage contract')-                        & set EVM.balance     (view EVM.balance contract')-                        & set EVM.nonce       (view EVM.nonce contract')-                        & set EVM.external    (view EVM.external contract')+                        & set #balance     (contract'.balance)+                        & set #nonce       (contract'.nonce)+                        & set #external    (contract'.external)      (_, _, Just c)  ->       return (EVM.initialContract . mkCode $ decipher c)     (_, _, Nothing) ->       error "must provide at least (rpc + address) or code" -  return $ (EVM.Transaction.initTx $ withCache $ vm0 baseFee miner ts blockNum prevRan calldata' callvalue' caller' contract')-    & set (EVM.env . EVM.storage) store+  return $ (EVM.Transaction.initTx $ withCache $ vm0 baseFee miner ts blockNum prevRan calldata callvalue caller contract)+    & set (#env % #storage) store    where     decipher = hexByteString "bytes" . strip0x-    block'   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block-    origin'  = addr (.origin) 0+    block   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block+    origin  = addr (.origin) 0     mkCode bs = if cmd.create                    then EVM.InitCode bs mempty                    else EVM.RuntimeCode (EVM.ConcreteRuntimeCode bs)-    address' = if cmd.create-          then addr (.address) (createAddress origin' (word (.nonce) 0))+    address = if cmd.create+          then addr (.address) (createAddress origin (word (.nonce) 0))           else addr (.address) 0xacab-    vm0 baseFee miner ts blockNum prevRan cd' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts-      { vmoptContract      = c-      , vmoptCalldata      = cd'-      , vmoptValue         = callvalue'-      , vmoptAddress       = address'-      , vmoptCaller        = caller'-      , vmoptOrigin        = origin'-      , vmoptGas           = word64 (.gas) 0xffffffffffffffff-      , vmoptGaslimit      = word64 (.gaslimit) 0xffffffffffffffff-      , vmoptBaseFee       = baseFee-      , vmoptPriorityFee   = word (.priorityFee) 0-      , vmoptCoinbase      = addr (.coinbase) miner-      , vmoptNumber        = word (.number) blockNum-      , vmoptTimestamp     = ts-      , vmoptBlockGaslimit = word64 (.gaslimit) 0xffffffffffffffff-      , vmoptGasprice      = word (.gasprice) 0-      , vmoptMaxCodeSize   = word (.maxcodesize) 0xffffffff-      , vmoptPrevRandao    = word (.prevRandao) prevRan-      , vmoptSchedule      = FeeSchedule.berlin-      , vmoptChainId       = word (.chainid) 1-      , vmoptCreate        = (.create) cmd-      , vmoptStorageBase   = EVM.Symbolic-      , vmoptTxAccessList  = mempty-      , vmoptAllowFFI      = False+    vm0 baseFee miner ts blockNum prevRan cd callvalue caller c = EVM.makeVm $ EVM.VMOpts+      { contract       = c+      , calldata       = cd+      , value          = callvalue+      , address        = address+      , caller         = caller+      , origin         = origin+      , gas            = word64 (.gas) 0xffffffffffffffff+      , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff+      , baseFee        = baseFee+      , priorityFee    = word (.priorityFee) 0+      , coinbase       = addr (.coinbase) miner+      , number         = word (.number) blockNum+      , timestamp      = ts+      , blockGaslimit  = word64 (.gaslimit) 0xffffffffffffffff+      , gasprice       = word (.gasprice) 0+      , maxCodeSize    = word (.maxcodesize) 0xffffffff+      , prevRandao     = word (.prevRandao) prevRan+      , schedule       = FeeSchedule.berlin+      , chainId        = word (.chainid) 1+      , create         = (.create) cmd+      , initialStorage = maybe AbstractStore parseInitialStorage (cmd.initialStorage)+      , txAccessList   = mempty+      , allowFFI       = False       }     word f def = fromMaybe def (f cmd)     addr f def = fromMaybe def (f cmd)     word64 f def = fromMaybe def (f cmd)++parseInitialStorage :: InitialStorage -> Expr Storage+parseInitialStorage = \case+  Empty -> EmptyStore+  Concrete s -> ConcreteStore (Map.fromList $ fmap (second Map.fromList) s)+  Abstract -> AbstractStore

@@ -2,7 +2,7 @@ name:   hevm version:-  0.50.4+  0.50.5 synopsis:   Ethereum virtual machine evaluator description:@@ -61,6 +61,11 @@     ghc-options: -Werror   if flag(devel)     ghc-options: -j+  ghc-options:+    -Wall+    -Wno-unticked-promoted-constructors+    -Wno-orphans+    -Wno-ambiguous-fields   default-language: GHC2021   default-extensions:     DuplicateRecordFields@@ -68,6 +73,7 @@     NoFieldSelectors     OverloadedRecordDot     OverloadedStrings+    OverloadedLabels     RecordWildCards     TypeFamilies     ViewPatterns@@ -81,7 +87,6 @@     EVM.Concrete,     EVM.Dapp,     EVM.Debug,-    EVM.Demand,     EVM.Dev,     EVM.Expr,     EVM.SMT,@@ -116,7 +121,6 @@     Paths_hevm   autogen-modules:     Paths_hevm-  ghc-options: -Wall -Wno-deprecations -Wno-unticked-promoted-constructors -Wno-orphans   if os(linux) || os(windows)     extra-libraries: stdc++   extra-libraries:@@ -158,8 +162,10 @@     free                              >= 5.1.3 && < 5.2,     haskeline                         >= 0.8.0 && < 0.9,     process                           >= 1.6.5 && < 1.7,-    lens                              >= 5.1.1 && < 5.2,-    lens-aeson                        >= 1.2.2 && < 1.3,+    optics-core                       >= 0.4.1 && < 0.5,+    optics-extra                      >= 0.4.2.1 && < 0.5,+    optics-th                         >= 0.4.1 && < 0.5,+    aeson-optics                      >= 1.2.0.1 && < 1.3,     monad-par                         >= 0.3.5 && < 0.4,     async                             >= 2.2.4 && < 2.3,     multiset                          >= 0.3.4 && < 0.4,@@ -193,7 +199,7 @@     hevm-cli   main-is:     hevm-cli.hs-  ghc-options: -Wall -threaded -with-rtsopts=-N -Wno-unticked-promoted-constructors -Wno-orphans+  ghc-options: -threaded -with-rtsopts=-N   other-modules:     Paths_hevm   if os(darwin)@@ -219,8 +225,6 @@     filepath,     free,     hevm,-    lens,-    lens-aeson,     memory,     mtl,     optparse-generic,@@ -234,7 +238,8 @@     vector,     vty,     stm,-    spawn+    spawn,+    optics-core   if os(windows)     buildable: False @@ -242,7 +247,6 @@  common test-base   import: shared-  ghc-options: -Wall -Wno-unticked-promoted-constructors -Wno-orphans   hs-source-dirs:     test   extra-libraries:@@ -266,7 +270,6 @@     filepath,     here,     hevm,-    lens,     mtl,     data-dword,     process,@@ -286,13 +289,17 @@     spawn >= 0.3,     witherable,     smt2-parser >= 0.1.0.1,-    operational+    operational,+    optics-core,+    optics-extra  library test-utils   import:     test-base   exposed-modules:-    EVM.TestUtils+    EVM.Test.Utils+    EVM.Test.Tracing+    EVM.Test.BlockchainTests   if os(windows)     buildable: False @@ -304,8 +311,9 @@   build-depends:     test-utils   other-modules:-    EVM.TestUtils-    EVM.Tracing+    EVM.Test.Utils+    EVM.Test.Tracing+    EVM.Test.BlockchainTests   if os(windows)     buildable: False   if os(darwin)@@ -353,6 +361,8 @@     bench.hs   hs-source-dirs:     bench+  ghc-options:+    -O2   if os(darwin)      extra-libraries: c++   else@@ -368,4 +378,9 @@     bytestring,     text,     hevm,-    here+    here,+    test-utils,+    filemanip,+    filepath,+    containers,+    mtl

@@ -1,2763 +1,2651 @@ {-# Language ImplicitParams #-}-{-# Language DataKinds #-}-{-# Language GADTs #-}-{-# Language TemplateHaskell #-}--module EVM where--import Prelude hiding (log, exponent, GT, LT)--import EVM.ABI-import EVM.Concrete (createAddress, create2Address)-import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord,-  writeByte, bufLength, indexWord, litAddr, readBytes, word256At, copySlice)-import EVM.Expr qualified as Expr-import EVM.FeeSchedule (FeeSchedule (..))-import EVM.Op-import EVM.Precompiled qualified-import EVM.Solidity-import EVM.Types hiding (IllegalOverflow, Error)-import EVM.Sign qualified--import Control.Lens hiding (op, (:<), (|>), (.>))-import Control.Monad.State.Strict hiding (state)-import Data.Bits (FiniteBits, countLeadingZeros, finiteBitSize)-import Data.ByteArray qualified as BA-import Data.ByteString (ByteString)-import Data.ByteString qualified as BS-import Data.ByteString.Lazy (fromStrict)-import Data.ByteString.Lazy qualified as LS-import Data.ByteString.Char8 qualified as Char8-import Data.Foldable (toList)-import Data.List (find)-import Data.Map.Strict (Map)-import Data.Map.Strict qualified as Map-import Data.Maybe (fromMaybe, fromJust)-import Data.Set (Set, insert, member, fromList)-import Data.Sequence (Seq)-import Data.Sequence qualified as Seq-import Data.Text (unpack)-import Data.Text.Encoding (decodeUtf8, encodeUtf8)-import Data.Tree-import Data.Tree.Zipper qualified as Zipper-import Data.Tuple.Curry-import Data.Vector qualified as RegularVector-import Data.Vector qualified as V-import Data.Vector.Storable (Vector)-import Data.Vector.Storable qualified as Vector-import Data.Vector.Storable.Mutable qualified as Vector-import Data.Word (Word8, Word32, Word64)-import Options.Generic as Options--import Crypto.Hash (Digest, SHA256, RIPEMD160)-import Crypto.Hash qualified as Crypto-import Crypto.Number.ModArithmetic (expFast)-import Crypto.PubKey.ECC.ECDSA (signDigestWith, PrivateKey(..), Signature(..))---- * Data types---- | EVM failure modes-data Error-  = BalanceTooLow W256 W256-  | UnrecognizedOpcode Word8-  | SelfDestruction-  | StackUnderrun-  | BadJumpDestination-  | Revert (Expr Buf)-  | OutOfGas Word64 Word64-  | BadCheatCode (Maybe Word32)-  | StackLimitExceeded-  | IllegalOverflow-  | Query Query-  | Choose Choose-  | StateChangeWhileStatic-  | InvalidMemoryAccess-  | CallDepthLimitReached-  | MaxCodeSizeExceeded W256 W256-  | InvalidFormat-  | PrecompileFailure-  | forall a . UnexpectedSymbolicArg Int String [Expr a]-  | DeadPath-  | NotUnique (Expr EWord)-  | SMTTimeout-  | FFI [AbiValue]-  | ReturnDataOutOfBounds-  | NonceOverflow-deriving instance Show Error---- | The possible result states of a VM-data VMResult-  = VMFailure Error -- ^ An operation failed-  | VMSuccess (Expr Buf) -- ^ Reached STOP, RETURN, or end-of-code--deriving instance Show VMResult---- | The state of a stepwise EVM execution-data VM = VM-  { _result         :: Maybe VMResult-  , _state          :: FrameState-  , _frames         :: [Frame]-  , _env            :: Env-  , _block          :: Block-  , _tx             :: TxState-  , _logs           :: [Expr Log]-  , _traces         :: Zipper.TreePos Zipper.Empty Trace-  , _cache          :: Cache-  , _burned         :: {-# UNPACK #-} !Word64-  , _iterations     :: Map CodeLocation Int-  , _constraints    :: [Prop]-  , _keccakEqs      :: [Prop]-  , _allowFFI       :: Bool-  , _overrideCaller :: Maybe (Expr EWord)-  }-  deriving (Show)--data Trace = Trace-  { _traceOpIx     :: Int-  , _traceContract :: Contract-  , _traceData     :: TraceData-  }-  deriving (Show)--data TraceData-  = EventTrace (Expr EWord) (Expr Buf) [Expr EWord]-  | FrameTrace FrameContext-  | QueryTrace Query-  | ErrorTrace Error-  | EntryTrace Text-  | ReturnTrace (Expr Buf) FrameContext-  deriving (Show)---- | Queries halt execution until resolved through RPC calls or SMT queries-data Query where-  PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query-  --PleaseMakeUnique    :: SBV a -> [SBool] -> (IsUnique a -> EVM ()) -> Query-  PleaseFetchSlot     :: Addr -> W256 -> (W256 -> EVM ()) -> Query-  PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query-  PleaseDoFFI         :: [String] -> (ByteString -> EVM ()) -> Query--data Choose where-  PleaseChoosePath    :: Expr EWord -> (Bool -> EVM ()) -> Choose--instance Show Query where-  showsPrec _ = \case-    PleaseFetchContract addr _ ->-      (("<EVM.Query: fetch contract " ++ show addr ++ ">") ++)-    PleaseFetchSlot addr slot _ ->-      (("<EVM.Query: fetch slot "-        ++ show slot ++ " for "-        ++ show addr ++ ">") ++)-    PleaseAskSMT condition constraints _ ->-      (("<EVM.Query: ask SMT about "-        ++ show condition ++ " in context "-        ++ show constraints ++ ">") ++)---     PleaseMakeUnique val constraints _ ->---       (("<EVM.Query: make value "---         ++ show val ++ " unique in context "---         ++ show constraints ++ ">") ++)-    PleaseDoFFI cmd _ ->-      (("<EVM.Query: do ffi: " ++ (show cmd)) ++)--instance Show Choose where-  showsPrec _ = \case-    PleaseChoosePath _ _ ->-      (("<EVM.Choice: waiting for user to select path (0,1)") ++)---- | Alias for the type of e.g. @exec1@.-type EVM a = State VM a--type CodeLocation = (Addr, Int)---- | The possible return values of a SMT query-data BranchCondition = Case Bool | Unknown | Inconsistent-  deriving Show---- | The possible return values of a `is unique` SMT query-data IsUnique a = Unique a | Multiple | InconsistentU | TimeoutU-  deriving Show---- | The cache is data that can be persisted for efficiency:--- any expensive query that is constant at least within a block.-data Cache = Cache-  { _fetchedContracts :: Map Addr Contract,-    _fetchedStorage :: Map W256 (Map W256 W256),-    _path :: Map (CodeLocation, Int) Bool-  } deriving Show--data StorageBase = Concrete | Symbolic-  deriving (Show, Eq)---- | A way to specify an initial VM state-data VMOpts = VMOpts-  { vmoptContract :: Contract-  , vmoptCalldata :: (Expr Buf, [Prop])-  , vmoptStorageBase :: StorageBase-  , vmoptValue :: Expr EWord-  , vmoptPriorityFee :: W256-  , vmoptAddress :: Addr-  , vmoptCaller :: Expr EWord-  , vmoptOrigin :: Addr-  , vmoptGas :: Word64-  , vmoptGaslimit :: Word64-  , vmoptNumber :: W256-  , vmoptTimestamp :: Expr EWord-  , vmoptCoinbase :: Addr-  , vmoptPrevRandao :: W256-  , vmoptMaxCodeSize :: W256-  , vmoptBlockGaslimit :: Word64-  , vmoptGasprice :: W256-  , vmoptBaseFee :: W256-  , vmoptSchedule :: FeeSchedule Word64-  , vmoptChainId :: W256-  , vmoptCreate :: Bool-  , vmoptTxAccessList :: Map Addr [W256]-  , vmoptAllowFFI :: Bool-  } deriving Show---- | An entry in the VM's "call/create stack"-data Frame = Frame-  { _frameContext   :: FrameContext-  , _frameState     :: FrameState-  }-  deriving (Show)---- | Call/create info-data FrameContext-  = CreationContext-    { creationContextAddress   :: Addr-    , creationContextCodehash  :: Expr EWord-    , creationContextReversion :: Map Addr Contract-    , creationContextSubstate  :: SubState-    }-  | CallContext-    { callContextTarget    :: Addr-    , callContextContext   :: Addr-    , callContextOffset    :: W256-    , callContextSize      :: W256-    , callContextCodehash  :: Expr EWord-    , callContextAbi       :: Maybe W256-    , callContextData      :: Expr Buf-    , callContextReversion :: (Map Addr Contract, Expr Storage)-    , callContextSubState  :: SubState-    }-  deriving (Show)---- | The "registers" of the VM along with memory and data stack-data FrameState = FrameState-  { _contract     :: Addr-  , _codeContract :: Addr-  , _code         :: ContractCode-  , _pc           :: {-# UNPACK #-} !Int-  , _stack        :: [Expr EWord]-  , _memory       :: Expr Buf-  , _memorySize   :: Word64-  , _calldata     :: Expr Buf-  , _callvalue    :: Expr EWord-  , _caller       :: Expr EWord-  , _gas          :: {-# UNPACK #-} !Word64-  , _returndata   :: Expr Buf-  , _static       :: Bool-  }-  deriving (Show)---- | The state that spans a whole transaction-data TxState = TxState-  { _gasprice            :: W256-  , _txgaslimit          :: Word64-  , _txPriorityFee       :: W256-  , _origin              :: Addr-  , _toAddr              :: Addr-  , _value               :: Expr EWord-  , _substate            :: SubState-  , _isCreate            :: Bool-  , _txReversion         :: Map Addr Contract-  }-  deriving (Show)---- | The "accrued substate" across a transaction-data SubState = SubState-  { _selfdestructs   :: [Addr]-  , _touchedAccounts :: [Addr]-  , _accessedAddresses :: Set Addr-  , _accessedStorageKeys :: Set (Addr, W256)-  , _refunds         :: [(Addr, Word64)]-  -- in principle we should include logs here, but do not for now-  }-  deriving (Show)--{- |-  A contract is either in creation (running its "constructor") or-  post-creation, and code in these two modes is treated differently-  by instructions like @EXTCODEHASH@, so we distinguish these two-  code types.--  The definition follows the structure of code output by solc. We need to use-  some heuristics here to deal with symbolic data regions that may be present-  in the bytecode since the fully abstract case is impractical:--  - initcode has concrete code, followed by an abstract data "section"-  - runtimecode has a fixed length, but may contain fixed size symbolic regions (due to immutable)--  hopefully we do not have to deal with dynamic immutable before we get a real data section...--}-data ContractCode-  = InitCode ByteString (Expr Buf) -- ^ "Constructor" code, during contract creation-  | RuntimeCode RuntimeCode -- ^ "Instance" code, after contract creation-  deriving (Show)---- | We have two variants here to optimize the fully concrete case.--- ConcreteRuntimeCode just wraps a ByteString--- SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).-data RuntimeCode-  = ConcreteRuntimeCode ByteString-  | SymbolicRuntimeCode (V.Vector (Expr Byte))-  deriving (Show, Eq, Ord)---- runtime err when used for symbolic code-instance Eq ContractCode where-  (InitCode a b) == (InitCode c d) = a == c && b == d-  (RuntimeCode x) == (RuntimeCode y) = x == y-  _ == _ = False--deriving instance Ord ContractCode---- | A contract can either have concrete or symbolic storage--- depending on what type of execution we are doing--- data Storage---   = Concrete (Map Word Expr EWord)---   | Symbolic [(Expr EWord, Expr EWord)] (SArray (WordN 256) (WordN 256))---   deriving (Show)---- to allow for Eq Contract (which useful for debugging vmtests)--- we mock an instance of Eq for symbolic storage.--- It should not (cannot) be used though.--- instance Eq Storage where---   (==) (Concrete a) (Concrete b) = fmap forceLit a == fmap forceLit b---   (==) (Symbolic _ _) (Concrete _) = False---   (==) (Concrete _) (Symbolic _ _) = False---   (==) _ _ = error "do not compare two symbolic arrays like this!"---- | The state of a contract-data Contract = Contract-  { _contractcode :: ContractCode-  , _balance      :: W256-  , _nonce        :: W256-  , _codehash     :: Expr EWord-  , _opIxMap      :: Vector Int-  , _codeOps      :: RegularVector.Vector (Int, Op)-  , _external     :: Bool-  }--deriving instance Show Contract---- | When doing symbolic execution, we have three different--- ways to model the storage of contracts. This determines--- not only the initial contract storage model but also how--- RPC or state fetched contracts will be modeled.-data StorageModel-  = ConcreteS    -- ^ Uses `Concrete` Storage. Reading / Writing from abstract-                 -- locations causes a runtime failure. Can be nicely combined with RPC.--  | SymbolicS    -- ^ Uses `Symbolic` Storage. Reading / Writing never reaches RPC,-                 -- but always done using an SMT array with no default value.--  | InitialS     -- ^ Uses `Symbolic` Storage. Reading / Writing never reaches RPC,-                 -- but always done using an SMT array with 0 as the default value.--  deriving (Read, Show)--instance ParseField StorageModel---- | Various environmental data-data Env = Env-  { _contracts    :: Map Addr Contract-  , _chainId      :: W256-  , _storage      :: Expr Storage-  , _origStorage  :: Map W256 (Map W256 W256)-  , _sha3Crack    :: Map W256 ByteString-  --, _keccakUsed   :: [([SWord 8], SWord 256)]-  }-  deriving (Show)----- | Data about the block-data Block = Block-  { _coinbase    :: Addr-  , _timestamp   :: Expr EWord-  , _number      :: W256-  , _prevRandao  :: W256-  , _gaslimit    :: Word64-  , _baseFee     :: W256-  , _maxCodeSize :: W256-  , _schedule    :: FeeSchedule Word64-  } deriving (Show, Generic)---blankState :: FrameState-blankState = FrameState-  { _contract     = 0-  , _codeContract = 0-  , _code         = RuntimeCode (ConcreteRuntimeCode "")-  , _pc           = 0-  , _stack        = mempty-  , _memory       = mempty-  , _memorySize   = 0-  , _calldata     = mempty-  , _callvalue    = (Lit 0)-  , _caller       = (Lit 0)-  , _gas          = 0-  , _returndata   = mempty-  , _static       = False-  }--makeLenses ''FrameState-makeLenses ''Frame-makeLenses ''Block-makeLenses ''TxState-makeLenses ''SubState-makeLenses ''Contract-makeLenses ''Env-makeLenses ''Cache-makeLenses ''Trace-makeLenses ''VM---- | An "external" view of a contract's bytecode, appropriate for--- e.g. @EXTCODEHASH@.-bytecode :: Getter Contract (Expr Buf)-bytecode = contractcode . to f-  where f (InitCode _ _) = mempty-        f (RuntimeCode (ConcreteRuntimeCode bs)) = ConcreteBuf bs-        f (RuntimeCode (SymbolicRuntimeCode ops)) = Expr.fromList ops--instance Semigroup Cache where-  a <> b = Cache-    { _fetchedContracts = Map.unionWith unifyCachedContract a._fetchedContracts b._fetchedContracts-    , _fetchedStorage = Map.unionWith unifyCachedStorage a._fetchedStorage b._fetchedStorage-    , _path = mappend a._path b._path-    }--unifyCachedStorage :: Map W256 W256 -> Map W256 W256 -> Map W256 W256-unifyCachedStorage _ _ = undefined---- only intended for use in Cache merges, where we expect--- everything to be Concrete-unifyCachedContract :: Contract -> Contract -> Contract-unifyCachedContract _ _ = undefined-  {--unifyCachedContract a b = a & set storage merged-  where merged = case (view storage a, view storage b) of-                   (ConcreteStore sa, ConcreteStore sb) ->-                     ConcreteStore (mappend sa sb)-                   _ ->-                     view storage a-   -}--instance Monoid Cache where-  mempty = Cache { _fetchedContracts = mempty,-                   _fetchedStorage = mempty,-                   _path = mempty-                 }---- * Data accessors--currentContract :: VM -> Maybe Contract-currentContract vm =-  Map.lookup vm._state._codeContract vm._env._contracts---- * Data constructors--makeVm :: VMOpts -> VM-makeVm o =-  let txaccessList = o.vmoptTxAccessList-      txorigin = o.vmoptOrigin-      txtoAddr = o.vmoptAddress-      initialAccessedAddrs = fromList $ [txorigin, txtoAddr] ++ [1..9] ++ (Map.keys txaccessList)-      initialAccessedStorageKeys = fromList $ foldMap (uncurry (map . (,))) (Map.toList txaccessList)-      touched = if o.vmoptCreate then [txorigin] else [txorigin, txtoAddr]-  in-  VM-  { _result = Nothing-  , _frames = mempty-  , _tx = TxState-    { _gasprice = o.vmoptGasprice-    , _txgaslimit = o.vmoptGaslimit-    , _txPriorityFee = o.vmoptPriorityFee-    , _origin = txorigin-    , _toAddr = txtoAddr-    , _value = o.vmoptValue-    , _substate = SubState mempty touched initialAccessedAddrs initialAccessedStorageKeys mempty-    --, _accessList = txaccessList-    , _isCreate = o.vmoptCreate-    , _txReversion = Map.fromList-      [(o.vmoptAddress , o.vmoptContract )]-    }-  , _logs = []-  , _traces = Zipper.fromForest []-  , _block = Block-    { _coinbase = o.vmoptCoinbase-    , _timestamp = o.vmoptTimestamp-    , _number = o.vmoptNumber-    , _prevRandao = o.vmoptPrevRandao-    , _maxCodeSize = o.vmoptMaxCodeSize-    , _gaslimit = o.vmoptBlockGaslimit-    , _baseFee = o.vmoptBaseFee-    , _schedule = o.vmoptSchedule-    }-  , _state = FrameState-    { _pc = 0-    , _stack = mempty-    , _memory = mempty-    , _memorySize = 0-    , _code = o.vmoptContract._contractcode-    , _contract = o.vmoptAddress-    , _codeContract = o.vmoptAddress-    , _calldata = fst o.vmoptCalldata-    , _callvalue = o.vmoptValue-    , _caller = o.vmoptCaller-    , _gas = o.vmoptGas-    , _returndata = mempty-    , _static = False-    }-  , _env = Env-    { _sha3Crack = mempty-    , _chainId = o.vmoptChainId-    , _storage = if o.vmoptStorageBase == Concrete then EmptyStore else AbstractStore-    , _origStorage = mempty-    , _contracts = Map.fromList-      [(o.vmoptAddress, o.vmoptContract )]-    --, _keccakUsed = mempty-    --, _storageModel = vmoptStorageModel o-    }-  , _cache = Cache mempty mempty mempty-  , _burned = 0-  , _constraints = snd o.vmoptCalldata-  , _keccakEqs = mempty-  , _iterations = mempty-  , _allowFFI = o.vmoptAllowFFI-  , _overrideCaller = Nothing-  }---- | Initialize empty contract with given code-initialContract :: ContractCode -> Contract-initialContract theContractCode = Contract-  { _contractcode = theContractCode-  , _codehash = hashcode theContractCode-  , _balance  = 0-  , _nonce    = if creation then 1 else 0-  , _opIxMap  = mkOpIxMap theContractCode-  , _codeOps  = mkCodeOps theContractCode-  , _external = False-  } where-      creation = case theContractCode of-        InitCode _ _  -> True-        RuntimeCode _ -> False---- * Opcode dispatch (exec1)---- | Update program counter-next :: (?op :: Word8) => EVM ()-next = modifying (state . pc) (+ (opSize ?op))---- | Executes the EVM one step-exec1 :: EVM ()-exec1 = do-  vm <- get--  let-    -- Convenient aliases-    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)--    fees@FeeSchedule {..} = vm._block._schedule--    doStop = finishFrame (FrameReturned mempty)--  if self > 0x0 && self <= 0x9 then do-    -- call to precompile-    let ?op = 0x00 -- dummy value-    case bufLength vm._state._calldata of-      (Lit calldatasize) -> do-          copyBytesToMemory vm._state._calldata (Lit calldatasize) (Lit 0) (Lit 0)-          executePrecompile self vm._state._gas 0 calldatasize 0 0 []-          vmx <- get-          case vmx._state._stack of-            (x:_) -> case x of-              Lit (num -> x' :: Integer) -> case x' of-                0 -> do-                  fetchAccount self $ \_ -> do-                    touchAccount self-                    vmError PrecompileFailure-                _ -> fetchAccount self $ \_ -> do-                    touchAccount self-                    out <- use (state . returndata)-                    finishFrame (FrameReturned out)-              e -> vmError $-                UnexpectedSymbolicArg vmx._state._pc "precompile returned a symbolic value" [e]-            _ ->-              underrun-      e -> vmError $ UnexpectedSymbolicArg vm._state._pc "cannot call precompiles with symbolic data" [e]--  else if vm._state._pc >= opslen vm._state._code-    then doStop--    else do-      let ?op = case vm._state._code of-                  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") $-                      unlitByte $ ops V.! vm._state._pc--      case getOp(?op) of--        OpPush n' -> do-          let n = fromIntegral 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-                RuntimeCode (SymbolicRuntimeCode ops) ->-                  let bytes = V.take n $ V.drop (1 + vm._state._pc) ops-                  in readWord (Lit 0) $ Expr.fromList $ padLeft' 32 bytes-          limitStack 1 $-            burn g_verylow $ do-              next-              pushSym xs--        OpDup i ->-          case preview (ix (fromIntegral i - 1)) stk of-            Nothing -> underrun-            Just y ->-              limitStack 1 $-                burn g_verylow $ do-                  next-                  pushSym y--        OpSwap i ->-          if length stk < (fromIntegral 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)--        OpLog n ->-          notStatic $-          case stk of-            (xOffset':xSize':xs) ->-              if length xs < (fromIntegral n)-              then underrun-              else-                forceConcrete2 (xOffset', xSize') "LOG" $ \(xOffset, xSize) -> do-                    let (topics, xs') = splitAt (fromIntegral 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) $-                      accessMemoryRange xOffset xSize $ do-                        traceTopLog logs'-                        next-                        assign (state . stack) xs'-                        assign logs logs'-            _ ->-              underrun--        OpStop -> doStop--        OpAdd -> stackOp2 g_verylow (uncurry Expr.add)-        OpMul -> stackOp2 g_low (uncurry Expr.mul)-        OpSub -> stackOp2 g_verylow (uncurry Expr.sub)--        OpDiv -> stackOp2 g_low (uncurry Expr.div)--        OpSdiv -> stackOp2 g_low (uncurry Expr.sdiv)--        OpMod-> stackOp2 g_low (uncurry Expr.mod)--        OpSmod -> stackOp2 g_low (uncurry Expr.smod)-        OpAddmod -> stackOp3 g_mid (uncurryN Expr.addmod)-        OpMulmod -> stackOp3 g_mid (uncurryN Expr.mulmod)--        OpLt -> stackOp2 g_verylow (uncurry Expr.lt)-        OpGt -> stackOp2 g_verylow (uncurry Expr.gt)-        OpSlt -> stackOp2 g_verylow (uncurry Expr.slt)-        OpSgt -> stackOp2 g_verylow (uncurry Expr.sgt)--        OpEq -> stackOp2 g_verylow (uncurry Expr.eq)-        OpIszero -> stackOp1 g_verylow Expr.iszero--        OpAnd -> stackOp2 g_verylow (uncurry Expr.and)-        OpOr -> stackOp2 g_verylow (uncurry Expr.or)-        OpXor -> stackOp2 g_verylow (uncurry Expr.xor)-        OpNot -> stackOp1 g_verylow Expr.not--        OpByte -> stackOp2 g_verylow (\(i, w) -> Expr.padByte $ Expr.indexWord i w)--        OpShl -> stackOp2 g_verylow (uncurry Expr.shl)-        OpShr -> stackOp2 g_verylow (uncurry Expr.shr)-        OpSar -> stackOp2 g_verylow (uncurry Expr.sar)--        -- more accurately refered to as KECCAK-        OpSha3 ->-          case stk of-            (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) $-                    accessMemoryRange xOffset xSize $ do-                      (hash, invMap) <- case readMemory xOffset' xSize' vm of-                                          ConcreteBuf bs -> do-                                            let hash' = keccak' bs-                                            eqs <- use keccakEqs-                                            assign keccakEqs $ PEq (Lit hash') (Keccak (ConcreteBuf bs)):eqs-                                            pure (Lit hash', Map.singleton hash' bs)-                                          buf -> pure (Keccak buf, mempty)-                      next-                      assign (state . stack) (hash : xs)-                      (env . sha3Crack) <>= invMap-            _ -> underrun--        OpAddress ->-          limitStack 1 $-            burn g_base (next >> push (num self))--        OpBalance ->-          case stk of-            (x':xs) -> forceConcrete x' "BALANCE" $ \x ->-              accessAndBurn (num x) $-                fetchAccount (num x) $ \c -> do-                  next-                  assign (state . stack) xs-                  push (num c._balance)-            [] ->-              underrun--        OpOrigin ->-          limitStack 1 . burn g_base $-            next >> push (num vm._tx._origin)--        OpCaller ->-          limitStack 1 . burn g_base $-            next >> pushSym vm._state._caller--        OpCallvalue ->-          limitStack 1 . burn g_base $-            next >> pushSym vm._state._callvalue--        OpCalldataload -> stackOp1 g_verylow $-          \ind -> Expr.readWord ind vm._state._calldata--        OpCalldatasize ->-          limitStack 1 . burn g_base $-            next >> pushSym (bufLength vm._state._calldata)--        OpCalldatacopy ->-          case stk of-            (xTo' : xFrom : xSize' : xs) ->-              forceConcrete2 (xTo', xSize') "CALLDATACOPY" $-                \(xTo, xSize) ->-                  burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $-                    accessMemoryRange xTo xSize $ do-                      next-                      assign (state . stack) xs-                      copyBytesToMemory vm._state._calldata xSize' xFrom xTo'-            _ -> underrun--        OpCodesize ->-          limitStack 1 . burn g_base $-            next >> pushSym (codelen vm._state._code)--        OpCodecopy ->-          case stk of-            (memOffset' : codeOffset : n' : xs) ->-              forceConcrete2 (memOffset', n') "CODECOPY" $-                \(memOffset,n) -> do-                  case toWord64 n of-                    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) $-                          accessMemoryRange memOffset n $ do-                            next-                            assign (state . stack) xs-                            copyBytesToMemory (toBuf vm._state._code) n' codeOffset memOffset'-                      else vmError IllegalOverflow-            _ -> underrun--        OpGasprice ->-          limitStack 1 . burn g_base $-            next >> push vm._tx._gasprice--        OpExtcodesize ->-          case stk of-            (x':xs) -> case x' of-              (Lit x) -> if x == num cheatCode-                then do-                  next-                  assign (state . stack) xs-                  pushSym (Lit 1)-                else-                  accessAndBurn (num x) $-                    fetchAccount (num x) $ \c -> do-                      next-                      assign (state . stack) xs-                      pushSym (bufLength (view bytecode c))-              _ -> do-                assign (state . stack) xs-                pushSym (CodeSize x')-                next-            [] ->-              underrun--        OpExtcodecopy ->-          case stk of-            ( extAccount'-              : memOffset'-              : codeOffset-              : codeSize'-              : xs ) ->-              forceConcrete3 (extAccount', memOffset', codeSize') "EXTCODECOPY" $-                \(extAccount, memOffset, codeSize) -> do-                  acc <- accessAccountForGas (num extAccount)-                  let cost = if acc then g_warm_storage_read else g_cold_account_access-                  burn (cost + g_copy * ceilDiv (num codeSize) 32) $-                    accessMemoryRange memOffset codeSize $-                      fetchAccount (num extAccount) $ \c -> do-                        next-                        assign (state . stack) xs-                        copyBytesToMemory (view bytecode c) codeSize' codeOffset memOffset'-            _ -> underrun--        OpReturndatasize ->-          limitStack 1 . burn g_base $-            next >> pushSym (bufLength vm._state._returndata)--        OpReturndatacopy ->-          case stk of-            (xTo' : xFrom : xSize' :xs) -> forceConcrete2 (xTo', xSize') "RETURNDATACOPY" $-              \(xTo, xSize) ->-                burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $-                  accessMemoryRange xTo xSize $ do-                    next-                    assign (state . stack) xs--                    let jump True = vmError EVM.ReturnDataOutOfBounds-                        jump False = copyBytesToMemory vm._state._returndata xSize' xFrom xTo'--                    case (xFrom, bufLength vm._state._returndata) of-                      (Lit f, Lit l) ->-                        jump $ l < f + xSize || f + xSize < f-                      _ -> do-                        let oob = Expr.lt (bufLength vm._state._returndata) (Expr.add xFrom xSize')-                            overflow = Expr.lt (Expr.add xFrom xSize') (xFrom)-                        loc <- codeloc-                        branch loc (Expr.or oob overflow) jump-            _ -> underrun--        OpExtcodehash ->-          case stk of-            (x':xs) -> forceConcrete x' "EXTCODEHASH" $ \x ->-              accessAndBurn (num x) $ do-                next-                assign (state . stack) xs-                fetchAccount (num x) $ \c ->-                   if accountEmpty c-                     then push (num (0 :: Int))-                     else pushSym $ keccak (view bytecode c)-            [] ->-              underrun--        OpBlockhash -> do-          -- We adopt the fake block hash scheme of the VMTests,-          -- so that blockhash(i) is the hash of i as decimal ASCII.-          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-            i -> BlockHash i--        OpCoinbase ->-          limitStack 1 . burn g_base $-            next >> push (num vm._block._coinbase)--        OpTimestamp ->-          limitStack 1 . burn g_base $-            next >> pushSym vm._block._timestamp--        OpNumber ->-          limitStack 1 . burn g_base $-            next >> push vm._block._number--        OpPrevRandao -> do-          limitStack 1 . burn g_base $-            next >> push vm._block._prevRandao--        OpGaslimit ->-          limitStack 1 . burn g_base $-            next >> push (num vm._block._gaslimit)--        OpChainid ->-          limitStack 1 . burn g_base $-            next >> push vm._env._chainId--        OpSelfbalance ->-          limitStack 1 . burn g_low $-            next >> push this._balance--        OpBaseFee ->-          limitStack 1 . burn g_base $-            next >> push vm._block._baseFee--        OpPop ->-          case stk of-            (_:xs) -> burn g_base (next >> assign (state . stack) xs)-            _      -> underrun--        OpMload ->-          case stk of-            (x':xs) -> forceConcrete x' "MLOAD" $ \x ->-              burn g_verylow $-                accessMemoryWord x $ do-                  next-                  assign (state . stack) (readWord (Lit x) mem : xs)-            _ -> underrun--        OpMstore ->-          case stk of-            (x':y:xs) -> forceConcrete x' "MSTORE index" $ \x ->-              burn g_verylow $-                accessMemoryWord x $ do-                  next-                  assign (state . memory) (writeWord (Lit x) y mem)-                  assign (state . stack) xs-            _ -> underrun--        OpMstore8 ->-          case stk of-            (x':y:xs) -> forceConcrete x' "MSTORE8" $ \x ->-              burn g_verylow $-                accessMemoryRange x 1 $ do-                  let yByte = indexWord (Lit 31) y-                  next-                  modifying (state . memory) (writeByte (Lit x) yByte)-                  assign (state . stack) xs-            _ -> underrun--        OpSload ->-          case stk of-            (x:xs) -> do-              acc <- accessStorageForGas self x-              let cost = if acc then g_warm_storage_read else g_cold_sload-              burn cost $-                accessStorage self x $ \y -> do-                  next-                  assign (state . stack) (y:xs)-            _ -> underrun--        OpSstore ->-          notStatic $-          case stk of-            (x:new:xs) ->-              accessStorage self x $ \current -> do-                availableGas <- use (state . gas)--                if num availableGas <= g_callstipend-                  then finishFrame (FrameErrored (OutOfGas availableGas (num g_callstipend)))-                  else do-                    let original = case readStorage (litAddr self) x (ConcreteStore vm._env._origStorage) of-                                     Just (Lit v) -> v-                                     _ -> 0-                    let storage_cost = case (maybeLitWord current, maybeLitWord new) of-                                 (Just current', Just new') ->-                                    if (current' == new') then g_sload-                                    else if (current' == original) && (original == 0) then g_sset-                                    else if (current' == original) then g_sreset-                                    else g_sload--                                 -- if any of the arguments are symbolic,-                                 -- assume worst case scenario-                                 _ -> g_sset--                    acc <- accessStorageForGas self x-                    let cold_storage_cost = if acc then 0 else g_cold_sload-                    burn (storage_cost + cold_storage_cost) $ do-                      next-                      assign (state . stack) xs-                      modifying (env . storage)-                        (writeStorage (litAddr self) x new)--                      case (maybeLitWord current, maybeLitWord new) of-                         (Just current', Just new') ->-                            unless (current' == new') $-                              if current' == original-                              then when (original /= 0 && new' == 0) $-                                      refund (g_sreset + g_access_list_storage_key)-                              else do-                                      when (original /= 0) $-                                        if new' == 0-                                        then refund (g_sreset + g_access_list_storage_key)-                                        else unRefund (g_sreset + g_access_list_storage_key)-                                      when (original == new') $-                                        if original == 0-                                        then refund (g_sset - g_sload)-                                        else refund (g_sreset - g_sload)-                         -- if any of the arguments are symbolic,-                         -- don't change the refund counter-                         _ -> noop-            _ -> underrun--        OpJump ->-          case stk of-            (x:xs) ->-              burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' ->-                case toInt x' of-                  Nothing -> vmError EVM.BadJumpDestination-                  Just i -> checkJump i xs-            _ -> underrun--        OpJumpi -> do-          case stk of-            (x:y:xs) -> forceConcrete x "JUMPI: symbolic jumpdest" $ \x' ->-                burn g_high $-                  let jump :: Bool -> EVM ()-                      jump False = assign (state . stack) xs >> next-                      jump _    = case toInt x' of-                        Nothing -> vmError EVM.BadJumpDestination-                        Just i -> checkJump i xs-                  in case maybeLitWord y of-                      Just y' -> jump (0 /= y')-                      -- if the jump condition is symbolic, we explore both sides-                      Nothing -> do-                        loc <- codeloc-                        branch loc y jump-            _ -> underrun--        OpPc ->-          limitStack 1 . burn g_base $-            next >> push (num vm._state._pc)--        OpMsize ->-          limitStack 1 . burn g_base $-            next >> push (num vm._state._memorySize)--        OpGas ->-          limitStack 1 . burn g_base $-            next >> push (num (vm._state._gas - g_base))--        OpJumpdest -> burn g_jumpdest next--        OpExp ->-          -- NOTE: this can be done symbolically using unrolling like this:-          --       https://hackage.haskell.org/package/sbv-9.0/docs/src/Data.SBV.Core.Model.html#.%5E-          --       However, it requires symbolic gas, since the gas depends on the exponent-          case stk of-            (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)-              in burn cost $ do-                next-                state . stack .= Expr.exp base exponent' : xs-            _ -> underrun--        OpSignextend -> stackOp2 g_low (uncurry Expr.sex)--        OpCreate ->-          notStatic $-          case stk of-            (xValue' : xOffset' : xSize' : xs) -> forceConcrete3 (xValue', xOffset', xSize') "CREATE" $-              \(xValue, xOffset, xSize) -> do-                accessMemoryRange xOffset xSize $ do-                  availableGas <- use (state . gas)-                  let-                    newAddr = createAddress self this._nonce-                    (cost, gas') = costOfCreate fees availableGas 0-                  _ <- accessAccountForGas newAddr-                  burn (cost - gas') $ do-                    -- unfortunately we have to apply some (pretty hacky)-                    -- heuristics here to parse the unstructured buffer read-                    -- from memory into a code and data section-                    let initCode = readMemory xOffset' xSize' vm-                    create self this (num gas') xValue xs newAddr initCode-            _ -> underrun--        OpCall ->-          case stk of-            ( xGas'-              : xTo-              : xValue'-              : xInOffset'-              : xInSize'-              : xOutOffset'-              : xOutSize'-              : xs-             ) -> 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-                    zoom state $ do-                      assign callvalue (Lit xValue)-                      assign caller $ fromMaybe (litAddr self) (vm ^. overrideCaller)-                      assign contract callee-                    assign overrideCaller Nothing-                    transfer self callee xValue-                    touchAccount self-                    touchAccount callee-            _ ->-              underrun--        OpCallcode ->-          case stk of-            ( 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-                    zoom state $ do-                      assign callvalue (Lit xValue)-                      assign caller $ fromMaybe (litAddr self) (vm ^. overrideCaller)-                    assign overrideCaller Nothing-                    touchAccount self-            _ ->-              underrun--        OpReturn ->-          case stk of-            (xOffset' : xSize' :_) -> forceConcrete2 (xOffset', xSize') "RETURN" $ \(xOffset, xSize) ->-              accessMemoryRange xOffset xSize $ do-                let-                  output = readMemory xOffset' xSize' vm-                  codesize = fromMaybe (error "RETURN: cannot return dynamically sized abstract data")-                               . unlit . bufLength $ output-                  maxsize = vm._block._maxCodeSize-                  creation = case vm._frames of-                    [] -> vm._tx._isCreate-                    frame:_ -> case frame._frameContext of-                       CreationContext {} -> True-                       CallContext {} -> False-                if creation-                then-                  if codesize > maxsize-                  then-                    finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))-                  else do-                    let frameReturned = burn (g_codedeposit * num codesize) $-                                          finishFrame (FrameReturned output)-                        frameErrored = finishFrame $ FrameErrored InvalidFormat-                    case readByte (Lit 0) output of-                      LitByte 0xef -> frameErrored-                      LitByte _ -> frameReturned-                      y -> do-                        loc <- codeloc-                        branch loc (Expr.eqByte y (LitByte 0xef)) $ \case-                          True -> frameErrored-                          False -> frameReturned-                else-                   finishFrame (FrameReturned output)-            _ -> underrun--        OpDelegatecall ->-          case stk of-            (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-                  touchAccount self-            _ -> underrun--        OpCreate2 -> notStatic $-          case stk of-            (xValue'-             :xOffset'-             :xSize'-             :xSalt'-             :xs) -> forceConcrete4 (xValue', xOffset', xSize', xSalt') "CREATE2" $-              \(xValue, xOffset, xSize, xSalt) ->-                accessMemoryRange xOffset xSize $ do-                  availableGas <- use (state . gas)--                  forceConcreteBuf (readMemory xOffset' xSize' vm) "CREATE2" $-                    \initCode -> do-                      let-                        newAddr  = create2Address self xSalt initCode-                        (cost, gas') = costOfCreate fees availableGas xSize-                      _ <- accessAccountForGas newAddr-                      burn (cost - gas') $ create self this gas' xValue xs newAddr (ConcreteBuf initCode)-            _ -> underrun--        OpStaticcall ->-          case stk of-            (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-                  zoom state $ do-                    assign callvalue (Lit 0)-                    assign caller $ fromMaybe (litAddr self) (vm ^. overrideCaller)-                    assign contract callee-                    assign static True-                  assign overrideCaller Nothing-                  touchAccount self-                  touchAccount callee-            _ ->-              underrun--        OpSelfdestruct ->-          notStatic $-          case stk of-            [] -> underrun-            (xTo':_) -> forceConcrete xTo' "SELFDESTRUCT" $ \(num -> xTo) -> do-              acc <- accessAccountForGas (num xTo)-              let cost = if acc then 0 else g_cold_account_access-                  funds = this._balance-                  recipientExists = accountExists xTo vm-                  c_new = if not recipientExists && funds /= 0-                          then g_selfdestruct_newaccount-                          else 0-              burn (g_selfdestruct + c_new + cost) $ do-                   selfdestruct self-                   touchAccount xTo--                   if funds /= 0-                   then fetchAccount xTo $ \_ -> do-                          env . contracts . ix xTo . balance += funds-                          assign (env . contracts . ix self . balance) 0-                          doStop-                   else doStop--        OpRevert ->-          case stk of-            (xOffset':xSize':_) -> forceConcrete2 (xOffset', xSize') "REVERT" $ \(xOffset, xSize) ->-              accessMemoryRange xOffset xSize $ do-                let output = readMemory xOffset' xSize' vm-                finishFrame (FrameReverted output)-            _ -> underrun--        OpUnknown xxx ->-          vmError (UnrecognizedOpcode xxx)--transfer :: Addr -> Addr -> W256 -> EVM ()-transfer xFrom xTo xValue =-  zoom (env . contracts) $ do-    ix xFrom . balance -= xValue-    ix xTo  . balance += xValue---- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.-callChecks-  :: (?op :: Word8)-  => Contract -> Word64 -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord]-   -- continuation with gas available for call-  -> (Word64 -> EVM ())-  -> EVM ()-callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue = do-  vm <- get-  let fees = vm._block._schedule-  accessMemoryRange xInOffset xInSize $-    accessMemoryRange xOutOffset xOutSize $ do-      availableGas <- use (state . gas)-      let recipientExists = accountExists xContext vm-      (cost, gas') <- costOfCall fees recipientExists xValue availableGas xGas xTo-      burn (cost - gas') $ do-        if xValue > num this._balance-        then do-          assign (state . stack) (Lit 0 : xs)-          assign (state . returndata) mempty-          pushTrace $ ErrorTrace $ BalanceTooLow xValue this._balance-          next-        else if length vm._frames >= 1024-             then do-               assign (state . stack) (Lit 0 : xs)-               assign (state . returndata) mempty-               pushTrace $ ErrorTrace CallDepthLimitReached-               next-             else continue gas'--precompiledContract-  :: (?op :: Word8)-  => Contract-  -> Word64-  -> Addr-  -> Addr-  -> W256-  -> W256 -> W256 -> W256 -> W256-  -> [Expr EWord]-  -> EVM ()-precompiledContract this xGas precompileAddr recipient xValue inOffset inSize outOffset outSize xs =-  callChecks this xGas recipient precompileAddr xValue inOffset inSize outOffset outSize xs $ \gas' ->-  do-    executePrecompile precompileAddr gas' inOffset inSize outOffset outSize xs-    self <- use (state . contract)-    stk <- use (state . stack)-    pc' <- use (state . pc)-    result' <- use result-    case result' of-      Nothing -> case stk of-        (x:_) -> case maybeLitWord x of-          Just 0 ->-            return ()-          Just 1 ->-            fetchAccount recipient $ \_ -> do-              transfer self recipient xValue-              touchAccount self-              touchAccount recipient-          _ -> vmError $ UnexpectedSymbolicArg pc' "unexpected return value from precompile" [x]-        _ -> underrun-      _ -> pure ()--executePrecompile-  :: (?op :: Word8)-  => Addr-  -> Word64 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord]-  -> EVM ()-executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  = do-  vm <- get-  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"-      precompileFail = burn (gasCap - cost) $ do-                         assign (state . stack) (Lit 0 : xs)-                         pushTrace $ ErrorTrace PrecompileFailure-                         next-  if cost > gasCap then-    burn gasCap $ do-      assign (state . stack) (Lit 0 : xs)-      next-  else-    burn cost $-      case preCompileAddr of-        -- ECRECOVER-        0x1 ->-          -- TODO: support symbolic variant-          forceConcreteBuf input "ECRECOVER" $ \input' -> do-            case EVM.Precompiled.execute 0x1 (truncpadlit 128 input') 32 of-              Nothing -> do-                -- return no output for invalid signature-                assign (state . stack) (Lit 1 : xs)-                assign (state . returndata) mempty-                next-              Just output -> do-                assign (state . stack) (Lit 1 : xs)-                assign (state . returndata) (ConcreteBuf output)-                copyBytesToMemory (ConcreteBuf output) (Lit outSize) (Lit 0) (Lit outOffset)-                next--        -- SHA2-256-        0x2 -> forceConcreteBuf input "SHA2-256" $ \input' -> do-          let-            hash = sha256Buf input'-            sha256Buf x = ConcreteBuf $ BA.convert (Crypto.hash x :: Digest SHA256)-          assign (state . stack) (Lit 1 : xs)-          assign (state . returndata) hash-          copyBytesToMemory hash (Lit outSize) (Lit 0) (Lit outOffset)-          next--        -- RIPEMD-160-        0x3 ->-         -- TODO: support symbolic variant-         forceConcreteBuf input "RIPEMD160" $ \input' ->--          let-            padding = BS.pack $ replicate 12 0-            hash' = BA.convert (Crypto.hash input' :: Digest RIPEMD160)-            hash  = ConcreteBuf $ padding <> hash'-          in do-            assign (state . stack) (Lit 1 : xs)-            assign (state . returndata) hash-            copyBytesToMemory hash (Lit outSize) (Lit 0) (Lit outOffset)-            next--        -- IDENTITY-        0x4 -> do-            assign (state . stack) (Lit 1 : xs)-            assign (state . returndata) input-            copyCallBytesToMemory input (Lit outSize) (Lit 0) (Lit outOffset)-            next--        -- MODEXP-        0x5 ->-         -- TODO: support symbolic variant-         forceConcreteBuf input "MODEXP" $ \input' ->--          let-            (lenb, lene, lenm) = parseModexpLength input'--            output = ConcreteBuf $-              if isZero (96 + lenb + lene) lenm input'-              then truncpadlit (num 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))-          in do-            assign (state . stack) (Lit 1 : xs)-            assign (state . returndata) output-            copyBytesToMemory output (Lit outSize) (Lit 0) (Lit outOffset)-            next--        -- ECADD-        0x6 ->-         -- TODO: support symbolic variant-         forceConcreteBuf input "ECADD" $ \input' ->-           case EVM.Precompiled.execute 0x6 (truncpadlit 128 input') 64 of-          Nothing -> precompileFail-          Just output -> do-            let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output-            assign (state . stack) (Lit 1 : xs)-            assign (state . returndata) truncpaddedOutput-            copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)-            next--        -- ECMUL-        0x7 ->-         -- TODO: support symbolic variant-         forceConcreteBuf input "ECMUL" $ \input' ->--          case EVM.Precompiled.execute 0x7 (truncpadlit 96 input') 64 of-          Nothing -> precompileFail-          Just output -> do-            let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output-            assign (state . stack) (Lit 1 : xs)-            assign (state . returndata) truncpaddedOutput-            copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)-            next--        -- ECPAIRING-        0x8 ->-         -- TODO: support symbolic variant-         forceConcreteBuf input "ECPAIR" $ \input' ->--          case EVM.Precompiled.execute 0x8 input' 32 of-          Nothing -> precompileFail-          Just output -> do-            let truncpaddedOutput = ConcreteBuf $ truncpadlit 32 output-            assign (state . stack) (Lit 1 : xs)-            assign (state . returndata) truncpaddedOutput-            copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)-            next--        -- BLAKE2-        0x9 ->-         -- TODO: support symbolic variant-         forceConcreteBuf input "BLAKE2" $ \input' -> do--          case (BS.length input', 1 >= BS.last input') of-            (213, True) -> case EVM.Precompiled.execute 0x9 input' 64 of-              Just output -> do-                let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output-                assign (state . stack) (Lit 1 : xs)-                assign (state . returndata) truncpaddedOutput-                copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)-                next-              Nothing -> precompileFail-            _ -> precompileFail---        _   -> notImplemented--truncpadlit :: Int -> ByteString -> ByteString-truncpadlit n xs = if m > n then BS.take n xs-                   else BS.append xs (BS.replicate (n - m) 0)-  where m = BS.length xs--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--parseModexpLength :: ByteString -> (W256, W256, W256)-parseModexpLength input =-  let lenb = word $ LS.toStrict $ lazySlice  0 32 input-      lene = word $ LS.toStrict $ lazySlice 32 64 input-      lenm = word $ LS.toStrict $ lazySlice 64 96 input-  in (lenb, lene, lenm)----- checks if a range of ByteString bs starting at offset and length size is all zeros.-isZero :: W256 -> W256 -> ByteString -> Bool-isZero offset size bs =-  LS.all (== 0) $-    LS.take (num size) $-      LS.drop (num offset) $-        fromStrict bs--asInteger :: LS.ByteString -> Integer-asInteger xs = if xs == mempty then 0-  else 256 * asInteger (LS.init xs)-      + num (LS.last xs)---- * Opcode helper actions--noop :: Monad m => m ()-noop = pure ()--pushTo :: MonadState s m => ASetter s s [a] [a] -> a -> m ()-pushTo f x = f %= (x :)--pushToSequence :: MonadState s m => ASetter s s (Seq a) (Seq a) -> a -> m ()-pushToSequence f x = f %= (Seq.|> x)--getCodeLocation :: VM -> CodeLocation-getCodeLocation vm = (vm._state._contract, vm._state._pc)--branch :: CodeLocation -> Expr EWord -> (Bool -> EVM ()) -> EVM ()-branch loc cond continue = do-  pathconds <- use constraints-  assign result . Just . VMFailure . Query $ PleaseAskSMT cond pathconds choosePath-  where-     choosePath (Case v) = do assign result Nothing-                              pushTo constraints $ if v then (cond ./= (Lit 0)) else (cond .== (Lit 0))-                              iteration <- use (iterations . at loc . non 0)-                              assign (cache . path . at (loc, iteration)) (Just v)-                              assign (iterations . at loc) (Just (iteration + 1))-                              continue v-     -- Both paths are possible; we ask for more input-     choosePath Unknown = assign result . Just . VMFailure . Choose . PleaseChoosePath cond $ choosePath . Case-     -- None of the paths are possible; fail this branch-     choosePath Inconsistent = vmError DeadPath----- | Construct RPC Query and halt execution until resolved-fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM ()-fetchAccount addr continue =-  use (env . contracts . at addr) >>= \case-    Just c -> continue c-    Nothing ->-      use (cache . fetchedContracts . at addr) >>= \case-        Just c -> do-          assign (env . contracts . at addr) (Just c)-          continue c-        Nothing -> do-          assign result . Just . VMFailure $ Query $-            PleaseFetchContract addr-              (\c -> do assign (cache . fetchedContracts . at addr) (Just c)-                        assign (env . contracts . at addr) (Just c)-                        assign result Nothing-                        continue c)--accessStorage-  :: Addr                   -- ^ Contract address-  -> Expr EWord             -- ^ Storage slot key-  -> (Expr EWord -> EVM ()) -- ^ Continuation-  -> EVM ()-accessStorage addr slot continue = do-  store <- use (env . storage)-  use (env . contracts . at addr) >>= \case-    Just c ->-      case readStorage (litAddr addr) slot store of-        -- Notice that if storage is symbolic, we always continue straight away-        Just x ->-          continue x-        Nothing ->-          if c._external then-            forceConcrete slot "cannot read symbolic slots via RPC" $ \litSlot -> do-              -- check if the slot is cached-              cachedStore <- use (cache . fetchedStorage)-              case Map.lookup (num addr) cachedStore >>= Map.lookup litSlot of-                Nothing -> mkQuery litSlot-                Just val -> continue (Lit val)-          else do-            modifying (env . storage) (writeStorage (litAddr addr) slot (Lit 0))-            continue $ Lit 0-    Nothing ->-      fetchAccount addr $ \_ ->-        accessStorage addr slot continue-  where-      mkQuery s = assign result . Just . VMFailure . Query $-                    PleaseFetchSlot addr s-                      (\x -> do-                          modifying (cache . fetchedStorage . ix (num addr)) (Map.insert s x)-                          modifying (env . storage) (writeStorage (litAddr addr) slot (Lit x))-                          assign result Nothing-                          continue (Lit x))--accountExists :: Addr -> VM -> Bool-accountExists addr vm =-  case Map.lookup addr vm._env._contracts of-    Just c -> not (accountEmpty c)-    Nothing -> False---- EIP 161-accountEmpty :: Contract -> Bool-accountEmpty c =-  case c._contractcode of-    RuntimeCode (ConcreteRuntimeCode "") -> True-    RuntimeCode (SymbolicRuntimeCode b) -> null b-    _ -> False-  && c._nonce == 0-  && c._balance  == 0---- * How to finalize a transaction-finalize :: EVM ()-finalize = do-  let-    revertContracts  = use (tx . txReversion) >>= assign (env . contracts)-    revertSubstate   = assign (tx . substate) (SubState mempty mempty mempty mempty mempty)--  use result >>= \case-    Nothing ->-      error "Finalising an unfinished tx."-    Just (VMFailure (EVM.Revert _)) -> do-      revertContracts-      revertSubstate-    Just (VMFailure _) -> do-      -- burn remaining gas-      assign (state . gas) 0-      revertContracts-      revertSubstate-    Just (VMSuccess output) -> do-      -- deposit the code from a creation tx-      pc' <- use (state . pc)-      creation <- use (tx . isCreate)-      createe  <- use (state . contract)-      createeExists <- (Map.member createe) <$> use (env . contracts)-      let onContractCode contractCode =-            when (creation && createeExists) $ replaceCode createe contractCode-      case output of-        ConcreteBuf bs ->-          onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)-        _ ->-          case Expr.toList output of-            Nothing ->-              vmError $ UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" [output]-            Just ops ->-              onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)--  -- compute and pay the refund to the caller and the-  -- corresponding payment to the miner-  txOrigin     <- use (tx . origin)-  sumRefunds   <- (sum . (snd <$>)) <$> (use (tx . substate . refunds))-  miner        <- use (block . coinbase)-  blockReward  <- num . (.r_block) <$> (use (block . schedule))-  gasPrice     <- use (tx . gasprice)-  priorityFee  <- use (tx . txPriorityFee)-  gasLimit     <- use (tx . txgaslimit)-  gasRemaining <- use (state . gas)--  let-    gasUsed      = gasLimit - gasRemaining-    cappedRefund = min (quot gasUsed 5) (num sumRefunds)-    originPay    = (num $ gasRemaining + cappedRefund) * gasPrice--    minerPay     = priorityFee * (num gasUsed)--  modifying (env . contracts)-     (Map.adjust (over balance (+ originPay)) txOrigin)-  modifying (env . contracts)-     (Map.adjust (over balance (+ minerPay)) miner)-  touchAccount miner--  -- pay out the block reward, recreating the miner if necessary-  preuse (env . contracts . ix miner) >>= \case-    Nothing -> modifying (env . contracts)-      (Map.insert miner (initialContract (EVM.RuntimeCode (ConcreteRuntimeCode ""))))-    Just _  -> noop-  modifying (env . contracts)-    (Map.adjust (over balance (+ blockReward)) miner)--  -- perform state trie clearing (EIP 161), of selfdestructs-  -- and touched accounts. addresses are cleared if they have-  --    a) selfdestructed, or-  --    b) been touched and-  --    c) are empty.-  -- (see Yellow Paper "Accrued Substate")-  ---  -- remove any destructed addresses-  destroyedAddresses <- use (tx . substate . selfdestructs)-  modifying (env . contracts)-    (Map.filterWithKey (\k _ -> (k `notElem` destroyedAddresses)))-  -- then, clear any remaining empty and touched addresses-  touchedAddresses <- use (tx . substate . touchedAccounts)-  modifying (env . contracts)-    (Map.filterWithKey-      (\k a -> not ((k `elem` touchedAddresses) && accountEmpty a)))---- | Loads the selected contract as the current contract to execute-loadContract :: Addr -> EVM ()-loadContract target =-  preuse (env . contracts . ix target . contractcode) >>=-    \case-      Nothing ->-        error "Call target doesn't exist"-      Just targetCode -> do-        assign (state . contract) target-        assign (state . code)     targetCode-        assign (state . codeContract) target--limitStack :: Int -> EVM () -> EVM ()-limitStack n continue = do-  stk <- use (state . stack)-  if length stk + n > 1024-    then vmError EVM.StackLimitExceeded-    else continue--notStatic :: EVM () -> EVM ()-notStatic continue = do-  bad <- use (state . static)-  if bad-    then vmError StateChangeWhileStatic-    else continue---- | Burn gas, failing if insufficient gas is available-burn :: Word64 -> EVM () -> EVM ()-burn n continue = do-  available <- use (state . gas)-  if n <= available-    then do-      state . gas -= n-      burned += n-      continue-    else-      vmError (OutOfGas available n)--forceConcrete :: Expr EWord -> String -> (W256 -> EVM ()) -> EVM ()-forceConcrete n msg continue = case maybeLitWord n of-  Nothing -> do-    vm <- get-    vmError $ UnexpectedSymbolicArg vm._state._pc msg [n]-  Just c -> continue c--forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM ()) -> EVM ()-forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of-  (Just c, Just d) -> continue (c, d)-  _ -> do-    vm <- get-    vmError $ UnexpectedSymbolicArg vm._state._pc msg [n, m]--forceConcrete3 :: (Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256) -> EVM ()) -> EVM ()-forceConcrete3 (k,n,m) msg continue = case (maybeLitWord k, maybeLitWord n, maybeLitWord m) of-  (Just c, Just d, Just f) -> continue (c, d, f)-  _ -> do-    vm <- get-    vmError $ UnexpectedSymbolicArg vm._state._pc msg [k, n, m]--forceConcrete4 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256) -> EVM ()) -> EVM ()-forceConcrete4 (k,l,n,m) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord n, maybeLitWord m) of-  (Just b, Just c, Just d, Just f) -> continue (b, c, d, f)-  _ -> do-    vm <- get-    vmError $ UnexpectedSymbolicArg vm._state._pc msg [k, l, n, m]--forceConcrete5 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256) -> EVM ()) -> EVM ()-forceConcrete5 (k,l,m,n,o) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o) of-  (Just a, Just b, Just c, Just d, Just e) -> continue (a, b, c, d, e)-  _ -> do-    vm <- get-    vmError $ UnexpectedSymbolicArg vm._state._pc msg [k, l, m, n, o]--forceConcrete6 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256, W256) -> EVM ()) -> EVM ()-forceConcrete6 (k,l,m,n,o,p) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o, maybeLitWord p) of-  (Just a, Just b, Just c, Just d, Just e, Just f) -> continue (a, b, c, d, e, f)-  _ -> do-    vm <- get-    vmError $ UnexpectedSymbolicArg vm._state._pc msg [k, l, m, n, o, p]--forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM ()) -> EVM ()-forceConcreteBuf (ConcreteBuf b) _ continue = continue b-forceConcreteBuf b msg _ = do-    vm <- get-    vmError $ UnexpectedSymbolicArg vm._state._pc msg [b]---- * Substate manipulation-refund :: Word64 -> EVM ()-refund n = do-  self <- use (state . contract)-  pushTo (tx . substate . refunds) (self, n)--unRefund :: Word64 -> EVM ()-unRefund n = do-  self <- use (state . contract)-  refs <- use (tx . substate . refunds)-  assign (tx . substate . refunds)-    (filter (\(a,b) -> not (a == self && b == n)) refs)--touchAccount :: Addr -> EVM()-touchAccount = pushTo ((tx . substate) . touchedAccounts)--selfdestruct :: Addr -> EVM()-selfdestruct = pushTo ((tx . substate) . selfdestructs)--accessAndBurn :: Addr -> EVM () -> EVM ()-accessAndBurn x cont = do-  FeeSchedule {..} <- use ( block . schedule )-  acc <- accessAccountForGas x-  let cost = if acc then g_warm_storage_read else g_cold_account_access-  burn cost cont---- | returns a wrapped boolean- if true, this address has been touched before in the txn (warm gas cost as in EIP 2929)--- otherwise cold-accessAccountForGas :: Addr -> EVM Bool-accessAccountForGas addr = do-  accessedAddrs <- use (tx . substate . accessedAddresses)-  let accessed = member addr accessedAddrs-  assign (tx . substate . accessedAddresses) (insert addr accessedAddrs)-  return accessed---- | returns a wrapped boolean- if true, this slot has been touched before in the txn (warm gas cost as in EIP 2929)--- otherwise cold-accessStorageForGas :: Addr -> Expr EWord -> EVM Bool-accessStorageForGas addr key = do-  accessedStrkeys <- use (tx . substate . accessedStorageKeys)-  case maybeLitWord key of-    Just litword -> do-      let accessed = member (addr, litword) accessedStrkeys-      assign (tx . substate . accessedStorageKeys) (insert (addr, litword) accessedStrkeys)-      return accessed-    _ -> return False---- * Cheat codes---- The cheat code is 7109709ecfa91a80626ff3989d68f67f5b1dd12d.--- Call this address using one of the cheatActions below to do--- special things, e.g. changing the block timestamp. Beware that--- these are necessarily hevm specific.-cheatCode :: Addr-cheatCode = num (keccak' "hevm cheat code")--cheat-  :: (?op :: Word8)-  => (W256, W256) -> (W256, W256)-  -> EVM ()-cheat (inOffset, inSize) (outOffset, outSize) = do-  mem <- use (state . memory)-  vm <- get-  let-    abi = readBytes 4 (Lit inOffset) mem-    input = readMemory (Lit $ inOffset + 4) (Lit $ inSize - 4) vm-  case maybeLitWord abi of-    Nothing -> vmError $ UnexpectedSymbolicArg vm._state._pc "symbolic cheatcode selector" [abi]-    Just (fromIntegral -> abi') ->-      case Map.lookup abi' cheatActions of-        Nothing ->-          vmError (BadCheatCode (Just abi'))-        Just action -> do-            action (Lit outOffset) (Lit outSize) input-            next-            push 1--type CheatAction = Expr EWord -> Expr EWord -> Expr Buf -> EVM ()--cheatActions :: Map Word32 CheatAction-cheatActions =-  Map.fromList-    [ action "ffi(string[])" $-        \sig outOffset outSize input -> do-          vm <- get-          if vm._allowFFI then-            case decodeBuf [AbiArrayDynamicType AbiStringType] input of-              CAbi valsArr -> case valsArr of-                [AbiArrayDynamic AbiStringType strsV] ->-                  let-                    cmd = fmap-                            (\case-                              (AbiString a) -> unpack $ decodeUtf8 a-                              _ -> "")-                            (V.toList strsV)-                    cont bs = do-                      let encoded = ConcreteBuf bs-                      assign (state . returndata) encoded-                      copyBytesToMemory encoded outSize (Lit 0) outOffset-                      assign result Nothing-                  in assign result (Just . VMFailure . Query $ (PleaseDoFFI cmd cont))-                _ -> vmError (BadCheatCode sig)-              _ -> vmError (BadCheatCode sig)-          else-            let msg = encodeUtf8 "ffi disabled: run again with --ffi if you want to allow tests to call external scripts"-            in vmError . EVM.Revert . ConcreteBuf $-              abiMethod "Error(string)" (AbiTuple . V.fromList $ [AbiString msg]),--      action "warp(uint256)" $-        \sig _ _ input -> case decodeStaticArgs 0 1 input of-          [x]  -> assign (block . timestamp) x-          _ -> vmError (BadCheatCode sig),--      action "roll(uint256)" $-        \sig _ _ input -> case decodeStaticArgs 0 1 input of-          [x] -> forceConcrete x "cannot roll to a symbolic block number" (assign (block . number))-          _ -> vmError (BadCheatCode sig),--      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') ->-              fetchAccount a' $ \_ -> do-                modifying (env . storage) (writeStorage (litAddr a') slot new)-          _ -> vmError (BadCheatCode sig),--      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') ->-              accessStorage a' slot $ \res -> do-                assign (state . returndata . word256At (Lit 0)) res-                assign (state . memory . word256At outOffset) res-          _ -> vmError (BadCheatCode sig),--      action "sign(uint256,bytes32)" $-        \sig outOffset _ input -> case decodeStaticArgs 0 2 input of-          [sk, hash] ->-            forceConcrete2 (sk, hash) "cannot sign symbolic data" $ \(sk', hash') -> do-              let (v,r,s) = EVM.Sign.sign hash' (toInteger sk')-                  encoded = encodeAbiValue $-                    AbiTuple (RegularVector.fromList-                      [ AbiUInt 8 $ num 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-          _ -> 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'-            case a of-              Nothing -> vmError (BadCheatCode sig)-              Just address -> do-                let expAddr = litAddr address-                assign (state . returndata . word256At (Lit 0)) expAddr-                assign (state . memory . word256At outOffset) expAddr-          _ -> vmError (BadCheatCode sig),--      action "prank(address)" $-        \sig _ _ input -> case decodeStaticArgs 0 1 input of-          [addr]  -> assign overrideCaller (Just addr)-          _ -> vmError (BadCheatCode sig)--    ]-  where-    action s f = (abiKeccak s, f (Just $ abiKeccak s))---- | We don't wanna introduce the machinery needed to sign with a random nonce,--- so we just use the same nonce every time (420). This is obviusly very--- insecure, but fine for testing purposes.-ethsign :: PrivateKey -> Digest Crypto.Keccak_256 -> Signature-ethsign sk digest = go 420-  where-    go k = case signDigestWith k sk digest of-       Nothing  -> go (k + 1)-       Just sig -> sig---- * General call implementation ("delegateCall")--- note that the continuation is ignored in the precompile case-delegateCall-  :: (?op :: Word8)-  => Contract -> Word64 -> Expr EWord -> Expr EWord -> W256 -> W256 -> W256 -> W256 -> W256-  -> [Expr EWord]-  -> (Addr -> EVM ())-  -> 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')) ->-      if xTo' > 0 && xTo' <= 9-      then precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs-      else if xTo' == cheatCode then-        do-          assign (state . stack) xs-          cheat (xInOffset, xInSize) (xOutOffset, xOutSize)-      else-        callChecks this gasGiven xContext' xTo' xValue xInOffset xInSize xOutOffset xOutSize xs $-        \xGas -> do-          vm0 <- get-          fetchAccount xTo' $ \target ->-                burn xGas $ do-                  let newContext = CallContext-                                    { callContextTarget    = xTo'-                                    , callContextContext   = xContext'-                                    , callContextOffset    = xOutOffset-                                    , callContextSize      = xOutSize-                                    , callContextCodehash  = target._codehash-                                    , callContextReversion = (vm0._env._contracts, vm0._env._storage)-                                    , callContextSubState  = vm0._tx._substate-                                    , callContextAbi =-                                        if xInSize >= 4-                                        then case unlit $ readBytes 4 (Lit xInOffset) vm0._state._memory-                                             of Nothing -> Nothing-                                                Just abi -> Just $ num abi-                                        else Nothing-                                    , callContextData = (readMemory (Lit xInOffset) (Lit xInSize) vm0)-                                    }--                  pushTrace (FrameTrace newContext)-                  next-                  vm1 <- get--                  pushTo frames $ Frame-                    { _frameState = vm1._state { _stack = xs }-                    , _frameContext = newContext-                    }--                  let clearInitCode = \case-                        (InitCode _ _) -> InitCode mempty mempty-                        a -> a--                  zoom state $ do-                    assign gas (num xGas)-                    assign pc 0-                    assign code (clearInitCode target._contractcode)-                    assign codeContract xTo'-                    assign stack mempty-                    assign memory mempty-                    assign memorySize 0-                    assign returndata mempty-                    assign calldata (copySlice (Lit xInOffset) (Lit 0) (Lit xInSize) vm0._state._memory mempty)--                  continue xTo'---- -- * Contract creation---- EIP 684-collision :: Maybe Contract -> Bool-collision c' = case c' of-  Just c -> c._nonce /= 0 || case c._contractcode of-    RuntimeCode (ConcreteRuntimeCode "") -> False-    RuntimeCode (SymbolicRuntimeCode b) -> not $ null b-    _ -> True-  Nothing -> False--create :: (?op :: Word8)-  => Addr -> Contract-  -> Word64 -> W256 -> [Expr EWord] -> Addr -> Expr Buf -> EVM ()-create self this xGas' xValue xs newAddr initCode = do-  vm0 <- get-  let xGas = num xGas'-  if this._nonce == num (maxBound :: Word64)-  then do-    assign (state . stack) (Lit 0 : xs)-    assign (state . returndata) mempty-    pushTrace $ ErrorTrace NonceOverflow-    next-  else if xValue > this._balance-  then do-    assign (state . stack) (Lit 0 : xs)-    assign (state . returndata) mempty-    pushTrace $ ErrorTrace $ BalanceTooLow xValue this._balance-    next-  else if length vm0._frames >= 1024-  then do-    assign (state . stack) (Lit 0 : xs)-    assign (state . returndata) mempty-    pushTrace $ ErrorTrace CallDepthLimitReached-    next-  else if collision $ Map.lookup newAddr vm0._env._contracts-  then burn xGas $ do-    assign (state . stack) (Lit 0 : xs)-    assign (state . returndata) mempty-    modifying (env . contracts . ix self . nonce) succ-    next-  else burn xGas $ do-    touchAccount self-    touchAccount newAddr-    let-    -- unfortunately we have to apply some (pretty hacky)-    -- heuristics here to parse the unstructured buffer read-    -- from memory into a code and data section-    -- TODO: comment explaining whats going on here-    let contract' = do-          prefixLen <- Expr.concPrefix initCode-          prefix <- Expr.toList $ Expr.take (num prefixLen) initCode-          let sym = Expr.drop (num prefixLen) initCode-          conc <- mapM unlitByte prefix-          pure $ InitCode (BS.pack $ V.toList conc) sym-    case contract' of-      Nothing ->-        vmError $ UnexpectedSymbolicArg vm0._state._pc "initcode must have a concrete prefix" []-      Just c -> do-        let-          newContract = initialContract c-          newContext  =-            CreationContext { creationContextAddress   = newAddr-                            , creationContextCodehash  = newContract._codehash-                            , creationContextReversion = vm0._env._contracts-                            , creationContextSubstate  = vm0._tx._substate-                            }--        zoom (env . contracts) $ do-          oldAcc <- use (at newAddr)-          let oldBal = maybe 0 (._balance) oldAcc--          assign (at newAddr) (Just (newContract & balance .~ oldBal))-          modifying (ix self . nonce) succ--        let resetStorage = \case-              ConcreteStore s -> ConcreteStore (Map.delete (num newAddr) s)-              AbstractStore -> AbstractStore-              EmptyStore -> EmptyStore-              SStore {} -> error "trying to reset symbolic storage with writes in create"-              GVar _  -> error "unexpected global variable"--        modifying (env . storage) resetStorage-        modifying (env . origStorage) (Map.delete (num newAddr))--        transfer self newAddr xValue--        pushTrace (FrameTrace newContext)-        next-        vm1 <- get-        pushTo frames $ Frame-          { _frameContext = newContext-          , _frameState   = vm1._state { _stack = xs }-          }--        assign state $-          blankState-            & set contract   newAddr-            & set codeContract newAddr-            & set code       c-            & set callvalue  (Lit xValue)-            & set caller     (litAddr self)-            & set gas        xGas'---- | Replace a contract's code, like when CREATE returns--- from the constructor code.-replaceCode :: Addr -> ContractCode -> EVM ()-replaceCode target newCode =-  zoom (env . contracts . at target) $-    get >>= \case-      Just now -> case now._contractcode of-        InitCode _ _ ->-          put . Just $-            (initialContract newCode)-              { _balance = now._balance-              , _nonce = now._nonce-              }-        RuntimeCode _ ->-          error ("internal error: can't replace code of deployed contract " <> show target)-      Nothing ->-        error "internal error: can't replace code of nonexistent contract"--replaceCodeOfSelf :: ContractCode -> EVM ()-replaceCodeOfSelf newCode = do-  vm <- get-  replaceCode vm._state._contract newCode--resetState :: EVM ()-resetState = do-  assign result Nothing-  assign frames []-  assign state  blankState----- * VM error implementation--vmError :: Error -> EVM ()-vmError e = finishFrame (FrameErrored e)--underrun :: EVM ()-underrun = vmError EVM.StackUnderrun---- | A stack frame can be popped in three ways.-data FrameResult-  = FrameReturned (Expr Buf) -- ^ STOP, RETURN, or no more code-  | FrameReverted (Expr Buf) -- ^ REVERT-  | FrameErrored Error -- ^ Any other error-  deriving Show---- | This function defines how to pop the current stack frame in either of--- the ways specified by 'FrameResult'.------ It also handles the case when the current stack frame is the only one;--- in this case, we set the final '_result' of the VM execution.-finishFrame :: FrameResult -> EVM ()-finishFrame how = do-  oldVm <- get--  case oldVm._frames of-    -- Is the current frame the only one?-    [] -> do-      case how of-          FrameReturned output -> assign result . Just $ VMSuccess output-          FrameReverted buffer -> assign result . Just $ VMFailure (EVM.Revert buffer)-          FrameErrored e       -> assign result . Just $ VMFailure e-      finalize--    -- Are there some remaining frames?-    nextFrame : remainingFrames -> do--      -- Insert a debug trace.-      insertTrace $-        case how of-          FrameErrored e ->-            ErrorTrace e-          FrameReverted e ->-            ErrorTrace (EVM.Revert e)-          FrameReturned output ->-            ReturnTrace output nextFrame._frameContext-      -- Pop to the previous level of the debug trace stack.-      popTrace--      -- Pop the top frame.-      assign frames remainingFrames-      -- Install the state of the frame to which we shall return.-      assign state nextFrame._frameState--      -- When entering a call, the gas allowance is counted as burned-      -- in advance; this unburns the remainder and adds it to the-      -- parent frame.-      let remainingGas = oldVm._state._gas-          reclaimRemainingGasAllowance = do-            modifying burned (subtract remainingGas)-            modifying (state . gas) (+ remainingGas)--      -- Now dispatch on whether we were creating or calling,-      -- and whether we shall return, revert, or error (six cases).-      case nextFrame._frameContext of--        -- Were we calling?-        CallContext _ _ (Lit -> outOffset) (Lit -> outSize) _ _ _ reversion substate' -> do--          -- Excerpt K.1. from the yellow paper:-          -- K.1. Deletion of an Account Despite Out-of-gas.-          -- At block 2675119, in the transaction 0xcf416c536ec1a19ed1fb89e4ec7ffb3cf73aa413b3aa9b77d60e4fd81a4296ba,-          -- an account at address 0x03 was called and an out-of-gas occurred during the call.-          -- Against the equation (197), this added 0x03 in the set of touched addresses, and this transaction turned σ[0x03] into ∅.--          -- In other words, we special case address 0x03 and keep it in the set of touched accounts during revert-          touched <- use (tx . substate . touchedAccounts)--          let-            substate'' = over touchedAccounts (maybe id cons (find (3 ==) touched)) substate'-            (contractsReversion, storageReversion) = reversion-            revertContracts = assign (env . contracts) contractsReversion-            revertStorage = assign (env . storage) storageReversion-            revertSubstate  = assign (tx . substate) substate''--          case how of-            -- Case 1: Returning from a call?-            FrameReturned output -> do-              assign (state . returndata) output-              copyCallBytesToMemory output outSize (Lit 0) outOffset-              reclaimRemainingGasAllowance-              push 1--            -- Case 2: Reverting during a call?-            FrameReverted output -> do-              revertContracts-              revertStorage-              revertSubstate-              assign (state . returndata) output-              copyCallBytesToMemory output outSize (Lit 0) outOffset-              reclaimRemainingGasAllowance-              push 0--            -- Case 3: Error during a call?-            FrameErrored _ -> do-              revertContracts-              revertStorage-              revertSubstate-              assign (state . returndata) mempty-              push 0-        -- Or were we creating?-        CreationContext _ _ reversion substate' -> do-          creator <- use (state . contract)-          let-            createe = oldVm._state._contract-            revertContracts = assign (env . contracts) reversion'-            revertSubstate  = assign (tx . substate) substate'--            -- persist the nonce through the reversion-            reversion' = (Map.adjust (over nonce (+ 1)) creator) reversion--          case how of-            -- Case 4: Returning during a creation?-            FrameReturned output -> do-              let onContractCode contractCode = do-                    replaceCode createe contractCode-                    assign (state . returndata) mempty-                    reclaimRemainingGasAllowance-                    push (num createe)-              case output of-                ConcreteBuf bs ->-                  onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)-                _ ->-                  case Expr.toList output of-                    Nothing -> vmError $-                      UnexpectedSymbolicArg-                        oldVm._state._pc-                        "runtime code cannot have an abstract length"-                        [output]-                    Just newCode -> do-                      onContractCode $ RuntimeCode (SymbolicRuntimeCode newCode)--            -- Case 5: Reverting during a creation?-            FrameReverted output -> do-              revertContracts-              revertSubstate-              assign (state . returndata) output-              reclaimRemainingGasAllowance-              push 0--            -- Case 6: Error during a creation?-            FrameErrored _ -> do-              revertContracts-              revertSubstate-              assign (state . returndata) mempty-              push 0----- * Memory helpers--accessUnboundedMemoryRange-  :: Word64-  -> Word64-  -> EVM ()-  -> EVM ()-accessUnboundedMemoryRange _ 0 continue = continue-accessUnboundedMemoryRange f l continue = do-  m0 <- num <$> use (state . memorySize)-  fees <- gets (._block._schedule)-  do-    let m1 = 32 * ceilDiv (max m0 (f + l)) 32-    burn (memoryCost fees m1 - memoryCost fees m0) $ do-      assign (state . memorySize) m1-      continue--accessMemoryRange-  :: W256-  -> W256-  -> EVM ()-  -> EVM ()-accessMemoryRange _ 0 continue = continue-accessMemoryRange f l continue =-  case (,) <$> toWord64 f <*> toWord64 l of-    Nothing -> vmError IllegalOverflow-    Just (f64, l64) ->-      if f64 + l64 < l64-        then vmError IllegalOverflow-        else accessUnboundedMemoryRange f64 l64 continue--accessMemoryWord-  :: W256 -> EVM () -> EVM ()-accessMemoryWord x = accessMemoryRange x 32--copyBytesToMemory-  :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM ()-copyBytesToMemory bs size xOffset yOffset =-  if size == (Lit 0) then noop-  else do-    mem <- use (state . memory)-    assign (state . memory) $-      copySlice xOffset yOffset size bs mem--copyCallBytesToMemory-  :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM ()-copyCallBytesToMemory bs size xOffset yOffset =-  if size == (Lit 0) then noop-  else do-    mem <- use (state . memory)-    assign (state . memory) $-      copySlice xOffset yOffset (Expr.min size (bufLength bs)) bs mem--readMemory :: Expr EWord -> Expr EWord -> VM -> Expr Buf-readMemory offset size vm = copySlice offset (Lit 0) size vm._state._memory mempty---- * Tracing--withTraceLocation :: TraceData -> EVM Trace-withTraceLocation x = do-  vm <- get-  let this = fromJust $ currentContract vm-  pure Trace-    { _traceData = x-    , _traceContract = this-    , _traceOpIx = fromMaybe 0 $ this._opIxMap Vector.!? vm._state._pc-    }--pushTrace :: TraceData -> EVM ()-pushTrace x = do-  trace <- withTraceLocation x-  modifying traces $-    \t -> Zipper.children $ Zipper.insert (Node trace []) t--insertTrace :: TraceData -> EVM ()-insertTrace x = do-  trace <- withTraceLocation x-  modifying traces $-    \t -> Zipper.nextSpace $ Zipper.insert (Node trace []) t--popTrace :: EVM ()-popTrace =-  modifying traces $-    \t -> case Zipper.parent t of-            Nothing -> error "internal error (trace root)"-            Just t' -> Zipper.nextSpace t'--zipperRootForest :: Zipper.TreePos Zipper.Empty a -> Forest a-zipperRootForest z =-  case Zipper.parent z of-    Nothing -> Zipper.toForest z-    Just z' -> zipperRootForest (Zipper.nextSpace z')--traceForest :: VM -> Forest Trace-traceForest vm = zipperRootForest vm._traces--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"---- * Stack manipulation--push :: W256 -> EVM ()-push = pushSym . Lit--pushSym :: Expr EWord -> EVM ()-pushSym x = state . stack %= (x :)---stackOp1-  :: (?op :: Word8)-  => Word64-  -> ((Expr EWord) -> (Expr EWord))-  -> EVM ()-stackOp1 cost f =-  use (state . stack) >>= \case-    (x:xs) ->-      burn cost $ do-        next-        let !y = f x-        state . stack .= y : xs-    _ ->-      underrun--stackOp2-  :: (?op :: Word8)-  => Word64-  -> (((Expr EWord), (Expr EWord)) -> (Expr EWord))-  -> EVM ()-stackOp2 cost f =-  use (state . stack) >>= \case-    (x:y:xs) ->-      burn cost $ do-        next-        state . stack .= f (x, y) : xs-    _ ->-      underrun--stackOp3-  :: (?op :: Word8)-  => Word64-  -> (((Expr EWord), (Expr EWord), (Expr EWord)) -> (Expr EWord))-  -> EVM ()-stackOp3 cost f =-  use (state . stack) >>= \case-    (x:y:z:xs) ->-      burn cost $ do-      next-      state . stack .= f (x, y, z) : xs-    _ ->-      underrun---- * Bytecode data functions--checkJump :: Int -> [Expr EWord] -> EVM ()-checkJump x xs = do-  theCode <- use (state . code)-  self <- use (state . codeContract)-  theCodeOps <- use (env . contracts . ix self . codeOps)-  theOpIxMap <- use (env . contracts . ix self . opIxMap)-  let op = case theCode of-        InitCode ops _ -> BS.indexMaybe ops x-        RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x-        RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= unlitByte-  case op of-    Nothing -> vmError EVM.BadJumpDestination-    Just b ->-      if 0x5b == b && OpJumpdest == snd (theCodeOps RegularVector.! (theOpIxMap Vector.! num x))-         then do-           state . stack .= xs-           state . pc .= num x-         else-           vmError EVM.BadJumpDestination--opSize :: Word8 -> Int-opSize x | x >= 0x60 && x <= 0x7f = num x - 0x60 + 2-opSize _                          = 1----  i of the resulting vector contains the operation index for--- the program counter value i.  This is needed because source map--- entries are per operation, not per byte.-mkOpIxMap :: ContractCode -> Vector Int-mkOpIxMap (InitCode conc _)-  = Vector.create $ Vector.new (BS.length conc) >>= \v ->-      -- Loop over the byte string accumulating a vector-mutating action.-      -- This is somewhat obfuscated, but should be fast.-      let (_, _, _, m) = BS.foldl' (go v) (0 :: Word8, 0, 0, return ()) conc-      in m >> return v-      where-        -- concrete case-        go v (0, !i, !j, !m) x | x >= 0x60 && x <= 0x7f =-          {- Start of PUSH op. -} (x - 0x60 + 1, i + 1, j,     m >> Vector.write v i j)-        go v (1, !i, !j, !m) _ =-          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> Vector.write v i j)-        go v (0, !i, !j, !m) _ =-          {- Other op. -}         (0,            i + 1, j + 1, m >> Vector.write v i j)-        go v (n, !i, !j, !m) _ =-          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j)--mkOpIxMap (RuntimeCode (ConcreteRuntimeCode ops)) =-  mkOpIxMap (InitCode ops mempty) -- a bit hacky--mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))-  = Vector.create $ Vector.new (length ops) >>= \v ->-      let (_, _, _, m) = foldl (go v) (0, 0, 0, return ()) (stripBytecodeMetadataSym $ V.toList ops)-      in m >> return v-      where-        go v (0, !i, !j, !m) x = case unlitByte x of-          Just x' -> if x' >= 0x60 && x' <= 0x7f-            -- start of PUSH op ---                     then (x' - 0x60 + 1, i + 1, j,     m >> Vector.write v i j)-            -- other data ---                     else (0,             i + 1, j + 1, m >> Vector.write v i j)-          _ -> error $ "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 >> Vector.write v i j)-        go v (n, !i, !j, !m) _ =-          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j)---vmOp :: VM -> Maybe Op-vmOp vm =-  let i  = vm ^. state . pc-      code' = vm ^. state . code-      (op, pushdata) = case code' of-        InitCode xs' _ ->-          (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')-        RuntimeCode (ConcreteRuntimeCode xs') ->-          (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')-        RuntimeCode (SymbolicRuntimeCode xs') ->-          ( fromMaybe (error "unexpected symbolic code") . unlitByte $ xs' V.! i , V.toList $ V.drop i xs')-  in if (opslen code' < i)-     then Nothing-     else Just (readOp op pushdata)--vmOpIx :: VM -> Maybe Int-vmOpIx vm =-  do self <- currentContract vm-     self._opIxMap Vector.!? vm._state._pc--opParams :: VM -> Map String (Expr EWord)-opParams vm =-  case vmOp vm of-    Just OpCreate ->-      params $ words "value offset size"-    Just OpCall ->-      params $ words "gas to value in-offset in-size out-offset out-size"-    Just OpSstore ->-      params $ words "index value"-    Just OpCodecopy ->-      params $ words "mem-offset code-offset code-size"-    Just OpSha3 ->-      params $ words "offset size"-    Just OpCalldatacopy ->-      params $ words "to from size"-    Just OpExtcodecopy ->-      params $ words "account mem-offset code-offset code-size"-    Just OpReturn ->-      params $ words "offset size"-    Just OpJumpi ->-      params $ words "destination condition"-    _ -> mempty-  where-    params xs =-      if length (vm ^. state . stack) >= length xs-      then Map.fromList (zip xs (vm ^. state . stack))-      else mempty---- Maps operation indicies into a pair of (bytecode index, operation)-mkCodeOps :: ContractCode -> RegularVector.Vector (Int, Op)-mkCodeOps contractCode =-  let l = case contractCode of-            InitCode bytes _ ->-              LitByte <$> (BS.unpack bytes)-            RuntimeCode (ConcreteRuntimeCode ops) ->-              LitByte <$> (BS.unpack $ stripBytecodeMetadata ops)-            RuntimeCode (SymbolicRuntimeCode ops) ->-              stripBytecodeMetadataSym $ V.toList ops-  in RegularVector.fromList . toList $ go 0 l-  where-    go !i !xs =-      case uncons xs of-        Nothing ->-          mempty-        Just (x, xs') ->-          let x' = fromMaybe (error "unexpected symbolic code argument") $ unlitByte x-              j = opSize x'-          in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)---- * Gas cost calculation helpers---- Gas cost function for CALL, transliterated from the Yellow Paper.-costOfCall-  :: FeeSchedule Word64-  -> Bool -> W256 -> Word64 -> Word64 -> Addr-  -> EVM (Word64, Word64)-costOfCall (FeeSchedule {..}) recipientExists xValue availableGas xGas target = do-  acc <- accessAccountForGas target-  let call_base_gas = if acc then g_warm_storage_read else g_cold_account_access-      c_new = if not recipientExists && xValue /= 0-            then g_newaccount-            else 0-      c_xfer = if xValue /= 0  then num 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))-                  else xGas-      c_callgas = if xValue /= 0 then c_gascap + g_callstipend else c_gascap-  return (c_gascap + c_extra, c_callgas)---- Gas cost of create, including hash cost if needed-costOfCreate-  :: FeeSchedule Word64-  -> Word64 -> W256 -> (Word64, Word64)-costOfCreate (FeeSchedule {..}) availableGas hashSize =-  (createCost + initGas, initGas)-  where-    createCost = g_create + hashCost-    hashCost   = g_sha3word * ceilDiv (num hashSize) 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)-  then-    max 200 ((multiplicationComplexity * iterCount) `div` 3)-  else-    maxBound -- TODO: this is not 100% correct, return Nothing on overflow-  where (lenb, lene, lenm) = parseModexpLength input-        ez = isZero (96 + lenb) lene input-        e' = word $ LS.toStrict $-          lazySlice (96 + lenb) (min 32 lene) input-        nwords :: Word64-        nwords = ceilDiv (num $ 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)-        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"-      inputLen = case input of-                   ConcreteBuf bs -> fromIntegral $ BS.length bs-                   AbstractBuf _ -> errorDynamicSize-                   buf -> case bufLength buf of-                            Lit l -> num l -- TODO: overflow-                            _ -> errorDynamicSize-  in case precompileAddr of-    -- ECRECOVER-    0x1 -> 3000-    -- SHA2-256-    0x2 -> num $ (((inputLen + 31) `div` 32) * 12) + 60-    -- RIPEMD-160-    0x3 -> num $ (((inputLen + 31) `div` 32) * 120) + 600-    -- IDENTITY-    0x4 -> num $ (((inputLen + 31) `div` 32) * 3) + 15-    -- MODEXP-    0x5 -> case input of-             ConcreteBuf i -> concreteModexpGasFee i-             _ -> error "Unsupported symbolic modexp gas calc "-    -- ECADD-    0x6 -> g_ecadd-    -- ECMUL-    0x7 -> g_ecmul-    -- ECPAIRING-    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)---- Gas cost of memory expansion-memoryCost :: FeeSchedule Word64 -> Word64 -> Word64-memoryCost FeeSchedule{..} byteCount =-  let-    wordCount = ceilDiv byteCount 32-    linearCost = g_memory * wordCount-    quadraticCost = div (wordCount * wordCount) 512-  in-    linearCost + quadraticCost---- * Arithmetic--ceilDiv :: (Num a, Integral a) => a -> a -> a-ceilDiv m n = div (m + n - 1) n--allButOne64th :: (Num a, Integral a) => a -> a-allButOne64th n = n - div n 64--log2 :: FiniteBits b => b -> Int-log2 x = finiteBitSize x - 1 - countLeadingZeros x--hashcode :: ContractCode -> Expr EWord-hashcode (InitCode ops args) = keccak $ (ConcreteBuf ops) <> args-hashcode (RuntimeCode (ConcreteRuntimeCode ops)) = keccak (ConcreteBuf ops)-hashcode (RuntimeCode (SymbolicRuntimeCode ops)) = keccak . Expr.fromList $ ops---- | The length of the code ignoring any constructor args.--- This represents the region that can contain executable opcodes-opslen :: ContractCode -> Int-opslen (InitCode ops _) = BS.length ops-opslen (RuntimeCode (ConcreteRuntimeCode ops)) = BS.length ops-opslen (RuntimeCode (SymbolicRuntimeCode ops)) = length ops---- | The length of the code including any constructor args.--- This can return an abstract value-codelen :: ContractCode -> Expr EWord-codelen c@(InitCode {}) = bufLength $ toBuf c-codelen (RuntimeCode (ConcreteRuntimeCode ops)) = Lit . num $ BS.length ops-codelen (RuntimeCode (SymbolicRuntimeCode ops)) = Lit . num $ length ops--toBuf :: ContractCode -> Expr Buf-toBuf (InitCode ops args) = ConcreteBuf ops <> args-toBuf (RuntimeCode (ConcreteRuntimeCode ops)) = ConcreteBuf ops-toBuf (RuntimeCode (SymbolicRuntimeCode ops)) = Expr.fromList ops---codeloc :: EVM CodeLocation-codeloc = do-  vm <- get-  let self = vm._state._contract-      loc = vm._state._pc-  pure (self, loc)---- * Emacs setup---- Local Variables:--- outline-regexp: "-- \\*+\\|data \\|newtype \\|type \\| +-- op: "--- outline-heading-alist:---   (("-- *" . 1) ("data " . 2) ("newtype " . 2) ("type " . 2))--- compile-command: "make"--- End:+{-# Language UndecidableInstances #-}+{-# Language TemplateHaskell #-}+{-# Language ScopedTypeVariables #-}+{-# Language GADTs #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DuplicateRecordFields #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE TypeApplications #-}++module EVM where++import Prelude hiding (log, exponent, GT, LT)++import Optics.Core+import Optics.TH+import Optics.State+import Optics.State.Operators+import Optics.Zoom+import Optics.Operators.Unsafe++import EVM.ABI+import EVM.Concrete (createAddress, create2Address)+import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord,+  writeByte, bufLength, indexWord, litAddr, readBytes, word256At, copySlice)+import EVM.Expr qualified as Expr+import EVM.FeeSchedule (FeeSchedule (..))+import EVM.Op+import EVM.Precompiled qualified+import EVM.Solidity+import EVM.Types hiding (IllegalOverflow, Error)+import EVM.Sign qualified++import Control.Monad.State.Strict hiding (state)+import Data.Bits (FiniteBits, countLeadingZeros, finiteBitSize)+import Data.ByteArray qualified as BA+import Data.ByteString (ByteString)+import Data.ByteString qualified as BS+import Data.ByteString.Lazy (fromStrict)+import Data.ByteString.Lazy qualified as LS+import Data.ByteString.Char8 qualified as Char8+import Data.Foldable (toList)+import Data.List (find)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Maybe (fromMaybe, fromJust)+import Data.Set (Set, insert, member, fromList)+import Data.Sequence (Seq)+import Data.Sequence qualified as Seq+import Data.Text (unpack)+import Data.Text.Encoding (decodeUtf8, encodeUtf8)+import Data.Tree+import Data.Tree.Zipper qualified as Zipper+import Data.Tuple.Curry+import Data.Vector qualified as RegularVector+import Data.Vector qualified as V+import Data.Vector.Storable (Vector)+import Data.Vector.Storable qualified as Vector+import Data.Vector.Storable.Mutable qualified as Vector+import Data.Word (Word8, Word32, Word64)+import Options.Generic as Options++import Crypto.Hash (Digest, SHA256, RIPEMD160)+import Crypto.Hash qualified as Crypto+import Crypto.Number.ModArithmetic (expFast)++-- * Data types++-- | EVM failure modes+data Error+  = BalanceTooLow W256 W256+  | UnrecognizedOpcode Word8+  | SelfDestruction+  | StackUnderrun+  | BadJumpDestination+  | Revert (Expr Buf)+  | OutOfGas Word64 Word64+  | BadCheatCode FunctionSelector+  | StackLimitExceeded+  | IllegalOverflow+  | Query Query+  | Choose Choose+  | StateChangeWhileStatic+  | InvalidMemoryAccess+  | CallDepthLimitReached+  | MaxCodeSizeExceeded W256 W256+  | InvalidFormat+  | PrecompileFailure+  | forall a . UnexpectedSymbolicArg Int String [Expr a]+  | DeadPath+  | NotUnique (Expr EWord)+  | SMTTimeout+  | FFI [AbiValue]+  | ReturnDataOutOfBounds+  | NonceOverflow+deriving instance Show Error++-- | The possible result states of a VM+data VMResult+  = VMFailure Error -- ^ An operation failed+  | VMSuccess (Expr Buf) -- ^ Reached STOP, RETURN, or end-of-code++deriving instance Show VMResult++-- | The state of a stepwise EVM execution+data VM = VM+  { result         :: Maybe VMResult+  , state          :: FrameState+  , frames         :: [Frame]+  , env            :: Env+  , block          :: Block+  , tx             :: TxState+  , logs           :: [Expr Log]+  , traces         :: Zipper.TreePos Zipper.Empty Trace+  , cache          :: Cache+  , burned         :: {-# UNPACK #-} !Word64+  , iterations     :: Map CodeLocation Int+  , constraints    :: [Prop]+  , keccakEqs      :: [Prop]+  , allowFFI       :: Bool+  , overrideCaller :: Maybe Addr+  }+  deriving (Show, Generic)++data Trace = Trace+  { opIx      :: Int+  , contract  :: Contract+  , tracedata :: TraceData+  }+  deriving (Show, Generic)++data TraceData+  = EventTrace (Expr EWord) (Expr Buf) [Expr EWord]+  | FrameTrace FrameContext+  | QueryTrace Query+  | ErrorTrace Error+  | EntryTrace Text+  | ReturnTrace (Expr Buf) FrameContext+  deriving (Show, Generic)++-- | Queries halt execution until resolved through RPC calls or SMT queries+data Query where+  PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query+  PleaseFetchSlot     :: Addr -> W256 -> (W256 -> EVM ()) -> Query+  PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query+  PleaseDoFFI         :: [String] -> (ByteString -> EVM ()) -> Query++data Choose where+  PleaseChoosePath    :: Expr EWord -> (Bool -> EVM ()) -> Choose++instance Show Query where+  showsPrec _ = \case+    PleaseFetchContract addr _ ->+      (("<EVM.Query: fetch contract " ++ show addr ++ ">") ++)+    PleaseFetchSlot addr slot _ ->+      (("<EVM.Query: fetch slot "+        ++ show slot ++ " for "+        ++ show addr ++ ">") ++)+    PleaseAskSMT condition constraints _ ->+      (("<EVM.Query: ask SMT about "+        ++ show condition ++ " in context "+        ++ show constraints ++ ">") ++)+    PleaseDoFFI cmd _ ->+      (("<EVM.Query: do ffi: " ++ (show cmd)) ++)++instance Show Choose where+  showsPrec _ = \case+    PleaseChoosePath _ _ ->+      (("<EVM.Choice: waiting for user to select path (0,1)") ++)++-- | Alias for the type of e.g. @exec1@.+type EVM a = State VM a++type CodeLocation = (Addr, Int)++-- | The possible return values of a SMT query+data BranchCondition = Case Bool | Unknown | Inconsistent+  deriving Show++-- | The possible return values of a `is unique` SMT query+data IsUnique a = Unique a | Multiple | InconsistentU | TimeoutU+  deriving Show++-- | The cache is data that can be persisted for efficiency:+-- any expensive query that is constant at least within a block.+data Cache = Cache+  { fetchedContracts :: Map Addr Contract,+    fetchedStorage :: Map W256 (Map W256 W256),+    path :: Map (CodeLocation, Int) Bool+  } deriving (Show, Generic)++-- | A way to specify an initial VM state+data VMOpts = VMOpts+  { contract :: Contract+  , calldata :: (Expr Buf, [Prop])+  , initialStorage :: Expr Storage+  , value :: Expr EWord+  , priorityFee :: W256+  , address :: Addr+  , caller :: Expr EWord+  , origin :: Addr+  , gas :: Word64+  , gaslimit :: Word64+  , number :: W256+  , timestamp :: Expr EWord+  , coinbase :: Addr+  , prevRandao :: W256+  , maxCodeSize :: W256+  , blockGaslimit :: Word64+  , gasprice :: W256+  , baseFee :: W256+  , schedule :: FeeSchedule Word64+  , chainId :: W256+  , create :: Bool+  , txAccessList :: Map Addr [W256]+  , allowFFI :: Bool+  } deriving Show+++-- | An entry in the VM's "call/create stack"+data Frame = Frame+  { context :: FrameContext+  , state   :: FrameState+  }+  deriving (Show)++-- | Call/create info+data FrameContext+  = CreationContext+    { address         :: Addr+    , codehash        :: Expr EWord+    , createreversion :: Map Addr Contract+    , substate        :: SubState+    }+  | CallContext+    { target        :: Addr+    , context       :: Addr+    , offset        :: W256+    , size          :: W256+    , codehash      :: Expr EWord+    , abi           :: Maybe W256+    , calldata      :: Expr Buf+    , callreversion :: (Map Addr Contract, Expr Storage)+    , subState      :: SubState+    }+  deriving (Show, Generic)++-- | The "registers" of the VM along with memory and data stack+data FrameState = FrameState+  { contract     :: Addr+  , codeContract :: Addr+  , code         :: ContractCode+  , pc           :: {-# UNPACK #-} !Int+  , stack        :: [Expr EWord]+  , memory       :: Expr Buf+  , memorySize   :: Word64+  , calldata     :: Expr Buf+  , callvalue    :: Expr EWord+  , caller       :: Expr EWord+  , gas          :: {-# UNPACK #-} !Word64+  , returndata   :: Expr Buf+  , static       :: Bool+  }+  deriving (Show, Generic)++-- | The state that spans a whole transaction+data TxState = TxState+  { gasprice    :: W256+  , gaslimit    :: Word64+  , priorityFee :: W256+  , origin      :: Addr+  , toAddr      :: Addr+  , value       :: Expr EWord+  , substate    :: SubState+  , isCreate    :: Bool+  , txReversion :: Map Addr Contract+  }+  deriving (Show)++-- | The "accrued substate" across a transaction+data SubState = SubState+  { selfdestructs       :: [Addr]+  , touchedAccounts     :: [Addr]+  , accessedAddresses   :: Set Addr+  , accessedStorageKeys :: Set (Addr, W256)+  , refunds             :: [(Addr, Word64)]+  -- in principle we should include logs here, but do not for now+  }+  deriving (Show)++{- |+  A contract is either in creation (running its "constructor") or+  post-creation, and code in these two modes is treated differently+  by instructions like @EXTCODEHASH@, so we distinguish these two+  code types.++  The definition follows the structure of code output by solc. We need to use+  some heuristics here to deal with symbolic data regions that may be present+  in the bytecode since the fully abstract case is impractical:++  - initcode has concrete code, followed by an abstract data "section"+  - runtimecode has a fixed length, but may contain fixed size symbolic regions (due to immutable)++  hopefully we do not have to deal with dynamic immutable before we get a real data section...+-}+data ContractCode+  = InitCode ByteString (Expr Buf) -- ^ "Constructor" code, during contract creation+  | RuntimeCode RuntimeCode -- ^ "Instance" code, after contract creation+  deriving (Show, Ord)++-- | We have two variants here to optimize the fully concrete case.+-- ConcreteRuntimeCode just wraps a ByteString+-- SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).+data RuntimeCode+  = ConcreteRuntimeCode ByteString+  | SymbolicRuntimeCode (V.Vector (Expr Byte))+  deriving (Show, Eq, Ord)++-- runtime err when used for symbolic code+instance Eq ContractCode where+  InitCode a b  == InitCode c d  = a == c && b == d+  RuntimeCode x == RuntimeCode y = x == y+  _ == _ = False++-- | The state of a contract+data Contract = Contract+  { contractcode :: ContractCode+  , balance      :: W256+  , nonce        :: W256+  , codehash     :: Expr EWord+  , opIxMap      :: Vector Int+  , codeOps      :: RegularVector.Vector (Int, Op)+  , external     :: Bool+  }+  deriving (Show)++-- | Various environmental data+data Env = Env+  { contracts    :: Map Addr Contract+  , chainId      :: W256+  , storage      :: Expr Storage+  , origStorage  :: Map W256 (Map W256 W256)+  , sha3Crack    :: Map W256 ByteString+  }+  deriving (Show, Generic)+++-- | Data about the block+data Block = Block+  { coinbase    :: Addr+  , timestamp   :: Expr EWord+  , number      :: W256+  , prevRandao  :: W256+  , gaslimit    :: Word64+  , baseFee     :: W256+  , maxCodeSize :: W256+  , schedule    :: FeeSchedule Word64+  } deriving (Show, Generic)+++makeFieldLabelsNoPrefix ''VM+makeFieldLabelsNoPrefix ''FrameState+makeFieldLabelsNoPrefix ''TxState+makeFieldLabelsNoPrefix ''SubState+makeFieldLabelsNoPrefix ''Cache+makeFieldLabelsNoPrefix ''Trace+makeFieldLabelsNoPrefix ''VMOpts+makeFieldLabelsNoPrefix ''Frame+makeFieldLabelsNoPrefix ''FrameContext+makeFieldLabelsNoPrefix ''Contract+makeFieldLabelsNoPrefix ''Env+makeFieldLabelsNoPrefix ''Block++blankState :: FrameState+blankState = FrameState+  { contract     = 0+  , codeContract = 0+  , code         = RuntimeCode (ConcreteRuntimeCode "")+  , pc           = 0+  , stack        = mempty+  , memory       = mempty+  , memorySize   = 0+  , calldata     = mempty+  , callvalue    = Lit 0+  , caller       = Lit 0+  , gas          = 0+  , returndata   = mempty+  , static       = False+  }++-- | An "external" view of a contract's bytecode, appropriate for+-- e.g. @EXTCODEHASH@.+bytecode :: Getter Contract (Expr Buf)+bytecode = #contractcode % to f+  where f (InitCode _ _) = mempty+        f (RuntimeCode (ConcreteRuntimeCode bs)) = ConcreteBuf bs+        f (RuntimeCode (SymbolicRuntimeCode ops)) = Expr.fromList ops++instance Semigroup Cache where+  a <> b = Cache+    { fetchedContracts = Map.unionWith unifyCachedContract a.fetchedContracts b.fetchedContracts+    , fetchedStorage = Map.unionWith unifyCachedStorage a.fetchedStorage b.fetchedStorage+    , path = mappend a.path b.path+    }++unifyCachedStorage :: Map W256 W256 -> Map W256 W256 -> Map W256 W256+unifyCachedStorage _ _ = undefined++-- only intended for use in Cache merges, where we expect+-- everything to be Concrete+unifyCachedContract :: Contract -> Contract -> Contract+unifyCachedContract _ _ = undefined+  {-+unifyCachedContract a b = a & set storage merged+  where merged = case (view storage a, view storage b) of+                   (ConcreteStore sa, ConcreteStore sb) ->+                     ConcreteStore (mappend sa sb)+                   _ ->+                     view storage a+   -}++instance Monoid Cache where+  mempty = Cache { fetchedContracts = mempty,+                   fetchedStorage = mempty,+                   path = mempty+                 }++-- * Data accessors++currentContract :: VM -> Maybe Contract+currentContract vm =+  Map.lookup vm.state.codeContract vm.env.contracts++-- * Data constructors++makeVm :: VMOpts -> VM+makeVm o =+  let txaccessList = o.txAccessList+      txorigin = o.origin+      txtoAddr = o.address+      initialAccessedAddrs = fromList $ [txorigin, txtoAddr] ++ [1..9] ++ (Map.keys txaccessList)+      initialAccessedStorageKeys = fromList $ foldMap (uncurry (map . (,))) (Map.toList txaccessList)+      touched = if o.create then [txorigin] else [txorigin, txtoAddr]+  in+  VM+  { result = Nothing+  , frames = mempty+  , tx = TxState+    { gasprice = o.gasprice+    , gaslimit = o.gaslimit+    , priorityFee = o.priorityFee+    , origin = txorigin+    , toAddr = txtoAddr+    , value = o.value+    , substate = SubState mempty touched initialAccessedAddrs initialAccessedStorageKeys mempty+    --, _accessList = txaccessList+    , isCreate = o.create+    , txReversion = Map.fromList+      [(o.address , o.contract )]+    }+  , logs = []+  , traces = Zipper.fromForest []+  , block = Block+    { coinbase = o.coinbase+    , timestamp = o.timestamp+    , number = o.number+    , prevRandao = o.prevRandao+    , maxCodeSize = o.maxCodeSize+    , gaslimit = o.blockGaslimit+    , baseFee = o.baseFee+    , schedule = o.schedule+    }+  , state = FrameState+    { pc = 0+    , stack = mempty+    , memory = mempty+    , memorySize = 0+    , code = o.contract.contractcode+    , contract = o.address+    , codeContract = o.address+    , calldata = fst o.calldata+    , callvalue = o.value+    , caller = o.caller+    , gas = o.gas+    , returndata = mempty+    , static = False+    }+  , env = Env+    { sha3Crack = mempty+    , chainId = o.chainId+    , storage = o.initialStorage+    , origStorage = mempty+    , contracts = Map.fromList+      [(o.address, o.contract )]+    }+  , cache = Cache mempty mempty mempty+  , burned = 0+  , constraints = snd o.calldata+  , keccakEqs = mempty+  , iterations = mempty+  , allowFFI = o.allowFFI+  , overrideCaller = Nothing+  }++-- | Initialize empty contract with given code+initialContract :: ContractCode -> Contract+initialContract contractCode = Contract+  { contractcode = contractCode+  , codehash = hashcode contractCode+  , balance  = 0+  , nonce    = if creation then 1 else 0+  , opIxMap  = mkOpIxMap contractCode+  , codeOps  = mkCodeOps contractCode+  , external = False+  } where+      creation = case contractCode of+        InitCode _ _  -> True+        RuntimeCode _ -> False++-- * Opcode dispatch (exec1)++-- | Update program counter+next :: (?op :: Word8) => EVM ()+next = modifying (#state % #pc) (+ (opSize ?op))++-- | Executes the EVM one step+exec1 :: EVM ()+exec1 = do+  vm <- get++  let+    -- Convenient aliases+    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)++    fees@FeeSchedule {..} = vm.block.schedule++    doStop = finishFrame (FrameReturned mempty)++  if self > 0x0 && self <= 0x9 then do+    -- call to precompile+    let ?op = 0x00 -- dummy value+    case bufLength vm.state.calldata of+      Lit calldatasize -> do+          copyBytesToMemory vm.state.calldata (Lit calldatasize) (Lit 0) (Lit 0)+          executePrecompile self vm.state.gas 0 calldatasize 0 0 []+          vmx <- get+          case vmx.state.stack of+            x:_ -> case x of+              Lit 0 ->+                fetchAccount self $ \_ -> do+                  touchAccount self+                  vmError PrecompileFailure+              Lit _ ->+                fetchAccount self $ \_ -> do+                  touchAccount self+                  out <- use (#state % #returndata)+                  finishFrame (FrameReturned out)+              e -> vmError $+                UnexpectedSymbolicArg vmx.state.pc "precompile returned a symbolic value" [e]+            _ ->+              underrun+      e -> vmError $ UnexpectedSymbolicArg vm.state.pc "cannot call precompiles with symbolic data" [e]++  else if vm.state.pc >= opslen vm.state.code+    then doStop++    else do+      let ?op = case vm.state.code of+                  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") $+                      unlitByte $ ops V.! vm.state.pc++      case getOp(?op) of++        OpPush n' -> do+          let n = fromIntegral 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+                RuntimeCode (SymbolicRuntimeCode ops) ->+                  let bytes = V.take n $ V.drop (1 + vm.state.pc) ops+                  in readWord (Lit 0) $ Expr.fromList $ padLeft' 32 bytes+          limitStack 1 $+            burn g_verylow $ do+              next+              pushSym xs++        OpDup i ->+          case preview (ix (fromIntegral i - 1)) stk of+            Nothing -> underrun+            Just y ->+              limitStack 1 $+                burn g_verylow $ do+                  next+                  pushSym y++        OpSwap i ->+          if length stk < (fromIntegral 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)++        OpLog n ->+          notStatic $+          case stk of+            (xOffset':xSize':xs) ->+              if length xs < (fromIntegral n)+              then underrun+              else+                forceConcrete2 (xOffset', xSize') "LOG" $ \(xOffset, xSize) -> do+                    let (topics, xs') = splitAt (fromIntegral 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) $+                      accessMemoryRange xOffset xSize $ do+                        traceTopLog logs'+                        next+                        assign (#state % #stack) xs'+                        assign #logs logs'+            _ ->+              underrun++        OpStop -> doStop++        OpAdd -> stackOp2 g_verylow (uncurry Expr.add)+        OpMul -> stackOp2 g_low (uncurry Expr.mul)+        OpSub -> stackOp2 g_verylow (uncurry Expr.sub)++        OpDiv -> stackOp2 g_low (uncurry Expr.div)++        OpSdiv -> stackOp2 g_low (uncurry Expr.sdiv)++        OpMod -> stackOp2 g_low (uncurry Expr.mod)++        OpSmod -> stackOp2 g_low (uncurry Expr.smod)+        OpAddmod -> stackOp3 g_mid (uncurryN Expr.addmod)+        OpMulmod -> stackOp3 g_mid (uncurryN Expr.mulmod)++        OpLt -> stackOp2 g_verylow (uncurry Expr.lt)+        OpGt -> stackOp2 g_verylow (uncurry Expr.gt)+        OpSlt -> stackOp2 g_verylow (uncurry Expr.slt)+        OpSgt -> stackOp2 g_verylow (uncurry Expr.sgt)++        OpEq -> stackOp2 g_verylow (uncurry Expr.eq)+        OpIszero -> stackOp1 g_verylow Expr.iszero++        OpAnd -> stackOp2 g_verylow (uncurry Expr.and)+        OpOr -> stackOp2 g_verylow (uncurry Expr.or)+        OpXor -> stackOp2 g_verylow (uncurry Expr.xor)+        OpNot -> stackOp1 g_verylow Expr.not++        OpByte -> stackOp2 g_verylow (\(i, w) -> Expr.padByte $ Expr.indexWord i w)++        OpShl -> stackOp2 g_verylow (uncurry Expr.shl)+        OpShr -> stackOp2 g_verylow (uncurry Expr.shr)+        OpSar -> stackOp2 g_verylow (uncurry Expr.sar)++        -- more accurately refered to as KECCAK+        OpSha3 ->+          case stk of+            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) $+                    accessMemoryRange xOffset xSize $ do+                      (hash, invMap) <- case readMemory xOffset' xSize' vm of+                                          ConcreteBuf bs -> do+                                            let hash' = keccak' bs+                                            eqs <- use #keccakEqs+                                            assign #keccakEqs $+                                              PEq (Lit hash') (Keccak (ConcreteBuf bs)):eqs+                                            pure (Lit hash', Map.singleton hash' bs)+                                          buf -> pure (Keccak buf, mempty)+                      next+                      assign (#state % #stack) (hash : xs)+                      modifying (#env % #sha3Crack) ((<>) invMap)+            _ -> underrun++        OpAddress ->+          limitStack 1 $+            burn g_base (next >> push (num self))++        OpBalance ->+          case stk of+            x':xs -> forceConcrete x' "BALANCE" $ \x ->+              accessAndBurn (num x) $+                fetchAccount (num x) $ \c -> do+                  next+                  assign (#state % #stack) xs+                  push (num c.balance)+            [] ->+              underrun++        OpOrigin ->+          limitStack 1 . burn g_base $+            next >> push (num vm.tx.origin)++        OpCaller ->+          limitStack 1 . burn g_base $+            next >> pushSym vm.state.caller++        OpCallvalue ->+          limitStack 1 . burn g_base $+            next >> pushSym vm.state.callvalue++        OpCalldataload -> stackOp1 g_verylow $+          \ind -> Expr.readWord ind vm.state.calldata++        OpCalldatasize ->+          limitStack 1 . burn g_base $+            next >> pushSym (bufLength vm.state.calldata)++        OpCalldatacopy ->+          case stk of+            xTo':xFrom:xSize':xs ->+              forceConcrete2 (xTo', xSize') "CALLDATACOPY" $+                \(xTo, xSize) ->+                  burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $+                    accessMemoryRange xTo xSize $ do+                      next+                      assign (#state % #stack) xs+                      copyBytesToMemory vm.state.calldata xSize' xFrom xTo'+            _ -> underrun++        OpCodesize ->+          limitStack 1 . burn g_base $+            next >> pushSym (codelen vm.state.code)++        OpCodecopy ->+          case stk of+            memOffset':codeOffset:n':xs ->+              forceConcrete2 (memOffset', n') "CODECOPY" $+                \(memOffset,n) -> do+                  case toWord64 n of+                    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) $+                          accessMemoryRange memOffset n $ do+                            next+                            assign (#state % #stack) xs+                            copyBytesToMemory (toBuf vm.state.code) n' codeOffset memOffset'+                      else vmError IllegalOverflow+            _ -> underrun++        OpGasprice ->+          limitStack 1 . burn g_base $+            next >> push vm.tx.gasprice++        OpExtcodesize ->+          case stk of+            x':xs -> case x' of+              Lit x -> if x == num cheatCode+                then do+                  next+                  assign (#state % #stack) xs+                  pushSym (Lit 1)+                else+                  accessAndBurn (num x) $+                    fetchAccount (num x) $ \c -> do+                      next+                      assign (#state % #stack) xs+                      pushSym (bufLength (view bytecode c))+              _ -> do+                assign (#state % #stack) xs+                pushSym (CodeSize x')+                next+            [] ->+              underrun++        OpExtcodecopy ->+          case stk of+            extAccount':memOffset':codeOffset:codeSize':xs ->+              forceConcrete3 (extAccount', memOffset', codeSize') "EXTCODECOPY" $+                \(extAccount, memOffset, codeSize) -> do+                  acc <- accessAccountForGas (num extAccount)+                  let cost = if acc then g_warm_storage_read else g_cold_account_access+                  burn (cost + g_copy * ceilDiv (num codeSize) 32) $+                    accessMemoryRange memOffset codeSize $+                      fetchAccount (num extAccount) $ \c -> do+                        next+                        assign (#state % #stack) xs+                        copyBytesToMemory (view bytecode c) codeSize' codeOffset memOffset'+            _ -> underrun++        OpReturndatasize ->+          limitStack 1 . burn g_base $+            next >> pushSym (bufLength vm.state.returndata)++        OpReturndatacopy ->+          case stk of+            xTo':xFrom:xSize':xs -> forceConcrete2 (xTo', xSize') "RETURNDATACOPY" $+              \(xTo, xSize) ->+                burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $+                  accessMemoryRange xTo xSize $ do+                    next+                    assign (#state % #stack) xs++                    let jump True = vmError EVM.ReturnDataOutOfBounds+                        jump False = copyBytesToMemory vm.state.returndata xSize' xFrom xTo'++                    case (xFrom, bufLength vm.state.returndata) of+                      (Lit f, Lit l) ->+                        jump $ l < f + xSize || f + xSize < f+                      _ -> do+                        let oob = Expr.lt (bufLength vm.state.returndata) (Expr.add xFrom xSize')+                            overflow = Expr.lt (Expr.add xFrom xSize') (xFrom)+                        loc <- codeloc+                        branch loc (Expr.or oob overflow) jump+            _ -> underrun++        OpExtcodehash ->+          case stk of+            x':xs -> forceConcrete x' "EXTCODEHASH" $ \x ->+              accessAndBurn (num x) $ do+                next+                assign (#state % #stack) xs+                fetchAccount (num x) $ \c ->+                   if accountEmpty c+                     then push (num (0 :: Int))+                     else pushSym $ keccak (view bytecode c)+            [] ->+              underrun++        OpBlockhash -> do+          -- We adopt the fake block hash scheme of the VMTests,+          -- so that blockhash(i) is the hash of i as decimal ASCII.+          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+            i -> BlockHash i++        OpCoinbase ->+          limitStack 1 . burn g_base $+            next >> push (num vm.block.coinbase)++        OpTimestamp ->+          limitStack 1 . burn g_base $+            next >> pushSym vm.block.timestamp++        OpNumber ->+          limitStack 1 . burn g_base $+            next >> push vm.block.number++        OpPrevRandao -> do+          limitStack 1 . burn g_base $+            next >> push vm.block.prevRandao++        OpGaslimit ->+          limitStack 1 . burn g_base $+            next >> push (num vm.block.gaslimit)++        OpChainid ->+          limitStack 1 . burn g_base $+            next >> push vm.env.chainId++        OpSelfbalance ->+          limitStack 1 . burn g_low $+            next >> push this.balance++        OpBaseFee ->+          limitStack 1 . burn g_base $+            next >> push vm.block.baseFee++        OpPop ->+          case stk of+            _:xs -> burn g_base (next >> assign (#state % #stack) xs)+            _    -> underrun++        OpMload ->+          case stk of+            x':xs -> forceConcrete x' "MLOAD" $ \x ->+              burn g_verylow $+                accessMemoryWord x $ do+                  next+                  assign (#state % #stack) (readWord (Lit x) mem : xs)+            _ -> underrun++        OpMstore ->+          case stk of+            x':y:xs -> forceConcrete x' "MSTORE index" $ \x ->+              burn g_verylow $+                accessMemoryWord x $ do+                  next+                  assign (#state % #memory) (writeWord (Lit x) y mem)+                  assign (#state % #stack) xs+            _ -> underrun++        OpMstore8 ->+          case stk of+            x':y:xs -> forceConcrete x' "MSTORE8" $ \x ->+              burn g_verylow $+                accessMemoryRange x 1 $ do+                  let yByte = indexWord (Lit 31) y+                  next+                  modifying (#state % #memory) (writeByte (Lit x) yByte)+                  assign (#state % #stack) xs+            _ -> underrun++        OpSload ->+          case stk of+            x:xs -> do+              acc <- accessStorageForGas self x+              let cost = if acc then g_warm_storage_read else g_cold_sload+              burn cost $+                accessStorage self x $ \y -> do+                  next+                  assign (#state % #stack) (y:xs)+            _ -> underrun++        OpSstore ->+          notStatic $+          case stk of+            x:new:xs ->+              accessStorage self x $ \current -> do+                availableGas <- use (#state % #gas)++                if num availableGas <= g_callstipend then+                  finishFrame (FrameErrored (OutOfGas availableGas (num g_callstipend)))+                else do+                  let+                    original =+                      case readStorage (litAddr self) x (ConcreteStore vm.env.origStorage) of+                        Just (Lit v) -> v+                        _ -> 0+                    storage_cost =+                      case (maybeLitWord current, maybeLitWord new) of+                        (Just current', Just new') ->+                           if (current' == new') then g_sload+                           else if (current' == original) && (original == 0) then g_sset+                           else if (current' == original) then g_sreset+                           else g_sload++                        -- if any of the arguments are symbolic,+                        -- assume worst case scenario+                        _ -> g_sset++                  acc <- accessStorageForGas self x+                  let cold_storage_cost = if acc then 0 else g_cold_sload+                  burn (storage_cost + cold_storage_cost) $ do+                    next+                    assign (#state % #stack) xs+                    modifying (#env % #storage) (writeStorage (litAddr self) x new)++                    case (maybeLitWord current, maybeLitWord new) of+                       (Just current', Just new') ->+                          unless (current' == new') $+                            if current' == original then+                              when (original /= 0 && new' == 0) $+                                refund (g_sreset + g_access_list_storage_key)+                            else do+                              when (original /= 0) $+                                if new' == 0+                                then refund (g_sreset + g_access_list_storage_key)+                                else unRefund (g_sreset + g_access_list_storage_key)+                              when (original == new') $+                                if original == 0+                                then refund (g_sset - g_sload)+                                else refund (g_sreset - g_sload)+                       -- if any of the arguments are symbolic,+                       -- don't change the refund counter+                       _ -> noop+            _ -> underrun++        OpJump ->+          case stk of+            x:xs ->+              burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' ->+                case toInt x' of+                  Nothing -> vmError EVM.BadJumpDestination+                  Just i -> checkJump i xs+            _ -> underrun++        OpJumpi -> do+          case stk of+            (x:y:xs) -> forceConcrete x "JUMPI: symbolic jumpdest" $ \x' ->+                burn g_high $+                  let jump :: Bool -> EVM ()+                      jump False = assign (#state % #stack) xs >> next+                      jump _    = case toInt x' of+                        Nothing -> vmError EVM.BadJumpDestination+                        Just i -> checkJump i xs+                  in case maybeLitWord y of+                    Just y' -> jump (0 /= y')+                    -- if the jump condition is symbolic, we explore both sides+                    Nothing -> do+                      loc <- codeloc+                      branch loc y jump+            _ -> underrun++        OpPc ->+          limitStack 1 . burn g_base $+            next >> push (num vm.state.pc)++        OpMsize ->+          limitStack 1 . burn g_base $+            next >> push (num vm.state.memorySize)++        OpGas ->+          limitStack 1 . burn g_base $+            next >> push (num (vm.state.gas - g_base))++        OpJumpdest -> burn g_jumpdest next++        OpExp ->+          -- NOTE: this can be done symbolically using unrolling like this:+          --       https://hackage.haskell.org/package/sbv-9.0/docs/src/Data.SBV.Core.Model.html#.%5E+          --       However, it requires symbolic gas, since the gas depends on the exponent+          case stk of+            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)+              in burn cost $ do+                next+                (#state % #stack) .= Expr.exp base exponent' : xs+            _ -> underrun++        OpSignextend -> stackOp2 g_low (uncurry Expr.sex)++        OpCreate ->+          notStatic $+          case stk of+            xValue':xOffset':xSize':xs -> forceConcrete3 (xValue', xOffset', xSize') "CREATE" $+              \(xValue, xOffset, xSize) -> do+                accessMemoryRange xOffset xSize $ do+                  availableGas <- use (#state % #gas)+                  let+                    newAddr = createAddress self this.nonce+                    (cost, gas') = costOfCreate fees availableGas 0+                  _ <- accessAccountForGas newAddr+                  burn (cost - gas') $ do+                    -- unfortunately we have to apply some (pretty hacky)+                    -- heuristics here to parse the unstructured buffer read+                    -- from memory into a code and data section+                    let initCode = readMemory xOffset' xSize' vm+                    create self this (num gas') xValue xs newAddr initCode+            _ -> underrun++        OpCall ->+          case stk of+            xGas':xTo:xValue':xInOffset':xInSize':xOutOffset':xOutSize':xs ->+              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+                    let from' = fromMaybe self vm.overrideCaller+                    zoom #state $ do+                      assign #callvalue (Lit xValue)+                      assign #caller (litAddr from')+                      assign #contract callee+                    assign #overrideCaller Nothing+                    transfer from' callee xValue+                    touchAccount self+                    touchAccount callee+            _ ->+              underrun++        OpCallcode ->+          case stk of+            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+                  zoom #state $ do+                    assign #callvalue (Lit xValue)+                    assign #caller $ litAddr $ fromMaybe self vm.overrideCaller+                  assign #overrideCaller Nothing+                  touchAccount self+            _ ->+              underrun++        OpReturn ->+          case stk of+            xOffset':xSize':_ -> forceConcrete2 (xOffset', xSize') "RETURN" $ \(xOffset, xSize) ->+              accessMemoryRange xOffset xSize $ do+                let+                  output = readMemory xOffset' xSize' vm+                  codesize = fromMaybe (error "RETURN: cannot return dynamically sized abstract data")+                               . unlit . bufLength $ output+                  maxsize = vm.block.maxCodeSize+                  creation = case vm.frames of+                    [] -> vm.tx.isCreate+                    frame:_ -> case frame.context of+                       CreationContext {} -> True+                       CallContext {} -> False+                if creation+                then+                  if codesize > maxsize+                  then+                    finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))+                  else do+                    let frameReturned = burn (g_codedeposit * num codesize) $+                                          finishFrame (FrameReturned output)+                        frameErrored = finishFrame $ FrameErrored InvalidFormat+                    case readByte (Lit 0) output of+                      LitByte 0xef -> frameErrored+                      LitByte _ -> frameReturned+                      y -> do+                        loc <- codeloc+                        branch loc (Expr.eqByte y (LitByte 0xef)) $ \case+                          True -> frameErrored+                          False -> frameReturned+                else+                   finishFrame (FrameReturned output)+            _ -> underrun++        OpDelegatecall ->+          case stk of+            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+                  touchAccount self+            _ -> underrun++        OpCreate2 -> notStatic $+          case stk of+            xValue':xOffset':xSize':xSalt':xs ->+              forceConcrete4 (xValue', xOffset', xSize', xSalt') "CREATE2" $+              \(xValue, xOffset, xSize, xSalt) ->+                accessMemoryRange xOffset xSize $ do+                  availableGas <- use (#state % #gas)++                  forceConcreteBuf (readMemory xOffset' xSize' vm) "CREATE2" $+                    \initCode -> do+                      let+                        newAddr  = create2Address self xSalt initCode+                        (cost, gas') = costOfCreate fees availableGas xSize+                      _ <- accessAccountForGas newAddr+                      burn (cost - gas') $ create self this gas' xValue xs newAddr (ConcreteBuf initCode)+            _ -> underrun++        OpStaticcall ->+          case stk of+            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+                  zoom #state $ do+                    assign #callvalue (Lit 0)+                    assign #caller $ litAddr $ fromMaybe self (vm.overrideCaller)+                    assign #contract callee+                    assign #static True+                  assign #overrideCaller Nothing+                  touchAccount self+                  touchAccount callee+            _ ->+              underrun++        OpSelfdestruct ->+          notStatic $+          case stk of+            [] -> underrun+            (xTo':_) -> forceConcrete xTo' "SELFDESTRUCT" $ \(num -> xTo) -> do+              acc <- accessAccountForGas (num xTo)+              let cost = if acc then 0 else g_cold_account_access+                  funds = this.balance+                  recipientExists = accountExists xTo vm+                  c_new = if not recipientExists && funds /= 0+                          then g_selfdestruct_newaccount+                          else 0+              burn (g_selfdestruct + c_new + cost) $ do+                   selfdestruct self+                   touchAccount xTo++                   if funds /= 0+                   then fetchAccount xTo $ \_ -> do+                          #env % #contracts % ix xTo % #balance %= (+ funds)+                          assign (#env % #contracts % ix self % #balance) 0+                          doStop+                   else doStop++        OpRevert ->+          case stk of+            xOffset':xSize':_ -> forceConcrete2 (xOffset', xSize') "REVERT" $ \(xOffset, xSize) ->+              accessMemoryRange xOffset xSize $ do+                let output = readMemory xOffset' xSize' vm+                finishFrame (FrameReverted output)+            _ -> underrun++        OpUnknown xxx ->+          vmError (UnrecognizedOpcode xxx)++transfer :: Addr -> Addr -> W256 -> EVM ()+transfer xFrom xTo xValue =+  zoom (#env % #contracts) $ do+    (ix xFrom % #balance) %= (subtract xValue)+    (ix xTo % #balance) %= (+ xValue)++-- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.+callChecks+  :: (?op :: Word8)+  => Contract -> Word64 -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord]+   -- continuation with gas available for call+  -> (Word64 -> EVM ())+  -> EVM ()+callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue = do+  vm <- get+  let fees = vm.block.schedule+  accessMemoryRange xInOffset xInSize $+    accessMemoryRange xOutOffset xOutSize $ do+      availableGas <- use (#state % #gas)+      let recipientExists = accountExists xContext vm+      (cost, gas') <- costOfCall fees recipientExists xValue availableGas xGas xTo+      burn (cost - gas') $ do+        if xValue > num this.balance+        then do+          assign (#state % #stack) (Lit 0 : xs)+          assign (#state % #returndata) mempty+          pushTrace $ ErrorTrace $ BalanceTooLow xValue this.balance+          next+        else if length vm.frames >= 1024+             then do+               assign (#state % #stack) (Lit 0 : xs)+               assign (#state % #returndata) mempty+               pushTrace $ ErrorTrace CallDepthLimitReached+               next+             else continue gas'++precompiledContract+  :: (?op :: Word8)+  => Contract+  -> Word64+  -> Addr+  -> Addr+  -> W256+  -> W256 -> W256 -> W256 -> W256+  -> [Expr EWord]+  -> EVM ()+precompiledContract this xGas precompileAddr recipient xValue inOffset inSize outOffset outSize xs =+  callChecks this xGas recipient precompileAddr xValue inOffset inSize outOffset outSize xs $ \gas' ->+  do+    executePrecompile precompileAddr gas' inOffset inSize outOffset outSize xs+    self <- use (#state % #contract)+    stk <- use (#state % #stack)+    pc' <- use (#state % #pc)+    result' <- use #result+    case result' of+      Nothing -> case stk of+        x:_ -> case maybeLitWord x of+          Just 0 ->+            pure ()+          Just 1 ->+            fetchAccount recipient $ \_ -> do+              transfer self recipient xValue+              touchAccount self+              touchAccount recipient+          _ -> vmError $ UnexpectedSymbolicArg pc' "unexpected return value from precompile" [x]+        _ -> underrun+      _ -> pure ()++executePrecompile+  :: (?op :: Word8)+  => Addr+  -> Word64 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord]+  -> EVM ()+executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  = do+  vm <- get+  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"+      precompileFail = burn (gasCap - cost) $ do+                         assign (#state % #stack) (Lit 0 : xs)+                         pushTrace $ ErrorTrace PrecompileFailure+                         next+  if cost > gasCap then+    burn gasCap $ do+      assign (#state % #stack) (Lit 0 : xs)+      next+  else burn cost $+    case preCompileAddr of+      -- ECRECOVER+      0x1 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "ECRECOVER" $ \input' -> do+          case EVM.Precompiled.execute 0x1 (truncpadlit 128 input') 32 of+            Nothing -> do+              -- return no output for invalid signature+              assign (#state % #stack) (Lit 1 : xs)+              assign (#state % #returndata) mempty+              next+            Just output -> do+              assign (#state % #stack) (Lit 1 : xs)+              assign (#state % #returndata) (ConcreteBuf output)+              copyBytesToMemory (ConcreteBuf output) (Lit outSize) (Lit 0) (Lit outOffset)+              next++      -- SHA2-256+      0x2 ->+        forceConcreteBuf input "SHA2-256" $ \input' -> do+          let+            hash = sha256Buf input'+            sha256Buf x = ConcreteBuf $ BA.convert (Crypto.hash x :: Digest SHA256)+          assign (#state % #stack) (Lit 1 : xs)+          assign (#state % #returndata) hash+          copyBytesToMemory hash (Lit outSize) (Lit 0) (Lit outOffset)+          next++      -- RIPEMD-160+      0x3 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "RIPEMD160" $ \input' -> do+          let+            padding = BS.pack $ replicate 12 0+            hash' = BA.convert (Crypto.hash input' :: Digest RIPEMD160)+            hash  = ConcreteBuf $ padding <> hash'+          assign (#state % #stack) (Lit 1 : xs)+          assign (#state % #returndata) hash+          copyBytesToMemory hash (Lit outSize) (Lit 0) (Lit outOffset)+          next++      -- IDENTITY+      0x4 -> do+          assign (#state % #stack) (Lit 1 : xs)+          assign (#state % #returndata) input+          copyCallBytesToMemory input (Lit outSize) (Lit 0) (Lit outOffset)+          next++      -- MODEXP+      0x5 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "MODEXP" $ \input' -> do+          let+            (lenb, lene, lenm) = parseModexpLength input'++            output = ConcreteBuf $+              if isZero (96 + lenb + lene) lenm input'+              then truncpadlit (num 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))+          assign (#state % #stack) (Lit 1 : xs)+          assign (#state % #returndata) output+          copyBytesToMemory output (Lit outSize) (Lit 0) (Lit outOffset)+          next++      -- ECADD+      0x6 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "ECADD" $ \input' ->+          case EVM.Precompiled.execute 0x6 (truncpadlit 128 input') 64 of+            Nothing -> precompileFail+            Just output -> do+              let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output+              assign (#state % #stack) (Lit 1 : xs)+              assign (#state % #returndata) truncpaddedOutput+              copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)+              next++      -- ECMUL+      0x7 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "ECMUL" $ \input' ->+          case EVM.Precompiled.execute 0x7 (truncpadlit 96 input') 64 of+          Nothing -> precompileFail+          Just output -> do+            let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output+            assign (#state % #stack) (Lit 1 : xs)+            assign (#state % #returndata) truncpaddedOutput+            copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)+            next++      -- ECPAIRING+      0x8 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "ECPAIR" $ \input' ->+          case EVM.Precompiled.execute 0x8 input' 32 of+          Nothing -> precompileFail+          Just output -> do+            let truncpaddedOutput = ConcreteBuf $ truncpadlit 32 output+            assign (#state % #stack) (Lit 1 : xs)+            assign (#state % #returndata) truncpaddedOutput+            copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)+            next++      -- BLAKE2+      0x9 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "BLAKE2" $ \input' -> do+          case (BS.length input', 1 >= BS.last input') of+            (213, True) -> case EVM.Precompiled.execute 0x9 input' 64 of+              Just output -> do+                let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output+                assign (#state % #stack) (Lit 1 : xs)+                assign (#state % #returndata) truncpaddedOutput+                copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)+                next+              Nothing -> precompileFail+            _ -> precompileFail++      _ -> notImplemented++truncpadlit :: Int -> ByteString -> ByteString+truncpadlit n xs = if m > n then BS.take n xs+                   else BS.append xs (BS.replicate (n - m) 0)+  where m = BS.length xs++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++parseModexpLength :: ByteString -> (W256, W256, W256)+parseModexpLength input =+  let lenb = word $ LS.toStrict $ lazySlice  0 32 input+      lene = word $ LS.toStrict $ lazySlice 32 64 input+      lenm = word $ LS.toStrict $ lazySlice 64 96 input+  in (lenb, lene, lenm)++--- checks if a range of ByteString bs starting at offset and length size is all zeros.+isZero :: W256 -> W256 -> ByteString -> Bool+isZero offset size bs =+  LS.all (== 0) $+    LS.take (num size) $+      LS.drop (num offset) $+        fromStrict bs++asInteger :: LS.ByteString -> Integer+asInteger xs = if xs == mempty then 0+  else 256 * asInteger (LS.init xs)+      + num (LS.last xs)++-- * Opcode helper actions++noop :: Monad m => m ()+noop = pure ()++pushTo :: MonadState s m => Lens s s [a] [a] -> a -> m ()+pushTo f x = f %= (x :)++pushToSequence :: MonadState s m => Setter s s (Seq a) (Seq a) -> a -> m ()+pushToSequence f x = f %= (Seq.|> x)++getCodeLocation :: VM -> CodeLocation+getCodeLocation vm = (vm.state.contract, vm.state.pc)++branch :: CodeLocation -> Expr EWord -> (Bool -> EVM ()) -> EVM ()+branch loc cond continue = do+  pathconds <- use #constraints+  assign #result . Just . VMFailure . Query $ PleaseAskSMT cond pathconds choosePath+  where+    choosePath (Case v) = do+      assign #result Nothing+      pushTo #constraints $ if v then (cond ./= Lit 0) else (cond .== Lit 0)+      iteration <- use (#iterations % at loc % non 0)+      assign (#cache % #path % at (loc, iteration)) (Just v)+      assign (#iterations % at loc) (Just (iteration + 1))+      continue v+    -- Both paths are possible; we ask for more input+    choosePath Unknown =+      assign #result . Just . VMFailure . Choose . PleaseChoosePath cond $ choosePath . Case+    -- None of the paths are possible; fail this branch+    choosePath Inconsistent = vmError DeadPath+++-- | Construct RPC Query and halt execution until resolved+fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM ()+fetchAccount addr continue =+  use (#env % #contracts % at addr) >>= \case+    Just c -> continue c+    Nothing ->+      use (#cache % #fetchedContracts % at addr) >>= \case+        Just c -> do+          assign (#env % #contracts % at addr) (Just c)+          continue c+        Nothing -> do+          assign (#result) . Just . VMFailure $ Query $+            PleaseFetchContract addr+              (\c -> do assign (#cache % #fetchedContracts % at addr) (Just c)+                        assign (#env % #contracts % at addr) (Just c)+                        assign #result Nothing+                        continue c)++accessStorage+  :: Addr+  -> Expr EWord+  -> (Expr EWord -> EVM ())+  -> EVM ()+accessStorage addr slot continue = do+  store <- (.env.storage) <$> get+  use (#env % #contracts % at addr) >>= \case+    Just c ->+      case readStorage (litAddr addr) slot store of+        -- Notice that if storage is symbolic, we always continue straight away+        Just x ->+          continue x+        Nothing ->+          if c.external then+            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+                Nothing -> mkQuery litSlot+                Just val -> continue (Lit val)+          else do+            -- TODO: is this actually needed?+            modifying (#env % #storage) (writeStorage (litAddr addr) slot (Lit 0))+            continue $ Lit 0+    Nothing ->+      fetchAccount addr $ \_ ->+        accessStorage addr slot continue+  where+      mkQuery s = assign #result . Just . VMFailure . Query $+                    PleaseFetchSlot addr s+                      (\x -> do+                          modifying (#cache % #fetchedStorage % ix (num addr)) (Map.insert s x)+                          modifying (#env % #storage) (writeStorage (litAddr addr) slot (Lit x))+                          assign #result Nothing+                          continue (Lit x))++accountExists :: Addr -> VM -> Bool+accountExists addr vm =+  case Map.lookup addr vm.env.contracts of+    Just c -> not (accountEmpty c)+    Nothing -> False++-- EIP 161+accountEmpty :: Contract -> Bool+accountEmpty c =+  case c.contractcode of+    RuntimeCode (ConcreteRuntimeCode "") -> True+    RuntimeCode (SymbolicRuntimeCode b) -> null b+    _ -> False+  && c.nonce == 0+  && c.balance  == 0++-- * How to finalize a transaction+finalize :: EVM ()+finalize = do+  let+    revertContracts  = use (#tx % #txReversion) >>= assign (#env % #contracts)+    revertSubstate   = assign (#tx % #substate) (SubState mempty mempty mempty mempty mempty)++  use #result >>= \case+    Nothing ->+      error "Finalising an unfinished tx."+    Just (VMFailure (EVM.Revert _)) -> do+      revertContracts+      revertSubstate+    Just (VMFailure _) -> do+      -- burn remaining gas+      assign (#state % #gas) 0+      revertContracts+      revertSubstate+    Just (VMSuccess output) -> do+      -- deposit the code from a creation tx+      pc' <- use (#state % #pc)+      creation <- use (#tx % #isCreate)+      createe  <- use (#state % #contract)+      createeExists <- (Map.member createe) <$> use (#env % #contracts)+      let onContractCode contractCode =+            when (creation && createeExists) $ replaceCode createe contractCode+      case output of+        ConcreteBuf bs ->+          onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)+        _ ->+          case Expr.toList output of+            Nothing ->+              vmError $ UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" [output]+            Just ops ->+              onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)++  -- compute and pay the refund to the caller and the+  -- corresponding payment to the miner+  block        <- use #block+  tx           <- use #tx+  gasRemaining <- use (#state % #gas)++  let+    sumRefunds   = sum (snd <$> tx.substate.refunds)+    blockReward  = num (block.schedule.r_block)+    gasUsed      = tx.gaslimit - gasRemaining+    cappedRefund = min (quot gasUsed 5) (num sumRefunds)+    originPay    = (num $ gasRemaining + cappedRefund) * tx.gasprice+    minerPay     = tx.priorityFee * (num gasUsed)++  modifying (#env % #contracts)+     (Map.adjust (over #balance (+ originPay)) tx.origin)+  modifying (#env % #contracts)+     (Map.adjust (over #balance (+ minerPay)) block.coinbase)+  touchAccount block.coinbase++  -- pay out the block reward, recreating the miner if necessary+  preuse (#env % #contracts % ix block.coinbase) >>= \case+    Nothing -> modifying (#env % #contracts)+      (Map.insert block.coinbase (initialContract (EVM.RuntimeCode (ConcreteRuntimeCode ""))))+    Just _  -> noop+  modifying (#env % #contracts)+    (Map.adjust (over #balance (+ blockReward)) block.coinbase)++  -- perform state trie clearing (EIP 161), of selfdestructs+  -- and touched accounts. addresses are cleared if they have+  --    a) selfdestructed, or+  --    b) been touched and+  --    c) are empty.+  -- (see Yellow Paper "Accrued Substate")+  --+  -- remove any destructed addresses+  destroyedAddresses <- use (#tx % #substate % #selfdestructs)+  modifying (#env % #contracts)+    (Map.filterWithKey (\k _ -> (k `notElem` destroyedAddresses)))+  -- then, clear any remaining empty and touched addresses+  touchedAddresses <- use (#tx % #substate % #touchedAccounts)+  modifying (#env % #contracts)+    (Map.filterWithKey+      (\k a -> not ((k `elem` touchedAddresses) && accountEmpty a)))++-- | Loads the selected contract as the current contract to execute+loadContract :: Addr -> EVM ()+loadContract target =+  preuse (#env % #contracts % ix target % #contractcode) >>=+    \case+      Nothing ->+        error "Call target doesn't exist"+      Just targetCode -> do+        assign (#state % #contract) target+        assign (#state % #code)     targetCode+        assign (#state % #codeContract) target++limitStack :: Int -> EVM () -> EVM ()+limitStack n continue = do+  stk <- use (#state % #stack)+  if length stk + n > 1024+    then vmError EVM.StackLimitExceeded+    else continue++notStatic :: EVM () -> EVM ()+notStatic continue = do+  bad <- use (#state % #static)+  if bad+    then vmError StateChangeWhileStatic+    else continue++-- | Burn gas, failing if insufficient gas is available+burn :: Word64 -> EVM () -> EVM ()+burn n continue = do+  available <- use (#state % #gas)+  if n <= available+    then do+      #state % #gas %= (subtract n)+      #burned %= (+ n)+      continue+    else+      vmError (OutOfGas available n)++forceConcrete :: Expr EWord -> String -> (W256 -> EVM ()) -> EVM ()+forceConcrete n msg continue = case maybeLitWord n of+  Nothing -> do+    vm <- get+    vmError $ UnexpectedSymbolicArg vm.state.pc msg [n]+  Just c -> continue c++forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM ()) -> EVM ()+forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of+  (Just c, Just d) -> continue (c, d)+  _ -> do+    vm <- get+    vmError $ UnexpectedSymbolicArg vm.state.pc msg [n, m]++forceConcrete3 :: (Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256) -> EVM ()) -> EVM ()+forceConcrete3 (k,n,m) msg continue = case (maybeLitWord k, maybeLitWord n, maybeLitWord m) of+  (Just c, Just d, Just f) -> continue (c, d, f)+  _ -> do+    vm <- get+    vmError $ UnexpectedSymbolicArg vm.state.pc msg [k, n, m]++forceConcrete4 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256) -> EVM ()) -> EVM ()+forceConcrete4 (k,l,n,m) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord n, maybeLitWord m) of+  (Just b, Just c, Just d, Just f) -> continue (b, c, d, f)+  _ -> do+    vm <- get+    vmError $ UnexpectedSymbolicArg vm.state.pc msg [k, l, n, m]++forceConcrete5 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256) -> EVM ()) -> EVM ()+forceConcrete5 (k,l,m,n,o) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o) of+  (Just a, Just b, Just c, Just d, Just e) -> continue (a, b, c, d, e)+  _ -> do+    vm <- get+    vmError $ UnexpectedSymbolicArg vm.state.pc msg [k, l, m, n, o]++forceConcrete6 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256, W256) -> EVM ()) -> EVM ()+forceConcrete6 (k,l,m,n,o,p) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o, maybeLitWord p) of+  (Just a, Just b, Just c, Just d, Just e, Just f) -> continue (a, b, c, d, e, f)+  _ -> do+    vm <- get+    vmError $ UnexpectedSymbolicArg vm.state.pc msg [k, l, m, n, o, p]++forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM ()) -> EVM ()+forceConcreteBuf (ConcreteBuf b) _ continue = continue b+forceConcreteBuf b msg _ = do+    vm <- get+    vmError $ UnexpectedSymbolicArg vm.state.pc msg [b]++-- * Substate manipulation+refund :: Word64 -> EVM ()+refund n = do+  self <- use (#state % #contract)+  pushTo (#tx % #substate % #refunds) (self, n)++unRefund :: Word64 -> EVM ()+unRefund n = do+  self <- use (#state % #contract)+  refs <- use (#tx % #substate % #refunds)+  assign (#tx % #substate % #refunds)+    (filter (\(a,b) -> not (a == self && b == n)) refs)++touchAccount :: Addr -> EVM()+touchAccount = pushTo ((#tx % #substate) % #touchedAccounts)++selfdestruct :: Addr -> EVM()+selfdestruct = pushTo ((#tx % #substate) % #selfdestructs)++accessAndBurn :: Addr -> EVM () -> EVM ()+accessAndBurn x cont = do+  FeeSchedule {..} <- use (#block % #schedule)+  acc <- accessAccountForGas x+  let cost = if acc then g_warm_storage_read else g_cold_account_access+  burn cost cont++-- | returns a wrapped boolean- if true, this address has been touched before in the txn (warm gas cost as in EIP 2929)+-- otherwise cold+accessAccountForGas :: Addr -> EVM Bool+accessAccountForGas addr = do+  accessedAddrs <- use (#tx % #substate % #accessedAddresses)+  let accessed = member addr accessedAddrs+  assign (#tx % #substate % #accessedAddresses) (insert addr accessedAddrs)+  pure accessed++-- | returns a wrapped boolean- if true, this slot has been touched before in the txn (warm gas cost as in EIP 2929)+-- otherwise cold+accessStorageForGas :: Addr -> Expr EWord -> EVM Bool+accessStorageForGas addr key = do+  accessedStrkeys <- use (#tx % #substate % #accessedStorageKeys)+  case maybeLitWord key of+    Just litword -> do+      let accessed = member (addr, litword) accessedStrkeys+      assign (#tx % #substate % #accessedStorageKeys) (insert (addr, litword) accessedStrkeys)+      pure accessed+    _ -> return False++-- * Cheat codes++-- The cheat code is 7109709ecfa91a80626ff3989d68f67f5b1dd12d.+-- Call this address using one of the cheatActions below to do+-- special things, e.g. changing the block timestamp. Beware that+-- these are necessarily hevm specific.+cheatCode :: Addr+cheatCode = num (keccak' "hevm cheat code")++cheat+  :: (?op :: Word8)+  => (W256, W256) -> (W256, W256)+  -> EVM ()+cheat (inOffset, inSize) (outOffset, outSize) = do+  mem <- use (#state % #memory)+  vm <- get+  let+    abi = readBytes 4 (Lit inOffset) mem+    input = readMemory (Lit $ inOffset + 4) (Lit $ inSize - 4) vm+  case maybeLitWord abi of+    Nothing -> vmError $ UnexpectedSymbolicArg vm.state.pc "symbolic cheatcode selector" [abi]+    Just (fromIntegral -> abi') ->+      case Map.lookup abi' cheatActions of+        Nothing ->+          vmError (BadCheatCode abi')+        Just action -> do+            action (Lit outOffset) (Lit outSize) input+            next+            push 1++type CheatAction = Expr EWord -> Expr EWord -> Expr Buf -> EVM ()++cheatActions :: Map FunctionSelector CheatAction+cheatActions =+  Map.fromList+    [ action "ffi(string[])" $+        \sig outOffset outSize input -> do+          vm <- get+          if vm.allowFFI then+            case decodeBuf [AbiArrayDynamicType AbiStringType] input of+              CAbi valsArr -> case valsArr of+                [AbiArrayDynamic AbiStringType strsV] ->+                  let+                    cmd = fmap+                            (\case+                              (AbiString a) -> unpack $ decodeUtf8 a+                              _ -> "")+                            (V.toList strsV)+                    cont bs = do+                      let encoded = ConcreteBuf bs+                      assign (#state % #returndata) encoded+                      copyBytesToMemory encoded outSize (Lit 0) outOffset+                      assign #result Nothing+                  in assign #result (Just . VMFailure . Query $ (PleaseDoFFI cmd cont))+                _ -> vmError (BadCheatCode sig)+              _ -> vmError (BadCheatCode sig)+          else+            let msg = encodeUtf8 "ffi disabled: run again with --ffi if you want to allow tests to call external scripts"+            in vmError . EVM.Revert . ConcreteBuf $+              abiMethod "Error(string)" (AbiTuple . V.fromList $ [AbiString msg]),++      action "warp(uint256)" $+        \sig _ _ input -> case decodeStaticArgs 0 1 input of+          [x]  -> assign (#block % #timestamp) x+          _ -> vmError (BadCheatCode sig),++      action "roll(uint256)" $+        \sig _ _ input -> case decodeStaticArgs 0 1 input of+          [x] -> forceConcrete x "cannot roll to a symbolic block number" (assign (#block % #number))+          _ -> vmError (BadCheatCode sig),++      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') ->+              fetchAccount a' $ \_ -> do+                modifying (#env % #storage) (writeStorage (litAddr a') slot new)+          _ -> vmError (BadCheatCode sig),++      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') ->+              accessStorage a' slot $ \res -> do+                assign (#state % #returndata % word256At (Lit 0)) res+                assign (#state % #memory % word256At outOffset) res+          _ -> vmError (BadCheatCode sig),++      action "sign(uint256,bytes32)" $+        \sig outOffset _ input -> case decodeStaticArgs 0 2 input of+          [sk, hash] ->+            forceConcrete2 (sk, hash) "cannot sign symbolic data" $ \(sk', hash') -> do+              let (v,r,s) = EVM.Sign.sign hash' (toInteger sk')+                  encoded = encodeAbiValue $+                    AbiTuple (RegularVector.fromList+                      [ AbiUInt 8 $ num 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+          _ -> 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'+            case a of+              Nothing -> vmError (BadCheatCode sig)+              Just address -> do+                let expAddr = litAddr address+                assign (#state % #returndata % word256At (Lit 0)) expAddr+                assign (#state % #memory % word256At outOffset) expAddr+          _ -> vmError (BadCheatCode sig),++      action "prank(address)" $+        \sig _ _ input -> case decodeStaticArgs 0 1 input of+          [addr]  -> assign #overrideCaller (Expr.exprToAddr addr)+          _ -> vmError (BadCheatCode sig)++    ]+  where+    action s f = (abiKeccak s, f (abiKeccak s))++-- * General call implementation ("delegateCall")+-- note that the continuation is ignored in the precompile case+delegateCall+  :: (?op :: Word8)+  => Contract -> Word64 -> Expr EWord -> Expr EWord -> W256 -> W256 -> W256 -> W256 -> W256+  -> [Expr EWord]+  -> (Addr -> EVM ())+  -> 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')) ->+      if xTo' > 0 && xTo' <= 9+      then precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs+      else if xTo' == cheatCode then+        do+          assign (#state % #stack) xs+          cheat (xInOffset, xInSize) (xOutOffset, xOutSize)+      else+        callChecks this gasGiven xContext' xTo' xValue xInOffset xInSize xOutOffset xOutSize xs $+        \xGas -> do+          vm0 <- get+          fetchAccount xTo' $ \target ->+                burn xGas $ do+                  let newContext = CallContext+                                    { target    = xTo'+                                    , context   = xContext'+                                    , offset    = xOutOffset+                                    , size      = xOutSize+                                    , codehash  = target.codehash+                                    , callreversion = (vm0.env.contracts, vm0.env.storage)+                                    , subState  = vm0.tx.substate+                                    , abi =+                                        if xInSize >= 4+                                        then case unlit $ readBytes 4 (Lit xInOffset) vm0.state.memory+                                             of Nothing -> Nothing+                                                Just abi -> Just $ num abi+                                        else Nothing+                                    , calldata = (readMemory (Lit xInOffset) (Lit xInSize) vm0)+                                    }++                  pushTrace (FrameTrace newContext)+                  next+                  vm1 <- get++                  pushTo #frames $ Frame+                    { state = vm1.state { stack = xs }+                    , context = newContext+                    }++                  let clearInitCode = \case+                        (InitCode _ _) -> InitCode mempty mempty+                        a -> a++                  zoom #state $ do+                    assign #gas (num xGas)+                    assign #pc 0+                    assign #code (clearInitCode target.contractcode)+                    assign #codeContract xTo'+                    assign #stack mempty+                    assign #memory mempty+                    assign #memorySize 0+                    assign #returndata mempty+                    assign #calldata (copySlice (Lit xInOffset) (Lit 0) (Lit xInSize) vm0.state.memory mempty)++                  continue xTo'++-- -- * Contract creation++-- EIP 684+collision :: Maybe Contract -> Bool+collision c' = case c' of+  Just c -> c.nonce /= 0 || case c.contractcode of+    RuntimeCode (ConcreteRuntimeCode "") -> False+    RuntimeCode (SymbolicRuntimeCode b) -> not $ null b+    _ -> True+  Nothing -> False++create :: (?op :: Word8)+  => Addr -> Contract+  -> Word64 -> W256 -> [Expr EWord] -> Addr -> Expr Buf -> EVM ()+create self this xGas' xValue xs newAddr initCode = do+  vm0 <- get+  let xGas = num xGas'+  if this.nonce == num (maxBound :: Word64)+  then do+    assign (#state % #stack) (Lit 0 : xs)+    assign (#state % #returndata) mempty+    pushTrace $ ErrorTrace NonceOverflow+    next+  else if xValue > this.balance+  then do+    assign (#state % #stack) (Lit 0 : xs)+    assign (#state % #returndata) mempty+    pushTrace $ ErrorTrace $ BalanceTooLow xValue this.balance+    next+  else if length vm0.frames >= 1024+  then do+    assign (#state % #stack) (Lit 0 : xs)+    assign (#state % #returndata) mempty+    pushTrace $ ErrorTrace CallDepthLimitReached+    next+  else if collision $ Map.lookup newAddr vm0.env.contracts+  then burn xGas $ do+    assign (#state % #stack) (Lit 0 : xs)+    assign (#state % #returndata) mempty+    modifying (#env % #contracts % ix self % #nonce) succ+    next+  else burn xGas $ do+    touchAccount self+    touchAccount newAddr+    let+    -- unfortunately we have to apply some (pretty hacky)+    -- heuristics here to parse the unstructured buffer read+    -- from memory into a code and data section+    -- TODO: comment explaining whats going on here+    let contract' = do+          prefixLen <- Expr.concPrefix initCode+          prefix <- Expr.toList $ Expr.take (num prefixLen) initCode+          let sym = Expr.drop (num prefixLen) initCode+          conc <- mapM unlitByte prefix+          pure $ InitCode (BS.pack $ V.toList conc) sym+    case contract' of+      Nothing ->+        vmError $ UnexpectedSymbolicArg vm0.state.pc "initcode must have a concrete prefix" []+      Just c -> do+        let+          newContract = initialContract c+          newContext  =+            CreationContext { address   = newAddr+                            , codehash  = newContract.codehash+                            , createreversion = vm0.env.contracts+                            , substate  = vm0.tx.substate+                            }++        zoom (#env % #contracts) $ do+          oldAcc <- use (at newAddr)+          let oldBal = maybe 0 (.balance) oldAcc++          assign (at newAddr) (Just (newContract & #balance .~ oldBal))+          modifying (ix self % #nonce) succ++        let resetStorage = \case+              ConcreteStore s -> ConcreteStore (Map.delete (num newAddr) s)+              AbstractStore -> AbstractStore+              EmptyStore -> EmptyStore+              SStore {} -> error "trying to reset symbolic storage with writes in create"+              GVar _  -> error "unexpected global variable"++        modifying (#env % #storage) resetStorage+        modifying (#env % #origStorage) (Map.delete (num newAddr))++        transfer self newAddr xValue++        pushTrace (FrameTrace newContext)+        next+        vm1 <- get+        pushTo #frames $ Frame+          { context = newContext+          , state   = vm1.state { stack = xs }+          }++        assign #state $+          blankState+            & set #contract     newAddr+            & set #codeContract newAddr+            & set #code         c+            & set #callvalue    (Lit xValue)+            & set #caller       (litAddr self)+            & set #gas          xGas'++-- | Replace a contract's code, like when CREATE returns+-- from the constructor code.+replaceCode :: Addr -> ContractCode -> EVM ()+replaceCode target newCode =+  zoom (#env % #contracts % at target) $+    get >>= \case+      Just now -> case now.contractcode of+        InitCode _ _ ->+          put . Just $+            (initialContract newCode)+              { balance = now.balance+              , nonce = now.nonce+              }+        RuntimeCode _ ->+          error ("internal error: can't replace code of deployed contract " <> show target)+      Nothing ->+        error "internal error: can't replace code of nonexistent contract"++replaceCodeOfSelf :: ContractCode -> EVM ()+replaceCodeOfSelf newCode = do+  vm <- get+  replaceCode vm.state.contract newCode++resetState :: EVM ()+resetState =+  modify' $ \vm -> vm { result = Nothing+                      , frames = []+                      , state  = blankState }++-- * VM error implementation++vmError :: Error -> EVM ()+vmError e = finishFrame (FrameErrored e)++underrun :: EVM ()+underrun = vmError EVM.StackUnderrun++-- | A stack frame can be popped in three ways.+data FrameResult+  = FrameReturned (Expr Buf) -- ^ STOP, RETURN, or no more code+  | FrameReverted (Expr Buf) -- ^ REVERT+  | FrameErrored Error -- ^ Any other error+  deriving Show++-- | This function defines how to pop the current stack frame in either of+-- the ways specified by 'FrameResult'.+--+-- It also handles the case when the current stack frame is the only one;+-- in this case, we set the final '_result' of the VM execution.+finishFrame :: FrameResult -> EVM ()+finishFrame how = do+  oldVm <- get++  case oldVm.frames of+    -- Is the current frame the only one?+    [] -> do+      case how of+          FrameReturned output -> assign #result . Just $ VMSuccess output+          FrameReverted buffer -> assign #result . Just $ VMFailure (EVM.Revert buffer)+          FrameErrored e       -> assign #result . Just $ VMFailure e+      finalize++    -- Are there some remaining frames?+    nextFrame : remainingFrames -> do++      -- Insert a debug trace.+      insertTrace $+        case how of+          FrameErrored e ->+            ErrorTrace e+          FrameReverted e ->+            ErrorTrace (EVM.Revert e)+          FrameReturned output ->+            ReturnTrace output nextFrame.context+      -- Pop to the previous level of the debug trace stack.+      popTrace++      -- Pop the top frame.+      assign #frames remainingFrames+      -- Install the state of the frame to which we shall return.+      assign #state nextFrame.state++      -- When entering a call, the gas allowance is counted as burned+      -- in advance; this unburns the remainder and adds it to the+      -- parent frame.+      let remainingGas = oldVm.state.gas+          reclaimRemainingGasAllowance = do+            modifying #burned (subtract remainingGas)+            modifying (#state % #gas) (+ remainingGas)++      -- Now dispatch on whether we were creating or calling,+      -- and whether we shall return, revert, or error (six cases).+      case nextFrame.context of++        -- Were we calling?+        CallContext _ _ (Lit -> outOffset) (Lit -> outSize) _ _ _ reversion substate' -> do++          -- Excerpt K.1. from the yellow paper:+          -- K.1. Deletion of an Account Despite Out-of-gas.+          -- At block 2675119, in the transaction 0xcf416c536ec1a19ed1fb89e4ec7ffb3cf73aa413b3aa9b77d60e4fd81a4296ba,+          -- an account at address 0x03 was called and an out-of-gas occurred during the call.+          -- Against the equation (197), this added 0x03 in the set of touched addresses, and this transaction turned σ[0x03] into ∅.++          -- In other words, we special case address 0x03 and keep it in the set of touched accounts during revert+          touched <- use (#tx % #substate % #touchedAccounts)++          let+            substate'' = over #touchedAccounts (maybe id cons (find (3 ==) touched)) substate'+            (contractsReversion, storageReversion) = reversion+            revertContracts = assign (#env % #contracts) contractsReversion+            revertStorage = assign (#env % #storage) storageReversion+            revertSubstate  = assign (#tx % #substate) substate''++          case how of+            -- Case 1: Returning from a call?+            FrameReturned output -> do+              assign (#state % #returndata) output+              copyCallBytesToMemory output outSize (Lit 0) outOffset+              reclaimRemainingGasAllowance+              push 1++            -- Case 2: Reverting during a call?+            FrameReverted output -> do+              revertContracts+              revertStorage+              revertSubstate+              assign (#state % #returndata) output+              copyCallBytesToMemory output outSize (Lit 0) outOffset+              reclaimRemainingGasAllowance+              push 0++            -- Case 3: Error during a call?+            FrameErrored _ -> do+              revertContracts+              revertStorage+              revertSubstate+              assign (#state % #returndata) mempty+              push 0+        -- Or were we creating?+        CreationContext _ _ reversion substate' -> do+          creator <- use (#state % #contract)+          let+            createe = oldVm.state.contract+            revertContracts = assign (#env % #contracts) reversion'+            revertSubstate  = assign (#tx % #substate) substate'++            -- persist the nonce through the reversion+            reversion' = (Map.adjust (over #nonce (+ 1)) creator) reversion++          case how of+            -- Case 4: Returning during a creation?+            FrameReturned output -> do+              let onContractCode contractCode = do+                    replaceCode createe contractCode+                    assign (#state % #returndata) mempty+                    reclaimRemainingGasAllowance+                    push (num createe)+              case output of+                ConcreteBuf bs ->+                  onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)+                _ ->+                  case Expr.toList output of+                    Nothing -> vmError $+                      UnexpectedSymbolicArg+                        oldVm.state.pc+                        "runtime code cannot have an abstract length"+                        [output]+                    Just newCode -> do+                      onContractCode $ RuntimeCode (SymbolicRuntimeCode newCode)++            -- Case 5: Reverting during a creation?+            FrameReverted output -> do+              revertContracts+              revertSubstate+              assign (#state % #returndata) output+              reclaimRemainingGasAllowance+              push 0++            -- Case 6: Error during a creation?+            FrameErrored _ -> do+              revertContracts+              revertSubstate+              assign (#state % #returndata) mempty+              push 0+++-- * Memory helpers++accessUnboundedMemoryRange+  :: Word64+  -> Word64+  -> EVM ()+  -> EVM ()+accessUnboundedMemoryRange _ 0 continue = continue+accessUnboundedMemoryRange f l continue = do+  m0 <- num <$> use (#state % #memorySize)+  fees <- gets (.block.schedule)+  let m1 = 32 * ceilDiv (max m0 (f + l)) 32+  burn (memoryCost fees m1 - memoryCost fees m0) $ do+    assign (#state % #memorySize) m1+    continue++accessMemoryRange+  :: W256+  -> W256+  -> EVM ()+  -> EVM ()+accessMemoryRange _ 0 continue = continue+accessMemoryRange f l continue =+  case (,) <$> toWord64 f <*> toWord64 l of+    Nothing -> vmError IllegalOverflow+    Just (f64, l64) ->+      if f64 + l64 < l64+        then vmError IllegalOverflow+        else accessUnboundedMemoryRange f64 l64 continue++accessMemoryWord+  :: W256 -> EVM () -> EVM ()+accessMemoryWord x = accessMemoryRange x 32++copyBytesToMemory+  :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM ()+copyBytesToMemory bs size xOffset yOffset =+  if size == Lit 0 then noop+  else do+    mem <- use (#state % #memory)+    assign (#state % #memory) $+      copySlice xOffset yOffset size bs mem++copyCallBytesToMemory+  :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM ()+copyCallBytesToMemory bs size xOffset yOffset =+  if size == Lit 0 then noop+  else do+    mem <- use (#state % #memory)+    assign (#state % #memory) $+      copySlice xOffset yOffset (Expr.min size (bufLength bs)) bs mem++readMemory :: Expr EWord -> Expr EWord -> VM -> Expr Buf+readMemory offset size vm = copySlice offset (Lit 0) size vm.state.memory mempty++-- * Tracing++withTraceLocation :: TraceData -> EVM Trace+withTraceLocation x = do+  vm <- get+  let this = fromJust $ currentContract vm+  pure Trace+    { tracedata = x+    , contract = this+    , opIx = fromMaybe 0 $ this.opIxMap Vector.!? vm.state.pc+    }++pushTrace :: TraceData -> EVM ()+pushTrace x = do+  trace <- withTraceLocation x+  modifying #traces $+    \t -> Zipper.children $ Zipper.insert (Node trace []) t++insertTrace :: TraceData -> EVM ()+insertTrace x = do+  trace <- withTraceLocation x+  modifying #traces $+    \t -> Zipper.nextSpace $ Zipper.insert (Node trace []) t++popTrace :: EVM ()+popTrace =+  modifying #traces $+    \t -> case Zipper.parent t of+            Nothing -> error "internal error (trace root)"+            Just t' -> Zipper.nextSpace t'++zipperRootForest :: Zipper.TreePos Zipper.Empty a -> Forest a+zipperRootForest z =+  case Zipper.parent z of+    Nothing -> Zipper.toForest z+    Just z' -> zipperRootForest (Zipper.nextSpace z')++traceForest :: VM -> Forest Trace+traceForest vm = zipperRootForest vm.traces++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"++-- * Stack manipulation++push :: W256 -> EVM ()+push = pushSym . Lit++pushSym :: Expr EWord -> EVM ()+pushSym x = #state % #stack %= (x :)++stackOp1+  :: (?op :: Word8)+  => Word64+  -> ((Expr EWord) -> (Expr EWord))+  -> EVM ()+stackOp1 cost f =+  use (#state % #stack) >>= \case+    x:xs ->+      burn cost $ do+        next+        let !y = f x+        (#state % #stack) .= y : xs+    _ ->+      underrun++stackOp2+  :: (?op :: Word8)+  => Word64+  -> (((Expr EWord), (Expr EWord)) -> (Expr EWord))+  -> EVM ()+stackOp2 cost f =+  use (#state % #stack) >>= \case+    x:y:xs ->+      burn cost $ do+        next+        (#state % #stack) .= f (x, y) : xs+    _ ->+      underrun++stackOp3+  :: (?op :: Word8)+  => Word64+  -> (((Expr EWord), (Expr EWord), (Expr EWord)) -> (Expr EWord))+  -> EVM ()+stackOp3 cost f =+  use (#state % #stack) >>= \case+    x:y:z:xs ->+      burn cost $ do+      next+      (#state % #stack) .= f (x, y, z) : xs+    _ ->+      underrun++-- * Bytecode data functions++use' :: (VM -> a) -> EVM a+use' f = do+  vm <- get+  pure (f vm)++checkJump :: Int -> [Expr EWord] -> EVM ()+checkJump x xs = do+  theCode <- use (#state % #code)+  self <- use (#state % #codeContract)+  codeOps <- preuse (#env % #contracts % ix self % #codeOps)+  opIxMap <- preuse (#env % #contracts % ix self % #opIxMap)+  case (codeOps, opIxMap) of+    (Just co, Just opMap) -> do+      let op = case theCode of+            InitCode ops _ -> BS.indexMaybe ops x+            RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x+            RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= unlitByte+      case op of+        Nothing -> vmError EVM.BadJumpDestination+        Just b ->+          if 0x5b == b && OpJumpdest == snd (co RegularVector.! (opMap Vector.! num x))+             then do+               #state % #stack .= xs+               #state % #pc .= num x+             else+               vmError EVM.BadJumpDestination+    (_, _) -> error "Internal Error: self not found in current contracts"+++opSize :: Word8 -> Int+opSize x | x >= 0x60 && x <= 0x7f = num x - 0x60 + 2+opSize _                          = 1++--  i of the resulting vector contains the operation index for+-- the program counter value i.  This is needed because source map+-- entries are per operation, not per byte.+mkOpIxMap :: ContractCode -> Vector Int+mkOpIxMap (InitCode conc _)+  = Vector.create $ Vector.new (BS.length conc) >>= \v ->+      -- Loop over the byte string accumulating a vector-mutating action.+      -- This is somewhat obfuscated, but should be fast.+      let (_, _, _, m) = BS.foldl' (go v) (0 :: Word8, 0, 0, pure ()) conc+      in m >> pure v+      where+        -- concrete case+        go v (0, !i, !j, !m) x | x >= 0x60 && x <= 0x7f =+          {- Start of PUSH op. -} (x - 0x60 + 1, i + 1, j,     m >> Vector.write v i j)+        go v (1, !i, !j, !m) _ =+          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> Vector.write v i j)+        go v (0, !i, !j, !m) _ =+          {- Other op. -}         (0,            i + 1, j + 1, m >> Vector.write v i j)+        go v (n, !i, !j, !m) _ =+          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j)++mkOpIxMap (RuntimeCode (ConcreteRuntimeCode ops)) =+  mkOpIxMap (InitCode ops mempty) -- a bit hacky++mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))+  = Vector.create $ Vector.new (length ops) >>= \v ->+      let (_, _, _, m) = foldl (go v) (0, 0, 0, pure ()) (stripBytecodeMetadataSym $ V.toList ops)+      in m >> pure v+      where+        go v (0, !i, !j, !m) x = case unlitByte x of+          Just x' -> if x' >= 0x60 && x' <= 0x7f+            -- start of PUSH op --+                     then (x' - 0x60 + 1, i + 1, j,     m >> Vector.write v i j)+            -- other data --+                     else (0,             i + 1, j + 1, m >> Vector.write v i j)+          _ -> error $ "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 >> Vector.write v i j)+        go v (n, !i, !j, !m) _ =+          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j)+++vmOp :: VM -> Maybe Op+vmOp vm =+  let i  = vm ^. #state % #pc+      code' = vm ^. #state % #code+      (op, pushdata) = case code' of+        InitCode xs' _ ->+          (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')+        RuntimeCode (ConcreteRuntimeCode xs') ->+          (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')+        RuntimeCode (SymbolicRuntimeCode xs') ->+          ( fromMaybe (error "unexpected symbolic code") . unlitByte $ xs' V.! i , V.toList $ V.drop i xs')+  in if (opslen code' < i)+     then Nothing+     else Just (readOp op pushdata)++vmOpIx :: VM -> Maybe Int+vmOpIx vm =+  do self <- currentContract vm+     self.opIxMap Vector.!? vm.state.pc++-- Maps operation indicies into a pair of (bytecode index, operation)+mkCodeOps :: ContractCode -> RegularVector.Vector (Int, Op)+mkCodeOps contractCode =+  let l = case contractCode of+            InitCode bytes _ ->+              LitByte <$> (BS.unpack bytes)+            RuntimeCode (ConcreteRuntimeCode ops) ->+              LitByte <$> (BS.unpack $ stripBytecodeMetadata ops)+            RuntimeCode (SymbolicRuntimeCode ops) ->+              stripBytecodeMetadataSym $ V.toList ops+  in RegularVector.fromList . toList $ go 0 l+  where+    go !i !xs =+      case uncons xs of+        Nothing ->+          mempty+        Just (x, xs') ->+          let x' = fromMaybe (error "unexpected symbolic code argument") $ unlitByte x+              j = opSize x'+          in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)++-- * Gas cost calculation helpers++-- Gas cost function for CALL, transliterated from the Yellow Paper.+costOfCall+  :: FeeSchedule Word64+  -> Bool -> W256 -> Word64 -> Word64 -> Addr+  -> EVM (Word64, Word64)+costOfCall (FeeSchedule {..}) recipientExists xValue availableGas xGas target = do+  acc <- accessAccountForGas target+  let call_base_gas = if acc then g_warm_storage_read else g_cold_account_access+      c_new = if not recipientExists && xValue /= 0+            then g_newaccount+            else 0+      c_xfer = if xValue /= 0  then num 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))+                  else xGas+      c_callgas = if xValue /= 0 then c_gascap + g_callstipend else c_gascap+  pure (c_gascap + c_extra, c_callgas)++-- Gas cost of create, including hash cost if needed+costOfCreate+  :: FeeSchedule Word64+  -> Word64 -> W256 -> (Word64, Word64)+costOfCreate (FeeSchedule {..}) availableGas hashSize =+  (createCost + initGas, initGas)+  where+    createCost = g_create + hashCost+    hashCost   = g_sha3word * ceilDiv (num hashSize) 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)+  then+    max 200 ((multiplicationComplexity * iterCount) `div` 3)+  else+    maxBound -- TODO: this is not 100% correct, return Nothing on overflow+  where+    (lenb, lene, lenm) = parseModexpLength input+    ez = isZero (96 + lenb) lene input+    e' = word $ LS.toStrict $+      lazySlice (96 + lenb) (min 32 lene) input+    nwords :: Word64+    nwords = ceilDiv (num $ 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)+    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"+      inputLen = case input of+                   ConcreteBuf bs -> fromIntegral $ BS.length bs+                   AbstractBuf _ -> errorDynamicSize+                   buf -> case bufLength buf of+                            Lit l -> num l -- TODO: overflow+                            _ -> errorDynamicSize+  in case precompileAddr of+    -- ECRECOVER+    0x1 -> 3000+    -- SHA2-256+    0x2 -> num $ (((inputLen + 31) `div` 32) * 12) + 60+    -- RIPEMD-160+    0x3 -> num $ (((inputLen + 31) `div` 32) * 120) + 600+    -- IDENTITY+    0x4 -> num $ (((inputLen + 31) `div` 32) * 3) + 15+    -- MODEXP+    0x5 -> case input of+             ConcreteBuf i -> concreteModexpGasFee i+             _ -> error "Unsupported symbolic modexp gas calc "+    -- ECADD+    0x6 -> g_ecadd+    -- ECMUL+    0x7 -> g_ecmul+    -- ECPAIRING+    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)++-- Gas cost of memory expansion+memoryCost :: FeeSchedule Word64 -> Word64 -> Word64+memoryCost FeeSchedule{..} byteCount =+  let+    wordCount = ceilDiv byteCount 32+    linearCost = g_memory * wordCount+    quadraticCost = div (wordCount * wordCount) 512+  in+    linearCost + quadraticCost++hashcode :: ContractCode -> Expr EWord+hashcode (InitCode ops args) = keccak $ (ConcreteBuf ops) <> args+hashcode (RuntimeCode (ConcreteRuntimeCode ops)) = keccak (ConcreteBuf ops)+hashcode (RuntimeCode (SymbolicRuntimeCode ops)) = keccak . Expr.fromList $ ops++-- | The length of the code ignoring any constructor args.+-- This represents the region that can contain executable opcodes+opslen :: ContractCode -> Int+opslen (InitCode ops _) = BS.length ops+opslen (RuntimeCode (ConcreteRuntimeCode ops)) = BS.length ops+opslen (RuntimeCode (SymbolicRuntimeCode ops)) = length ops++-- | The length of the code including any constructor args.+-- This can return an abstract value+codelen :: ContractCode -> Expr EWord+codelen c@(InitCode {}) = bufLength $ toBuf c+codelen (RuntimeCode (ConcreteRuntimeCode ops)) = Lit . num $ BS.length ops+codelen (RuntimeCode (SymbolicRuntimeCode ops)) = Lit . num $ length ops++toBuf :: ContractCode -> Expr Buf+toBuf (InitCode ops args) = ConcreteBuf ops <> args+toBuf (RuntimeCode (ConcreteRuntimeCode ops)) = ConcreteBuf ops+toBuf (RuntimeCode (SymbolicRuntimeCode ops)) = Expr.fromList ops++codeloc :: EVM CodeLocation+codeloc = do+  vm <- get+  pure (vm.state.contract, vm.state.pc)++-- * Arithmetic++ceilDiv :: (Num a, Integral a) => a -> a -> a+ceilDiv m n = div (m + n - 1) n++allButOne64th :: (Num a, Integral a) => a -> a+allButOne64th n = n - div n 64++log2 :: FiniteBits b => b -> Int+log2 x = finiteBitSize x - 1 - countLeadingZeros x

@@ -343,11 +343,12 @@ decodeAbiValue = runGet . getAbi  selector :: Text -> BS.ByteString-selector s = BSLazy.toStrict . runPut $ putWord32be (abiKeccak (encodeUtf8 s))+selector s = BSLazy.toStrict . runPut $+  putWord32be (abiKeccak (encodeUtf8 s)).unFunctionSelector  abiMethod :: Text -> AbiValue -> BS.ByteString abiMethod s args = BSLazy.toStrict . runPut $ do-  putWord32be (abiKeccak (encodeUtf8 s))+  putWord32be (abiKeccak (encodeUtf8 s)).unFunctionSelector   putAbi args  parseTypeName :: Vector AbiType -> Text -> Maybe AbiType

@@ -5,9 +5,8 @@ import EVM.RLP import EVM.Types -import Control.Lens    ((^?), ix) import Data.Bits       (Bits (..), shiftR)-import Data.ByteString (ByteString)+import Data.ByteString (ByteString, (!?)) import Data.Maybe      (fromMaybe) import Data.Word       (Word8) @@ -18,7 +17,7 @@   word (padRight 32 (BS.drop i bs))  readByteOrZero :: Int -> ByteString -> Word8-readByteOrZero i bs = fromMaybe 0 (bs ^? ix i)+readByteOrZero i bs = fromMaybe 0 (bs !? i)  byteStringSliceWithDefaultZeroes :: Int -> Int -> ByteString -> ByteString byteStringSliceWithDefaultZeroes offset size bs =

@@ -5,7 +5,7 @@ import EVM.Concrete import EVM.Debug (srcMapCodePos) import EVM.Solidity-import EVM.Types (W256, abiKeccak, keccak', Addr, regexMatches, unlit, unlitByte)+import EVM.Types (W256, abiKeccak, keccak', Addr, regexMatches, unlit, unlitByte, FunctionSelector)  import Control.Arrow ((>>>)) import Data.Aeson (Value)@@ -20,7 +20,6 @@ import Data.Text (Text, isPrefixOf, pack, unpack) import Data.Text.Encoding (encodeUtf8) import Data.Vector qualified as V-import Data.Word (Word32)  data DappInfo = DappInfo   { root       :: FilePath@@ -29,7 +28,7 @@   , solcByCode :: [(Code, SolcContract)] -- for contracts with `immutable` vars.   , sources    :: SourceCache   , unitTests  :: [(Text, [(Test, [AbiType])])]-  , abiMap     :: Map Word32 Method+  , abiMap     :: Map FunctionSelector Method   , eventMap   :: Map W256 Event   , errorMap   :: Map W256 SolError   , astIdMap   :: Map Int Value@@ -98,7 +97,7 @@ -- Tests beginning with "test" are interpreted as concrete tests, whereas -- tests beginning with "prove" are interpreted as symbolic tests. -unitTestMarkerAbi :: Word32+unitTestMarkerAbi :: FunctionSelector unitTestMarkerAbi = abiKeccak (encodeUtf8 "IS_TEST()")  findAllUnitTests :: [SolcContract] -> [(Text, [(Test, [AbiType])])]@@ -141,12 +140,12 @@ extractSig (InvariantTest sig) = sig  traceSrcMap :: DappInfo -> Trace -> Maybe SrcMap-traceSrcMap dapp trace = srcMap dapp trace._traceContract trace._traceOpIx+traceSrcMap dapp trace = srcMap dapp trace.contract trace.opIx  srcMap :: DappInfo -> Contract -> Int -> Maybe SrcMap srcMap dapp contr opIndex = do   sol <- findSrc contr dapp-  case contr._contractcode of+  case contr.contractcode of     (InitCode _ _) ->       Seq.lookup opIndex sol.creationSrcmap     (RuntimeCode _) ->@@ -154,10 +153,10 @@  findSrc :: Contract -> DappInfo -> Maybe SolcContract findSrc c dapp = do-  hash <- unlit c._codehash+  hash <- unlit c.codehash   case Map.lookup hash dapp.solcByHash of     Just (_, v) -> Just v-    Nothing -> lookupCode c._contractcode dapp+    Nothing -> lookupCode c.contractcode dapp   lookupCode :: ContractCode -> DappInfo -> Maybe SolcContract

@@ -2,13 +2,13 @@  module EVM.Debug where -import EVM          (Contract, nonce, balance, bytecode, codehash)-import EVM.Solidity (SrcMap, srcMapFile, srcMapOffset, srcMapLength, SourceCache(..))+import EVM          (Contract, bytecode)+import EVM.Solidity (SrcMap(..), SourceCache(..)) import EVM.Types    (Addr) import EVM.Expr     (bufLength)  import Control.Arrow   (second)-import Control.Lens+import Optics.Core import Data.ByteString (ByteString) import Data.Map        (Map) import Data.Text       (Text)@@ -32,9 +32,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 (fromIntegral (c ^. #balance)))+    , (text "nonce", int (fromIntegral (c ^. #nonce)))     ]  prettyContracts :: Map Addr Contract -> Doc@@ -45,12 +45,12 @@  srcMapCodePos :: SourceCache -> SrcMap -> Maybe (Text, Int) srcMapCodePos cache sm =-  fmap (second f) $ cache.files ^? ix sm.srcMapFile+  fmap (second f) $ cache.files ^? ix sm.file   where-    f v = ByteString.count 0xa (ByteString.take (sm.srcMapOffset - 1) v) + 1+    f v = ByteString.count 0xa (ByteString.take sm.offset v) + 1  srcMapCode :: SourceCache -> SrcMap -> Maybe ByteString srcMapCode cache sm =-  fmap f $ cache.files ^? ix sm.srcMapFile+  fmap f $ cache.files ^? ix sm.file   where-    f (_, v) = ByteString.take (min 80 sm.srcMapLength) (ByteString.drop sm.srcMapOffset v)+    f (_, v) = ByteString.take (min 80 sm.length) (ByteString.drop sm.offset v)

@@ -1,13 +0,0 @@-module EVM.Demand (demand) where--import Control.DeepSeq (NFData, force)-import Control.Exception.Base (evaluate)-import Control.Monad.IO.Class (MonadIO, liftIO)---- | This is an easy way to force full evaluation of a value inside of--- the IO monad, being essentially just the composition of @evaluate@--- and @force@.-demand :: (MonadIO m, NFData a) => a -> m ()-demand x = do-  _ <- liftIO (evaluate (force x))-  return ()

@@ -365,44 +365,44 @@   where     contractCode = RuntimeCode (ConcreteRuntimeCode bs)     c = Contract-      { _contractcode = contractCode-      , _balance      = 0-      , _nonce        = 0-      , _codehash     = keccak (ConcreteBuf bs)-      , _opIxMap      = mkOpIxMap contractCode-      , _codeOps      = mkCodeOps contractCode-      , _external     = False+      { contractcode = contractCode+      , balance      = 0+      , nonce        = 0+      , codehash     = keccak (ConcreteBuf bs)+      , opIxMap      = mkOpIxMap contractCode+      , codeOps      = mkCodeOps contractCode+      , external     = False       }     vm = makeVm $ VMOpts-      { EVM.vmoptContract      = c-      , EVM.vmoptCalldata      = (AbstractBuf "txdata", [])-      , EVM.vmoptValue         = CallValue 0-      , EVM.vmoptAddress       = Addr 0xffffffffffffffff-      , EVM.vmoptCaller        = Lit 0-      , EVM.vmoptOrigin        = Addr 0xffffffffffffffff-      , EVM.vmoptGas           = 0xffffffffffffffff-      , EVM.vmoptGaslimit      = 0xffffffffffffffff-      , EVM.vmoptStorageBase   = Symbolic-      , EVM.vmoptBaseFee       = 0-      , EVM.vmoptPriorityFee   = 0-      , EVM.vmoptCoinbase      = 0-      , EVM.vmoptNumber        = 0-      , EVM.vmoptTimestamp     = Var "timestamp"-      , EVM.vmoptBlockGaslimit = 0-      , EVM.vmoptGasprice      = 0-      , EVM.vmoptMaxCodeSize   = 0xffffffff-      , EVM.vmoptPrevRandao    = 420-      , EVM.vmoptSchedule      = FeeSchedule.berlin-      , EVM.vmoptChainId       = 1-      , EVM.vmoptCreate        = False-      , EVM.vmoptTxAccessList  = mempty-      , EVM.vmoptAllowFFI      = False+      { contract       = c+      , calldata       = (AbstractBuf "txdata", [])+      , value          = CallValue 0+      , address        = Addr 0xffffffffffffffff+      , caller         = Lit 0+      , origin         = Addr 0xffffffffffffffff+      , gas            = 0xffffffffffffffff+      , gaslimit       = 0xffffffffffffffff+      , initialStorage = AbstractStore+      , baseFee        = 0+      , priorityFee    = 0+      , coinbase       = 0+      , number         = 0+      , timestamp      = Var "timestamp"+      , blockGaslimit  = 0+      , gasprice       = 0+      , maxCodeSize    = 0xffffffff+      , prevRandao     = 420+      , schedule       = FeeSchedule.berlin+      , chainId        = 1+      , create         = False+      , txAccessList   = mempty+      , allowFFI       = False       }   -- | Builds the Expr for the given evm bytecode object buildExpr :: SolverGroup -> ByteString -> IO (Expr End)-buildExpr solvers bs = evalStateT (interpret (Fetch.oracle solvers Nothing) Nothing Nothing runExpr) (initVm bs)+buildExpr solvers bs = interpret (Fetch.oracle solvers Nothing) Nothing Nothing (initVm bs) runExpr  dai :: IO ByteString dai = do

@@ -7,7 +7,7 @@  import qualified EVM.FeeSchedule as FeeSchedule -import Control.Lens+import Optics.Core import Control.Monad.Trans.State.Strict (get, State) import Data.ByteString (ByteString) import Data.Maybe (isNothing)@@ -19,43 +19,43 @@ vmForEthrunCreation :: ByteString -> VM vmForEthrunCreation creationCode =   (makeVm $ VMOpts-    { vmoptContract = initialContract (InitCode creationCode mempty)-    , vmoptCalldata = mempty-    , vmoptValue = (Lit 0)-    , vmoptStorageBase = Concrete-    , vmoptAddress = createAddress ethrunAddress 1-    , vmoptCaller = litAddr ethrunAddress-    , vmoptOrigin = ethrunAddress-    , vmoptCoinbase = 0-    , vmoptNumber = 0-    , vmoptTimestamp = (Lit 0)-    , vmoptBlockGaslimit = 0-    , vmoptGasprice = 0-    , vmoptPrevRandao = 42069-    , vmoptGas = 0xffffffffffffffff-    , vmoptGaslimit = 0xffffffffffffffff-    , vmoptBaseFee = 0-    , vmoptPriorityFee = 0-    , vmoptMaxCodeSize = 0xffffffff-    , vmoptSchedule = FeeSchedule.berlin-    , vmoptChainId = 1-    , vmoptCreate = False-    , vmoptTxAccessList = mempty-    , vmoptAllowFFI = False-    }) & set (env . contracts . at ethrunAddress)+    { contract = initialContract (InitCode creationCode mempty)+    , calldata = mempty+    , value = (Lit 0)+    , initialStorage = EmptyStore+    , address = createAddress ethrunAddress 1+    , caller = litAddr ethrunAddress+    , origin = ethrunAddress+    , coinbase = 0+    , number = 0+    , timestamp = (Lit 0)+    , blockGaslimit = 0+    , gasprice = 0+    , prevRandao = 42069+    , gas = 0xffffffffffffffff+    , gaslimit = 0xffffffffffffffff+    , baseFee = 0+    , priorityFee = 0+    , maxCodeSize = 0xffffffff+    , schedule = FeeSchedule.berlin+    , chainId = 1+    , create = False+    , txAccessList = mempty+    , allowFFI = False+    }) & set (#env % #contracts % at ethrunAddress)              (Just (initialContract (RuntimeCode (ConcreteRuntimeCode ""))))  exec :: State VM VMResult exec = do   vm <- get-  case vm._result of+  case vm.result of     Nothing -> exec1 >> exec     Just r -> pure r  run :: State VM VM run = do   vm <- get-  case vm._result of+  case vm.result of     Nothing -> exec1 >> run     Just _ -> pure vm @@ -64,7 +64,7 @@   where     go i = do       vm <- get-      if p vm && isNothing vm._result+      if p vm && isNothing vm.result         then do           go $! (i + 1)       else

@@ -15,7 +15,7 @@ import Data.Maybe import Data.List -import Control.Lens (lens)+import Optics.Core  import EVM.Types import EVM.Traversals@@ -215,19 +215,18 @@     then val     else readByte i src readByte i@(Lit x) (WriteWord (Lit idx) val src)-  = if idx <= x && x <= idx + 31+  = if x - idx < 32     then case val of            (Lit _) -> indexWord (Lit $ x - idx) val            _ -> IndexWord (Lit $ x - idx) val     else readByte i src readByte i@(Lit x) (CopySlice (Lit srcOffset) (Lit dstOffset) (Lit size) src dst)-  = if dstOffset <= x && x < (dstOffset + size)+  = if x - dstOffset < size     then readByte (Lit $ x - (dstOffset - srcOffset)) src     else readByte i dst readByte i@(Lit x) buf@(CopySlice _ (Lit dstOffset) (Lit size) _ dst)-  -- the byte we are trying to read is compeletely outside of the sliced reegion-  -- we check that there is no overflow and that addresses do not wrap around-  = if (x < dstOffset || x >= dstOffset + size) && (dstOffset <= dstOffset + size)+  -- the byte we are trying to read is compeletely outside of the sliced region+  = if x - dstOffset >= size     then readByte i dst     else ReadByte (Lit x) buf @@ -249,7 +248,7 @@   | idx == idx' = val   | otherwise = case (idx, idx') of     (Lit i, Lit i') ->-      if i >= i' + 32 || i + 32 <= i'+      if i' - i >= 32 && i' - i <= (maxBound :: W256) - 31       -- the region we are trying to read is completely outside of the WriteWord       then readWord idx buf       -- the region we are trying to read partially overlaps the WriteWord@@ -259,10 +258,9 @@     _ -> readWordFromBytes idx b readWord (Lit idx) b@(CopySlice (Lit srcOff) (Lit dstOff) (Lit size) src dst)   -- the region we are trying to read is enclosed in the sliced region-  | idx >= dstOff && idx + 32 <= dstOff + size = readWord (Lit $ srcOff + (idx - dstOff)) src-  -- the region we are trying to read is compeletely outside of the sliced reegion-  -- we check that there is no overflow and that addresses do not wrap around-  | (idx >= dstOff + size || idx + 32 <= dstOff) && (dstOff<= dstOff + size) = readWord (Lit idx) dst+  | (idx - dstOff) < size && 32 <= size - (idx - dstOff) = readWord (Lit $ srcOff + (idx - dstOff)) src+  -- the region we are trying to read is compeletely outside of the sliced region+  | (idx - dstOff) >= size && (idx - dstOff) <= (maxBound :: W256) - 31 = readWord (Lit idx) dst   -- the region we are trying to read partially overlaps the sliced region   | otherwise = readWordFromBytes (Lit idx) b readWord i b = readWordFromBytes i b@@ -468,15 +466,11 @@       b <- Map.lookup a bufEnv       go l b -word256At-  :: Functor f-  => Expr EWord -> (Expr EWord -> f (Expr EWord))-  -> Expr Buf -> f (Expr Buf)+word256At :: Expr EWord -> Lens (Expr Buf) (Expr Buf) (Expr EWord) (Expr EWord) word256At i = lens getter setter where   getter = readWord i   setter m x = writeWord i x m - -- | Returns the first n bytes of buf take :: W256 -> Expr Buf -> Expr Buf take n = slice (Lit 0) (Lit n)@@ -530,34 +524,36 @@ -- | Removes any irrelevant writes when reading from a buffer simplifyReads :: Expr a -> Expr a simplifyReads = \case-  ReadWord (Lit idx) b -> readWord (Lit idx) (stripWrites idx (idx + 31) b)-  ReadByte (Lit idx) b -> readByte (Lit idx) (stripWrites idx idx b)+  ReadWord (Lit idx) b -> readWord (Lit idx) (stripWrites idx 32 b)+  ReadByte (Lit idx) b -> readByte (Lit idx) (stripWrites idx 1 b)   a -> a  -- | Strips writes from the buffer that can be statically determined to be out of range -- TODO: are the bounds here correct? I think there might be some off by one mistakes... stripWrites :: W256 -> W256 -> Expr Buf -> Expr Buf-stripWrites bottom top = \case+stripWrites off size = \case   AbstractBuf s -> AbstractBuf s-  ConcreteBuf b -> ConcreteBuf $ BS.take (num top+1) b+  ConcreteBuf b -> ConcreteBuf $ if off <= off + size+                                 then BS.take (num $ off+size) b+                                 else b   WriteByte (Lit idx) v prev-    -> if idx < bottom || idx > top-       then stripWrites bottom top prev-       else WriteByte (Lit idx) v (stripWrites bottom top prev)+    -> if idx - off >= size+       then stripWrites off size prev+       else WriteByte (Lit idx) v (stripWrites off size prev)   -- TODO: handle partial overlaps   WriteWord (Lit idx) v prev-    -> if idx + 31 < bottom || idx > top-       then stripWrites bottom top prev-       else WriteWord (Lit idx) v (stripWrites bottom top prev)-  CopySlice (Lit srcOff) (Lit dstOff) (Lit size) src dst-    -> if dstOff + size < bottom || dstOff > top-       then stripWrites bottom top dst-       else CopySlice (Lit srcOff) (Lit dstOff) (Lit size)-                      (stripWrites srcOff (srcOff + size) src)-                      (stripWrites bottom top dst)-  WriteByte i v prev -> WriteByte i v (stripWrites bottom top prev)-  WriteWord i v prev -> WriteWord i v (stripWrites bottom top prev)-  CopySlice srcOff dstOff size src dst -> CopySlice srcOff dstOff size src dst+    -> if idx - off >= size && idx - off <= (maxBound :: W256) - 31+       then stripWrites off size prev+       else WriteWord (Lit idx) v (stripWrites off size prev)+  CopySlice (Lit srcOff) (Lit dstOff) (Lit size') src dst+    -> if dstOff - off >= size && dstOff - off <= (maxBound :: W256) - size' - 1+       then stripWrites off size dst+       else CopySlice (Lit srcOff) (Lit dstOff) (Lit size')+                      (stripWrites srcOff size' src)+                      (stripWrites off size dst)+  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"  @@ -792,8 +788,14 @@     -- Double NOT is a no-op, since it's a bitwise inversion     go (EVM.Types.Not (EVM.Types.Not a)) = a +    -- Some trivial min / max eliminations     go (Max (Lit 0) a) = a     go (Min (Lit 0) _) = Lit 0++    -- If a >= b then the value of the `Max` expression can never be < b+    go o@(LT (Max (Lit a) _) (Lit b))+      | a >= b = Lit 0+      | otherwise = o      go a = a 

@@ -33,7 +33,7 @@   ) where  import EVM          (VM, Contract, Cache)-import EVM          (balance, nonce, storage, bytecode, env, contracts, cache, fetchedStorage, fetchedContracts)+import EVM          (bytecode) import EVM.Types    (Addr, W256, Expr(..), num) import EVM.Expr     (writeStorage, litAddr) @@ -41,7 +41,9 @@  import Prelude hiding (Word) -import Control.Lens    (view, set, at, ix, (&), over, assign)+import Optics.Core+import Optics.State+ import Control.Monad.State.Strict (execState, when) import Data.ByteString (ByteString) import Data.Ord        (comparing)@@ -112,15 +114,15 @@ contractFacts a x store = case view bytecode x of   ConcreteBuf b ->     storageFacts a store ++-    [ BalanceFact a x._balance-    , NonceFact   a x._nonce+    [ BalanceFact a x.balance+    , NonceFact   a x.nonce     , CodeFact    a b     ]   _ ->     -- here simply ignore storing the bytecode     storageFacts a store ++-    [ BalanceFact a x._balance-    , NonceFact   a x._nonce+    [ BalanceFact a x.balance+    , NonceFact   a x.nonce     ]  @@ -136,13 +138,13 @@  cacheFacts :: Cache -> Set Fact cacheFacts c = Set.fromList $ do-  (k, v) <- Map.toList c._fetchedContracts-  contractFacts k v c._fetchedStorage+  (k, v) <- Map.toList c.fetchedContracts+  contractFacts k v c.fetchedStorage  vmFacts :: VM -> Set Fact vmFacts vm = Set.fromList $ do-  (k, v) <- Map.toList vm._env._contracts-  case vm._env._storage of+  (k, v) <- Map.toList vm.env.contracts+  case vm.env.storage of     EmptyStore -> contractFacts k v Map.empty     ConcreteStore s -> contractFacts k v s     _ -> error "cannot serialize an abstract store"@@ -158,30 +160,30 @@ apply1 vm fact =   case fact of     CodeFact    {..} -> flip execState vm $ do-      assign (env . contracts . at addr) (Just (EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode blob))))-      when (vm._state._contract == addr) $ EVM.loadContract addr+      assign (#env % #contracts % at addr) (Just (EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode blob))))+      when (vm.state.contract == addr) $ EVM.loadContract addr     StorageFact {..} ->-      vm & over (env . storage) (writeStorage (litAddr addr) (Lit which) (Lit what))+      vm & over (#env % #storage) (writeStorage (litAddr addr) (Lit which) (Lit what))     BalanceFact {..} ->-      vm & set (env . contracts . ix addr . balance) what+      vm & set (#env % #contracts % ix addr % #balance) what     NonceFact   {..} ->-      vm & set (env . contracts . ix addr . nonce) what+      vm & set (#env % #contracts % ix addr % #nonce) what  apply2 :: VM -> Fact -> VM apply2 vm fact =   case fact of     CodeFact    {..} -> flip execState vm $ do-      assign (cache . fetchedContracts . at addr) (Just (EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode blob))))-      when (vm._state._contract == addr) $ EVM.loadContract addr+      assign (#cache % #fetchedContracts % at addr) (Just (EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode blob))))+      when (vm.state.contract == addr) $ EVM.loadContract addr     StorageFact {..} -> let-        store = vm._cache._fetchedStorage+        store = vm.cache.fetchedStorage         ctrct = Map.findWithDefault Map.empty (num addr) store       in-        vm & set (cache . fetchedStorage) (Map.insert (num addr) (Map.insert which what ctrct) store)+        vm & set (#cache % #fetchedStorage) (Map.insert (num addr) (Map.insert which what ctrct) store)     BalanceFact {..} ->-      vm & set (cache . fetchedContracts . ix addr . balance) what+      vm & set (#cache % #fetchedContracts % ix addr % #balance) what     NonceFact   {..} ->-      vm & set (cache . fetchedContracts . ix addr . nonce) what+      vm & set (#cache % #fetchedContracts % ix addr % #nonce) what  -- Sort facts in the right order for `apply1` to work. instance Ord Fact where

@@ -10,7 +10,7 @@  import EVM.Facts (Fact (..), File (..), Path (..), Data (..), fileToFact, factToFile) -import Control.Lens+import Optics.Core import Data.Set   (Set) import Data.Maybe (catMaybes) @@ -45,5 +45,5 @@ loadFacts :: RepoAt -> IO (Set Fact) loadFacts (RepoAt src) =   fmap-    (prune . Set.map (fileToFact . view (from fileRepr)))+    (prune . Set.map (fileToFact . review fileRepr))     (Git.load src)

@@ -9,15 +9,16 @@ import EVM.Types    (Addr, W256, hexText, Expr(Lit), Expr(..), Prop(..), (.&&), (./=)) import EVM.SMT import EVM.Solvers-import EVM          (EVM, Contract, Block, initialContract, nonce, balance, external)+import EVM          (EVM, Contract, Block, initialContract) import qualified EVM.FeeSchedule as FeeSchedule  import qualified EVM -import Control.Lens hiding ((.=))+import Optics.Core+ import Control.Monad.Trans.Maybe import Data.Aeson hiding (Error)-import Data.Aeson.Lens+import Data.Aeson.Optics import qualified Data.ByteString as BS import Data.Text (Text, unpack, pack) import Data.Maybe (fromMaybe)@@ -85,39 +86,49 @@   x <- case q of     QueryCode addr -> do         m <- f (rpc "eth_getCode" [toRPC addr, toRPC n])-        return $ hexText . view _String <$> m+        pure $ do+          t <- preview _String <$> m+          hexText <$> t     QueryNonce addr -> do         m <- f (rpc "eth_getTransactionCount" [toRPC addr, toRPC n])-        return $ readText . view _String <$> m+        pure $ do+          t <- preview _String <$> m+          readText <$> t     QueryBlock -> do       m <- f (rpc "eth_getBlockByNumber" [toRPC n, toRPC False])       return $ m >>= parseBlock     QueryBalance addr -> do         m <- f (rpc "eth_getBalance" [toRPC addr, toRPC n])-        return $ readText . view _String <$> m+        pure $ do+          t <- preview _String <$> m+          readText <$> t     QuerySlot addr slot -> do         m <- f (rpc "eth_getStorageAt" [toRPC addr, toRPC slot, toRPC n])-        return $ readText . view _String <$> m+        pure $ do+          t <- preview _String <$> m+          readText <$> t     QueryChainId -> do         m <- f (rpc "eth_chainId" [toRPC n])-        return $ readText . view _String <$> m+        pure $ do+          t <- preview _String <$> m+          readText <$> t   return x   parseBlock :: (AsValue s, Show s) => s -> Maybe EVM.Block parseBlock j = do-  coinbase   <- readText <$> j ^? key "miner" . _String-  timestamp  <- Lit . readText <$> j ^? key "timestamp" . _String-  number     <- readText <$> j ^? key "number" . _String-  gasLimit   <- readText <$> j ^? key "gasLimit" . _String+  coinbase   <- readText <$> j ^? key "miner" % _String+  timestamp  <- Lit . readText <$> j ^? key "timestamp" % _String+  number     <- readText <$> j ^? key "number" % _String+  gasLimit   <- readText <$> j ^? key "gasLimit" % _String   let-   baseFee = readText <$> j ^? key "baseFeePerGas" . _String+   baseFee = readText <$> j ^? key "baseFeePerGas" % _String    -- It seems unclear as to whether this field should still be called mixHash or renamed to prevRandao    -- According to https://github.com/ethereum/EIPs/blob/master/EIPS/eip-4399.md it should be renamed    -- but alchemy is still returning mixHash-   mixhash = readText <$> j ^? key "mixHash" . _String-   prevRandao = readText <$> j ^? key "prevRandao" . _String-   difficulty = readText <$> j ^? key "difficulty" . _String+   mixhash = readText <$> j ^? key "mixHash" % _String+   prevRandao = readText <$> j ^? key "prevRandao" % _String+   difficulty = readText <$> j ^? key "difficulty" % _String    prd = case (prevRandao, mixhash, difficulty) of      (Just p, _, _) -> p      (Nothing, Just mh, Just 0x0) -> mh@@ -129,7 +140,7 @@ fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value) fetchWithSession url sess x = do   r <- asValue =<< Session.post sess (unpack url) x-  return (r ^? responseBody . key "result")+  return (r ^? (lensVL responseBody) % key "result")  fetchContractWithSession   :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)@@ -144,9 +155,9 @@    return $     initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode theCode))-      & set nonce    theNonce-      & set balance  theBalance-      & set external True+      & set #nonce    theNonce+      & set #balance  theBalance+      & set #external True  fetchSlotWithSession   :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe W256)@@ -159,19 +170,24 @@   fetchQuery n (fetchWithSession url sess) QueryBlock  fetchBlockFrom :: BlockNumber -> Text -> IO (Maybe Block)-fetchBlockFrom n url =-  Session.withAPISession-    (fetchBlockWithSession n url)+fetchBlockFrom n url = do+  sess <- Session.newAPISession+  fetchBlockWithSession n url sess  fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)-fetchContractFrom n url addr =-  Session.withAPISession-    (fetchContractWithSession n url addr)+fetchContractFrom n url addr = do+  sess <- Session.newAPISession+  fetchContractWithSession n url addr sess  fetchSlotFrom :: BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256)-fetchSlotFrom n url addr slot =-  Session.withAPISession-    (\s -> fetchSlotWithSession n url s addr slot)+fetchSlotFrom n url addr slot = do+  sess <- Session.newAPISession+  fetchSlotWithSession n url sess addr slot++fetchChainIdFrom :: Text -> IO (Maybe W256)+fetchChainIdFrom url = do+  sess <- Session.newAPISession+  fetchQuery Latest (fetchWithSession url sess) QueryChainId  http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher http smtjobs smttimeout n url q =

@@ -35,10 +35,10 @@ import EVM.Hexdump (prettyHex) import EVM.Solidity (SolcContract(..), Method(..), contractName, abiMap) import EVM.Types (maybeLitWord, W256(..),num, word, Expr(..), EType(..), Addr,-  ByteStringS(..), Error(..))+  ByteStringS(..), Error(..), FunctionSelector)  import Control.Arrow ((>>>))-import Control.Lens (preview, ix, _2)+import Optics.Core import Data.Binary.Get (runGetOrFail) import Data.Bits (shiftR) import Data.ByteString (ByteString)@@ -48,7 +48,6 @@ import Data.Char qualified as Char import Data.DoubleWord (signedWord) import Data.Foldable (toList)-import Data.Functor ((<&>)) import Data.Map qualified as Map import Data.Maybe (catMaybes, fromMaybe, fromJust) import Data.Text (Text, pack, unpack, intercalate, dropEnd, splitOn)@@ -56,7 +55,6 @@ import Data.Text.Encoding (decodeUtf8, decodeUtf8') import Data.Tree.View (showTree) import Data.Vector (Vector)-import Data.Word (Word32) import Numeric (showHex)  data Signedness = Signed | Unsigned@@ -107,9 +105,9 @@       name = case Map.lookup addr contracts of         Nothing -> ""         Just contract ->-          let hash = maybeLitWord contract._codehash+          let hash = maybeLitWord contract.codehash           in case hash of-               Just h -> maybeContractName' (preview (ix h . _2) dappinfo.solcByHash)+               Just h -> maybeContractName' (preview (ix h % _2) dappinfo.solcByHash)                Nothing -> ""   in     name <> "@" <> (pack $ show addr)@@ -192,14 +190,14 @@  showTrace :: DappInfo -> VM -> Trace -> Text showTrace dapp vm trace =-  let ?context = DappContext { info = dapp, env = vm._env._contracts }+  let ?context = DappContext { info = dapp, env = vm.env.contracts }   in let     pos =       case showTraceLocation dapp trace of         Left x -> " \x1b[1m" <> x <> "\x1b[0m"         Right x -> " \x1b[1m(" <> x <> ")\x1b[0m"     fullAbiMap = dapp.abiMap-  in case trace._traceData of+  in case trace.tracedata of     EventTrace _ bytes topics ->       let logn = mconcat             [ "\x1b[36m"@@ -241,7 +239,7 @@                       --     bytes             data                       -- ) anonymous;                       let-                        sig = fromIntegral $ shiftR topic 224 :: Word32+                        sig = fromIntegral $ shiftR topic 224 :: FunctionSelector                         usr = case maybeLitWord t2 of                           Just w ->                             pack $ show (fromIntegral w :: Addr)@@ -298,7 +296,7 @@       t     FrameTrace (CreationContext addr (Lit hash) _ _ ) -> -- FIXME: irrefutable pattern       "create "-      <> maybeContractName (preview (ix hash . _2) dapp.solcByHash)+      <> maybeContractName (preview (ix hash % _2) dapp.solcByHash)       <> "@" <> pack (show addr)       <> pos     FrameTrace (CreationContext addr _ _ _ ) ->@@ -311,7 +309,7 @@                      then "call "                      else "delegatecall "           hash' = fromJust $ maybeLitWord hash-      in case preview (ix hash' . _2) dapp.solcByHash of+      in case preview (ix hash' % _2) dapp.solcByHash of         Nothing ->           calltype             <> pack (show target)

@@ -48,11 +48,11 @@  -- variable names in SMT that we want to get values for data CexVars = CexVars-  { calldataV :: [Text]-  , buffersV :: Map Text (Expr EWord) -- buffers and guesses at their maximum size-  , storeReads :: [(Expr EWord, Expr EWord)] -- a list of relevant store reads-  , blockContextV :: [Text]-  , txContextV :: [Text]+  { calldata     :: [Text]+  , buffers      :: Map Text (Expr EWord) -- buffers and guesses at their maximum size+  , storeReads   :: [(Expr EWord, Expr EWord)] -- a list of relevant store reads+  , blockContext :: [Text]+  , txContext    :: [Text]   }   deriving (Eq, Show) @@ -61,11 +61,11 @@  instance Monoid CexVars where     mempty = CexVars-      { calldataV = mempty-      , buffersV = mempty+      { calldata = mempty+      , buffers = mempty       , storeReads = mempty-      , blockContextV = mempty-      , txContextV = mempty+      , blockContext = mempty+      , txContext = mempty       }  -- | A model for a buffer, either in it's compressed form (for storing parsed@@ -97,7 +97,7 @@ flattenBufs :: SMTCex -> Maybe SMTCex flattenBufs cex = do   bs <- mapM collapse cex.buffers-  pure $ cex { buffers = bs}+  pure $ cex{ buffers = bs }  -- | Attemps to collapse a compressed buffer representation down to a flattened one collapse :: BufModel -> Maybe BufModel@@ -161,7 +161,7 @@   <> readAssumes   <> SMT2 [""] mempty   <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty-  <> SMT2 [] mempty{storeReads = storageReads}+  <> SMT2 [] mempty{ storeReads = storageReads }    where     (ps_elim, bufs, stores) = eliminateProps ps@@ -319,8 +319,8 @@ declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2 declareBufs props bufEnv storeEnv = SMT2 ("; buffers" : fmap declareBuf allBufs <> ("; buffer lengths" : fmap declareLength allBufs)) cexvars   where-    cexvars = mempty{buffersV = discoverMaxReads props bufEnv storeEnv}-    allBufs = fmap fromLazyText $ Map.keys cexvars.buffersV+    cexvars = (mempty :: CexVars){ buffers = discoverMaxReads props bufEnv storeEnv }+    allBufs = fmap fromLazyText $ Map.keys cexvars.buffers     declareBuf n = "(declare-const " <> n <> " (Array (_ BitVec 256) (_ BitVec 8)))"     declareLength n = "(declare-const " <> n <> "_length" <> " (_ BitVec 256))" @@ -329,21 +329,21 @@ declareVars names = SMT2 (["; variables"] <> fmap declare names) cexvars   where     declare n = "(declare-const " <> n <> " (_ BitVec 256))"-    cexvars = mempty{calldataV = fmap toLazyText names}+    cexvars = mempty{ calldata = fmap toLazyText names }   declareFrameContext :: [Builder] -> SMT2 declareFrameContext names = SMT2 (["; frame context"] <> fmap declare names) cexvars   where     declare n = "(declare-const " <> n <> " (_ BitVec 256))"-    cexvars = mempty{txContextV = fmap toLazyText names}+    cexvars = (mempty :: CexVars){ txContext = fmap toLazyText names }   declareBlockContext :: [Builder] -> SMT2 declareBlockContext names = SMT2 (["; block context"] <> fmap declare names) cexvars   where     declare n = "(declare-const " <> n <> " (_ BitVec 256))"-    cexvars = mempty{blockContextV = fmap toLazyText names}+    cexvars = (mempty :: CexVars){ blockContext = fmap toLazyText names }   prelude :: SMT2

@@ -42,12 +42,14 @@ import EVM.ABI import EVM.Types +import Optics.Core+import Optics.Operators.Unsafe+ import Control.Applicative-import Control.Lens hiding (Indexed, (.=)) import Control.Monad import Data.Aeson hiding (json) import Data.Aeson.Types-import Data.Aeson.Lens+import Data.Aeson.Optics import Data.Aeson.Key qualified as Key import Data.Aeson.KeyMap qualified as KeyMap import Data.Scientific@@ -73,7 +75,7 @@ import Data.Text.IO (readFile, writeFile) import Data.Vector (Vector) import Data.Vector qualified as Vector-import Data.Word (Word8, Word32)+import Data.Word (Word8) import GHC.Generics (Generic) import Prelude hiding (readFile, writeFile) import System.IO hiding (readFile, writeFile)@@ -125,7 +127,7 @@   , creationCode     :: ByteString   , contractName     :: Text   , constructorInputs :: [(Text, AbiType)]-  , abiMap           :: Map Word32 Method+  , abiMap           :: Map FunctionSelector Method   , eventMap         :: Map W256 Event   , errorMap         :: Map W256 SolError   , immutableReferences :: Map W256 [Reference]@@ -177,11 +179,11 @@   deriving (Show, Eq, Ord, Generic)  data SrcMap = SM {-  srcMapOffset :: {-# UNPACK #-} !Int,-  srcMapLength :: {-# UNPACK #-} !Int,-  srcMapFile   :: {-# UNPACK #-} !Int,-  srcMapJump   :: JumpType,-  srcMapModifierDepth :: {-# UNPACK #-} !Int+  offset        :: {-# UNPACK #-} !Int,+  length        :: {-# UNPACK #-} !Int,+  file          :: {-# UNPACK #-} !Int,+  jump          :: JumpType,+  modifierDepth :: {-# UNPACK #-} !Int } deriving (Show, Eq, Ord, Generic)  data SrcMapParseState@@ -281,7 +283,7 @@   (json, path) <- yul' src   let f = (json ^?! key "contracts") ^?! key (Key.fromText path)       c = f ^?! key (Key.fromText $ if Text.null contract then "object" else contract)-      bytecode = c ^?! key "evm" ^?! key "bytecode" ^?! key "object" . _String+      bytecode = c ^?! key "evm" ^?! key "bytecode" ^?! key "object" % _String   pure $ toCode <$> (Just bytecode)  yulRuntime :: Text -> Text -> IO (Maybe ByteString)@@ -289,7 +291,7 @@   (json, path) <- yul' src   let f = (json ^?! key "contracts") ^?! key (Key.fromText path)       c = f ^?! key (Key.fromText $ if Text.null contract then "object" else contract)-      bytecode = c ^?! key "evm" ^?! key "deployedBytecode" ^?! key "object" . _String+      bytecode = c ^?! key "evm" ^?! key "deployedBytecode" ^?! key "object" % _String   pure $ toCode <$> (Just bytecode)  solidity :: Text -> Text -> IO (Maybe ByteString)@@ -323,26 +325,26 @@ -- deprecate me soon readCombinedJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)]) readCombinedJSON json = do-  contracts <- f . KeyMap.toHashMapText <$> (json ^? key "contracts" . _Object)-  sources <- toList . fmap (view _String) <$> json ^? key "sourceList" . _Array-  return (contracts, Map.fromList (HMap.toList asts), [ (x, Nothing) | x <- sources])+  contracts <- f . KeyMap.toHashMapText <$> (json ^? key "contracts" % _Object)+  sources <- toList . fmap (preview _String) <$> json ^? key "sourceList" % _Array+  return (contracts, Map.fromList (HMap.toList asts), [ (x, Nothing) | Just x <- sources])   where-    asts = KeyMap.toHashMapText $ fromMaybe (error "JSON lacks abstract syntax trees.") (json ^? key "sources" . _Object)+    asts = KeyMap.toHashMapText $ fromMaybe (error "JSON lacks abstract syntax trees.") (json ^? key "sources" % _Object)     f x = Map.fromList . HMap.toList $ HMap.mapWithKey g x     g s x =       let-        theRuntimeCode = toCode (x ^?! key "bin-runtime" . _String)-        theCreationCode = toCode (x ^?! key "bin" . _String)+        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+                 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)),+        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,@@ -354,9 +356,9 @@  readStdJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)]) readStdJSON json = do-  contracts <- KeyMap.toHashMapText <$> json ^? key "contracts" . _Object+  contracts <- KeyMap.toHashMapText <$> json ^? key "contracts" % _Object   -- TODO: support the general case of "urls" and "content" in the standard json-  sources <- KeyMap.toHashMapText <$>  json ^? key "sources" . _Object+  sources <- KeyMap.toHashMapText <$>  json ^? key "sources" % _Object   let asts = force "JSON lacks abstract syntax trees." . preview (key "ast") <$> sources       contractMap = f contracts       contents src = (src, encodeUtf8 <$> HMap.lookup src (mconcat $ Map.elems $ snd <$> contractMap))@@ -364,28 +366,30 @@   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 (view _Object x))+    g (s, x) = h s <$> HMap.toList (KeyMap.toHashMapText (fromMaybe (error "Could not parse json object") (preview _Object x)))     h :: Text -> (Text, Value) -> (Text, (SolcContract, HMap.HashMap Text Text))     h s (c, x) =       let         evmstuff = x ^?! key "evm"         runtime = evmstuff ^?! key "deployedBytecode"         creation =  evmstuff ^?! key "bytecode"-        theRuntimeCode = toCode $ fromMaybe "" $ runtime ^? key "object" . _String-        theCreationCode = toCode $ fromMaybe "" $ creation ^? key "object" . _String+        theRuntimeCode = toCode $ fromMaybe "" $ runtime ^? key "object" % _String+        theCreationCode = toCode $ fromMaybe "" $ creation ^? key "object" % _String         srcContents :: Maybe (HMap.HashMap Text Text)-        srcContents = do metadata <- x ^? key "metadata" . _String-                         srcs <- KeyMap.toHashMapText <$> metadata ^? key "sources" . _Object-                         return $ (view (key "content" . _String)) <$> (HMap.filter (isJust . preview (key "content")) srcs)+        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))+                           (HMap.filter (isJust . preview (key "content")) srcs)         abis = force ("abi key not found in " <> show x) $-          toList <$> x ^? key "abi" . _Array+          toList <$> x ^? key "abi" % _Array       in (s <> ":" <> c, (SolcContract {         runtimeCode      = theRuntimeCode,         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 "internal error: srcmap-runtime" (makeSrcMaps (runtime ^?! key "sourceMap" % _String)),+        creationSrcmap   = force "internal error: srcmap" (makeSrcMaps (creation ^?! key "sourceMap" % _String)),         contractName = s <> ":" <> c,         constructorInputs = mkConstructor abis,         abiMap        = mkAbiMap abis,@@ -399,55 +403,55 @@                _ -> Nothing       }, fromMaybe mempty srcContents)) -mkAbiMap :: [Value] -> Map Word32 Method+mkAbiMap :: [Value] -> Map FunctionSelector Method mkAbiMap abis = Map.fromList $   let-    relevant = filter (\y -> "function" == y ^?! key "type" . _String) abis+    relevant = filter (\y -> "function" == y ^?! key "type" % _String) abis     f abi =       (abiKeccak (encodeUtf8 (signature abi)),-       Method { name = abi ^?! key "name" . _String+       Method { name = abi ^?! key "name" % _String               , methodSignature = signature abi               , inputs = map parseMethodInput-                 (toList (abi ^?! key "inputs" . _Array))+                 (toList (abi ^?! key "inputs" % _Array))               , output = map parseMethodInput-                 (toList (abi ^?! key "outputs" . _Array))+                 (toList (abi ^?! key "outputs" % _Array))               , mutability = parseMutability-                 (abi ^?! key "stateMutability" . _String)+                 (abi ^?! key "stateMutability" % _String)               })   in f <$> relevant  mkEventMap :: [Value] -> Map W256 Event mkEventMap abis = Map.fromList $   let-    relevant = filter (\y -> "event" == y ^?! key "type" . _String) abis+    relevant = filter (\y -> "event" == y ^?! key "type" % _String) abis     f abi =      ( keccak' (encodeUtf8 (signature abi))      , Event-       (abi ^?! key "name" . _String)-       (case abi ^?! key "anonymous" . _Bool of+       (abi ^?! key "name" % _String)+       (case abi ^?! key "anonymous" % _Bool of          True -> Anonymous          False -> NotAnonymous)        (map (\y ->-        ( y ^?! key "name" . _String+        ( y ^?! key "name" % _String         , force "internal error: type" (parseTypeName' y)-        , if y ^?! key "indexed" . _Bool+        , if y ^?! key "indexed" % _Bool           then Indexed           else NotIndexed         ))-       (toList $ abi ^?! key "inputs" . _Array))+       (toList $ abi ^?! key "inputs" % _Array))      )   in f <$> relevant  mkErrorMap :: [Value] -> Map W256 SolError mkErrorMap abis = Map.fromList $   let-    relevant = filter (\y -> "error" == y ^?! key "type" . _String) abis+    relevant = filter (\y -> "error" == y ^?! key "type" % _String) abis     f abi =      ( stripKeccak $ keccak' (encodeUtf8 (signature abi))      , SolError-       (abi ^?! key "name" . _String)+       (abi ^?! key "name" % _String)        (map (force "internal error: type" . parseTypeName')-       (toList $ abi ^?! key "inputs" . _Array))+       (toList $ abi ^?! key "inputs" % _Array))      )   in f <$> relevant   where@@ -458,24 +462,24 @@ mkConstructor abis =   let     isConstructor y =-      "constructor" == y ^?! key "type" . _String+      "constructor" == y ^?! key "type" % _String   in     case filter isConstructor abis of-      [abi] -> map parseMethodInput (toList (abi ^?! key "inputs" . _Array))+      [abi] -> map parseMethodInput (toList (abi ^?! key "inputs" % _Array))       [] -> [] -- default constructor has zero inputs       _  -> error "strange: contract has multiple constructors"  mkStorageLayout :: Maybe Value -> Maybe (Map Text StorageItem) mkStorageLayout Nothing = Nothing mkStorageLayout (Just json) = do-  items <- json ^? key "storage" . _Array+  items <- json ^? key "storage" % _Array   types <- json ^? key "types"   fmap Map.fromList (forM (Vector.toList items) $ \item ->-    do name <- item ^? key "label" . _String-       offset <- item ^? key "offset" . _Number >>= toBoundedInteger-       slot <- item ^? key "slot" . _String-       typ <- Key.fromText <$> item ^? key "type" . _String-       slotType <- types ^?! key typ ^? key "label" . _String+    do name <- item ^? key "label" % _String+       offset <- item ^? key "offset" % _Number >>= toBoundedInteger+       slot <- item ^? key "slot" % _String+       typ <- Key.fromText <$> item ^? key "type" % _String+       slotType <- types ^?! key typ ^? key "label" % _String        return (name, StorageItem (read $ Text.unpack slotType) offset (read $ Text.unpack slot)))  signature :: AsValue s => s -> Text@@ -484,10 +488,10 @@     "fallback" -> "<fallback>"     _ ->       fold [-        fromMaybe "<constructor>" (abi ^? key "name" . _String), "(",+        fromMaybe "<constructor>" (abi ^? key "name" % _String), "(",         intercalate ","-          (map (\x -> x ^?! key "type" . _String)-            (toList $ abi ^?! key "inputs" . _Array)),+          (map (\x -> x ^?! key "type" % _String)+            (toList $ abi ^?! key "inputs" % _Array)),         ")"       ] @@ -495,8 +499,8 @@ parseTypeName' :: AsValue s => s -> Maybe AbiType parseTypeName' x =   parseTypeName-    (fromMaybe mempty $ x ^? key "components" . _Array . to parseComponents)-    (x ^?! key "type" . _String)+    (fromMaybe mempty $ x ^? key "components" % _Array % to parseComponents)+    (x ^?! key "type" % _String)   where parseComponents = fmap $ snd . parseMethodInput  parseMutability :: Text -> Mutability@@ -509,7 +513,7 @@ -- This actually can also parse a method output! :O parseMethodInput :: AsValue s => s -> (Text, AbiType) parseMethodInput x =-  ( x ^?! key "name" . _String+  ( x ^?! key "name" % _String   , force "internal error: method type" (parseTypeName' x)   ) @@ -707,7 +711,7 @@        Map.fromList       . mapMaybe         (\v -> do-          src <- preview (key "src" . _String) v+          src <- preview (key "src" % _String) v           [i, n, f] <- mapM (readMaybe . Text.unpack) (Text.split (== ':') src)           return ((i, n, f), v)         )