hevm 0.51.3 → 0.52.0

raw patch · 55 files changed

+10119/−12270 lines, 55 filesdep +pretty-hexdep +system-cxx-std-libdep −ansi-wl-pprintdep −tuplePVP ok

version bump matches the API change (PVP)

Dependencies added: pretty-hex, system-cxx-std-lib

Dependencies removed: ansi-wl-pprint, tuple

API changes (from Hackage documentation)

Files

• CHANGELOG.md +114/−0
• bench/bench.hs +15/−28
• bench/contracts/deposit.sol +182/−0
• bench/contracts/vat.sol +246/−0
• cli/cli.hs +599/−0
• hevm-cli/hevm-cli.hs +0/−716
• hevm.cabal +22/−57
• src/EVM.hs +2627/−2316
• src/EVM/ABI.hs +79/−76
• src/EVM/Concrete.hs +9/−35
• src/EVM/Dapp.hs +44/−44
• src/EVM/Debug.hs +0/−52
• src/EVM/Dev.hs +0/−498
• src/EVM/Exec.hs +16/−15
• src/EVM/Expr.hs +443/−107
• src/EVM/Facts.hs +0/−231
• src/EVM/Facts/Git.hs +0/−48
• src/EVM/FeeSchedule.hs +16/−95
• src/EVM/Fetch.hs +26/−23
• src/EVM/Format.hs +258/−54
• src/EVM/Hexdump.hs +0/−129
• src/EVM/Keccak.hs +26/−4
• src/EVM/Patricia.hs +0/−226
• src/EVM/SMT.hs +288/−202
• src/EVM/Solidity.hs +46/−112
• src/EVM/Solvers.hs +48/−19
• src/EVM/Stepper.hs +34/−45
• src/EVM/StorageLayout.hs +0/−152
• src/EVM/SymExec.hs +272/−175
• src/EVM/TTY.hs +0/−1047
• src/EVM/TTYCenteredList.hs +0/−70
• src/EVM/Transaction.hs +13/−23
• src/EVM/Traversals.hs +120/−222
• src/EVM/Types.hs +212/−199
• src/EVM/UnitTest.hs +127/−650
• test/EVM/Test/BlockchainTests.hs +140/−132
• test/EVM/Test/Tracing.hs +234/−160
• test/EVM/Test/Utils.hs +9/−23
• test/contracts/fail/cheatCodes.sol +0/−39
• test/contracts/fail/dsProveFail.sol +0/−66
• test/contracts/fail/invariantFail.sol +0/−50
• test/contracts/fail/trivial.sol +0/−9
• test/contracts/lib/erc20.sol +0/−201
• test/contracts/lib/test.sol +0/−469
• test/contracts/pass/abstract.sol +0/−15
• test/contracts/pass/cheatCodes.sol +0/−125
• test/contracts/pass/constantinople.sol +0/−331
• test/contracts/pass/dsProvePass.sol +0/−83
• test/contracts/pass/invariants.sol +0/−41
• test/contracts/pass/libraries.sol +0/−18
• test/contracts/pass/loops.sol +0/−12
• test/contracts/pass/rpc.sol +0/−16
• test/contracts/pass/trivial.sol +0/−9
• test/rpc.hs +41/−38
• test/test.hs +3813/−2763

@@ -5,6 +5,119 @@ 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.52.0] - 2023-10-26++This is a major breaking release that removes several user facing features and includes non trivial+breakage for library users. These changes mean the code is significantly simpler, more performant,+and allow support for new features like fully symbolic addresses.++In addition to the changes below, this release includes significant work on performance+optimization for symbolic execution.++## Added++The major new user facing feature in this release is support for fully symbolic addresses (including+fully symbolic addresses for deployed contracts). This allows tests to be writen that call+`vm.prank` with a symbolic value, making some tests (e.g. access control, token transfer logic) much+more comprehensive.++Some restrictions around reading balances from and transfering value between symbolic addresses are+currently in place. Currently, if the address is symbolic, then you will only be able to read it's+balance, or transfer value to/from it, if it is the address of a contract that is actually deployed.+This is required to ensure soundness in the face of aliasing between symbolic addresses. We intend+to lift this restriction in a future release.++### Other++- Support for `vm.deal`+- Support for `vm.assume` (this is semantically identical to using `require`, but does simplify the+    process of porting exisitng fuzz tests to be symbolic)+- the `check` prefix now recognized for symbolic tests+- `hevm test` now takes a `--number` argument to specify which block should be used when making rpc queries++## Changed++### Revert Semantics in Solidity Tests++solidity tests no longer consider reverts to be a failure, and check only for the ds-test failed bit+or user defined assertion failures (i.e. `Panic(0x01)`). This makes writing tests much easier as+users no longer have to consider trivial reverts (e.g. arithmetic overflow).++A positive (i.e. `prove`/`check`) test with no rechable assertion violations that does not have any+succesful branches will still be considered a failure.++## Removed++hevm has been around for a while, and over time has accumulated many features. We decided to remove+some of these features in the interest of focusing our attention, increasing our iteration speed and+simplifying maintainance. The following user facing features have been removed from this release:++- The visual debugger has been removed+- All concrete ds-test executors have been removed (i.e. plain, fuzzer, invariant)+- Rpc caching and state serialization has been removed (i.e. all `--cache` / `--state` flags)+- The various `DAPP_TEST` variables are no longer observed+- The `--initial-storage` flag no longer accepts a concrete prestore (valid values are now `Empty` or `Abstract`)++## Fixed++This release also includes many small bugfixes:++- CopySlice wraparound issue especially during CopyCallBytesToMemory+- Contracts deployed during symbolic execution are created with an empty storage (instead of abstract in previous versions)+- EVM.Solidity.toCode to include contractName in error string+- Better cex reconstruction in cases where branches do not refer to all input variables in calldata+- Correctly handle empty bytestring compiled contracts' JSON+- No more false positives when keccak is called with inputs of different sizes+- `test` now falls back to displaying an unecoded bytestring for calldata when the model returned by the solver has a different length the length of the arguments in the test signature.+- we now generate correct counterexamples for branches where only a subset of input variables are referenced by the path conditions+- `vm.prank` now works correctly when passed a symbolic address+- storage layout information will now be parsed from the output of `forge build` if it is available++## API Changes++### Reworked Storage Model / Symbolic Addresses++Adding symbolic addresses required some fairly significant changes to the way that we model storage.+We introduced a new address type to `Expr` (`Expr EAddr`), that allows us to model fully symbolic+addresses. Instead of modelling storage as a global symbolic 2D map (`address -> word -> word`) in+`vm.env`, each contract now has it's own symbolic 1D map (`word -> word`), that is stored in the+`vm.contracts` mapping. `vm.contracts` is now keyed on `Expr EAddr` instead of `Addr`. Addresses+that are keys to the `vm.contracts` mapping are asserted to be distinct in our smt encoding. This+allows us to support symbolic addresses in a fully static manner (i.e. we do not currently need to+make any extra smt queries when looking up storage for a symbolic address).++### Mutable Memory & ST++We now use a mutable representation of memory if it is currently completely concrete. This is a+significant performance improvement, and fixed a particulary egregious memory leak. It does entail+the use of the `ST` monad, and introduces a new type parameter to the `VM` type that tags a given+instance with it's thread local state. Library users will now need to either use the ST moand and+`runST` or `stToIO` to compose and sequence vm executions.++## GHC 9.4++Hevm is now built with ghc9.4. While earlier compiler versions may continue to work for now, they+are no longer explicitly tested or supported.++### Other++- Contract balances can now be fully symbolic+- Contract code can now be fully abstract. Calls into contracts with unknown code will fail with `UnexpectedSymbolicArg`.+- Run expression simplification on branch conditions+- SLoad/SStore simplifications based on assumptions regarding Keccak non-collision&preimage+- Improved Prop simplification+- CopySlice+WriteWord+ConcreteBuf now truncates ConcreteBuf in special cases+- Better simplification of Eq IR elements+- Run a toplevel constant folding reasoning system on branch conditions+- `evalProp` is renamed to `simplifyProp` for consistency+- Mem explosion in `writeWord` function was possible in case `offset` was close to 2^256. Fixed.+- BufLength was not simplified via bufLength function. Fixed.+- `VMOpts` no longer takes an initial store, and instead takes a `baseState`+  which can be either `EmptyBase` or `AbstractBase`. This controls whether+  storage should be inialized as empty or fully abstract. Regardless of this+  setting contracts that are deployed at runtime via a call to+  `CREATE`/`CREATE2` have zero initialized storage.+ ## [0.51.3] - 2023-07-14  ## Fixed@@ -16,6 +129,7 @@ ## Changed  - Removed sha3Crack which has been deprecated for keccakEqs+- Abstraction-refinement for more complicated expressions such as MULMOD  ## Added 

@@ -3,30 +3,23 @@ import GHC.Natural import Control.Monad import Data.Maybe-import System.Environment (lookupEnv, getEnv)+import System.Environment (getEnv)  import qualified Paths_hevm as Paths  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 import EVM.Solidity import EVM.Solvers-import EVM.ABI-import EVM.Dapp-import EVM.Types-import qualified EVM.TTY as TTY+import EVM.Format (hexByteString) import qualified EVM.Stepper as Stepper import qualified EVM.Fetch as Fetch @@ -34,10 +27,10 @@  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]+  [ mkbench erc20 "erc20" 0 [1]+  , mkbench (pure vat) "vat" 0 [4]+  , mkbench (pure deposit) "deposit" 32 [4]+  , mkbench (pure uniV2Pair) "uniV2" 10 [4]   , withResource bcjsons (pure . const ()) blockchainTests   ] @@ -59,7 +52,7 @@     parseSuite path = do       contents <- LazyByteString.readFile path       case BCTests.parseBCSuite contents of-        Left e -> pure (path, mempty)+        Left _ -> pure (path, mempty)         Right tests -> pure (path, tests)  -- | executes all provided bc tests in sequence and accumulates a boolean value representing their success.@@ -67,7 +60,7 @@ blockchainTests :: IO (Map.Map FilePath (Map.Map String BCTests.Case)) -> Benchmark blockchainTests ts = bench "blockchain-tests" $ nfIO $ do   tests <- ts-  putStrLn "\n    executing tests:"+  putStrLn "    executing blockchain tests"   let cases = concat . Map.elems . (fmap Map.toList) $ tests       ignored = Map.keys BCTests.commonProblematicTests   foldM (\acc (n, c) ->@@ -75,7 +68,6 @@       then pure True       else do         res <- runBCTest c-        putStrLn $ "      " <> n         pure $ acc && res     ) True cases @@ -83,8 +75,8 @@ 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+  vm0 <- BCTests.vmForCase x+  result <- Stepper.interpret (Fetch.zero 0 Nothing) vm0 Stepper.runFully   maybeReason <- BCTests.checkExpectation False x result   pure $ isNothing maybeReason @@ -92,17 +84,12 @@ --- 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 -> Natural -> Integer -> ByteString -> IO () findPanics solver count iters c = do-  (_, res) <- withSolvers solver count Nothing $ \s -> do+  _ <- withSolvers solver count Nothing $ \s -> do     let opts = defaultVeriOpts-          { maxIter = iters-          , askSmtIters = (+ 1) <$> iters+          { maxIter = Just iters+          , askSmtIters = iters + 1           }     checkAssert s allPanicCodes c Nothing [] opts   putStrLn "done"@@ -112,7 +99,7 @@ -- assertion violations takes an iteration bound, as well as a list of solver -- counts to benchmark, allowing us to construct benchmarks that compare the -- performance impact of increasing solver parallelisation-mkbench :: IO ByteString -> String -> Maybe Integer -> [Natural] -> Benchmark+mkbench :: IO ByteString -> String -> Integer -> [Natural] -> Benchmark mkbench c name iters counts = localOption WallTime $ env c (bgroup name . bmarks)   where     bmarks c' = concat $ [

@@ -0,0 +1,182 @@+/**+ *Submitted for verification at Etherscan.io on 2020-10-14+*/++// ┏━━━┓━┏┓━┏┓━━┏━━━┓━━┏━━━┓━━━━┏━━━┓━━━━━━━━━━━━━━━━━━━┏┓━━━━━┏━━━┓━━━━━━━━━┏┓━━━━━━━━━━━━━━┏┓━+// ┃┏━━┛┏┛┗┓┃┃━━┃┏━┓┃━━┃┏━┓┃━━━━┗┓┏┓┃━━━━━━━━━━━━━━━━━━┏┛┗┓━━━━┃┏━┓┃━━━━━━━━┏┛┗┓━━━━━━━━━━━━┏┛┗┓+// ┃┗━━┓┗┓┏┛┃┗━┓┗┛┏┛┃━━┃┃━┃┃━━━━━┃┃┃┃┏━━┓┏━━┓┏━━┓┏━━┓┏┓┗┓┏┛━━━━┃┃━┗┛┏━━┓┏━┓━┗┓┏┛┏━┓┏━━┓━┏━━┓┗┓┏┛+// ┃┏━━┛━┃┃━┃┏┓┃┏━┛┏┛━━┃┃━┃┃━━━━━┃┃┃┃┃┏┓┃┃┏┓┃┃┏┓┃┃━━┫┣┫━┃┃━━━━━┃┃━┏┓┃┏┓┃┃┏┓┓━┃┃━┃┏┛┗━┓┃━┃┏━┛━┃┃━+// ┃┗━━┓━┃┗┓┃┃┃┃┃┃┗━┓┏┓┃┗━┛┃━━━━┏┛┗┛┃┃┃━┫┃┗┛┃┃┗┛┃┣━━┃┃┃━┃┗┓━━━━┃┗━┛┃┃┗┛┃┃┃┃┃━┃┗┓┃┃━┃┗┛┗┓┃┗━┓━┃┗┓+// ┗━━━┛━┗━┛┗┛┗┛┗━━━┛┗┛┗━━━┛━━━━┗━━━┛┗━━┛┃┏━┛┗━━┛┗━━┛┗┛━┗━┛━━━━┗━━━┛┗━━┛┗┛┗┛━┗━┛┗┛━┗━━━┛┗━━┛━┗━┛+// ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┃┃━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━+// ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┗┛━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━++// SPDX-License-Identifier: CC0-1.0++pragma solidity 0.6.11;++// This interface is designed to be compatible with the Vyper version.+/// @notice This is the Ethereum 2.0 deposit contract interface.+/// For more information see the Phase 0 specification under https://github.com/ethereum/eth2.0-specs+interface IDepositContract {+    /// @notice A processed deposit event.+    event DepositEvent(+        bytes pubkey,+        bytes withdrawal_credentials,+        bytes amount,+        bytes signature,+        bytes index+    );++    /// @notice Submit a Phase 0 DepositData object.+    /// @param pubkey A BLS12-381 public key.+    /// @param withdrawal_credentials Commitment to a public key for withdrawals.+    /// @param signature A BLS12-381 signature.+    /// @param deposit_data_root The SHA-256 hash of the SSZ-encoded DepositData object.+    /// Used as a protection against malformed input.+    function deposit(+        bytes calldata pubkey,+        bytes calldata withdrawal_credentials,+        bytes calldata signature,+        bytes32 deposit_data_root+    ) external payable;++    /// @notice Query the current deposit root hash.+    /// @return The deposit root hash.+    function get_deposit_root() external view returns (bytes32);++    /// @notice Query the current deposit count.+    /// @return The deposit count encoded as a little endian 64-bit number.+    function get_deposit_count() external view returns (bytes memory);+}++// Based on official specification in https://eips.ethereum.org/EIPS/eip-165+interface ERC165 {+    /// @notice Query if a contract implements an interface+    /// @param interfaceId The interface identifier, as specified in ERC-165+    /// @dev Interface identification is specified in ERC-165. This function+    ///  uses less than 30,000 gas.+    /// @return `true` if the contract implements `interfaceId` and+    ///  `interfaceId` is not 0xffffffff, `false` otherwise+    function supportsInterface(bytes4 interfaceId) external pure returns (bool);+}++// This is a rewrite of the Vyper Eth2.0 deposit contract in Solidity.+// It tries to stay as close as possible to the original source code.+/// @notice This is the Ethereum 2.0 deposit contract interface.+/// For more information see the Phase 0 specification under https://github.com/ethereum/eth2.0-specs+contract DepositContract is IDepositContract, ERC165 {+    uint constant DEPOSIT_CONTRACT_TREE_DEPTH = 32;+    // NOTE: this also ensures `deposit_count` will fit into 64-bits+    uint constant MAX_DEPOSIT_COUNT = 2**DEPOSIT_CONTRACT_TREE_DEPTH - 1;++    bytes32[DEPOSIT_CONTRACT_TREE_DEPTH] branch;+    uint256 deposit_count;++    bytes32[DEPOSIT_CONTRACT_TREE_DEPTH] zero_hashes;++    constructor() public {+        // Compute hashes in empty sparse Merkle tree+        for (uint height = 0; height < DEPOSIT_CONTRACT_TREE_DEPTH - 1; height++)+            zero_hashes[height + 1] = sha256(abi.encodePacked(zero_hashes[height], zero_hashes[height]));+    }++    function get_deposit_root() override external view returns (bytes32) {+        bytes32 node;+        uint size = deposit_count;+        for (uint height = 0; height < DEPOSIT_CONTRACT_TREE_DEPTH; height++) {+            if ((size & 1) == 1)+                node = sha256(abi.encodePacked(branch[height], node));+            else+                node = sha256(abi.encodePacked(node, zero_hashes[height]));+            size /= 2;+        }+        return sha256(abi.encodePacked(+            node,+            to_little_endian_64(uint64(deposit_count)),+            bytes24(0)+        ));+    }++    function get_deposit_count() override external view returns (bytes memory) {+        return to_little_endian_64(uint64(deposit_count));+    }++    function deposit(+        bytes calldata pubkey,+        bytes calldata withdrawal_credentials,+        bytes calldata signature,+        bytes32 deposit_data_root+    ) override external payable {+        // Extended ABI length checks since dynamic types are used.+        require(pubkey.length == 48, "DepositContract: invalid pubkey length");+        require(withdrawal_credentials.length == 32, "DepositContract: invalid withdrawal_credentials length");+        require(signature.length == 96, "DepositContract: invalid signature length");++        // Check deposit amount+        require(msg.value >= 1 ether, "DepositContract: deposit value too low");+        require(msg.value % 1 gwei == 0, "DepositContract: deposit value not multiple of gwei");+        uint deposit_amount = msg.value / 1 gwei;+        require(deposit_amount <= type(uint64).max, "DepositContract: deposit value too high");++        // Emit `DepositEvent` log+        bytes memory amount = to_little_endian_64(uint64(deposit_amount));+        emit DepositEvent(+            pubkey,+            withdrawal_credentials,+            amount,+            signature,+            to_little_endian_64(uint64(deposit_count))+        );++        // Compute deposit data root (`DepositData` hash tree root)+        bytes32 pubkey_root = sha256(abi.encodePacked(pubkey, bytes16(0)));+        bytes32 signature_root = sha256(abi.encodePacked(+            sha256(abi.encodePacked(signature[:64])),+            sha256(abi.encodePacked(signature[64:], bytes32(0)))+        ));+        bytes32 node = sha256(abi.encodePacked(+            sha256(abi.encodePacked(pubkey_root, withdrawal_credentials)),+            sha256(abi.encodePacked(amount, bytes24(0), signature_root))+        ));++        // Verify computed and expected deposit data roots match+        require(node == deposit_data_root, "DepositContract: reconstructed DepositData does not match supplied deposit_data_root");++        // Avoid overflowing the Merkle tree (and prevent edge case in computing `branch`)+        require(deposit_count < MAX_DEPOSIT_COUNT, "DepositContract: merkle tree full");++        // Add deposit data root to Merkle tree (update a single `branch` node)+        deposit_count += 1;+        uint size = deposit_count;+        for (uint height = 0; height < DEPOSIT_CONTRACT_TREE_DEPTH; height++) {+            if ((size & 1) == 1) {+                branch[height] = node;+                return;+            }+            node = sha256(abi.encodePacked(branch[height], node));+            size /= 2;+        }+        // As the loop should always end prematurely with the `return` statement,+        // this code should be unreachable. We assert `false` just to be safe.+        assert(false);+    }++    function supportsInterface(bytes4 interfaceId) override external pure returns (bool) {+        return interfaceId == type(ERC165).interfaceId || interfaceId == type(IDepositContract).interfaceId;+    }++    function to_little_endian_64(uint64 value) internal pure returns (bytes memory ret) {+        ret = new bytes(8);+        bytes8 bytesValue = bytes8(value);+        // Byteswapping during copying to bytes.+        ret[0] = bytesValue[7];+        ret[1] = bytesValue[6];+        ret[2] = bytesValue[5];+        ret[3] = bytesValue[4];+        ret[4] = bytesValue[3];+        ret[5] = bytesValue[2];+        ret[6] = bytesValue[1];+        ret[7] = bytesValue[0];+    }+}

@@ -0,0 +1,246 @@+// SPDX-License-Identifier: AGPL-3.0-or-later++/// vat.sol -- Dai CDP database++// Copyright (C) 2018 Rain <rainbreak@riseup.net>+//+// This program is free software: you can redistribute it and/or modify+// it under the terms of the GNU Affero General Public License as published by+// the Free Software Foundation, either version 3 of the License, or+// (at your option) any later version.+//+// This program is distributed in the hope that it will be useful,+// but WITHOUT ANY WARRANTY; without even the implied warranty of+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the+// GNU Affero General Public License for more details.+//+// You should have received a copy of the GNU Affero General Public License+// along with this program.  If not, see <https://www.gnu.org/licenses/>.++pragma solidity ^0.6.12;++// FIXME: This contract was altered compared to the production version.+// It doesn't use LibNote anymore.+// New deployments of this contract will need to include custom events (TO DO).++contract Vat {+    // --- Auth ---+    mapping (address => uint) public wards;+    function rely(address usr) external auth { require(live == 1, "Vat/not-live"); wards[usr] = 1; }+    function deny(address usr) external auth { require(live == 1, "Vat/not-live"); wards[usr] = 0; }+    modifier auth {+        require(wards[msg.sender] == 1, "Vat/not-authorized");+        _;+    }++    mapping(address => mapping (address => uint)) public can;+    function hope(address usr) external { can[msg.sender][usr] = 1; }+    function nope(address usr) external { can[msg.sender][usr] = 0; }+    function wish(address bit, address usr) internal view returns (bool) {+        return either(bit == usr, can[bit][usr] == 1);+    }++    // --- Data ---+    struct Ilk {+        uint256 Art;   // Total Normalised Debt     [wad]+        uint256 rate;  // Accumulated Rates         [ray]+        uint256 spot;  // Price with Safety Margin  [ray]+        uint256 line;  // Debt Ceiling              [rad]+        uint256 dust;  // Urn Debt Floor            [rad]+    }+    struct Urn {+        uint256 ink;   // Locked Collateral  [wad]+        uint256 art;   // Normalised Debt    [wad]+    }++    mapping (bytes32 => Ilk)                       public ilks;+    mapping (bytes32 => mapping (address => Urn )) public urns;+    mapping (bytes32 => mapping (address => uint)) public gem;  // [wad]+    mapping (address => uint256)                   public dai;  // [rad]+    mapping (address => uint256)                   public sin;  // [rad]++    uint256 public debt;  // Total Dai Issued    [rad]+    uint256 public vice;  // Total Unbacked Dai  [rad]+    uint256 public Line;  // Total Debt Ceiling  [rad]+    uint256 public live;  // Active Flag++    // --- Init ---+    constructor() public {+        wards[msg.sender] = 1;+        live = 1;+    }++    // --- Math ---+    function _add(uint x, int y) internal pure returns (uint z) {+        z = x + uint(y);+        require(y >= 0 || z <= x);+        require(y <= 0 || z >= x);+    }+    function _sub(uint x, int y) internal pure returns (uint z) {+        z = x - uint(y);+        require(y <= 0 || z <= x);+        require(y >= 0 || z >= x);+    }+    function _mul(uint x, int y) internal pure returns (int z) {+        z = int(x) * y;+        require(int(x) >= 0);+        require(y == 0 || z / y == int(x));+    }+    function _add(uint x, uint y) internal pure returns (uint z) {+        require((z = x + y) >= x);+    }+    function _sub(uint x, uint y) internal pure returns (uint z) {+        require((z = x - y) <= x);+    }+    function _mul(uint x, uint y) internal pure returns (uint z) {+        require(y == 0 || (z = x * y) / y == x);+    }++    // --- Administration ---+    function init(bytes32 ilk) external auth {+        require(ilks[ilk].rate == 0, "Vat/ilk-already-init");+        ilks[ilk].rate = 10 ** 27;+    }+    function file(bytes32 what, uint data) external auth {+        require(live == 1, "Vat/not-live");+        if (what == "Line") Line = data;+        else revert("Vat/file-unrecognized-param");+    }+    function file(bytes32 ilk, bytes32 what, uint data) external auth {+        require(live == 1, "Vat/not-live");+        if (what == "spot") ilks[ilk].spot = data;+        else if (what == "line") ilks[ilk].line = data;+        else if (what == "dust") ilks[ilk].dust = data;+        else revert("Vat/file-unrecognized-param");+    }+    function cage() external auth {+        live = 0;+    }++    // --- Fungibility ---+    function slip(bytes32 ilk, address usr, int256 wad) external auth {+        gem[ilk][usr] = _add(gem[ilk][usr], wad);+    }+    function flux(bytes32 ilk, address src, address dst, uint256 wad) external {+        require(wish(src, msg.sender), "Vat/not-allowed");+        gem[ilk][src] = _sub(gem[ilk][src], wad);+        gem[ilk][dst] = _add(gem[ilk][dst], wad);+    }+    function move(address src, address dst, uint256 rad) external {+        require(wish(src, msg.sender), "Vat/not-allowed");+        dai[src] = _sub(dai[src], rad);+        dai[dst] = _add(dai[dst], rad);+    }++    function either(bool x, bool y) internal pure returns (bool z) {+        assembly{ z := or(x, y)}+    }+    function both(bool x, bool y) internal pure returns (bool z) {+        assembly{ z := and(x, y)}+    }++    // --- CDP Manipulation ---+    function frob(bytes32 i, address u, address v, address w, int dink, int dart) external {+        // system is live+        require(live == 1, "Vat/not-live");++        Urn memory urn = urns[i][u];+        Ilk memory ilk = ilks[i];+        // ilk has been initialised+        require(ilk.rate != 0, "Vat/ilk-not-init");++        urn.ink = _add(urn.ink, dink);+        urn.art = _add(urn.art, dart);+        ilk.Art = _add(ilk.Art, dart);++        int dtab = _mul(ilk.rate, dart);+        uint tab = _mul(ilk.rate, urn.art);+        debt     = _add(debt, dtab);++        // either debt has decreased, or debt ceilings are not exceeded+        require(either(dart <= 0, both(_mul(ilk.Art, ilk.rate) <= ilk.line, debt <= Line)), "Vat/ceiling-exceeded");+        // urn is either less risky than before, or it is safe+        require(either(both(dart <= 0, dink >= 0), tab <= _mul(urn.ink, ilk.spot)), "Vat/not-safe");++        // urn is either more safe, or the owner consents+        require(either(both(dart <= 0, dink >= 0), wish(u, msg.sender)), "Vat/not-allowed-u");+        // collateral src consents+        require(either(dink <= 0, wish(v, msg.sender)), "Vat/not-allowed-v");+        // debt dst consents+        require(either(dart >= 0, wish(w, msg.sender)), "Vat/not-allowed-w");++        // urn has no debt, or a non-dusty amount+        require(either(urn.art == 0, tab >= ilk.dust), "Vat/dust");++        gem[i][v] = _sub(gem[i][v], dink);+        dai[w]    = _add(dai[w],    dtab);++        urns[i][u] = urn;+        ilks[i]    = ilk;+    }+    // --- CDP Fungibility ---+    function fork(bytes32 ilk, address src, address dst, int dink, int dart) external {+        Urn storage u = urns[ilk][src];+        Urn storage v = urns[ilk][dst];+        Ilk storage i = ilks[ilk];++        u.ink = _sub(u.ink, dink);+        u.art = _sub(u.art, dart);+        v.ink = _add(v.ink, dink);+        v.art = _add(v.art, dart);++        uint utab = _mul(u.art, i.rate);+        uint vtab = _mul(v.art, i.rate);++        // both sides consent+        require(both(wish(src, msg.sender), wish(dst, msg.sender)), "Vat/not-allowed");++        // both sides safe+        require(utab <= _mul(u.ink, i.spot), "Vat/not-safe-src");+        require(vtab <= _mul(v.ink, i.spot), "Vat/not-safe-dst");++        // both sides non-dusty+        require(either(utab >= i.dust, u.art == 0), "Vat/dust-src");+        require(either(vtab >= i.dust, v.art == 0), "Vat/dust-dst");+    }+    // --- CDP Confiscation ---+    function grab(bytes32 i, address u, address v, address w, int dink, int dart) external auth {+        Urn storage urn = urns[i][u];+        Ilk storage ilk = ilks[i];++        urn.ink = _add(urn.ink, dink);+        urn.art = _add(urn.art, dart);+        ilk.Art = _add(ilk.Art, dart);++        int dtab = _mul(ilk.rate, dart);++        gem[i][v] = _sub(gem[i][v], dink);+        sin[w]    = _sub(sin[w],    dtab);+        vice      = _sub(vice,      dtab);+    }++    // --- Settlement ---+    function heal(uint rad) external {+        address u = msg.sender;+        sin[u] = _sub(sin[u], rad);+        dai[u] = _sub(dai[u], rad);+        vice   = _sub(vice,   rad);+        debt   = _sub(debt,   rad);+    }+    function suck(address u, address v, uint rad) external auth {+        sin[u] = _add(sin[u], rad);+        dai[v] = _add(dai[v], rad);+        vice   = _add(vice,   rad);+        debt   = _add(debt,   rad);+    }++    // --- Rates ---+    function fold(bytes32 i, address u, int rate) external auth {+        require(live == 1, "Vat/not-live");+        Ilk storage ilk = ilks[i];+        ilk.rate = _add(ilk.rate, rate);+        int rad  = _mul(ilk.Art, rate);+        dai[u]   = _add(dai[u], rad);+        debt     = _add(debt,   rad);+    }+}

@@ -0,0 +1,599 @@+-- Main file of the hevm CLI program++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE TemplateHaskell #-}++module Main where++import Control.Monad (when, forM_, unless)+import Control.Monad.ST (RealWorld, stToIO)+import Data.ByteString (ByteString)+import Data.DoubleWord (Word256)+import Data.List (intersperse)+import Data.Maybe (fromMaybe, mapMaybe, fromJust)+import Data.Text qualified as T+import Data.Text.IO qualified as T+import Data.Version (showVersion)+import Data.Word (Word64)+import GHC.Conc (getNumProcessors)+import Numeric.Natural (Natural)+import Optics.Core ((&), set)+import Witch (unsafeInto)+import Options.Generic as Options+import Paths_hevm qualified as Paths+import System.IO (stderr)+import System.Directory (withCurrentDirectory, getCurrentDirectory, doesDirectoryExist)+import System.FilePath ((</>))+import System.Exit (exitFailure, exitWith, ExitCode(..))++import EVM (initialContract, abstractContract, makeVm)+import EVM.ABI (Sig(..))+import EVM.Dapp (dappInfo, DappInfo, emptyDapp)+import EVM.Expr qualified as Expr+import EVM.Concrete qualified as Concrete+import GitHash+import EVM.FeeSchedule (feeSchedule)+import EVM.Fetch qualified as Fetch+import EVM.Format (hexByteString, strip0x, showTraceTree, formatExpr)+import EVM.Solidity+import EVM.Solvers+import EVM.Stepper qualified+import EVM.SymExec+import EVM.Transaction qualified+import EVM.Types hiding (word)+import EVM.UnitTest++-- This record defines the program's command-line options+-- automatically via the `optparse-generic` package.+data Command w+  = Symbolic -- Symbolically explore an abstract program, or specialized with specified env & calldata+  -- vm opts+      { code          :: w ::: Maybe ByteString <?> "Program bytecode"+      , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"+      , address       :: w ::: Maybe Addr       <?> "Tx: address"+      , caller        :: w ::: Maybe Addr       <?> "Tx: caller"+      , origin        :: w ::: Maybe Addr       <?> "Tx: origin"+      , coinbase      :: w ::: Maybe Addr       <?> "Block: coinbase"+      , value         :: w ::: Maybe W256       <?> "Tx: Eth amount"+      , nonce         :: w ::: Maybe Word64     <?> "Nonce of origin"+      , gas           :: w ::: Maybe Word64     <?> "Tx: gas amount"+      , number        :: w ::: Maybe W256       <?> "Block: number"+      , timestamp     :: w ::: Maybe W256       <?> "Block: timestamp"+      , basefee       :: w ::: Maybe W256       <?> "Block: base fee"+      , priorityFee   :: w ::: Maybe W256       <?> "Tx: priority fee"+      , gaslimit      :: w ::: Maybe Word64     <?> "Tx: gas limit"+      , gasprice      :: w ::: Maybe W256       <?> "Tx: gas price"+      , create        :: w ::: Bool             <?> "Tx: creation"+      , maxcodesize   :: w ::: Maybe W256       <?> "Block: max code size"+      , prevRandao    :: w ::: Maybe W256       <?> "Block: prevRandao"+      , chainid       :: w ::: Maybe W256       <?> "Env: chainId"+  -- remote state opts+      , rpc           :: w ::: Maybe URL        <?> "Fetch state from a remote node"+      , block         :: w ::: Maybe W256       <?> "Block state is be fetched from"++  -- symbolic execution opts+      , root          :: w ::: Maybe String       <?> "Path to  project root directory (default: . )"+      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a Foundry or DappTools project (default: Foundry)"+      , initialStorage :: w ::: Maybe (InitialStorage) <?> "Starting state for storage: Empty, Abstract (default Abstract)"+      , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"+      , arg           :: w ::: [String]           <?> "Values to encode"+      , 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 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"+      , assertions    :: w ::: Maybe [Word256]    <?> "Comma separated list of solc panic codes to check for (default: user defined assertion violations only)"+      , askSmtIterations :: w ::: Integer         <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"+      , numSolvers    :: w ::: Maybe Natural      <?> "Number of solver instances to use (default: number of cpu cores)"+      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"+      , abstractArithmetic    :: w ::: Bool             <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"+      , abstractMemory    :: w ::: Bool                      <?> "Use abstraction-refinement for Memory. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"+      }+  | Equivalence -- prove equivalence between two programs+      { codeA         :: w ::: ByteString       <?> "Bytecode of the first program"+      , codeB         :: w ::: ByteString       <?> "Bytecode of the second program"+      , 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 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"+      , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"+      , askSmtIterations :: w ::: Integer       <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"+      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"+      , abstractArithmetic    :: w ::: Bool             <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"+      , abstractMemory    :: w ::: Bool                      <?> "Use abstraction-refinement for Memory. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"+      }+  | Exec -- Execute a given program with specified env & calldata+      { code        :: w ::: Maybe ByteString  <?> "Program bytecode"+      , calldata    :: w ::: Maybe ByteString  <?> "Tx: calldata"+      , address     :: w ::: Maybe Addr        <?> "Tx: address"+      , caller      :: w ::: Maybe Addr        <?> "Tx: caller"+      , origin      :: w ::: Maybe Addr        <?> "Tx: origin"+      , coinbase    :: w ::: Maybe Addr        <?> "Block: coinbase"+      , value       :: w ::: Maybe W256        <?> "Tx: Eth amount"+      , nonce       :: w ::: Maybe Word64      <?> "Nonce of origin"+      , gas         :: w ::: Maybe Word64      <?> "Tx: gas amount"+      , number      :: w ::: Maybe W256        <?> "Block: number"+      , timestamp   :: w ::: Maybe W256        <?> "Block: timestamp"+      , basefee     :: w ::: Maybe W256        <?> "Block: base fee"+      , priorityFee :: w ::: Maybe W256        <?> "Tx: priority fee"+      , gaslimit    :: w ::: Maybe Word64      <?> "Tx: gas limit"+      , gasprice    :: w ::: Maybe W256        <?> "Tx: gas price"+      , create      :: w ::: Bool              <?> "Tx: creation"+      , maxcodesize :: w ::: Maybe W256        <?> "Block: max code size"+      , prevRandao  :: w ::: Maybe W256        <?> "Block: prevRandao"+      , chainid     :: w ::: Maybe W256        <?> "Env: chainId"+      , trace       :: w ::: Bool              <?> "Dump trace"+      , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"+      , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"+      , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"+      , projectType :: w ::: Maybe ProjectType <?> "Is this a Foundry or DappTools project (default: Foundry)"+      }+  | Test -- Run DSTest unit tests+      { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"+      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a Foundry or DappTools project (default: Foundry)"+      , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"+      , number        :: w ::: Maybe W256               <?> "Block: number"+      , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"+      , coverage      :: w ::: Bool                     <?> "Coverage analysis"+      , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"+      , 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 seconds (default: 300)"+      , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point"+      , loopDetectionHeuristic :: w ::: LoopHeuristic   <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"+      , abstractArithmetic    :: w ::: Bool             <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"+      , abstractMemory    :: w ::: Bool                      <?> "Use abstraction-refinement for Memory. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"+      , askSmtIterations :: w ::: Integer               <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"+      }+  | Version++  deriving (Options.Generic)++type URL = Text+++-- For some reason haskell can't derive a+-- parseField instance for (Text, ByteString)+instance Options.ParseField (Text, ByteString)++deriving instance Options.ParseField Word256+deriving instance Options.ParseField [Word256]++instance Options.ParseRecord (Command Options.Wrapped) where+  parseRecord =+    Options.parseRecordWithModifiers Options.lispCaseModifiers++data InitialStorage+  = Empty+  | Abstract+  deriving (Show, Read, Options.ParseField)++getFullVersion :: [Char]+getFullVersion = showVersion Paths.version <> " [" <> gitVersion <> "]"+  where+    gitInfo = $$tGitInfoCwdTry+    gitVersion = case gitInfo of+      Right val -> "git rev " <> giBranch val <>  "@" <> giHash val+      Left _ -> "no git revision present"++main :: IO ()+main = do+  cmd <- Options.unwrapRecord "hevm -- Ethereum evaluator"+  case cmd of+    Version {} ->putStrLn getFullVersion+    Symbolic {} -> do+      root <- getRoot cmd+      withCurrentDirectory root $ assert cmd+    Equivalence {} -> equivalence cmd+    Exec {} ->+      launchExec cmd+    Test {} -> do+      root <- getRoot cmd+      withCurrentDirectory root $ do+        cores <- unsafeInto <$> getNumProcessors+        solver <- getSolver cmd+        withSolvers solver cores cmd.smttimeout $ \solvers -> do+          buildOut <- readBuildOutput root (getProjectType cmd)+          case buildOut of+            Left e -> do+              putStrLn $ "Error: " <> e+              exitFailure+            Right out -> do+              -- TODO: which functions here actually require a BuildOutput, and which can take it as a Maybe?+              testOpts <- unitTestOptions cmd solvers (Just out)+              res <- unitTest testOpts out.contracts+              unless res exitFailure++equivalence :: Command Options.Unwrapped -> IO ()+equivalence cmd = do+  let bytecodeA = hexByteString "--code" . strip0x $ cmd.codeA+      bytecodeB = hexByteString "--code" . strip0x $ cmd.codeB+      veriOpts = VeriOpts { simp = True+                          , debug = False+                          , maxIter = cmd.maxIterations+                          , askSmtIters = cmd.askSmtIterations+                          , loopHeuristic = cmd.loopDetectionHeuristic+                          , abstRefineConfig = AbstRefineConfig cmd.abstractArithmetic cmd.abstractMemory+                          , rpcInfo = Nothing+                          }+  calldata <- buildCalldata cmd+  solver <- getSolver cmd+  withSolvers solver 3 Nothing $ \s -> do+    res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata+    case any isCex res of+      False -> do+        putStrLn "No discrepancies found"+        when (any isTimeout res) $ do+          putStrLn "But timeout(s) occurred"+          exitFailure+      True -> do+        let cexs = mapMaybe getCex res+        T.putStrLn . T.unlines $+          [ "Not equivalent. The following inputs result in differing behaviours:"+          , "" , "-----", ""+          ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (formatCex (AbstractBuf "txdata") Nothing) cexs)+        exitFailure++getSolver :: Command Options.Unwrapped -> IO Solver+getSolver cmd = case cmd.solver of+                  Nothing -> pure Z3+                  Just s -> case T.unpack s of+                              "z3" -> pure Z3+                              "cvc5" -> pure CVC5+                              input -> do+                                putStrLn $ "unrecognised solver: " <> input+                                exitFailure++getSrcInfo :: Command Options.Unwrapped -> IO DappInfo+getSrcInfo cmd = do+  root <- getRoot cmd+  withCurrentDirectory root $ do+    outExists <- doesDirectoryExist (root </> "out")+    if outExists+    then do+      buildOutput <- readBuildOutput root (getProjectType cmd)+      case buildOutput of+        Left _ -> pure emptyDapp+        Right o -> pure $ dappInfo root o+    else pure emptyDapp++getProjectType :: Command Options.Unwrapped -> ProjectType+getProjectType cmd = fromMaybe Foundry cmd.projectType++getRoot :: Command Options.Unwrapped -> IO FilePath+getRoot cmd = maybe getCurrentDirectory pure (cmd.root)+++-- | Builds a buffer representing calldata based on the given cli arguments+buildCalldata :: Command Options.Unwrapped -> IO (Expr Buf, [Prop])+buildCalldata cmd = case (cmd.calldata, cmd.sig) of+  -- fully abstract calldata+  (Nothing, Nothing) -> pure $ mkCalldata Nothing []+  -- fully concrete calldata+  (Just c, Nothing) -> pure (ConcreteBuf (hexByteString "bytes" . strip0x $ c), [])+  -- calldata according to given abi with possible specializations from the `arg` list+  (Nothing, Just sig') -> do+    method' <- functionAbi sig'+    pure $ mkCalldata (Just (Sig method'.methodSignature (snd <$> method'.inputs))) cmd.arg+  -- both args provided+  (_, _) -> do+    putStrLn "incompatible options provided: --calldata and --sig"+    exitFailure+++-- If function signatures are known, they should always be given for best results.+assert :: Command Options.Unwrapped -> IO ()+assert cmd = do+  let block'  = maybe Fetch.Latest Fetch.BlockNumber cmd.block+      rpcinfo = (,) block' <$> cmd.rpc+  calldata <- buildCalldata cmd+  preState <- symvmFromCommand cmd calldata+  let errCodes = fromMaybe defaultPanicCodes cmd.assertions+  cores <- unsafeInto <$> getNumProcessors+  let solverCount = fromMaybe cores cmd.numSolvers+  solver <- getSolver cmd+  withSolvers solver solverCount cmd.smttimeout $ \solvers -> do+    let opts = VeriOpts { simp = True+                        , debug = cmd.smtdebug+                        , maxIter = cmd.maxIterations+                        , askSmtIters = cmd.askSmtIterations+                        , loopHeuristic = cmd.loopDetectionHeuristic+                        , abstRefineConfig = AbstRefineConfig cmd.abstractArithmetic cmd.abstractMemory+                        , rpcInfo = rpcinfo+    }+    (expr, res) <- verify solvers opts preState (Just $ checkAssertions errCodes)+    case res of+      [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+            counterexamples+              | null cexs = []+              | otherwise =+                 [ ""+                 , "Discovered the following counterexamples:"+                 , ""+                 ] <> fmap (formatCex (fst calldata) Nothing) cexs+            unknowns+              | null timeouts = []+              | otherwise =+                 [ ""+                 , "Could not determine reachability of the following end states:"+                 , ""+                 ] <> fmap (formatExpr) timeouts+        T.putStrLn $ T.unlines (counterexamples <> unknowns)+        showExtras solvers cmd calldata expr+        exitFailure++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))++isTestOrLib :: Text -> Bool+isTestOrLib file = T.isSuffixOf ".t.sol" file || areAnyPrefixOf ["src/test/", "src/tests/", "lib/"] file++areAnyPrefixOf :: [Text] -> Text -> Bool+areAnyPrefixOf prefixes t = any (flip T.isPrefixOf t) prefixes++launchExec :: Command Options.Unwrapped -> IO ()+launchExec cmd = do+  dapp <- getSrcInfo cmd+  vm <- vmFromCommand cmd+  let+    block = maybe Fetch.Latest Fetch.BlockNumber cmd.block+    rpcinfo = (,) block <$> cmd.rpc++  -- TODO: we shouldn't need solvers to execute this code+  withSolvers Z3 0 Nothing $ \solvers -> do+    vm' <- EVM.Stepper.interpret (Fetch.oracle solvers rpcinfo) vm EVM.Stepper.runFully+    when cmd.trace $ T.hPutStr stderr (showTraceTree dapp vm')+    case vm'.result of+      Just (VMFailure (Revert msg)) -> do+        let res = case msg of+                    ConcreteBuf bs -> bs+                    _ -> "<symbolic>"+        putStrLn $ "Revert: " <> (show $ ByteStringS res)+        exitWith (ExitFailure 2)+      Just (VMFailure err) -> do+        putStrLn $ "Error: " <> show err+        exitWith (ExitFailure 2)+      Just (Unfinished p) -> do+        putStrLn $ "Could not continue execution: " <> show p+        exitWith (ExitFailure 2)+      Just (VMSuccess buf) -> do+        let msg = case buf of+              ConcreteBuf msg' -> msg'+              _ -> "<symbolic>"+        print $ "Return: " <> (show $ ByteStringS msg)+      _ ->+        internalError "no EVM result"++-- | Creates a (concrete) VM from command line options+vmFromCommand :: Command Options.Unwrapped -> IO (VM RealWorld)+vmFromCommand cmd = do+  (miner,ts,baseFee,blockNum,prevRan) <- case cmd.rpc of+    Nothing -> pure (LitAddr 0,Lit 0,0,0,0)+    Just url -> Fetch.fetchBlockFrom block url >>= \case+      Nothing -> error "Error: Could not fetch block"+      Just Block{..} -> pure ( coinbase+                             , timestamp+                             , baseFee+                             , number+                             , prevRandao+                             )++  contract <- case (cmd.rpc, cmd.address, cmd.code) of+    (Just url, Just addr', Just c) -> do+      Fetch.fetchContractFrom block url addr' >>= \case+        Nothing ->+          error $ "Error: contract not found: " <> show address+        Just contract ->+          -- if both code and url is given,+          -- fetch the contract and overwrite the code+          pure $+            initialContract  (mkCode $ hexByteString "--code" $ strip0x c)+              & set #balance  (contract.balance)+              & set #nonce    (contract.nonce)+              & set #external (contract.external)++    (Just url, Just addr', Nothing) ->+      Fetch.fetchContractFrom block url addr' >>= \case+        Nothing ->+          error $ "Error: contract not found: " <> show address+        Just contract -> pure contract++    (_, _, Just c)  ->+      pure $+        initialContract (mkCode $ hexByteString "--code" $ strip0x c)++    (_, _, Nothing) ->+      error "Error: must provide at least (rpc + address) or code"++  let ts' = case maybeLitWord ts of+        Just t -> t+        Nothing -> internalError "unexpected symbolic timestamp when executing vm test"++  vm <- stToIO $ vm0 baseFee miner ts' blockNum prevRan contract+  pure $ EVM.Transaction.initTx vm+    where+        block   = maybe Fetch.Latest Fetch.BlockNumber cmd.block+        value   = word (.value) 0+        caller  = addr (.caller) (LitAddr 0)+        origin  = addr (.origin) (LitAddr 0)+        calldata = ConcreteBuf $ bytes (.calldata) ""+        decipher = hexByteString "bytes" . strip0x+        mkCode bs = if cmd.create+                    then InitCode bs mempty+                    else RuntimeCode (ConcreteRuntimeCode bs)+        address = if cmd.create+                  then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddr origin) (W64 $ word64 (.nonce) 0))+                  else addr (.address) (LitAddr 0xacab)++        vm0 baseFee miner ts blockNum prevRan c = makeVm $ VMOpts+          { contract       = c+          , otherContracts = []+          , calldata       = (calldata, [])+          , value          = Lit value+          , address        = address+          , caller         = 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+          , chainId        = word (.chainid) 1+          , create         = (.create) cmd+          , baseState      = EmptyBase+          , txAccessList   = mempty -- TODO: support me soon+          , allowFFI       = False+          }+        word f def = fromMaybe def (f cmd)+        word64 f def = fromMaybe def (f cmd)+        addr f def = maybe def LitAddr (f cmd)+        bytes f def = maybe def decipher (f cmd)++symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM RealWorld)+symvmFromCommand cmd calldata = do+  (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of+    Nothing -> pure (SymAddr "miner",0,0,0)+    Just url -> Fetch.fetchBlockFrom block url >>= \case+      Nothing -> error "Error: Could not fetch block"+      Just Block{..} -> pure ( coinbase+                             , number+                             , baseFee+                             , prevRandao+                             )++  let+    caller = SymAddr "caller"+    ts = maybe Timestamp Lit cmd.timestamp+    callvalue = maybe TxValue Lit cmd.value++  contract <- case (cmd.rpc, cmd.address, cmd.code) of+    (Just url, Just addr', _) ->+      Fetch.fetchContractFrom block url addr' >>= \case+        Nothing ->+          error "Error: contract not found."+        Just contract' -> pure contract''+          where+            contract'' = case cmd.code of+              Nothing -> contract'+              -- if both code and url is given,+              -- fetch the contract and overwrite the code+              Just c -> initialContract (mkCode $ decipher c)+                        & set #origStorage (contract'.origStorage)+                        & set #balance     (contract'.balance)+                        & set #nonce       (contract'.nonce)+                        & set #external    (contract'.external)++    (_, _, Just c)  ->+      pure ((`abstractContract` address) . mkCode $ decipher c)+    (_, _, Nothing) ->+      error "Error: must provide at least (rpc + address) or code"++  vm <- stToIO $ vm0 baseFee miner ts blockNum prevRan calldata callvalue caller contract+  pure $ EVM.Transaction.initTx vm++  where+    decipher = hexByteString "bytes" . strip0x+    block = maybe Fetch.Latest Fetch.BlockNumber cmd.block+    origin = eaddr (.origin) (SymAddr "origin")+    mkCode bs = if cmd.create+                   then InitCode bs mempty+                   else RuntimeCode (ConcreteRuntimeCode bs)+    address = eaddr (.address) (SymAddr "entrypoint")+    vm0 baseFee miner ts blockNum prevRan cd callvalue caller c = makeVm $ VMOpts+      { contract       = c+      , otherContracts = []+      , 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       = eaddr (.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+      , chainId        = word (.chainid) 1+      , create         = (.create) cmd+      , baseState      = maybe AbstractBase parseInitialStorage (cmd.initialStorage)+      , txAccessList   = mempty+      , allowFFI       = False+      }+    word f def = fromMaybe def (f cmd)+    word64 f def = fromMaybe def (f cmd)+    eaddr f def = maybe def LitAddr (f cmd)++unitTestOptions :: Command Options.Unwrapped -> SolverGroup -> Maybe BuildOutput -> IO (UnitTestOptions RealWorld)+unitTestOptions cmd solvers buildOutput = do+  root <- getRoot cmd+  let srcInfo = maybe emptyDapp (dappInfo root) buildOutput++  let rpcinfo = case (cmd.number, cmd.rpc) of+          (Just block, Just url) -> Just (Fetch.BlockNumber block, url)+          (Nothing, Just url) -> Just (Fetch.Latest, url)+          _ -> Nothing+  params <- paramsFromRpc rpcinfo++  let+    testn = params.number+    block' = if 0 == testn+       then Fetch.Latest+       else Fetch.BlockNumber testn++  pure UnitTestOptions+    { solvers = solvers+    , rpcInfo = case cmd.rpc of+         Just url -> Just (block', url)+         Nothing  -> Nothing+    , maxIter = cmd.maxIterations+    , askSmtIters = cmd.askSmtIterations+    , smtDebug = cmd.smtdebug+    , smtTimeout = cmd.smttimeout+    , solver = cmd.solver+    , verbose = cmd.verbose+    , match = T.pack $ fromMaybe ".*" cmd.match+    , testParams = params+    , dapp = srcInfo+    , ffiAllowed = cmd.ffi+    }+parseInitialStorage :: InitialStorage -> BaseState+parseInitialStorage Empty = EmptyBase+parseInitialStorage Abstract = AbstractBase

@@ -1,716 +0,0 @@--- Main file of the hevm CLI program--{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveAnyClass #-}-{-# LANGUAGE TemplateHaskell #-}--module Main where--import Control.Monad (void, when, forM_, unless)-import Control.Monad.State.Strict (liftIO)-import Data.Bifunctor (second)-import Data.ByteString (ByteString)-import Data.ByteString qualified as ByteString-import Data.ByteString.Char8 qualified as Char8-import Data.ByteString.Lazy qualified as LazyByteString-import Data.DoubleWord (Word256)-import Data.List (intersperse)-import Data.Map qualified as Map-import Data.Maybe (fromMaybe, mapMaybe)-import Data.Text (pack)-import Data.Text qualified as T-import Data.Text.IO qualified as T-import Data.Version (showVersion)-import Data.Word (Word64)-import GHC.Conc (getNumProcessors)-import Numeric.Natural (Natural)-import Optics.Core ((&), (%), set)-import Witch (unsafeInto)-import Options.Generic as Options-import Paths_hevm qualified as Paths-import System.IO (stderr)-import System.Directory (withCurrentDirectory, getCurrentDirectory, doesDirectoryExist)-import System.FilePath ((</>))-import System.Exit (exitFailure, exitWith, ExitCode(..))--import EVM (initialContract, makeVm)-import EVM.Concrete (createAddress)-import EVM.Dapp (findUnitTests, dappInfo, DappInfo, emptyDapp)-import EVM.Debug (Mode(..))-import EVM.Expr qualified as Expr-import EVM.Facts qualified as Facts-import EVM.Facts.Git qualified as Git-import GitHash-import EVM.FeeSchedule qualified as FeeSchedule-import EVM.Fetch qualified-import EVM.Format (hexByteString, strip0x, showTraceTree, formatExpr)-import EVM.Solidity-import EVM.Solvers-import EVM.Stepper qualified-import EVM.SymExec-import EVM.Transaction qualified-import EVM.TTY qualified as TTY-import EVM.Types hiding (word)-import EVM.UnitTest---- This record defines the program's command-line options--- automatically via the `optparse-generic` package.-data Command w-  = Symbolic -- Symbolically explore an abstract program, or specialized with specified env & calldata-  -- vm opts-      { code          :: w ::: Maybe ByteString <?> "Program bytecode"-      , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"-      , address       :: w ::: Maybe Addr       <?> "Tx: address"-      , caller        :: w ::: Maybe Addr       <?> "Tx: caller"-      , origin        :: w ::: Maybe Addr       <?> "Tx: origin"-      , coinbase      :: w ::: Maybe Addr       <?> "Block: coinbase"-      , value         :: w ::: Maybe W256       <?> "Tx: Eth amount"-      , nonce         :: w ::: Maybe W256       <?> "Nonce of origin"-      , gas           :: w ::: Maybe Word64     <?> "Tx: gas amount"-      , number        :: w ::: Maybe W256       <?> "Block: number"-      , timestamp     :: w ::: Maybe W256       <?> "Block: timestamp"-      , basefee       :: w ::: Maybe W256       <?> "Block: base fee"-      , priorityFee   :: w ::: Maybe W256       <?> "Tx: priority fee"-      , gaslimit      :: w ::: Maybe Word64     <?> "Tx: gas limit"-      , gasprice      :: w ::: Maybe W256       <?> "Tx: gas price"-      , create        :: w ::: Bool             <?> "Tx: creation"-      , maxcodesize   :: w ::: Maybe W256       <?> "Block: max code size"-      , prevRandao    :: w ::: Maybe W256       <?> "Block: prevRandao"-      , chainid       :: w ::: Maybe W256       <?> "Env: chainId"-  -- remote state opts-      , rpc           :: w ::: Maybe URL        <?> "Fetch state from a remote node"-      , block         :: w ::: Maybe W256       <?> "Block state is be fetched from"-      , state         :: w ::: Maybe String     <?> "Path to state repository"-      , cache         :: w ::: Maybe String     <?> "Path to rpc cache repository"--  -- symbolic execution opts-      , root          :: w ::: Maybe String       <?> "Path to  project root directory (default: . )"-      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a Foundry or DappTools project (default: Foundry)"-      , 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 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"-      , assertions    :: w ::: Maybe [Word256]    <?> "Comma seperated list of solc panic codes to check for (default: everything except arithmetic overflow)"-      , askSmtIterations :: w ::: Integer         <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"-      , numSolvers    :: w ::: Maybe Natural      <?> "Number of solver instances to use (default: number of cpu cores)"-      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"-      }-  | Equivalence -- prove equivalence between two programs-      { codeA         :: w ::: ByteString       <?> "Bytecode of the first program"-      , codeB         :: w ::: ByteString       <?> "Bytecode of the second program"-      , 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 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"-      , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"-      , askSmtIterations :: w ::: Integer       <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"-      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"-      }-  | Exec -- Execute a given program with specified env & calldata-      { code        :: w ::: Maybe ByteString  <?> "Program bytecode"-      , calldata    :: w ::: Maybe ByteString  <?> "Tx: calldata"-      , address     :: w ::: Maybe Addr        <?> "Tx: address"-      , caller      :: w ::: Maybe Addr        <?> "Tx: caller"-      , origin      :: w ::: Maybe Addr        <?> "Tx: origin"-      , coinbase    :: w ::: Maybe Addr        <?> "Block: coinbase"-      , value       :: w ::: Maybe W256        <?> "Tx: Eth amount"-      , nonce       :: w ::: Maybe W256        <?> "Nonce of origin"-      , gas         :: w ::: Maybe Word64      <?> "Tx: gas amount"-      , number      :: w ::: Maybe W256        <?> "Block: number"-      , timestamp   :: w ::: Maybe W256        <?> "Block: timestamp"-      , basefee     :: w ::: Maybe W256        <?> "Block: base fee"-      , priorityFee :: w ::: Maybe W256        <?> "Tx: priority fee"-      , gaslimit    :: w ::: Maybe Word64      <?> "Tx: gas limit"-      , gasprice    :: w ::: Maybe W256        <?> "Tx: gas price"-      , create      :: w ::: Bool              <?> "Tx: creation"-      , maxcodesize :: w ::: Maybe W256        <?> "Block: max code size"-      , prevRandao  :: w ::: Maybe W256        <?> "Block: prevRandao"-      , chainid     :: w ::: Maybe W256        <?> "Env: chainId"-      , debug       :: w ::: Bool              <?> "Run interactively"-      , jsontrace   :: w ::: Bool              <?> "Print json trace output at every step"-      , trace       :: w ::: Bool              <?> "Dump trace"-      , state       :: w ::: Maybe String      <?> "Path to state repository"-      , cache       :: w ::: Maybe String      <?> "Path to rpc cache repository"-      , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"-      , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"-      , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"-      , projectType :: w ::: Maybe ProjectType <?> "Is this a Foundry or DappTools project (default: Foundry)"-      }-  | Test -- Run DSTest unit tests-      { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"-      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a Foundry or DappTools project (default: Foundry)"-      , debug         :: w ::: Bool                     <?> "Run interactively"-      , jsontrace     :: w ::: Bool                     <?> "Print json trace output at every step"-      , fuzzRuns      :: w ::: Maybe Int                <?> "Number of times to run fuzz tests"-      , depth         :: w ::: Maybe Int                <?> "Number of transactions to explore"-      , replay        :: w ::: Maybe (Text, ByteString) <?> "Custom fuzz case to run/debug"-      , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"-      , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"-      , coverage      :: w ::: Bool                     <?> "Coverage analysis"-      , state         :: w ::: Maybe String             <?> "Path to state repository"-      , cache         :: w ::: Maybe String             <?> "Path to rpc cache repository"-      , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"-      , covMatch      :: w ::: Maybe String             <?> "Coverage filter - only print coverage for files matching regex"-      , 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 seconds (default: 300)"-      , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point"-      , loopDetectionHeuristic :: w ::: LoopHeuristic   <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"-      , askSmtIterations :: w ::: Integer               <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"-      }-  | Version--  deriving (Options.Generic)--type URL = Text----- For some reason haskell can't derive a--- parseField instance for (Text, ByteString)-instance Options.ParseField (Text, ByteString)--deriving instance Options.ParseField Word256-deriving instance Options.ParseField [Word256]--instance Options.ParseRecord (Command Options.Wrapped) where-  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-  | x.jsontrace = JsonTrace-  | otherwise = Run--applyCache :: (Maybe String, Maybe String) -> IO (VM -> VM)-applyCache (state, cache) =-  let applyState = flip Facts.apply-      applyCache' = flip Facts.applyCache-  in case (state, cache) of-    (Nothing, Nothing) -> do-      pure id-    (Nothing, Just cachePath) -> do-      facts <- Git.loadFacts (Git.RepoAt cachePath)-      pure $ applyCache' facts-    (Just statePath, Nothing) -> do-      facts <- Git.loadFacts (Git.RepoAt statePath)-      pure $ applyState facts-    (Just statePath, Just cachePath) -> do-      cacheFacts <- Git.loadFacts (Git.RepoAt cachePath)-      stateFacts <- Git.loadFacts (Git.RepoAt statePath)-      pure $ (applyState stateFacts) . (applyCache' cacheFacts)--unitTestOptions :: Command Options.Unwrapped -> SolverGroup -> Maybe BuildOutput -> IO UnitTestOptions-unitTestOptions cmd solvers buildOutput = do-  root <- getRoot cmd-  let srcInfo = maybe emptyDapp (dappInfo root) buildOutput--  vmModifier <- applyCache (cmd.state, cmd.cache)--  params <- getParametersFromEnvironmentVariables cmd.rpc--  let-    testn = params.number-    block' = if 0 == testn-       then EVM.Fetch.Latest-       else EVM.Fetch.BlockNumber testn--  pure UnitTestOptions-    { solvers = solvers-    , rpcInfo = case cmd.rpc of-         Just url -> Just (block', url)-         Nothing  -> Nothing-    , maxIter = cmd.maxIterations-    , askSmtIters = cmd.askSmtIterations-    , smtDebug = cmd.smtdebug-    , smtTimeout = cmd.smttimeout-    , solver = cmd.solver-    , covMatch = pack <$> cmd.covMatch-    , verbose = cmd.verbose-    , match = pack $ fromMaybe ".*" cmd.match-    , maxDepth = cmd.depth-    , fuzzRuns = fromMaybe 100 cmd.fuzzRuns-    , replay = do-        arg' <- cmd.replay-        pure (fst arg', LazyByteString.fromStrict (hexByteString "--replay" $ strip0x $ snd arg'))-    , vmModifier = vmModifier-    , testParams = params-    , dapp = srcInfo-    , ffiAllowed = cmd.ffi-    }--getFullVersion :: [Char]-getFullVersion = showVersion Paths.version <> " [" <> gitVersion <> "]"-  where-    gitInfo = $$tGitInfoCwdTry-    gitVersion = case gitInfo of-      Right val -> "git rev " <> giBranch val <>  "@" <> giHash val-      Left _ -> "no git revision present"--main :: IO ()-main = do-  cmd <- Options.unwrapRecord "hevm -- Ethereum evaluator"-  case cmd of-    Version {} ->putStrLn getFullVersion-    Symbolic {} -> do-      root <- getRoot cmd-      withCurrentDirectory root $ assert cmd-    Equivalence {} -> equivalence cmd-    Exec {} ->-      launchExec cmd-    Test {} -> do-      root <- getRoot cmd-      withCurrentDirectory root $ do-        cores <- unsafeInto <$> getNumProcessors-        solver <- getSolver cmd-        withSolvers solver cores cmd.smttimeout $ \solvers -> do-          buildOut <- readBuildOutput root (getProjectType cmd)-          case buildOut of-            Left e -> do-              putStrLn $ "Error: " <> e-              exitFailure-            Right out -> do-              -- TODO: which functions here actually require a BuildOutput, and which can take it as a Maybe?-              testOpts <- unitTestOptions cmd solvers (Just out)-              case (cmd.coverage, optsMode cmd) of-                (False, Run) -> do-                  res <- unitTest testOpts out.contracts cmd.cache-                  unless res exitFailure-                (False, Debug) -> liftIO $ TTY.main testOpts root (Just out)-                (False, JsonTrace) -> internalError "json traces not implemented for dappTest"-                (True, _) -> liftIO $ dappCoverage testOpts (optsMode cmd) out---equivalence :: Command Options.Unwrapped -> IO ()-equivalence cmd = do-  let bytecodeA = hexByteString "--code" . strip0x $ cmd.codeA-      bytecodeB = hexByteString "--code" . strip0x $ cmd.codeB-      veriOpts = VeriOpts { simp = True-                          , debug = False-                          , maxIter = cmd.maxIterations-                          , askSmtIters = cmd.askSmtIterations-                          , loopHeuristic = cmd.loopDetectionHeuristic-                          , rpcInfo = Nothing-                          }-  calldata <- buildCalldata cmd-  solver <- getSolver cmd-  withSolvers solver 3 Nothing $ \s -> do-    res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata-    case any isCex res of-      False -> do-        putStrLn "No discrepancies found"-        when (any isTimeout res) $ do-          putStrLn "But timeout(s) occurred"-          exitFailure-      True -> do-        let cexs = mapMaybe getCex res-        T.putStrLn . T.unlines $-          [ "Not equivalent. The following inputs result in differing behaviours:"-          , "" , "-----", ""-          ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (formatCex (AbstractBuf "txdata")) cexs)-        exitFailure--getSolver :: Command Options.Unwrapped -> IO Solver-getSolver cmd = case cmd.solver of-                  Nothing -> pure Z3-                  Just s -> case T.unpack s of-                              "z3" -> pure Z3-                              "cvc5" -> pure CVC5-                              input -> do-                                putStrLn $ "unrecognised solver: " <> input-                                exitFailure--getSrcInfo :: Command Options.Unwrapped -> IO DappInfo-getSrcInfo cmd = do-  root <- getRoot cmd-  withCurrentDirectory root $ do-    outExists <- doesDirectoryExist (root </> "out")-    if outExists-    then do-      buildOutput <- readBuildOutput root (getProjectType cmd)-      case buildOutput of-        Left _ -> pure emptyDapp-        Right o -> pure $ dappInfo root o-    else pure emptyDapp--getProjectType :: Command Options.Unwrapped -> ProjectType-getProjectType cmd = fromMaybe Foundry cmd.projectType--getRoot :: Command Options.Unwrapped -> IO FilePath-getRoot cmd = maybe getCurrentDirectory pure (cmd.root)----- | Builds a buffer representing calldata based on the given cli arguments-buildCalldata :: Command Options.Unwrapped -> IO (Expr Buf, [Prop])-buildCalldata cmd = case (cmd.calldata, cmd.sig) of-  -- fully abstract calldata-  (Nothing, Nothing) -> pure $ mkCalldata Nothing []-  -- fully concrete calldata-  (Just c, Nothing) -> pure (ConcreteBuf (hexByteString "bytes" . strip0x $ c), [])-  -- calldata according to given abi with possible specializations from the `arg` list-  (Nothing, Just sig') -> do-    method' <- functionAbi sig'-    pure $ mkCalldata (Just (Sig method'.methodSignature (snd <$> method'.inputs))) cmd.arg-  -- both args provided-  (_, _) -> do-    putStrLn "incompatible options provided: --calldata and --sig"-    exitFailure----- If function signatures are known, they should always be given for best results.-assert :: Command Options.Unwrapped -> IO ()-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-  let errCodes = fromMaybe defaultPanicCodes cmd.assertions-  cores <- unsafeInto <$> getNumProcessors-  let solverCount = fromMaybe cores cmd.numSolvers-  solver <- getSolver cmd-  withSolvers solver solverCount cmd.smttimeout $ \solvers -> do-    if cmd.debug then do-      srcInfo <- getSrcInfo cmd-      void $ TTY.runFromVM-        solvers-        rpcinfo-        cmd.maxIterations-        srcInfo-        preState-    else do-      let opts = VeriOpts {-        simp = True,-        debug = cmd.smtdebug,-        maxIter = cmd.maxIterations,-        askSmtIters = cmd.askSmtIterations,-        loopHeuristic = cmd.loopDetectionHeuristic,-        rpcInfo = rpcinfo-      }-      (expr, res) <- verify solvers opts preState (Just $ checkAssertions errCodes)-      case res of-        [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-              counterexamples-                | null cexs = []-                | otherwise =-                   [ ""-                   , "Discovered the following counterexamples:"-                   , ""-                   ] <> fmap (formatCex (fst calldata)) cexs-              unknowns-                | null timeouts = []-                | otherwise =-                   [ ""-                   , "Could not determine reachability of the following end states:"-                   , ""-                   ] <> fmap (formatExpr) timeouts-          T.putStrLn $ T.unlines (counterexamples <> unknowns)-          showExtras solvers cmd calldata expr-          exitFailure--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--getTimeout :: ProofResult a b c -> Maybe c-getTimeout (Timeout c) = Just c-getTimeout _ = Nothing--dappCoverage :: UnitTestOptions -> Mode -> BuildOutput -> IO ()-dappCoverage opts _ bo@(BuildOutput (Contracts cs) cache) = do-  let unitTests = findUnitTests opts.match $ Map.elems cs-  covs <- mconcat <$> mapM-    (coverageForUnitTestContract opts cs cache) unitTests-  let-    dapp = dappInfo "." bo-    f (k, vs) = do-      when (shouldPrintCoverage opts.covMatch (T.pack k)) $ do-        putStr ("\x1b[0m" ++ "————— hevm coverage for ") -- Prefixed with color reset-        putStrLn (k ++ " —————")-        putStrLn ""-        forM_ vs $ \(n, bs) -> do-          case ByteString.find (\x -> x /= 0x9 && x /= 0x20 && x /= 0x7d) bs of-            Nothing -> putStr "\x1b[38;5;240m" -- Gray (Coverage status isn't relevant)-            Just _ ->-              case n of-                -1 -> putStr "\x1b[38;5;240m" -- Gray (Coverage status isn't relevant)-                0  -> putStr "\x1b[31m" -- Red (Uncovered)-                _  -> putStr "\x1b[32m" -- Green (Covered)-          Char8.putStrLn bs-        putStrLn ""-  mapM_ f (Map.toList (coverageReport dapp covs))--shouldPrintCoverage :: Maybe Text -> Text -> Bool-shouldPrintCoverage (Just covMatch) file = regexMatches covMatch file-shouldPrintCoverage Nothing file = not (isTestOrLib file)--isTestOrLib :: Text -> Bool-isTestOrLib file = T.isSuffixOf ".t.sol" file || areAnyPrefixOf ["src/test/", "src/tests/", "lib/"] file--areAnyPrefixOf :: [Text] -> Text -> Bool-areAnyPrefixOf prefixes t = any (flip T.isPrefixOf t) prefixes--launchExec :: Command Options.Unwrapped -> IO ()-launchExec cmd = do-  dapp <- getSrcInfo cmd-  vm <- vmFromCommand cmd-  -- TODO: we shouldn't need solvers to execute this code-  withSolvers Z3 0 Nothing $ \solvers -> do-    case optsMode cmd of-      Run -> do-        vm' <- EVM.Stepper.interpret (EVM.Fetch.oracle solvers rpcinfo) vm EVM.Stepper.runFully-        when cmd.trace $ T.hPutStr stderr (showTraceTree dapp vm')-        case vm'.result of-          Just (VMFailure (Revert msg)) -> do-            let res = case msg of-                        ConcreteBuf bs -> bs-                        _ -> "<symbolic>"-            putStrLn $ "Revert: " <> (show $ ByteStringS res)-            exitWith (ExitFailure 2)-          Just (VMFailure err) -> do-            putStrLn $ "Error: " <> show err-            exitWith (ExitFailure 2)-          Just (Unfinished p) -> do-            putStrLn $ "Could not continue execution: " <> show p-            exitWith (ExitFailure 2)-          Just (VMSuccess buf) -> do-            let msg = case buf of-                  ConcreteBuf msg' -> msg'-                  _ -> "<symbolic>"-            print $ "Return: " <> (show $ ByteStringS msg)-            case cmd.state of-              Nothing -> pure ()-              Just path ->-                Git.saveFacts (Git.RepoAt path) (Facts.vmFacts vm')-            case cmd.cache of-              Nothing -> pure ()-              Just path ->-                Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts vm'.cache)-          _ ->-            internalError "no EVM result"--      Debug -> void $ TTY.runFromVM solvers rpcinfo Nothing dapp vm-      --JsonTrace -> void $ execStateT (interpretWithTrace fetcher EVM.Stepper.runFully) vm-      _ -> internalError "TODO"-     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 VM-vmFromCommand cmd = do-  withCache <- applyCache (cmd.state, cmd.cache)--  (miner,ts,baseFee,blockNum,prevRan) <- case cmd.rpc of-    Nothing -> pure (0,Lit 0,0,0,0)-    Just url -> EVM.Fetch.fetchBlockFrom block url >>= \case-      Nothing -> error "Error: Could not fetch block"-      Just Block{..} -> pure ( coinbase-                             , timestamp-                             , baseFee-                             , number-                             , prevRandao-                             )--  contract <- case (cmd.rpc, cmd.address, cmd.code) of-    (Just url, Just addr', Just c) -> do-      EVM.Fetch.fetchContractFrom block url addr' >>= \case-        Nothing ->-          error $ "Error: contract not found: " <> show address-        Just contract ->-          -- if both code and url is given,-          -- fetch the contract and overwrite the code-          pure $-            initialContract  (mkCode $ hexByteString "--code" $ strip0x c)-              & set #balance  (contract.balance)-              & set #nonce    (contract.nonce)-              & set #external (contract.external)--    (Just url, Just addr', Nothing) ->-      EVM.Fetch.fetchContractFrom block url addr' >>= \case-        Nothing ->-          error $ "Error: contract not found: " <> show address-        Just contract -> pure contract--    (_, _, Just c)  ->-      pure $-        initialContract (mkCode $ hexByteString "--code" $ strip0x c)--    (_, _, Nothing) ->-      error "Error: must provide at least (rpc + address) or code"--  let ts' = case maybeLitWord ts of-        Just t -> t-        Nothing -> internalError "unexpected symbolic timestamp when executing vm test"--  pure $ EVM.Transaction.initTx $ withCache (vm0 baseFee miner ts' blockNum prevRan contract)-    where-        block   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block-        value   = word (.value) 0-        caller  = addr (.caller) 0-        origin  = addr (.origin) 0-        calldata = ConcreteBuf $ bytes (.calldata) ""-        decipher = hexByteString "bytes" . strip0x-        mkCode bs = if cmd.create-                    then InitCode bs mempty-                    else RuntimeCode (ConcreteRuntimeCode bs)-        address = if cmd.create-              then addr (.address) (createAddress origin (word (.nonce) 0))-              else addr (.address) 0xacab--        vm0 baseFee miner ts blockNum prevRan c = makeVm $ VMOpts-          { contract      = c-          , calldata      = (calldata, [])-          , value         = Lit value-          , address       = address-          , caller        = Expr.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)-        addr f def = fromMaybe def (f cmd)-        bytes f def = maybe def decipher (f cmd)--symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM)-symvmFromCommand cmd calldata = do-  (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of-    Nothing -> pure (0,0,0,0)-    Just url -> EVM.Fetch.fetchBlockFrom block url >>= \case-      Nothing -> error "Error: Could not fetch block"-      Just Block{..} -> pure ( coinbase-                             , number-                             , baseFee-                             , prevRandao-                             )--  let-    caller = Caller 0-    ts = maybe Timestamp Lit cmd.timestamp-    callvalue = maybe (CallValue 0) Lit cmd.value-  -- TODO: rework this, ConcreteS not needed anymore-  let store = maybe AbstractStore parseInitialStorage (cmd.initialStorage)-  withCache <- applyCache (cmd.state, cmd.cache)--  contract <- case (cmd.rpc, cmd.address, cmd.code) of-    (Just url, Just addr', _) ->-      EVM.Fetch.fetchContractFrom block url addr' >>= \case-        Nothing ->-          error "Error: contract not found."-        Just contract' -> pure contract''-          where-            contract'' = case cmd.code of-              Nothing -> contract'-              -- if both code and url is given,-              -- fetch the contract and overwrite the code-              Just c -> initialContract (mkCode $ decipher c)-                        -- TODO: fix this-                        -- & set EVM.origStorage (view EVM.origStorage contract')-                        & set #balance     (contract'.balance)-                        & set #nonce       (contract'.nonce)-                        & set #external    (contract'.external)--    (_, _, Just c)  ->-      pure (initialContract . mkCode $ decipher c)-    (_, _, Nothing) ->-      error "Error: must provide at least (rpc + address) or code"--  pure $ (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-    mkCode bs = if cmd.create-                   then InitCode bs mempty-                   else RuntimeCode (ConcreteRuntimeCode bs)-    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 = makeVm $ 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,44 +2,24 @@ name:   hevm version:-  0.51.3+  0.52.0 synopsis:-  Ethereum virtual machine evaluator-description:-  Hevm implements the Ethereum virtual machine semantics.-  .-  It can be used as a library, and it also comes with an executable-  that can run unit test suites, optionally with a visual TTY debugger.+  Symbolic EVM Evaluator homepage:-  https://github.com/dapphub/dapptools+  https://github.com/ethereum/hevm license:   AGPL-3.0-only author:-  Mikael Brockman, Martin Lundfall, dxo+  dxo, Martin Lundfall, Mikael Brockman maintainer:-  mikael@brockman.se, martin.lundfall@gmail.com, git@d-xo.org+  git@d-xo.org category:   Ethereum build-type:   Simple extra-source-files:   CHANGELOG.md-  bench/contracts/erc20.sol-  test/contracts/lib/test.sol-  test/contracts/lib/erc20.sol-  test/contracts/pass/trivial.sol-  test/contracts/pass/abstract.sol-  test/contracts/pass/cheatCodes.sol-  test/contracts/pass/constantinople.sol-  test/contracts/pass/dsProvePass.sol-  test/contracts/pass/invariants.sol-  test/contracts/pass/libraries.sol-  test/contracts/pass/loops.sol-  test/contracts/pass/rpc.sol-  test/contracts/fail/trivial.sol-  test/contracts/fail/cheatCodes.sol-  test/contracts/fail/dsProveFail.sol-  test/contracts/fail/invariantFail.sol+  bench/contracts/*.sol   test/scripts/convert_trace_to_json.sh  flag ci@@ -78,6 +58,7 @@     -Wno-unticked-promoted-constructors     -Wno-orphans     -Wno-ambiguous-fields+    -optc-Wno-ignored-attributes   default-language: GHC2021   default-extensions:     DuplicateRecordFields@@ -89,6 +70,7 @@     RecordWildCards     TypeFamilies     ViewPatterns+    DataKinds  library   import: shared@@ -98,25 +80,18 @@     EVM.Assembler,     EVM.Concrete,     EVM.Dapp,-    EVM.Debug,-    EVM.Dev,     EVM.Expr,     EVM.SMT,     EVM.Solvers,     EVM.Exec,-    EVM.Facts,-    EVM.Facts.Git,     EVM.Format,     EVM.Fetch,     EVM.FeeSchedule,-    EVM.Hexdump,     EVM.Op,-    EVM.Patricia,     EVM.Precompiled,     EVM.RLP,     EVM.Solidity,     EVM.Stepper,-    EVM.StorageLayout,     EVM.SymExec,     EVM.Traversals,     EVM.CSE,@@ -125,16 +100,21 @@     EVM.Types,     EVM.UnitTest,     EVM.Sign,-  if !os(windows)-    exposed-modules:-      EVM.TTY,-      EVM.TTYCenteredList   other-modules:     Paths_hevm   autogen-modules:     Paths_hevm-  if os(linux) || os(windows)+  if impl(ghc >= 9.4) && !os(darwin)+    -- darwin is skipped because it produces this error when building+    -- > ghc: loadArchive: Neither an archive, nor a fat archive: `/nix/store/l3lkdfm7sg1wwc850451cikqds766h15-clang-wrapper-11.1.0/bin/clang++'+    build-depends: system-cxx-std-lib+  elif !os(darwin)     extra-libraries: stdc+++  else+    -- extra-libraries: c+++    -- https://gitlab.haskell.org/ghc/ghc/-/issues/11829+    ld-options: -Wl,-keep_dwarf_unwind+    ghc-options: -fcompact-unwind   extra-libraries:     secp256k1, ff, gmp   c-sources:@@ -161,7 +141,6 @@     text                              >= 1.2.3 && < 2.1,     unordered-containers              >= 0.2.10 && < 0.3,     vector                            >= 0.12.1 && < 0.14,-    ansi-wl-pprint                    >= 0.6.9 && < 0.7,     base16                            >= 0.3.2.0 && < 0.3.3.0,     megaparsec                        >= 9.0.0 && < 10.0,     mtl                               >= 2.2.2 && < 2.3,@@ -183,6 +162,7 @@     multiset                          >= 0.3.4 && < 0.4,     operational                       >= 0.2.3 && < 0.3,     optparse-generic                  >= 1.3.1 && < 1.5,+    pretty-hex                        >= 1.1 && < 1.2,     quickcheck-text                   >= 0.1.2 && < 0.2,     restless-git                      >= 0.7 && < 0.8,     rosezipper                        >= 0.2 && < 0.3,@@ -192,7 +172,6 @@     regex-tdfa                        >= 1.2.3 && < 1.4,     base                              >= 4.9 && < 5,     here                              >= 1.2.13 && < 1.3,-    tuple                             >= 0.3.0.2 && < 0.4,     smt2-parser                       >= 0.1.0.1,     word-wrap                         >= 0.5 && < 0.6,     spool                             >= 0.1 && < 0.2,@@ -210,22 +189,17 @@ executable hevm   import: shared   hs-source-dirs:-    hevm-cli+    cli   main-is:-    hevm-cli.hs+    cli.hs   ghc-options: -threaded -with-rtsopts=-N   other-modules:     Paths_hevm   if os(darwin)     extra-libraries: c++-    ld-options: -Wl,-keep_dwarf_unwind-    ghc-options: -fcompact-unwind-  else-    extra-libraries: stdc++   build-depends:     QuickCheck,     aeson,-    ansi-wl-pprint,     async,     base,     base16,@@ -266,8 +240,6 @@   import: shared   hs-source-dirs:     test-  extra-libraries:-    secp256k1   other-modules:     Paths_hevm   autogen-modules:@@ -336,11 +308,6 @@     buildable: False   if os(darwin)     extra-libraries: c++-    -- https://gitlab.haskell.org/ghc/ghc/-/issues/11829-    ld-options: -Wl,-keep_dwarf_unwind-    ghc-options: -fcompact-unwind-  else-    extra-libraries: stdc++  --- Test Suites --- @@ -383,9 +350,7 @@   ghc-options:     -O2   if os(darwin)-     extra-libraries: c++-  else-     extra-libraries: stdc+++    extra-libraries: c++   other-modules:     Paths_hevm   autogen-modules:

@@ -12,2319 +12,2630 @@ 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-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 (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.Typeable-import Data.Vector qualified as V-import Data.Vector.Storable qualified as SV-import Data.Vector.Storable.Mutable qualified as SV-import Data.Word (Word8, Word32, Word64)-import Witch (into, unsafeInto)--import Crypto.Hash (Digest, SHA256, RIPEMD160)-import Crypto.Hash qualified as Crypto-import Crypto.Number.ModArithmetic (expFast)--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---- * 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, o.coinbase] ++ [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-    { 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 (internalError "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 -> partial $-                     UnexpectedSymbolicArg vmx.state.pc "precompile returned a symbolic value" (wrap [e])-            _ ->-              underrun-      e -> partial $-             UnexpectedSymbolicArg vm.state.pc "cannot call precompiles with symbolic data" (wrap [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 (internalError "could not analyze symbolic code") $-                      maybeLitByte $ ops V.! vm.state.pc--      case getOp (?op) of--        OpPush0 -> do-          limitStack 1 $-            burn g_base $ do-              next-              pushSym (Lit 0)--        OpPush n' -> do-          let n = into n'-              !xs = case vm.state.code of-                InitCode conc _ -> Lit $ word $ padRight n $ BS.take n (BS.drop (1 + vm.state.pc) conc)-                RuntimeCode (ConcreteRuntimeCode bs) -> Lit $ word $ BS.take n $ BS.drop (1 + vm.state.pc) bs-                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 (into i - 1)) stk of-            Nothing -> underrun-            Just y ->-              limitStack 1 $-                burn g_verylow $ do-                  next-                  pushSym y--        OpSwap i ->-          if length stk < (into i) + 1-            then underrun-            else-              burn g_verylow $ do-                next-                zoom (#state % #stack) $ do-                  assign (ix 0) (stk ^?! ix (into i))-                  assign (ix (into i)) (stk ^?! ix 0)--        OpLog n ->-          notStatic $-          case stk of-            (xOffset':xSize':xs) ->-              if length xs < (into n)-              then underrun-              else-                forceConcrete2 (xOffset', xSize') "LOG" $ \(xOffset, xSize) -> do-                    let (topics, xs') = splitAt (into n) xs-                        bytes         = readMemory xOffset' xSize' vm-                        logs'         = (LogEntry (litAddr self) bytes topics) : vm.logs-                    burn (g_log + g_logdata * (unsafeInto xSize) + into 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 (unsafeInto xSize) 32) $-                    accessMemoryRange xOffset xSize $ do-                      hash <- 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'-                                          buf -> pure $ Keccak buf-                      next-                      assign (#state % #stack) (hash : xs)-            _ -> underrun--        OpAddress ->-          limitStack 1 $-            burn g_base (next >> push (into self))--        OpBalance ->-          case stk of-            x':xs -> forceConcrete x' "BALANCE" $ \x ->-              accessAndBurn (unsafeInto x) $-                fetchAccount (unsafeInto x) $ \c -> do-                  next-                  assign (#state % #stack) xs-                  push c.balance-            [] ->-              underrun--        OpOrigin ->-          limitStack 1 . burn g_base $-            next >> push (into 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 (unsafeInto 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 (unsafeInto 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 == into cheatCode-                then do-                  next-                  assign (#state % #stack) xs-                  pushSym (Lit 1)-                else-                  accessAndBurn (unsafeInto x) $-                    fetchAccount (unsafeInto 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 (unsafeInto extAccount)-                  let cost = if acc then g_warm_storage_read else g_cold_account_access-                  burn (cost + g_copy * ceilDiv (unsafeInto codeSize) 32) $-                    accessMemoryRange memOffset codeSize $-                      fetchAccount (unsafeInto 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 (unsafeInto xSize) 32) $-                  accessMemoryRange xTo xSize $ do-                    next-                    assign (#state % #stack) xs--                    let jump True = vmError 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 (unsafeInto x) $ do-                next-                assign (#state % #stack) xs-                fetchAccount (unsafeInto x) $ \c ->-                   if accountEmpty c-                     then push 0-                     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 (into i :: Integer) & show & Char8.pack & keccak' & Lit-            i -> BlockHash i--        OpCoinbase ->-          limitStack 1 . burn g_base $-            next >> push (into 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 (into 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 availableGas <= g_callstipend then-                  finishFrame (FrameErrored (OutOfGas availableGas 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 current' == 0-                                then unRefund (g_sreset + g_access_list_storage_key)-                                else when (new' == 0) $ refund (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 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 BadJumpDestination-                        Just i -> checkJump i xs-                  in do-                    loc <- codeloc-                    branch loc y jump-            _ -> underrun--        OpPc ->-          limitStack 1 . burn g_base $-            next >> push (unsafeInto vm.state.pc)--        OpMsize ->-          limitStack 1 . burn g_base $-            next >> push (into vm.state.memorySize)--        OpGas ->-          limitStack 1 . burn g_base $-            next >> push (into (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 * unsafeInto (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 xSize False-                  _ <- accessAccountForGas newAddr-                  burn cost $ do-                    let initCode = readMemory xOffset' xSize' vm-                    create self this xSize 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 (unsafeInto xGas) xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do-                    let from' = fromMaybe self vm.overrideCaller-                    zoom #state $ do-                      assign #callvalue (Lit xValue)-                      assign #caller (litAddr from')-                      assign #contract callee-                    assign #overrideCaller Nothing-                    touchAccount from'-                    touchAccount callee-                    transfer from' callee xValue-            _ ->-              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 (unsafeInto xGas) xTo (litAddr self) xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do-                  zoom #state $ do-                    assign #callvalue (Lit xValue)-                    assign #caller $ litAddr $ fromMaybe self vm.overrideCaller-                  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 (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data")-                               . maybeLitWord . 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 * unsafeInto 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 (unsafeInto 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 True-                      _ <- accessAccountForGas newAddr-                      burn cost $-                        create self this xSize 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 (unsafeInto xGas) xTo xTo 0 xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do-                  zoom #state $ do-                    assign #callvalue (Lit 0)-                    assign #caller $ litAddr $ fromMaybe self (vm.overrideCaller)-                    assign #contract callee-                    assign #static True-                  assign #overrideCaller Nothing-                  touchAccount self-                  touchAccount callee-            _ ->-              underrun--        OpSelfdestruct ->-          notStatic $-          case stk of-            [] -> underrun-            (xTo':_) -> forceConcrete xTo' "SELFDESTRUCT" $ \(unsafeInto -> xTo) -> do-              acc <- accessAccountForGas xTo-              let cost = if acc then 0 else g_cold_account_access-                  funds = this.balance-                  recipientExists = accountExists xTo vm-                  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 _ _ 0 = pure ()-transfer xFrom xTo xValue = do-    sb <- preuse $ #env % #contracts % ix xFrom % #balance-    case sb of-      Just srcBal ->-        if xValue > srcBal-        then vmError $ BalanceTooLow xValue srcBal-        else do-          (#env % #contracts % ix xFrom % #balance) %= (subtract xValue)-          (#env % #contracts % ix xTo % #balance) %= (+ xValue)-      Nothing -> vmError $ BalanceTooLow xValue 0---- | 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 > 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-          _ -> partial $ UnexpectedSymbolicArg pc' "unexpected return value from precompile" (wrap [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 = internalError $ "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 (unsafeInto lenm) (asBE (0 :: Int))-              else-                let-                  b = asInteger $ lazySlice 96 lenb input'-                  e = asInteger $ lazySlice (96 + lenb) lene input'-                  m = asInteger $ lazySlice (96 + lenb + lene) lenm input'-                in-                  padLeft (unsafeInto lenm) (asBE (expFast b e m))-          assign (#state % #stack) (Lit 1 : xs)-          assign (#state % #returndata) output-          copyBytesToMemory output (Lit outSize) (Lit 0) (Lit outOffset)-          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 (unsafeInto size) (LS.drop (unsafeInto offset) (fromStrict bs))-  in bs' <> LS.replicate (unsafeInto size - LS.length bs') 0--parseModexpLength :: ByteString -> (W256, W256, W256)-parseModexpLength input =-  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 (unsafeInto size) $-      LS.drop (unsafeInto offset) $-        fromStrict bs--asInteger :: LS.ByteString -> Integer-asInteger xs = if xs == mempty then 0-  else 256 * asInteger (LS.init xs)-      + into (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)--query :: Query -> EVM ()-query = assign #result . Just . HandleEffect . Query--choose :: Choose -> EVM ()-choose = assign #result . Just . HandleEffect . Choose--branch :: CodeLocation -> Expr EWord -> (Bool -> EVM ()) -> EVM ()-branch loc cond continue = do-  pathconds <- use #constraints-  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,[]))-      stack <- use (#state % #stack)-      assign (#cache % #path % at (loc, iteration)) (Just v)-      assign (#iterations % at loc) (Just (iteration + 1, stack))-      continue v-    -- Both paths are possible; we ask for more input-    choosePath Unknown =-      choose . PleaseChoosePath cond $ choosePath . Case---- | 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 . HandleEffect . 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 (into 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 = query $-                    PleaseFetchSlot addr s-                      (\x -> do-                          modifying (#cache % #fetchedStorage % ix (into addr)) (Map.insert s x)-                          modifying (#env % #storage) (writeStorage (litAddr addr) slot (Lit x))-                          assign #result Nothing-                          continue (Lit x))--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-    Just (VMFailure (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 ->-              partial $-                UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" (wrap [output])-            Just ops ->-              onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)-    _ ->-      internalError "Finalising an unfinished tx."--  -- 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)-    gasUsed      = tx.gaslimit - gasRemaining-    cappedRefund = min (quot gasUsed 5) sumRefunds-    originPay    = (into $ gasRemaining + cappedRefund) * tx.gasprice-    minerPay     = tx.priorityFee * (into gasUsed)--  modifying (#env % #contracts)-     (Map.adjust (over #balance (+ originPay)) tx.origin)-  modifying (#env % #contracts)-     (Map.adjust (over #balance (+ minerPay)) block.coinbase)-  touchAccount 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 ->-        internalError "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 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-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [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-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [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-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [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-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [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-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [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-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [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-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [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 = unsafeInto (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-  pushTrace $ FrameTrace (CallContext cheatCode cheatCode inOffset inSize (Lit 0) (maybeLitWord abi) input (vm.env.contracts, vm.env.storage) vm.tx.substate)-  case maybeLitWord abi of-    Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc "symbolic cheatcode selector" (wrap [abi])-    Just (unsafeInto -> abi') ->-      case Map.lookup abi' cheatActions of-        Nothing ->-          vmError (BadCheatCode abi')-        Just action -> do-            action (Lit outOffset) (Lit outSize) input-            popTrace-            next-            push 1--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 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 . 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" $ \(unsafeInto -> 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" $ \(unsafeInto -> 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 (V.fromList-                      [ AbiUInt 8 $ into v-                      , AbiBytes 32 (word256Bytes r)-                      , AbiBytes 32 (word256Bytes s)-                      ])-              assign (#state % #returndata) (ConcreteBuf encoded)-              copyBytesToMemory (ConcreteBuf encoded) (Lit . unsafeInto . BS.length $ encoded) (Lit 0) outOffset-          _ -> vmError (BadCheatCode sig),--      action "addr(uint256)" $-        \sig outOffset _ input -> case decodeStaticArgs 0 1 input of-          [sk] -> forceConcrete sk "cannot derive address for a symbolic key" $ \sk' -> do-            let a = EVM.Sign.deriveAddr $ into 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" $-    \((unsafeInto -> xTo'), (unsafeInto -> xContext')) ->-      if xTo' > 0 && xTo' <= 9-      then precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs-      else if xTo' == cheatCode then-        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 (maybeLitWord $ readBytes 4 (Lit xInOffset) vm0.state.memory)-                                        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 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-  -> W256 -> Word64 -> W256 -> [Expr EWord] -> Addr -> Expr Buf -> EVM ()-create self this xSize xGas xValue xs newAddr initCode = do-  vm0 <- get-  if this.nonce == into (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 xSize > vm0.block.maxCodeSize * 2-  then do-    assign (#state % #stack) (Lit 0 : xs)-    assign (#state % #returndata) mempty-    vmError $ MaxInitCodeSizeExceeded (vm0.block.maxCodeSize * 2) xSize-  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-    let contract' = do-          prefixLen <- Expr.concPrefix initCode-          prefix <- Expr.toList $ Expr.take (unsafeInto prefixLen) initCode-          let sym = Expr.drop (unsafeInto prefixLen) initCode-          conc <- mapM maybeLitByte prefix-          pure $ InitCode (BS.pack $ V.toList conc) sym-    case contract' of-      Nothing ->-        partial $ 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 (into newAddr) s)-              AbstractStore -> AbstractStore-              EmptyStore -> EmptyStore-              SStore {} -> internalError "trying to reset symbolic storage with writes in create"-              GVar _  -> internalError "unexpected global variable"--        modifying (#env % #storage) resetStorage-        modifying (#env % #origStorage) (Map.delete (into 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 _ ->-          internalError $ "can't replace code of deployed contract " <> show target-      Nothing ->-        internalError "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 :: EvmError -> EVM ()-vmError e = finishFrame (FrameErrored e)--partial :: PartialExec -> EVM ()-partial e = assign #result (Just (Unfinished e))--wrap :: Typeable a => [Expr a] -> [SomeExpr]-wrap = fmap SomeExpr--underrun :: EVM ()-underrun = vmError 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 EvmError -- ^ 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 (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 (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 internalError(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 (into createe)-              case output of-                ConcreteBuf bs ->-                  onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)-                _ ->-                  case Expr.toList output of-                    Nothing -> partial $-                      UnexpectedSymbolicArg-                        oldVm.state.pc-                        "runtime code cannot have an abstract length"-                        (wrap [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 <- 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 SV.!? 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 -> internalError "internal internalError(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--traceForest' :: Expr End -> Forest Trace-traceForest' (Success _ (Traces f _) _ _) = f-traceForest' (Partial _ (Traces f _) _) = f-traceForest' (Failure _ (Traces f _) _) = f-traceForest' (ITE {}) = internalError"Internal Error: ITE does not contain a trace"-traceForest' (GVar {}) = internalError"Internal Error: Unexpected GVar"--traceContext :: Expr End -> Map Addr Contract-traceContext (Success _ (Traces _ c) _ _) = c-traceContext (Partial _ (Traces _ c) _) = c-traceContext (Failure _ (Traces _ c) _) = c-traceContext (ITE {}) = internalError"Internal Error: ITE does not contain a trace"-traceContext (GVar {}) = internalError"Internal Error: Unexpected GVar"--traceTopLog :: [Expr Log] -> EVM ()-traceTopLog [] = noop-traceTopLog ((LogEntry addr bytes topics) : _) = do-  trace <- withTraceLocation (EventTrace addr bytes topics)-  modifying #traces $-    \t -> Zipper.nextSpace (Zipper.insert (Node trace []) t)-traceTopLog ((GVar _) : _) = internalError "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-  vm <- get-  case isValidJumpDest vm x of-    True -> do-      #state % #stack .= xs-      #state % #pc .= x-    False -> vmError BadJumpDestination--isValidJumpDest :: VM -> Int -> Bool-isValidJumpDest vm x = let-    code = vm.state.code-    self = vm.state.codeContract-    contract = fromMaybe-      (internalError "self not found in current contracts")-      (Map.lookup self vm.env.contracts)-    op = case code of-      InitCode ops _ -> BS.indexMaybe ops x-      RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x-      RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByte-  in case op of-       Nothing -> False-       Just b -> 0x5b == b && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap SV.! x))--opSize :: Word8 -> Int-opSize x | x >= 0x60 && x <= 0x7f = into 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 -> SV.Vector Int-mkOpIxMap (InitCode conc _)-  = SV.create $ SV.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 >> SV.write v i j)-        go v (1, !i, !j, !m) _ =-          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> SV.write v i j)-        go v (0, !i, !j, !m) _ =-          {- Other op. -}         (0,            i + 1, j + 1, m >> SV.write v i j)-        go v (n, !i, !j, !m) _ =-          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)--mkOpIxMap (RuntimeCode (ConcreteRuntimeCode ops)) =-  mkOpIxMap (InitCode ops mempty) -- a bit hacky--mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))-  = SV.create $ SV.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 maybeLitByte x of-          Just x' -> if x' >= 0x60 && x' <= 0x7f-            -- start of PUSH op ---                     then (x' - 0x60 + 1, i + 1, j,     m >> SV.write v i j)-            -- other data ---                     else (0,             i + 1, j + 1, m >> SV.write v i j)-          _ -> internalError $ "cannot analyze symbolic code:\nx: " <> show x <> " i: " <> show i <> " j: " <> show j--        go v (1, !i, !j, !m) _ =-          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> SV.write v i j)-        go v (n, !i, !j, !m) _ =-          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.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 (internalError "unexpected symbolic code") . maybeLitByte $ xs' V.! i , V.toList $ V.drop i xs')-  in if (opslen code' < i)-     then Nothing-     else Just (readOp op pushdata)--vmOpIx :: VM -> Maybe Int-vmOpIx vm =-  do self <- currentContract vm-     self.opIxMap SV.!? vm.state.pc---- Maps operation indicies into a pair of (bytecode index, operation)-mkCodeOps :: ContractCode -> V.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 V.fromList . toList $ go 0 l-  where-    go !i !xs =-      case uncons xs of-        Nothing ->-          mempty-        Just (x, xs') ->-          let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByte x-              j = opSize x'-          in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)---- * 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 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 -> Bool -> (Word64, Word64)-costOfCreate (FeeSchedule {..}) availableGas size hashNeeded = (createCost, initGas)-  where-    byteCost   = if hashNeeded then g_sha3word + g_initcodeword else g_initcodeword-    createCost = g_create + codeCost-    codeCost   = byteCost * (ceilDiv (unsafeInto size) 32)-    initGas    = allButOne64th (availableGas - createCost)--concreteModexpGasFee :: ByteString -> Word64-concreteModexpGasFee input =-  if lenb < into (maxBound :: Word32) &&-     (lene < into (maxBound :: Word32) || (lenb == 0 && lenm == 0)) &&-     lenm < into (maxBound :: Word64)-  then-    max 200 ((multiplicationComplexity * iterCount) `div` 3)-  else-    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 (unsafeInto $ max lenb lenm) 8-    multiplicationComplexity = nwords * nwords-    iterCount' :: Word64-    iterCount' | lene <= 32 && ez = 0-               | lene <= 32 = unsafeInto (log2 e')-               | e' == 0 = 8 * (unsafeInto lene - 32)-               | otherwise = unsafeInto (log2 e') + 8 * (unsafeInto lene - 32)-    iterCount = max iterCount' 1---- Gas cost of precompiles-costOfPrecompile :: FeeSchedule Word64 -> Addr -> Expr Buf -> Word64-costOfPrecompile (FeeSchedule {..}) precompileAddr input =-  let errorDynamicSize = internalError "precompile input cannot have a dynamic size"-      inputLen = case input of-                   ConcreteBuf bs -> unsafeInto $ BS.length bs-                   AbstractBuf _ -> errorDynamicSize-                   buf -> case bufLength buf of-                            Lit l -> unsafeInto l -- TODO: overflow-                            _ -> errorDynamicSize-  in case precompileAddr of-    -- ECRECOVER-    0x1 -> 3000-    -- SHA2-256-    0x2 -> (((inputLen + 31) `div` 32) * 12) + 60-    -- RIPEMD-160-    0x3 -> (((inputLen + 31) `div` 32) * 120) + 600-    -- IDENTITY-    0x4 -> (((inputLen + 31) `div` 32) * 3) + 15-    -- MODEXP-    0x5 -> case input of-             ConcreteBuf i -> concreteModexpGasFee i-             _ -> internalError "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 * (unsafeInto $ asInteger $ lazySlice 0 4 i)-             _ -> internalError "Unsupported symbolic blake2 gas calc"-    _ -> internalError $ "unimplemented precompiled contract " ++ show precompileAddr---- Gas cost of memory expansion-memoryCost :: FeeSchedule Word64 -> Word64 -> Word64-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 . unsafeInto $ BS.length ops-codelen (RuntimeCode (SymbolicRuntimeCode ops)) = Lit . unsafeInto $ 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+import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord,+  writeByte, bufLength, indexWord, litAddr, readBytes, word256At, copySlice, wordToAddr)+import EVM.Expr qualified as Expr+import EVM.FeeSchedule (FeeSchedule (..))+import EVM.Op+import EVM.Precompiled qualified+import EVM.Solidity+import EVM.Types+import EVM.Sign qualified+import EVM.Concrete qualified as Concrete++import Control.Monad.ST (ST)+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, isJust)+import Data.Set (insert, member, fromList)+import Data.Sequence (Seq)+import Data.Sequence qualified as Seq+import Data.Text (unpack, pack)+import Data.Text.Encoding (decodeUtf8)+import Data.Tree+import Data.Tree.Zipper qualified as Zipper+import Data.Typeable+import Data.Vector qualified as V+import Data.Vector.Storable qualified as SV+import Data.Vector.Storable.Mutable qualified as SV+import Data.Vector.Unboxed qualified as VUnboxed+import Data.Vector.Unboxed.Mutable qualified as VUnboxed.Mutable+import Data.Word (Word8, Word32, Word64)+import Witch (into, tryFrom, unsafeInto)++import Crypto.Hash (Digest, SHA256, RIPEMD160)+import Crypto.Hash qualified as Crypto+import Crypto.Number.ModArithmetic (expFast)++blankState :: ST s (FrameState s)+blankState = do+  memory <- ConcreteMemory <$> VUnboxed.Mutable.new 0+  pure $ FrameState+    { contract     = LitAddr 0+    , codeContract = LitAddr 0+    , code         = RuntimeCode (ConcreteRuntimeCode "")+    , pc           = 0+    , stack        = mempty+    , memory+    , memorySize   = 0+    , calldata     = mempty+    , callvalue    = Lit 0+    , caller       = LitAddr 0+    , gas          = 0+    , returndata   = mempty+    , static       = False+    }++-- | An "external" view of a contract's bytecode, appropriate for+-- e.g. @EXTCODEHASH@.+bytecode :: Getter Contract (Maybe (Expr Buf))+bytecode = #code % to f+  where f (InitCode _ _) = Just mempty+        f (RuntimeCode (ConcreteRuntimeCode bs)) = Just $ ConcreteBuf bs+        f (RuntimeCode (SymbolicRuntimeCode ops)) = Just $ Expr.fromList ops+        f (UnknownCode _) = Nothing++-- * Data accessors++currentContract :: VM s -> Maybe Contract+currentContract vm =+  Map.lookup vm.state.codeContract vm.env.contracts++-- * Data constructors++makeVm :: VMOpts -> ST s (VM s)+makeVm o = do+  let txaccessList = o.txAccessList+      txorigin = o.origin+      txtoAddr = o.address+      initialAccessedAddrs = fromList $+           [txorigin, txtoAddr, o.coinbase]+        ++ (fmap LitAddr [1..9])+        ++ (Map.keys txaccessList)+      initialAccessedStorageKeys = fromList $ foldMap (uncurry (map . (,))) (Map.toList txaccessList)+      touched = if o.create then [txorigin] else [txorigin, txtoAddr]+  memory <- ConcreteMemory <$> VUnboxed.Mutable.new 0+  pure $ 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+      , isCreate = o.create+      , txReversion = Map.fromList ((o.address,o.contract):o.otherContracts)+      }+    , 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+      , memorySize = 0+      , code = o.contract.code+      , 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+      { chainId = o.chainId+      , contracts = Map.fromList ((o.address,o.contract):o.otherContracts)+      , freshAddresses = 0+      }+    , cache = Cache mempty mempty+    , burned = 0+    , constraints = snd o.calldata+    , keccakEqs = mempty+    , iterations = mempty+    , config = RuntimeConfig+      { allowFFI = o.allowFFI+      , overrideCaller = Nothing+      , baseState = o.baseState+      }+    }++-- | Initialize an abstract contract with unknown code+unknownContract :: Expr EAddr -> Contract+unknownContract addr = Contract+  { code        = UnknownCode addr+  , storage     = AbstractStore addr+  , origStorage = AbstractStore addr+  , balance     = Balance addr+  , nonce       = Nothing+  , codehash    = hashcode (UnknownCode addr)+  , opIxMap     = mempty+  , codeOps     = mempty+  , external    = False+  }++-- | Initialize an abstract contract with known code+abstractContract :: ContractCode -> Expr EAddr -> Contract+abstractContract code addr = Contract+  { code        = code+  , storage     = AbstractStore addr+  , origStorage = AbstractStore addr+  , balance     = Balance addr+  , nonce       = if isCreation code then Just 1 else Just 0+  , codehash    = hashcode code+  , opIxMap     = mkOpIxMap code+  , codeOps     = mkCodeOps code+  , external    = False+  }++-- | Initialize an empty contract without code+emptyContract :: Contract+emptyContract = initialContract (RuntimeCode (ConcreteRuntimeCode ""))++-- | Initialize empty contract with given code+initialContract :: ContractCode -> Contract+initialContract code = Contract+  { code        = code+  , storage     = ConcreteStore mempty+  , origStorage = ConcreteStore mempty+  , balance     = Lit 0+  , nonce       = if isCreation code then Just 1 else Just 0+  , codehash    = hashcode code+  , opIxMap     = mkOpIxMap code+  , codeOps     = mkCodeOps code+  , external    = False+  }++isCreation :: ContractCode -> Bool+isCreation = \case+  InitCode _ _  -> True+  RuntimeCode _ -> False+  UnknownCode _ -> False++-- * Opcode dispatch (exec1)++-- | Update program counter+next :: (?op :: Word8) => EVM s ()+next = modifying (#state % #pc) (+ (opSize ?op))++-- | Executes the EVM one step+exec1 :: EVM s ()+exec1 = do+  vm <- get++  let+    -- Convenient aliases+    stk  = vm.state.stack+    self = vm.state.contract+    this = fromMaybe (internalError "state contract") (Map.lookup self vm.env.contracts)++    fees@FeeSchedule {..} = vm.block.schedule++    doStop = finishFrame (FrameReturned mempty)++    litSelf = maybeLitAddr self++  if isJust litSelf && (fromJust litSelf) > 0x0 && (fromJust litSelf) <= 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 (fromJust litSelf) 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 -> partial $+                     UnexpectedSymbolicArg vmx.state.pc "precompile returned a symbolic value" (wrap [e])+            _ ->+              underrun+      e -> partial $+             UnexpectedSymbolicArg vm.state.pc "cannot call precompiles with symbolic data" (wrap [e])++  else if vm.state.pc >= opslen vm.state.code+    then doStop++    else do+      let ?op = case vm.state.code of+                  UnknownCode _ -> internalError "Cannot execute unknown code"+                  InitCode conc _ -> BS.index conc vm.state.pc+                  RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs vm.state.pc+                  RuntimeCode (SymbolicRuntimeCode ops) ->+                    fromMaybe (internalError "could not analyze symbolic code") $+                      maybeLitByte $ ops V.! vm.state.pc++      case getOp (?op) of++        OpPush0 -> do+          limitStack 1 $+            burn g_base $ do+              next+              pushSym (Lit 0)++        OpPush n' -> do+          let n = into n'+              !xs = case vm.state.code of+                UnknownCode _ -> internalError "Cannot execute unknown code"+                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 (into i - 1)) stk of+            Nothing -> underrun+            Just y ->+              limitStack 1 $+                burn g_verylow $ do+                  next+                  pushSym y++        OpSwap i ->+          if length stk < (into i) + 1+            then underrun+            else+              burn g_verylow $ do+                next+                zoom (#state % #stack) $ do+                  assign (ix 0) (stk ^?! ix (into i))+                  assign (ix (into i)) (stk ^?! ix 0)++        OpLog n ->+          notStatic $+          case stk of+            (xOffset':xSize':xs) ->+              if length xs < (into n)+              then underrun+              else+                forceConcrete2 (xOffset', xSize') "LOG" $ \(xOffset, xSize) -> do+                    bytes <- readMemory xOffset' xSize'+                    let (topics, xs') = splitAt (into n) xs+                        logs'         = (LogEntry (WAddr self) bytes topics) : vm.logs+                    case (tryFrom xSize) of+                      (Right sz) ->+                        burn (g_log + g_logdata * sz + (into n) * g_logtopic) $+                          accessMemoryRange xOffset xSize $ do+                            traceTopLog logs'+                            next+                            assign (#state % #stack) xs'+                            assign #logs logs'+                      _ -> vmError IllegalOverflow+            _ ->+              underrun++        OpStop -> doStop++        OpAdd -> stackOp2 g_verylow Expr.add+        OpMul -> stackOp2 g_low Expr.mul+        OpSub -> stackOp2 g_verylow Expr.sub++        OpDiv -> stackOp2 g_low Expr.div++        OpSdiv -> stackOp2 g_low Expr.sdiv++        OpMod -> stackOp2 g_low Expr.mod++        OpSmod -> stackOp2 g_low Expr.smod+        OpAddmod -> stackOp3 g_mid Expr.addmod+        OpMulmod -> stackOp3 g_mid Expr.mulmod++        OpLt -> stackOp2 g_verylow Expr.lt+        OpGt -> stackOp2 g_verylow Expr.gt+        OpSlt -> stackOp2 g_verylow Expr.slt+        OpSgt -> stackOp2 g_verylow Expr.sgt++        OpEq -> stackOp2 g_verylow Expr.eq+        OpIszero -> stackOp1 g_verylow Expr.iszero++        OpAnd -> stackOp2 g_verylow Expr.and+        OpOr -> stackOp2 g_verylow Expr.or+        OpXor -> stackOp2 g_verylow Expr.xor+        OpNot -> stackOp1 g_verylow Expr.not++        OpByte -> stackOp2 g_verylow (\i w -> Expr.padByte $ Expr.indexWord i w)++        OpShl -> stackOp2 g_verylow Expr.shl+        OpShr -> stackOp2 g_verylow Expr.shr+        OpSar -> stackOp2 g_verylow 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 (unsafeInto xSize) 32) $+                    accessMemoryRange xOffset xSize $ do+                      hash <- readMemory xOffset' xSize' >>= \case+                        ConcreteBuf bs -> do+                          let hash' = keccak' bs+                          eqs <- use #keccakEqs+                          assign #keccakEqs $+                            PEq (Lit hash') (Keccak (ConcreteBuf bs)):eqs+                          pure $ Lit hash'+                        buf -> pure $ Keccak buf+                      next+                      assign (#state % #stack) (hash : xs)+            _ -> underrun++        OpAddress ->+          limitStack 1 $+            burn g_base (next >> pushAddr self)++        OpBalance ->+          case stk of+            x:xs -> forceAddr x "BALANCE" $ \a ->+              accessAndBurn a $+                fetchAccount a $ \c -> do+                  next+                  assign (#state % #stack) xs+                  pushSym c.balance+            [] ->+              underrun++        OpOrigin ->+          limitStack 1 . burn g_base $+            next >> pushAddr vm.tx.origin++        OpCaller ->+          limitStack 1 . burn g_base $+            next >> pushAddr 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 (unsafeInto 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 (unsafeInto n) 32) $+                          accessMemoryRange memOffset n $ do+                            next+                            assign (#state % #stack) xs+                            case toBuf vm.state.code of+                              Just b -> copyBytesToMemory b n' codeOffset memOffset'+                              Nothing -> internalError "Cannot produce a buffer from UnknownCode"+                      else vmError IllegalOverflow+            _ -> underrun++        OpGasprice ->+          limitStack 1 . burn g_base $+            next >> push vm.tx.gasprice++        OpExtcodesize ->+          case stk of+            x':xs -> forceAddr x' "EXTCODESIZE" $ \x -> do+              let impl = accessAndBurn x $+                           fetchAccount x $ \c -> do+                             next+                             assign (#state % #stack) xs+                             case view bytecode c of+                               Just b -> pushSym (bufLength b)+                               Nothing -> pushSym $ CodeSize x+              case x of+                a@(LitAddr _) -> if a == cheatCode+                  then do+                    next+                    assign (#state % #stack) xs+                    pushSym (Lit 1)+                  else impl+                _ -> impl+            [] ->+              underrun++        OpExtcodecopy ->+          case stk of+            extAccount':memOffset':codeOffset:codeSize':xs ->+              forceConcrete2 (memOffset', codeSize') "EXTCODECOPY" $ \(memOffset, codeSize) -> do+                forceAddr extAccount' "EXTCODECOPY" $ \extAccount -> do+                  acc <- accessAccountForGas extAccount+                  let cost = if acc then g_warm_storage_read else g_cold_account_access+                  burn (cost + g_copy * ceilDiv (unsafeInto codeSize) 32) $+                    accessMemoryRange memOffset codeSize $+                      fetchAccount extAccount $ \c -> do+                        next+                        assign (#state % #stack) xs+                        case view bytecode c of+                          Just b -> copyBytesToMemory b codeSize' codeOffset memOffset'+                          Nothing -> do+                            pc <- use (#state % #pc)+                            partial $ UnexpectedSymbolicArg pc "Cannot copy from unknown code at" (wrap [extAccount])+            _ -> 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 (unsafeInto xSize) 32) $+                  accessMemoryRange xTo xSize $ do+                    next+                    assign (#state % #stack) xs++                    let jump True = vmError 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)+                        branch (Expr.or oob overflow) jump+            _ -> underrun++        OpExtcodehash ->+          case stk of+            x':xs -> forceAddr x' "EXTCODEHASH" $ \x ->+              accessAndBurn x $ do+                next+                assign (#state % #stack) xs+                fetchAccount x $ \c ->+                   if accountEmpty c+                     then push (W256 0)+                     else case view bytecode c of+                            Just b -> pushSym $ keccak b+                            Nothing -> pushSym $ CodeHash x+            [] ->+              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 (into i :: Integer) & show & Char8.pack & keccak' & Lit+            i -> BlockHash i++        OpCoinbase ->+          limitStack 1 . burn g_base $+            next >> pushAddr 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 (into vm.block.gaslimit)++        OpChainid ->+          limitStack 1 . burn g_base $+            next >> push vm.env.chainId++        OpSelfbalance ->+          limitStack 1 . burn g_low $+            next >> pushSym 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+                  buf <- readMemory (Lit x) (Lit 32)+                  let w = Expr.readWordFromBytes (Lit 0) buf+                  assign (#state % #stack) (w : xs)+            _ -> underrun++        OpMstore ->+          case stk of+            x':y:xs -> forceConcrete x' "MSTORE index" $ \x ->+              burn g_verylow $+                accessMemoryWord x $ do+                  next+                  gets (.state.memory) >>= \case+                    ConcreteMemory mem -> do+                      case y of+                        Lit w ->+                          writeMemory mem (unsafeInto x) (word256Bytes w)+                        _ -> do+                          -- copy out and move to symbolic memory+                          buf <- freezeMemory mem+                          assign (#state % #memory) (SymbolicMemory $ writeWord (Lit x) y buf)+                    SymbolicMemory mem ->+                      assign (#state % #memory) (SymbolicMemory $ 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+                  gets (.state.memory) >>= \case+                    ConcreteMemory mem -> do+                      case yByte of+                        LitByte byte ->+                          writeMemory mem (unsafeInto x) (BS.pack [byte])+                        _ -> do+                          -- copy out and move to symbolic memory+                          buf <- freezeMemory mem+                          assign (#state % #memory) (SymbolicMemory $ writeByte (Lit x) yByte buf)+                    SymbolicMemory mem ->+                      assign (#state % #memory) (SymbolicMemory $ writeByte (Lit x) yByte mem)++                  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 availableGas <= g_callstipend then+                  finishFrame (FrameErrored (OutOfGas availableGas g_callstipend))+                else do+                  let+                    original =+                      case Expr.simplify $ SLoad x this.origStorage of+                        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 % #contracts % ix self % #storage) (writeStorage 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 current' == 0+                                then unRefund (g_sreset + g_access_list_storage_key)+                                else when (new' == 0) $ refund (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 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 s ()+                      jump False = assign (#state % #stack) xs >> next+                      jump _    = case toInt x' of+                        Nothing -> vmError BadJumpDestination+                        Just i -> checkJump i xs+                  in branch y jump+            _ -> underrun++        OpPc ->+          limitStack 1 . burn g_base $+            next >> push (unsafeInto vm.state.pc)++        OpMsize ->+          limitStack 1 . burn g_base $+            next >> push (into vm.state.memorySize)++        OpGas ->+          limitStack 1 . burn g_base $+            next >> push (into (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 * unsafeInto (ceilDiv (1 + log2 exponent) 8)+              in burn cost $ do+                next+                (#state % #stack) .= Expr.exp base exponent' : xs+            _ -> underrun++        OpSignextend -> stackOp2 g_low Expr.sex++        OpCreate ->+          notStatic $+          case stk of+            xValue:xOffset':xSize':xs -> forceConcrete2 (xOffset', xSize') "CREATE" $+              \(xOffset, xSize) -> do+                accessMemoryRange xOffset xSize $ do+                  availableGas <- use (#state % #gas)+                  let+                    (cost, gas') = costOfCreate fees availableGas xSize False+                  newAddr <- createAddress self this.nonce+                  _ <- accessAccountForGas newAddr+                  burn cost $ do+                    initCode <- readMemory xOffset' xSize'+                    create self this xSize gas' xValue xs newAddr initCode+            _ -> underrun++        OpCall ->+          case stk of+            xGas':xTo':xValue:xInOffset':xInSize':xOutOffset':xOutSize':xs ->+              forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "CALL" $+              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->+                branch (Expr.gt xValue (Lit 0)) $ \gt0 -> do+                  (if gt0 then notStatic else id) $+                    forceAddr xTo' "unable to determine a call target" $ \xTo ->+                      case tryFrom xGas of+                        Left _ -> vmError IllegalOverflow+                        Right gas ->+                          delegateCall this gas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $+                            \callee -> do+                              let from' = fromMaybe self vm.config.overrideCaller+                              zoom #state $ do+                                assign #callvalue xValue+                                assign #caller from'+                                assign #contract callee+                              assign (#config % #overrideCaller) Nothing+                              touchAccount from'+                              touchAccount callee+                              transfer from' callee xValue+            _ ->+              underrun++        OpCallcode ->+          case stk of+            xGas':xTo':xValue:xInOffset':xInSize':xOutOffset':xOutSize':xs ->+              forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "CALLCODE" $+              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->+                forceAddr xTo' "unable to determine a call target" $ \xTo ->+                  case tryFrom xGas of+                    Left _ -> vmError IllegalOverflow+                    Right gas ->+                      delegateCall this gas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do+                        zoom #state $ do+                          assign #callvalue xValue+                          assign #caller $ fromMaybe self vm.config.overrideCaller+                        assign (#config % #overrideCaller) Nothing+                        touchAccount self+            _ ->+              underrun++        OpReturn ->+          case stk of+            xOffset':xSize':_ -> forceConcrete2 (xOffset', xSize') "RETURN" $ \(xOffset, xSize) ->+              accessMemoryRange xOffset xSize $ do+                output <- readMemory xOffset' xSize'+                let+                  codesize = fromMaybe (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data")+                               . maybeLitWord . 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 * unsafeInto codesize) $+                                          finishFrame (FrameReturned output)+                        frameErrored = finishFrame $ FrameErrored InvalidFormat+                    case readByte (Lit 0) output of+                      LitByte 0xef -> frameErrored+                      LitByte _ -> frameReturned+                      y -> branch (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) ->+                case wordToAddr xTo of+                  Nothing -> do+                    loc <- codeloc+                    let msg = "Unable to determine a call target"+                    partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]+                  Just xTo' ->+                    case tryFrom xGas of+                      Left _ -> vmError IllegalOverflow+                      Right gas ->+                        delegateCall this gas xTo' self (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $+                          \_ -> touchAccount self+            _ -> underrun++        OpCreate2 -> notStatic $+          case stk of+            xValue:xOffset':xSize':xSalt':xs ->+              forceConcrete3 (xOffset', xSize', xSalt') "CREATE2" $+              \(xOffset, xSize, xSalt) ->+                accessMemoryRange xOffset xSize $ do+                  availableGas <- use (#state % #gas)+                  buf <- readMemory xOffset' xSize'+                  forceConcreteBuf buf "CREATE2" $+                    \initCode -> do+                      let+                        (cost, gas') = costOfCreate fees availableGas xSize True+                      newAddr <- create2Address self xSalt initCode+                      _ <- accessAccountForGas newAddr+                      burn cost $+                        create self this xSize 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+                case wordToAddr xTo of+                  Nothing -> do+                    loc <- codeloc+                    let msg = "Unable to determine a call target"+                    partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]+                  Just xTo' ->+                    case tryFrom xGas of+                      Left _ -> vmError IllegalOverflow+                      Right gas ->+                        delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $+                          \callee -> do+                            zoom #state $ do+                              assign #callvalue (Lit 0)+                              assign #caller $ fromMaybe self (vm.config.overrideCaller)+                              assign #contract callee+                              assign #static True+                            assign (#config % #overrideCaller) Nothing+                            touchAccount self+                            touchAccount callee+            _ ->+              underrun++        OpSelfdestruct ->+          notStatic $+          case stk of+            [] -> underrun+            (xTo':_) -> forceAddr xTo' "SELFDESTRUCT" $ \case+              xTo@(LitAddr _) -> do+                acc <- accessAccountForGas xTo+                let cost = if acc then 0 else g_cold_account_access+                    funds = this.balance+                    recipientExists = accountExists xTo vm+                branch (Expr.iszero $ Expr.eq funds (Lit 0)) $ \hasFunds -> do+                  let c_new = if (not recipientExists) && hasFunds+                              then g_selfdestruct_newaccount+                              else 0+                  burn (g_selfdestruct + c_new + cost) $ do+                    selfdestruct self+                    touchAccount xTo++                    if hasFunds+                    then fetchAccount xTo $ \_ -> do+                           #env % #contracts % ix xTo % #balance %= (Expr.add funds)+                           assign (#env % #contracts % ix self % #balance) (Lit 0)+                           doStop+                    else do+                      doStop+              a -> do+                pc <- use (#state % #pc)+                partial $ UnexpectedSymbolicArg pc "trying to self destruct to a symbolic address" (wrap [a])++        OpRevert ->+          case stk of+            xOffset':xSize':_ -> forceConcrete2 (xOffset', xSize') "REVERT" $ \(xOffset, xSize) ->+              accessMemoryRange xOffset xSize $ do+                output <- readMemory xOffset' xSize'+                finishFrame (FrameReverted output)+            _ -> underrun++        OpUnknown xxx ->+          vmError $ UnrecognizedOpcode xxx++transfer :: Expr EAddr -> Expr EAddr -> Expr EWord -> EVM s ()+transfer _ _ (Lit 0) = pure ()+transfer src dst val = do+  sb <- preuse $ #env % #contracts % ix src % #balance+  db <- preuse $ #env % #contracts % ix dst % #balance+  baseState <- use (#config % #baseState)+  let mkc = case baseState of+              AbstractBase -> unknownContract+              EmptyBase -> const emptyContract+  case (sb, db) of+    -- both sender and recipient in state+    (Just srcBal, Just _) ->+      branch (Expr.gt val srcBal) $ \case+        True -> vmError $ BalanceTooLow val srcBal+        False -> do+          (#env % #contracts % ix src % #balance) %= (`Expr.sub` val)+          (#env % #contracts % ix dst % #balance) %= (`Expr.add` val)+    -- sender not in state+    (Nothing, Just _) -> do+      case src of+        LitAddr _ -> do+          (#env % #contracts) %= (Map.insert src (mkc src))+          transfer src dst val+        SymAddr _ -> do+          pc <- use (#state % #pc)+          partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth from a symbolic address that is not present in the state" (wrap [src])+        GVar _ -> internalError "Unexpected GVar"+    -- recipient not in state+    (_ , Nothing) -> do+      case dst of+        LitAddr _ -> do+          (#env % #contracts) %= (Map.insert dst (mkc dst))+          transfer src dst val+        SymAddr _ -> do+          pc <- use (#state % #pc)+          partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth to a symbolic address that is not present in the state" (wrap [dst])+        GVar _ -> internalError "Unexpected GVar"++-- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.+callChecks+  :: (?op :: Word8)+  => Contract -> Word64 -> Expr EAddr -> Expr EAddr -> Expr EWord -> W256 -> W256 -> W256 -> W256 -> [Expr EWord]+   -- continuation with gas available for call+  -> (Word64 -> EVM s ())+  -> EVM s ()+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') $+        branch (Expr.gt xValue this.balance) $ \case+          True -> do+            assign (#state % #stack) (Lit 0 : xs)+            assign (#state % #returndata) mempty+            pushTrace $ ErrorTrace (BalanceTooLow xValue this.balance)+            next+          False ->+            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+  -> Expr EWord+  -> W256 -> W256 -> W256 -> W256+  -> [Expr EWord]+  -> EVM s ()+precompiledContract this xGas precompileAddr recipient xValue inOffset inSize outOffset outSize xs+  = callChecks this xGas (LitAddr recipient) (LitAddr 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 (LitAddr recipient) $ \_ -> do+                touchAccount self+                touchAccount (LitAddr recipient)+                transfer self (LitAddr recipient) xValue+            _ -> partial $+                   UnexpectedSymbolicArg pc' "unexpected return value from precompile" (wrap [x])+          _ -> underrun+        _ -> pure ()++executePrecompile+  :: (?op :: Word8)+  => Addr+  -> Word64 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord]+  -> EVM s ()+executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  = do+  vm <- get+  input <- readMemory (Lit inOffset) (Lit inSize)+  let fees = vm.block.schedule+      cost = costOfPrecompile fees preCompileAddr input+      notImplemented = internalError $ "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 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 (unsafeInto lenm) (asBE (0 :: Int))+              else+                let+                  b = asInteger $ lazySlice 96 lenb input'+                  e = asInteger $ lazySlice (96 + lenb) lene input'+                  m = asInteger $ lazySlice (96 + lenb + lene) lenm input'+                in+                  padLeft (unsafeInto lenm) (asBE (expFast b e m))+          assign (#state % #stack) (Lit 1 : xs)+          assign (#state % #returndata) output+          copyBytesToMemory output (Lit outSize) (Lit 0) (Lit outOffset)+          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 (unsafeInto size) (LS.drop (unsafeInto offset) (fromStrict bs))+  in bs' <> LS.replicate (unsafeInto size - LS.length bs') 0++parseModexpLength :: ByteString -> (W256, W256, W256)+parseModexpLength input =+  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 (unsafeInto size) $+      LS.drop (unsafeInto offset) $+        fromStrict bs++asInteger :: LS.ByteString -> Integer+asInteger xs = if xs == mempty then 0+  else 256 * asInteger (LS.init xs)+      + into (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 s -> CodeLocation+getCodeLocation vm = (vm.state.contract, vm.state.pc)++query :: Query s -> EVM s ()+query = assign #result . Just . HandleEffect . Query++choose :: Choose s -> EVM s ()+choose = assign #result . Just . HandleEffect . Choose++branch :: forall s. Expr EWord -> (Bool -> EVM s ()) -> EVM s ()+branch cond continue = do+  loc <- codeloc+  pathconds <- use #constraints+  query $ PleaseAskSMT cond pathconds (choosePath loc)+  where+    condSimp = Expr.simplify cond+    choosePath :: CodeLocation -> BranchCondition -> EVM s ()+    choosePath loc (Case v) = do+      assign #result Nothing+      pushTo #constraints $ if v then Expr.simplifyProp (condSimp ./= Lit 0) else Expr.simplifyProp (condSimp .== Lit 0)+      (iteration, _) <- use (#iterations % at loc % non (0,[]))+      stack <- use (#state % #stack)+      assign (#cache % #path % at (loc, iteration)) (Just v)+      assign (#iterations % at loc) (Just (iteration + 1, stack))+      continue v+    -- Both paths are possible; we ask for more input+    choosePath loc Unknown =+      choose . PleaseChoosePath condSimp $ choosePath loc . Case++-- | Construct RPC Query and halt execution until resolved+fetchAccount :: Expr EAddr -> (Contract -> EVM s ()) -> EVM s ()+fetchAccount addr continue =+  use (#env % #contracts % at addr) >>= \case+    Just c -> continue c+    Nothing -> case addr of+      SymAddr _ -> do+        pc <- use (#state % #pc)+        partial $ UnexpectedSymbolicArg pc "trying to access a symbolic address that isn't already present in storage" (wrap [addr])+      LitAddr a -> do+        use (#cache % #fetched % at a) >>= \case+          Just c -> do+            assign (#env % #contracts % at addr) (Just c)+            continue c+          Nothing -> do+            base <- use (#config % #baseState)+            assign (#result) . Just . HandleEffect . Query $+              PleaseFetchContract a base+                (\c -> do assign (#cache % #fetched % at a) (Just c)+                          assign (#env % #contracts % at addr) (Just c)+                          assign #result Nothing+                          continue c)+      GVar _ -> internalError "Unexpected GVar"++accessStorage+  :: Expr EAddr+  -> Expr EWord+  -> (Expr EWord -> EVM s ())+  -> EVM s ()+accessStorage addr slot continue = do+  use (#env % #contracts % at addr) >>= \case+    Just c ->+      case readStorage slot c.storage of+        Just x ->+          continue x+        Nothing ->+          if c.external then+            forceConcreteAddr addr "cannot read storage from symbolic addresses via rpc" $ \addr' ->+              forceConcrete slot "cannot read symbolic slots via RPC" $ \slot' -> do+                -- check if the slot is cached+                contract <- preuse (#cache % #fetched % ix addr')+                case contract of+                  Nothing -> internalError "contract marked external not found in cache"+                  Just fetched -> case readStorage (Lit slot') fetched.storage of+                              Nothing -> mkQuery addr' slot'+                              Just val -> continue val+          else do+            modifying (#env % #contracts % ix addr % #storage) (writeStorage slot (Lit 0))+            continue $ Lit 0+    Nothing ->+      fetchAccount addr $ \_ ->+        accessStorage addr slot continue+  where+      mkQuery a s = query $+        PleaseFetchSlot a s+          (\x -> do+              modifying (#cache % #fetched % ix a % #storage) (writeStorage (Lit s) (Lit x))+              modifying (#env % #contracts % ix (LitAddr a) % #storage) (writeStorage (Lit s) (Lit x))+              assign #result Nothing+              continue (Lit x))++accountExists :: Expr EAddr -> VM s -> 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.code of+    RuntimeCode (ConcreteRuntimeCode "") -> True+    RuntimeCode (SymbolicRuntimeCode b) -> null b+    _ -> False+  && c.nonce == (Just 0)+  -- TODO: handle symbolic balance...+  && c.balance == Lit 0++-- * How to finalize a transaction+finalize :: EVM s ()+finalize = do+  let+    revertContracts  = use (#tx % #txReversion) >>= assign (#env % #contracts)+    revertSubstate   = assign (#tx % #substate) (SubState mempty mempty mempty mempty mempty)++  use #result >>= \case+    Just (VMFailure (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 ->+              partial $+                UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" (wrap [output])+            Just ops ->+              onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)+    _ ->+      internalError "Finalising an unfinished tx."++  -- 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)+    gasUsed      = tx.gaslimit - gasRemaining+    cappedRefund = min (quot gasUsed 5) sumRefunds+    originPay    = (into $ gasRemaining + cappedRefund) * tx.gasprice+    minerPay     = tx.priorityFee * (into gasUsed)++  modifying (#env % #contracts)+     (Map.adjust (over #balance (Expr.add (Lit originPay))) tx.origin)+  modifying (#env % #contracts)+     (Map.adjust (over #balance (Expr.add (Lit minerPay))) block.coinbase)+  touchAccount 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 :: Expr EAddr -> State (VM s) ()+loadContract target =+  preuse (#env % #contracts % ix target % #code) >>=+    \case+      Nothing ->+        internalError "Call target doesn't exist"+      Just targetCode -> do+        assign (#state % #contract) target+        assign (#state % #code)     targetCode+        assign (#state % #codeContract) target++limitStack :: Int -> EVM s () -> EVM s ()+limitStack n continue = do+  stk <- use (#state % #stack)+  if length stk + n > 1024+    then vmError StackLimitExceeded+    else continue++notStatic :: EVM s () -> EVM s ()+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 s () -> EVM s ()+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)++forceAddr :: Expr EWord -> String -> (Expr EAddr -> EVM s ()) -> EVM s ()+forceAddr n msg continue = case wordToAddr n of+  Nothing -> do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])+  Just c -> continue c++forceConcrete :: Expr EWord -> String -> (W256 -> EVM s ()) -> EVM s ()+forceConcrete n msg continue = case maybeLitWord n of+  Nothing -> do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])+  Just c -> continue c++forceConcreteAddr :: Expr EAddr -> String -> (Addr -> EVM s ()) -> EVM s ()+forceConcreteAddr n msg continue = case maybeLitAddr n of+  Nothing -> do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])+  Just c -> continue c++forceConcreteAddr2 :: (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM s ()) -> EVM s ()+forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddr n, maybeLitAddr m) of+  (Just c, Just d) -> continue (c,d)+  _ -> do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])++forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM s ()) -> EVM s ()+forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of+  (Just c, Just d) -> continue (c, d)+  _ -> do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])++forceConcrete3 :: (Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256) -> EVM s ()) -> EVM s ()+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+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, n, m])++forceConcrete4 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256) -> EVM s ()) -> EVM s ()+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+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, l, n, m])++forceConcrete5 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256) -> EVM s ()) -> EVM s ()+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+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [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 s ()) -> EVM s ()+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+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, l, m, n, o, p])++forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM s ()) -> EVM s ()+forceConcreteBuf (ConcreteBuf b) _ continue = continue b+forceConcreteBuf b msg _ = do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [b])++-- * Substate manipulation+refund :: Word64 -> EVM s ()+refund n = do+  self <- use (#state % #contract)+  pushTo (#tx % #substate % #refunds) (self, n)++unRefund :: Word64 -> EVM s ()+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 :: Expr EAddr -> EVM s ()+touchAccount = pushTo ((#tx % #substate) % #touchedAccounts)++selfdestruct :: Expr EAddr -> EVM s ()+selfdestruct = pushTo ((#tx % #substate) % #selfdestructs)++accessAndBurn :: Expr EAddr -> EVM s () -> EVM s ()+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 :: Expr EAddr -> EVM s 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 :: Expr EAddr -> Expr EWord -> EVM s 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 :: Expr EAddr+cheatCode = LitAddr $ unsafeInto (keccak' "hevm cheat code")++cheat+  :: (?op :: Word8)+  => (W256, W256) -> (W256, W256)+  -> EVM s ()+cheat (inOffset, inSize) (outOffset, outSize) = do+  vm <- get+  input <- readMemory (Lit $ inOffset + 4) (Lit $ inSize - 4)+  abi <- readBytes 4 (Lit 0) <$> readMemory (Lit inOffset) (Lit 4)+  pushTrace $ FrameTrace (CallContext cheatCode cheatCode inOffset inSize (Lit 0) (maybeLitWord abi) input vm.env.contracts vm.tx.substate)+  case maybeLitWord abi of+    Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc "symbolic cheatcode selector" (wrap [abi])+    Just (unsafeInto -> abi') ->+      case Map.lookup abi' cheatActions of+        Nothing ->+          vmError (BadCheatCode abi')+        Just action -> do+            action (Lit outOffset) (Lit outSize) input+            popTrace+            next+            push 1++type CheatAction s = Expr EWord -> Expr EWord -> Expr Buf -> EVM s ()++cheatActions :: Map FunctionSelector (CheatAction s)+cheatActions =+  Map.fromList+    [ action "ffi(string[])" $+        \sig outOffset outSize input -> do+          vm <- get+          if vm.config.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 query (PleaseDoFFI cmd cont)+                _ -> vmError (BadCheatCode sig)+              _ -> vmError (BadCheatCode sig)+          else+            let msg = "ffi disabled: run again with --ffi if you want to allow tests to call external scripts"+            in partial $ UnexpectedSymbolicArg vm.state.pc msg [],++      action "warp(uint256)" $+        \sig _ _ input -> case decodeStaticArgs 0 1 input of+          [x]  -> assign (#block % #timestamp) x+          _ -> vmError (BadCheatCode sig),++      action "deal(address,uint256)" $+        \sig _ _ input -> case decodeStaticArgs 0 2 input of+          [a, amt] ->+            forceAddr a "vm.deal: cannot decode target into an address" $ \usr ->+              fetchAccount usr $ \_ -> do+                assign (#env % #contracts % ix usr % #balance) amt+          _ -> vmError (BadCheatCode sig),++      action "assume(bool)" $+        \sig _ _ input -> case decodeStaticArgs 0 1 input of+          [c] -> modifying #constraints ((:) (PEq c (Lit 1)))+          _ -> 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] -> case wordToAddr a of+            Just a'@(LitAddr _) -> fetchAccount a' $ \_ ->+              modifying (#env % #contracts % ix a' % #storage) (writeStorage slot new)+            _ -> vmError (BadCheatCode sig)+          _ -> vmError (BadCheatCode sig),++      action "load(address,bytes32)" $+        \sig outOffset _ input -> case decodeStaticArgs 0 2 input of+          [a, slot] -> case wordToAddr a of+            Just a'@(LitAddr _) -> fetchAccount a' $ \_ ->+              accessStorage a' slot $ \res -> do+                assign (#state % #returndata % word256At (Lit 0)) res+                let buf = writeWord (Lit 0) res (ConcreteBuf "")+                copyBytesToMemory buf (Lit 32) (Lit 0) outOffset+            _ -> vmError (BadCheatCode sig)+          _ -> 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 (V.fromList+                      [ AbiUInt 8 $ into v+                      , AbiBytes 32 (word256Bytes r)+                      , AbiBytes 32 (word256Bytes s)+                      ])+              assign (#state % #returndata) (ConcreteBuf encoded)+              copyBytesToMemory (ConcreteBuf encoded) (Lit . unsafeInto . BS.length $ encoded) (Lit 0) outOffset+          _ -> vmError (BadCheatCode sig),++      action "addr(uint256)" $+        \sig outOffset _ input -> case decodeStaticArgs 0 1 input of+          [sk] -> forceConcrete sk "cannot derive address for a symbolic key" $ \sk' -> do+            let a = EVM.Sign.deriveAddr $ into sk'+            case a of+              Nothing -> vmError (BadCheatCode sig)+              Just address -> do+                let expAddr = litAddr address+                assign (#state % #returndata % word256At (Lit 0)) expAddr+                let buf = ConcreteBuf $ word256Bytes (into address)+                copyBytesToMemory buf (Lit 32) (Lit 0) outOffset+          _ -> vmError (BadCheatCode sig),++      action "prank(address)" $+        \sig _ _ input -> case decodeStaticArgs 0 1 input of+          [addr]  -> case wordToAddr addr of+            Just a -> assign (#config % #overrideCaller) (Just a)+            Nothing -> vmError (BadCheatCode sig)+          _ -> 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 EAddr -> Expr EAddr -> Expr EWord -> W256 -> W256 -> W256 -> W256+  -> [Expr EWord]+  -> (Expr EAddr -> EVM s ())+  -> EVM s ()+delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue+  | isPrecompileAddr xTo+      = forceConcreteAddr2 (xTo, xContext) "Cannot call precompile with symbolic addresses" $+          \(xTo', xContext') ->+            precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs+  | xTo == cheatCode = do+      assign (#state % #stack) xs+      cheat (xInOffset, xInSize) (xOutOffset, xOutSize)+  | otherwise =+      callChecks this gasGiven xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs $+        \xGas -> do+          vm0 <- get+          fetchAccount xTo $ \target -> case target.code of+              UnknownCode _ -> do+                pc <- use (#state % #pc)+                partial $ UnexpectedSymbolicArg pc "call target has unknown code" (wrap [xTo])+              _ -> do+                burn xGas $ do+                  calldata <- readMemory (Lit xInOffset) (Lit xInSize)+                  abi <- maybeLitWord . readBytes 4 (Lit 0) <$> readMemory (Lit xInOffset) (Lit 4)+                  let newContext = CallContext+                                    { target    = xTo+                                    , context   = xContext+                                    , offset    = xOutOffset+                                    , size      = xOutSize+                                    , codehash  = target.codehash+                                    , callreversion = vm0.env.contracts+                                    , subState  = vm0.tx.substate+                                    , abi+                                    , calldata+                                    }+                  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++                  newMemory <- ConcreteMemory <$> VUnboxed.Mutable.new 0+                  zoom #state $ do+                    assign #gas xGas+                    assign #pc 0+                    assign #code (clearInitCode target.code)+                    assign #codeContract xTo+                    assign #stack mempty+                    assign #memory newMemory+                    assign #memorySize 0+                    assign #returndata mempty+                    assign #calldata calldata+                  continue xTo++-- -- * Contract creation++-- EIP 684+collision :: Maybe Contract -> Bool+collision c' = case c' of+  Just c -> c.nonce /= Just 0 || case c.code of+    RuntimeCode (ConcreteRuntimeCode "") -> False+    RuntimeCode (SymbolicRuntimeCode b) -> not $ null b+    _ -> True+  Nothing -> False++create :: (?op :: Word8)+  => Expr EAddr -> Contract+  -> W256 -> Word64 -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM s ()+create self this xSize xGas xValue xs newAddr initCode = do+  vm0 <- get+  if xSize > vm0.block.maxCodeSize * 2+  then do+    assign (#state % #stack) (Lit 0 : xs)+    assign (#state % #returndata) mempty+    vmError $ MaxInitCodeSizeExceeded (vm0.block.maxCodeSize * 2) xSize+  else if this.nonce == Just maxBound+  then do+    assign (#state % #stack) (Lit 0 : xs)+    assign (#state % #returndata) mempty+    pushTrace $ ErrorTrace NonceOverflow+    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) (fmap ((+) 1))+    next+  -- do we have enough balance+  else branch (Expr.gt xValue this.balance) $ \case+      True -> do+        assign (#state % #stack) (Lit 0 : xs)+        assign (#state % #returndata) mempty+        pushTrace $ ErrorTrace $ BalanceTooLow xValue this.balance+        next+        touchAccount self+        touchAccount newAddr+      -- are we overflowing the nonce+      False -> burn xGas $ do+        case parseInitCode initCode of+          Nothing ->+            partial $ 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 (Lit 0) (.balance) oldAcc++              assign (at newAddr) (Just (newContract & #balance .~ oldBal))+              modifying (ix self % #nonce) (fmap ((+) 1))++            let+              resetStorage :: Expr Storage -> Expr Storage+              resetStorage = \case+                  ConcreteStore _ -> ConcreteStore mempty+                  AbstractStore a -> AbstractStore a+                  SStore _ _ p -> resetStorage p+                  GVar _  -> error "unexpected global variable"++            modifying (#env % #contracts % ix newAddr % #storage) resetStorage+            modifying (#env % #contracts % ix newAddr % #origStorage) resetStorage++            transfer self newAddr xValue++            pushTrace (FrameTrace newContext)+            next+            vm1 <- get+            pushTo #frames $ Frame+              { context = newContext+              , state   = vm1.state { stack = xs }+              }++            state <- lift blankState+            assign #state $ state+              { contract     = newAddr+              , codeContract = newAddr+              , code         = c+              , callvalue    = xValue+              , caller       = self+              , gas          = xGas+              }++-- | Parses a raw Buf into an InitCode+--+-- solidity implements constructor args by appending them to the end of+-- the initcode. we support this internally by treating initCode as a+-- concrete region (initCode) followed by a potentially symbolic region+-- (arguments).+--+-- when constructing a contract that has symbolic construcor args, we+-- need to apply some heuristics to convert the (unstructured) initcode+-- in memory into this structured representation. The (unsound, bad,+-- hacky) way that we do this, is by: looking for the first potentially+-- symbolic byte in the input buffer and then splitting it there into code / data.+parseInitCode :: Expr Buf -> Maybe ContractCode+parseInitCode (ConcreteBuf b) = Just (InitCode b mempty)+parseInitCode buf = if V.null conc+                    then Nothing+                    else Just $ InitCode (BS.pack $ V.toList conc) sym+  where+    conc = Expr.concretePrefix buf+    -- unsafeInto: findIndex will always be positive+    sym = Expr.drop (unsafeInto (V.length conc)) buf++-- | Replace a contract's code, like when CREATE returns+-- from the constructor code.+replaceCode :: Expr EAddr -> ContractCode -> EVM s ()+replaceCode target newCode =+  zoom (#env % #contracts % at target) $+    get >>= \case+      Just now -> case now.code of+        InitCode _ _ ->+          put . Just $+            ((initialContract newCode) :: Contract)+              { balance = now.balance+              , nonce = now.nonce+              , storage = now.storage+              }+        RuntimeCode _ ->+          internalError $ "Can't replace code of deployed contract " <> show target+        UnknownCode _ ->+          internalError "Can't replace unknown code"+      Nothing ->+        internalError "Can't replace code of nonexistent contract"++replaceCodeOfSelf :: ContractCode -> EVM s ()+replaceCodeOfSelf newCode = do+  vm <- get+  replaceCode vm.state.contract newCode++resetState :: EVM s ()+resetState = do+  state <- lift blankState+  modify' $ \vm -> vm { result = Nothing, frames = [], state }++-- * VM error implementation++vmError :: EvmError -> EVM s ()+vmError e = finishFrame (FrameErrored e)++partial :: PartialExec -> EVM s ()+partial e = assign #result (Just (Unfinished e))++wrap :: Typeable a => [Expr a] -> [SomeExpr]+wrap = fmap SomeExpr++underrun :: EVM s ()+underrun = vmError 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 EvmError -- ^ 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 s ()+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 (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 (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 internalError(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 (LitAddr 3 ==) touched)) substate'+            revertContracts = assign (#env % #contracts) reversion+            revertSubstate  = assign (#tx % #substate) substate''++          case how of+            -- Case 1: Returning from a call?+            FrameReturned output -> do+              assign (#state % #returndata) output+              copyCallBytesToMemory output outSize outOffset+              reclaimRemainingGasAllowance+              push 1++            -- Case 2: Reverting during a call?+            FrameReverted output -> do+              revertContracts+              revertSubstate+              assign (#state % #returndata) output+              copyCallBytesToMemory output outSize outOffset+              reclaimRemainingGasAllowance+              push 0++            -- Case 3: Error during a call?+            FrameErrored _ -> do+              revertContracts+              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 (fmap ((+) 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+                    pushAddr createe+              case output of+                ConcreteBuf bs ->+                  onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)+                _ ->+                  case Expr.toList output of+                    Nothing -> partial $+                      UnexpectedSymbolicArg+                        oldVm.state.pc+                        "runtime code cannot have an abstract length"+                        (wrap [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 s ()+  -> EVM s ()+accessUnboundedMemoryRange _ 0 continue = continue+accessUnboundedMemoryRange f l continue = do+  m0 <- use (#state % #memorySize)+  fees <- gets (.block.schedule)+  let m1 = 32 * ceilDiv (max m0 (f + l)) 32+  burn (memoryCost fees m1 - memoryCost fees m0) $ do+    assign (#state % #memorySize) m1+    continue++accessMemoryRange+  :: W256+  -> W256+  -> EVM s ()+  -> EVM s ()+accessMemoryRange _ 0 continue = continue+accessMemoryRange offs sz continue =+  case (,) <$> toWord64 offs <*> toWord64 sz of+    Nothing -> vmError IllegalOverflow+    Just (offs64, sz64) ->+      if offs64 + sz64 < sz64+        then vmError IllegalOverflow+        else accessUnboundedMemoryRange offs64 sz64 continue++accessMemoryWord+  :: W256 -> EVM s () -> EVM s ()+accessMemoryWord x = accessMemoryRange x 32++copyBytesToMemory+  :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM s ()+copyBytesToMemory bs size srcOffset memOffset =+  if size == Lit 0 then noop+  else do+    gets (.state.memory) >>= \case+      ConcreteMemory mem ->+        case (bs, size, srcOffset, memOffset) of+          (ConcreteBuf b, Lit size', Lit srcOffset', Lit memOffset') -> do+            let src =+                  if srcOffset' >= unsafeInto (BS.length b) then+                    BS.replicate (unsafeInto size') 0+                  else+                    BS.take (unsafeInto size') $+                    padRight (unsafeInto size') $+                    BS.drop (unsafeInto srcOffset') b++            writeMemory mem (unsafeInto memOffset') src+          _ -> do+            -- copy out and move to symbolic memory+            buf <- freezeMemory mem+            assign (#state % #memory) $+              SymbolicMemory $ copySlice srcOffset memOffset size bs buf+      SymbolicMemory mem ->+        assign (#state % #memory) $+          SymbolicMemory $ copySlice srcOffset memOffset size bs mem++copyCallBytesToMemory+  :: Expr Buf -> Expr EWord -> Expr EWord -> EVM s ()+copyCallBytesToMemory bs size yOffset =+  copyBytesToMemory bs (Expr.min size (bufLength bs)) (Lit 0) yOffset++readMemory :: Expr EWord -> Expr EWord -> EVM s (Expr Buf)+readMemory offset' size' = do+  vm <- get+  case vm.state.memory of+    ConcreteMemory mem -> do+      case (offset', size') of+        (Lit offset, Lit size) -> do+          let memSize :: Word64 = unsafeInto (VUnboxed.Mutable.length mem)+          if size > Expr.maxBytes ||+             offset + size > Expr.maxBytes ||+             offset >= into memSize then+            -- reads past memory are all zeros+            pure $ ConcreteBuf $ BS.replicate (unsafeInto size) 0+          else do+            let pastEnd = (unsafeInto offset + unsafeInto size) - unsafeInto memSize+            let fromMemSize = if pastEnd > 0 then unsafeInto size - pastEnd else unsafeInto size++            buf <- VUnboxed.freeze $ VUnboxed.Mutable.slice (unsafeInto offset) fromMemSize mem+            let dataFromMem = BS.pack $ VUnboxed.toList buf+            pure $ ConcreteBuf $ dataFromMem <> BS.replicate pastEnd 0+        _ -> do+          buf <- freezeMemory mem+          pure $ copySlice offset' (Lit 0) size' buf mempty+    SymbolicMemory mem ->+      pure $ copySlice offset' (Lit 0) size' mem mempty++-- * Tracing++withTraceLocation :: TraceData -> EVM s Trace+withTraceLocation x = do+  vm <- get+  let this = fromJust $ currentContract vm+  pure Trace+    { tracedata = x+    , contract = this+    , opIx = fromMaybe 0 $ this.opIxMap SV.!? vm.state.pc+    }++pushTrace :: TraceData -> EVM s ()+pushTrace x = do+  trace <- withTraceLocation x+  modifying #traces $+    \t -> Zipper.children $ Zipper.insert (Node trace []) t++insertTrace :: TraceData -> EVM s ()+insertTrace x = do+  trace <- withTraceLocation x+  modifying #traces $+    \t -> Zipper.nextSpace $ Zipper.insert (Node trace []) t++popTrace :: EVM s ()+popTrace =+  modifying #traces $+    \t -> case Zipper.parent t of+            Nothing -> internalError "internal internalError(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 s -> Forest Trace+traceForest vm = zipperRootForest vm.traces++traceForest' :: Expr End -> Forest Trace+traceForest' (Success _ (Traces f _) _ _) = f+traceForest' (Partial _ (Traces f _) _) = f+traceForest' (Failure _ (Traces f _) _) = f+traceForest' (ITE {}) = internalError"Internal Error: ITE does not contain a trace"+traceForest' (GVar {}) = internalError"Internal Error: Unexpected GVar"++traceContext :: Expr End -> Map (Expr EAddr) Contract+traceContext (Success _ (Traces _ c) _ _) = c+traceContext (Partial _ (Traces _ c) _) = c+traceContext (Failure _ (Traces _ c) _) = c+traceContext (ITE {}) = internalError"Internal Error: ITE does not contain a trace"+traceContext (GVar {}) = internalError"Internal Error: Unexpected GVar"++traceTopLog :: [Expr Log] -> EVM s ()+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 _) : _) = internalError "unexpected global variable"++-- * Stack manipulation++push :: W256 -> EVM s ()+push = pushSym . Lit++pushSym :: Expr EWord -> EVM s ()+pushSym x = #state % #stack %= (x :)++pushAddr :: Expr EAddr -> EVM s ()+pushAddr (LitAddr x) = #state % #stack %= (Lit (into x) :)+pushAddr x@(SymAddr _) = #state % #stack %= (WAddr x :)+pushAddr (GVar _) = internalError "Unexpected GVar"++stackOp1+  :: (?op :: Word8)+  => Word64+  -> (Expr EWord -> Expr EWord)+  -> EVM s ()+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 s ()+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 s ()+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 s -> a) -> EVM s a+use' f = do+  vm <- get+  pure (f vm)++checkJump :: Int -> [Expr EWord] -> EVM s ()+checkJump x xs = noJumpIntoInitData x $ do+  vm <- get+  case isValidJumpDest vm x of+    True -> do+      #state % #stack .= xs+      #state % #pc .= x+    False -> vmError BadJumpDestination++-- fails with partial if we're trying to jump into the symbolic region of an `InitCode`+noJumpIntoInitData :: Int -> EVM s () -> EVM s ()+noJumpIntoInitData idx cont = do+  vm <- get+  case vm.state.code of+    -- init code is totally concrete, so we don't return partial if we're+    -- jumping beyond the range of `ops`+    InitCode _ (ConcreteBuf "") -> cont+    -- init code has a symbolic region, so check if we're trying to jump into+    -- the symbolic region and return partial if we are+    InitCode ops _ -> if idx > BS.length ops+                      then partial $ JumpIntoSymbolicCode vm.state.pc idx+                      else cont+    -- we're not executing init code, so nothing to check here+    _ -> cont++isValidJumpDest :: VM s -> Int -> Bool+isValidJumpDest vm x = let+    code = vm.state.code+    self = vm.state.codeContract+    contract = fromMaybe+      (internalError "self not found in current contracts")+      (Map.lookup self vm.env.contracts)+    op = case code of+      UnknownCode _ -> internalError "Cannot analyze jumpdests for unknown code"+      InitCode ops _ -> BS.indexMaybe ops x+      RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x+      RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByte+  in case op of+       Nothing -> False+       Just b -> 0x5b == b && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap SV.! x))++opSize :: Word8 -> Int+opSize x | x >= 0x60 && x <= 0x7f = into 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 -> SV.Vector Int+mkOpIxMap (UnknownCode _) = internalError "Cannot build opIxMap for unknown code"+mkOpIxMap (InitCode conc _)+  = SV.create $ SV.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 >> SV.write v i j)+        go v (1, !i, !j, !m) _ =+          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> SV.write v i j)+        go v (0, !i, !j, !m) _ =+          {- Other op. -}         (0,            i + 1, j + 1, m >> SV.write v i j)+        go v (n, !i, !j, !m) _ =+          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)++mkOpIxMap (RuntimeCode (ConcreteRuntimeCode ops)) =+  mkOpIxMap (InitCode ops mempty) -- a bit hacky++mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))+  = SV.create $ SV.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 maybeLitByte x of+          Just x' -> if x' >= 0x60 && x' <= 0x7f+            -- start of PUSH op --+                     then (x' - 0x60 + 1, i + 1, j,     m >> SV.write v i j)+            -- other data --+                     else (0,             i + 1, j + 1, m >> SV.write v i j)+          _ -> internalError $ "cannot analyze symbolic code:\nx: " <> show x <> " i: " <> show i <> " j: " <> show j++        go v (1, !i, !j, !m) _ =+          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> SV.write v i j)+        go v (n, !i, !j, !m) _ =+          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)+++vmOp :: VM s -> Maybe Op+vmOp vm =+  let i  = vm ^. #state % #pc+      code' = vm ^. #state % #code+      (op, pushdata) = case code' of+        UnknownCode _ -> internalError "cannot get op from unknown code"+        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 (internalError "unexpected symbolic code") . maybeLitByte $ xs' V.! i , V.toList $ V.drop i xs')+  in if (opslen code' < i)+     then Nothing+     else Just (readOp op pushdata)++vmOpIx :: VM s -> Maybe Int+vmOpIx vm =+  do self <- currentContract vm+     self.opIxMap SV.!? vm.state.pc++-- Maps operation indicies into a pair of (bytecode index, operation)+mkCodeOps :: ContractCode -> V.Vector (Int, Op)+mkCodeOps contractCode =+  let l = case contractCode of+            UnknownCode _ -> internalError "Cannot make codeOps for unknown code"+            InitCode bytes _ ->+              LitByte <$> (BS.unpack bytes)+            RuntimeCode (ConcreteRuntimeCode ops) ->+              LitByte <$> (BS.unpack $ stripBytecodeMetadata ops)+            RuntimeCode (SymbolicRuntimeCode ops) ->+              stripBytecodeMetadataSym $ V.toList ops+  in V.fromList . toList $ go 0 l+  where+    go !i !xs =+      case uncons xs of+        Nothing ->+          mempty+        Just (x, xs') ->+          let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByte x+              j = opSize x'+          in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)++-- * Gas cost calculation helpers++-- Gas cost function for CALL, transliterated from the Yellow Paper.+costOfCall+  :: FeeSchedule Word64+  -> Bool -> Expr EWord -> Word64 -> Word64 -> Expr EAddr+  -> EVM s (Word64, Word64)+costOfCall (FeeSchedule {..}) recipientExists (Lit 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 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)+-- calls are free if value is symbolic :)+costOfCall _ _ _ _ _ _ = pure (0,0)++-- Gas cost of create, including hash cost if needed+costOfCreate+  :: FeeSchedule Word64+  -> Word64 -> W256 -> Bool -> (Word64, Word64)+costOfCreate (FeeSchedule {..}) availableGas size hashNeeded = (createCost, initGas)+  where+    byteCost   = if hashNeeded then g_sha3word + g_initcodeword else g_initcodeword+    createCost = g_create + codeCost+    codeCost   = byteCost * (ceilDiv (unsafeInto size) 32)+    initGas    = allButOne64th (availableGas - createCost)++concreteModexpGasFee :: ByteString -> Word64+concreteModexpGasFee input =+  if lenb < into (maxBound :: Word32) &&+     (lene < into (maxBound :: Word32) || (lenb == 0 && lenm == 0)) &&+     lenm < into (maxBound :: Word64)+  then+    max 200 ((multiplicationComplexity * iterCount) `div` 3)+  else+    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 (unsafeInto $ max lenb lenm) 8+    multiplicationComplexity = nwords * nwords+    iterCount' :: Word64+    iterCount' | lene <= 32 && ez = 0+               | lene <= 32 = unsafeInto (log2 e')+               | e' == 0 = 8 * (unsafeInto lene - 32)+               | otherwise = unsafeInto (log2 e') + 8 * (unsafeInto lene - 32)+    iterCount = max iterCount' 1++-- Gas cost of precompiles+costOfPrecompile :: FeeSchedule Word64 -> Addr -> Expr Buf -> Word64+costOfPrecompile (FeeSchedule {..}) precompileAddr input =+  let errorDynamicSize = internalError "precompile input cannot have a dynamic size"+      inputLen = case input of+                   ConcreteBuf bs -> unsafeInto $ BS.length bs+                   AbstractBuf _ -> errorDynamicSize+                   buf -> case bufLength buf of+                            Lit l -> unsafeInto l -- TODO: overflow+                            _ -> errorDynamicSize+  in case precompileAddr of+    -- ECRECOVER+    0x1 -> 3000+    -- SHA2-256+    0x2 -> (((inputLen + 31) `div` 32) * 12) + 60+    -- RIPEMD-160+    0x3 -> (((inputLen + 31) `div` 32) * 120) + 600+    -- IDENTITY+    0x4 -> (((inputLen + 31) `div` 32) * 3) + 15+    -- MODEXP+    0x5 -> case input of+             ConcreteBuf i -> concreteModexpGasFee i+             _ -> internalError "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 * (unsafeInto $ asInteger $ lazySlice 0 4 i)+             _ -> internalError "Unsupported symbolic blake2 gas calc"+    _ -> internalError $ "unimplemented precompiled contract " ++ show precompileAddr++-- Gas cost of memory expansion+memoryCost :: FeeSchedule Word64 -> Word64 -> Word64+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 (UnknownCode a) = CodeHash a+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 (UnknownCode _) = internalError "Cannot produce concrete opslen for unknown code"+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 (UnknownCode a) = CodeSize a+codelen c@(InitCode {}) = case toBuf c of+  Just b -> bufLength b+  Nothing -> internalError "impossible"+-- these are never going to be negative so unsafeInto is fine here+codelen (RuntimeCode (ConcreteRuntimeCode ops)) = Lit . unsafeInto $ BS.length ops+codelen (RuntimeCode (SymbolicRuntimeCode ops)) = Lit . unsafeInto $ length ops++toBuf :: ContractCode -> Maybe (Expr Buf)+toBuf (UnknownCode _) = Nothing+toBuf (InitCode ops args) = Just $ ConcreteBuf ops <> args+toBuf (RuntimeCode (ConcreteRuntimeCode ops)) = Just $ ConcreteBuf ops+toBuf (RuntimeCode (SymbolicRuntimeCode ops)) = Just $ Expr.fromList ops++codeloc :: EVM s CodeLocation+codeloc = do+  vm <- get+  pure (vm.state.contract, vm.state.pc)++createAddress :: Expr EAddr -> Maybe W64 -> EVM s (Expr EAddr)+createAddress (LitAddr a) (Just n) = pure $ Concrete.createAddress a n+createAddress (GVar _) _ = internalError "Unexpected GVar"+createAddress _ _ = freshSymAddr++create2Address :: Expr EAddr -> W256 -> ByteString -> EVM s (Expr EAddr)+create2Address (LitAddr a) s b = pure $ Concrete.create2Address a s b+create2Address (SymAddr _) _ _ = freshSymAddr+create2Address (GVar _) _ _ = internalError "Unexpected GVar"++freshSymAddr :: EVM s (Expr EAddr)+freshSymAddr = do+  modifying (#env % #freshAddresses) (+ 1)+  n <- use (#env % #freshAddresses)+  pure $ SymAddr ("freshSymAddr" <> (pack $ show n))++isPrecompileAddr :: Expr EAddr -> Bool+isPrecompileAddr = \case+  LitAddr a -> 0x0 < a && a <= 0x09+  SymAddr _ -> False+  GVar _ -> internalError "Unexpected GVar"++-- * 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++writeMemory :: MutableMemory s -> Int -> ByteString -> EVM s ()+writeMemory memory offset buf = do+  memory' <- expandMemory (offset + BS.length buf)+  mapM_ (uncurry (VUnboxed.Mutable.write memory'))+        (zip [offset..] (BS.unpack buf))+  where+  expandMemory targetSize = do+    let toAlloc = targetSize - VUnboxed.Mutable.length memory+    if toAlloc > 0 then do+      memory' <- VUnboxed.Mutable.grow memory toAlloc+      assign (#state % #memory) (ConcreteMemory memory')+      pure memory'+    else+      pure memory++freezeMemory :: MutableMemory s -> EVM s (Expr Buf)+freezeMemory memory =+  ConcreteBuf . BS.pack . VUnboxed.toList <$> VUnboxed.freeze memory