content: {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE TemplateHaskell #-}
  
  module EVM where
  
  import Prelude hiding (exponent, Foldable(..))
  
  import Optics.Core
  import Optics.State
  import Optics.State.Operators
  import Optics.Zoom
  
  import EVM.ABI
  import EVM.Expr (readStorage, concStoreContains, writeStorage, readByte, readWord, writeWord,
    writeByte, bufLength, indexWord, readBytes, copySlice, wordToAddr, maybeLitByteSimp, maybeLitWordSimp, maybeLitAddrSimp)
  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.Types qualified as Expr (Expr(Gas))
  import EVM.Sign qualified
  import EVM.Concrete qualified as Concrete
  import EVM.CheatsTH
  import EVM.Effects (Config (..))
  
  import Control.Monad (unless, when)
  import Control.Monad.ST (ST)
  import Control.Monad.State.Strict (MonadState, State, get, gets, lift, modify', put)
  import Data.Bits (FiniteBits, countLeadingZeros, finiteBitSize)
  import Data.ByteArray qualified as BA
  import Data.ByteString (ByteString)
  import Data.ByteString qualified as BS
  import Data.ByteString.Char8 qualified as BS8
  import Data.ByteString.Base16 qualified as BS16
  import Data.ByteString.Lazy (fromStrict)
  import Data.ByteString.Lazy qualified as LS
  import Data.ByteString.Char8 qualified as Char8
  import Data.DoubleWord (Int256, Word256)
  import Data.Either (partitionEithers)
  import Data.Either.Extra (maybeToEither)
  import Data.Foldable (toList, Foldable(..))
  import Data.List (find, isPrefixOf)
  import Data.List.Split (splitOn)
  import Data.Map.Strict (Map)
  import Data.Map.Strict qualified as Map
  import Data.Maybe (fromMaybe, fromJust, isJust, isNothing, mapMaybe)
  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 VS
  import Data.Vector.Storable.Mutable qualified as VS.Mutable
  import Data.Vector.Storable.ByteString (vectorToByteString, byteStringToVector)
  import Data.Word (Word8, Word32, Word64)
  import Text.Read (readMaybe)
  import Witch (into, tryFrom, unsafeInto, tryInto)
  
  import Crypto.Hash (Digest, SHA256, RIPEMD160)
  import Crypto.Hash qualified as Crypto
  import Crypto.Number.ModArithmetic (expFast)
  
  blankState :: VMOps t => ST s (FrameState t s)
  blankState = do
    memory <- ConcreteMemory <$> VS.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          = initialGas
      , returndata   = mempty
      , static       = False
      , overrideCaller = Nothing
      , resetCaller  = 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 t s -> Maybe Contract
  currentContract vm =
    Map.lookup vm.state.codeContract vm.env.contracts
  
  -- * Data constructors
  --
  makeVm :: VMOps t => VMOpts t -> ST s (VM t 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 <$> VS.Mutable.new 0
    pure $ setEIP4788Storage o $ 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 mempty
        , isCreate = o.create
        , txReversion = Map.fromList ((o.address,o.contract):o.otherContracts)
        }
      , logs = []
      , traces = Zipper.fromForest []
      , block = block
      , 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
        , overrideCaller = Nothing
        , resetCaller = False
        }
      , env = env
      , burned = initialGas
      , constraints = snd o.calldata
      , iterations = mempty
      , config = RuntimeConfig
        { allowFFI = o.allowFFI
        , baseState = o.baseState
        }
      , forks = Seq.singleton (ForkState env block mempty "")
      , currentFork = 0
      , labels = mempty
      , osEnv = mempty
      , freshVar = 0
      , exploreDepth = 0
      , keccakPreImgs = fromList []
      , pathsVisited = mempty
      }
      where
      env = Env
        { chainId = o.chainId
        , contracts = Map.fromList ((o.address,o.contract):o.otherContracts)
        , freshAddresses = o.freshAddresses
        , freshGasVals = 0
        }
      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
        }
  
  -- https://eips.ethereum.org/EIPS/eip-4788
  setEIP4788Storage :: VMOpts t -> VM t s -> VM t s
  setEIP4788Storage o vm = do
    let beaconRootsAddress = LitAddr 0x000F3df6D732807Ef1319fB7B8bB8522d0Beac02
    case Map.lookup beaconRootsAddress vm.env.contracts of
      Just beaconRootsContract -> do
        -- https://eips.ethereum.org/EIPS/eip-4788#pseudocode
        -- https://eips.ethereum.org/EIPS/eip-4788#block-processing
        -- > Clients may decide to omit an explicit EVM call and directly set the
        -- > storage values. Note: While this is a valid optimization for Ethereum
        -- > mainnet, it could be problematic on non-mainnet situations in case
        -- > a different contract is used.
        let
          historyBufferLength = 8191
          timestampIdx = Expr.mod o.timestamp (Lit historyBufferLength)
          rootIdx = Expr.add timestampIdx (Lit historyBufferLength)
          storage =
            Expr.writeStorage timestampIdx o.timestamp .
            Expr.writeStorage rootIdx (Lit o.beaconRoot) $
            beaconRootsContract.storage
        vm {
          env = vm.env {
            contracts = Map.insert beaconRootsAddress
                                   (beaconRootsContract { storage } :: Contract)
                                   vm.env.contracts
          }
        }
      Nothing -> vm
  
  -- | Initialize an abstract contract with unknown code
  unknownContract :: Expr EAddr -> Contract
  unknownContract addr = Contract
    { code        = UnknownCode addr
    , storage     = AbstractStore addr Nothing
    , tStorage    = AbstractStore addr Nothing
    , origStorage = AbstractStore addr Nothing
    , 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 Nothing
    , tStorage    = AbstractStore addr Nothing
    , origStorage = AbstractStore addr Nothing
    , 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
    , tStorage    = 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 t s ()
  next = modifying' (#state % #pc) (+ (opSize ?op))
  
  getOpW8 :: forall (t :: VMType) s . FrameState t s -> Word8
  getOpW8 state = case state.code of
        UnknownCode _ -> internalError "Cannot execute unknown code"
        InitCode conc _ -> BS.index conc state.pc
        RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs state.pc
        RuntimeCode (SymbolicRuntimeCode ops) ->
          fromMaybe (internalError "could not analyze symbolic code") $
            maybeLitByteSimp $ ops V.! state.pc
  
  getOpName :: forall (t :: VMType) s . FrameState t s -> [Char]
  getOpName state = intToOpName $ fromEnum $ getOpW8 state
  
  -- | Executes the EVM one step
  exec1 :: forall (t :: VMType) s. (VMOps t, Typeable t) => Config ->  EVM t s ()
  exec1 conf = 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 = maybeLitAddrSimp self
  
    if isJust litSelf && (fromJust litSelf) > 0x0 && (fromJust litSelf) <= 0xa then do
      -- call to precompile
      let ?op = 0x00 -- dummy value
      let calldatasize = bufLength vm.state.calldata
      copyBytesToMemory vm.state.calldata calldatasize (Lit 0) (Lit 0)
      executePrecompile (fromJust litSelf) vm.state.gas (Lit 0) calldatasize (Lit 0) (Lit 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 -> unexpectedSymArg "precompile returned a symbolic value" [e]
        _ ->
          underrun
  
    else if vm.state.pc >= opslen vm.state.code
      then doStop
  
      else do
        let ?conf = conf
        let ?op = getOpW8 vm.state
        case getOp (?op) of
  
          OpPush0 -> {-# SCC "OpPush0" #-} do
            limitStack 1 $
              burn g_base $ do
                next
                pushSym (Lit 0)
  
          OpPush n' -> {-# SCC "OpPushN" #-} 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 -> {-# SCC "OpDup" #-}
            case preview (ix (into i - 1)) stk of
              Nothing -> underrun
              Just y ->
                limitStack 1 $
                  burn g_verylow $ do
                    next
                    pushSym y
  
          OpSwap i -> {-# SCC "OpSwap" #-}
            case (stk ^? ix_i, stk ^? ix_0) of
              (Just ei, Just e0) ->
                burn g_verylow $ do
                  next
                  zoom (#state % #stack) $ do
                    ix_i .= e0
                    ix_0 .= ei
              _ -> underrun
            where
              (ix_i, ix_0) = (ix (into i), ix 0)
  
          OpLog n -> {-# SCC "OpLog" #-}
            notStatic $
            case stk of
              (xOffset:xSize:xs) ->
                if length xs < (into n)
                then underrun
                else do
                  bytes <- readMemory xOffset xSize
                  let (topics, xs') = splitAt (into n) xs
                      logs'         = (LogEntry (WAddr self) bytes topics) : vm.logs
                  burnLog xSize n $
                    accessMemoryRange xOffset xSize $ do
                      traceTopLog logs'
                      next
                      assign' (#state % #stack) xs'
                      assign #logs logs'
              _ ->
                underrun
  
          OpStop -> {-# SCC "OpStop" #-} doStop
  
          OpAdd -> {-# SCC "OpAdd" #-} stackOp2 g_verylow Expr.add
          OpMul -> {-# SCC "OpMul" #-} stackOp2 g_low Expr.mul
          OpSub -> {-# SCC "OpSub" #-} stackOp2 g_verylow Expr.sub
  
          OpDiv -> {-# SCC "OpDiv" #-} stackOp2 g_low Expr.div
  
          OpSdiv -> {-# SCC "OpSdiv" #-} stackOp2 g_low Expr.sdiv
  
          OpMod -> {-# SCC "OpMod" #-} stackOp2 g_low Expr.mod
  
          OpSmod -> {-# SCC "OpSmod" #-} stackOp2 g_low Expr.smod
          OpAddmod -> {-# SCC "OpAddmod" #-} stackOp3 g_mid Expr.addmod
          OpMulmod -> {-# SCC "OpMulmod" #-} stackOp3 g_mid Expr.mulmod
  
          OpLt -> {-# SCC "OpLt" #-} stackOp2 g_verylow Expr.lt
          OpGt -> {-# SCC "OpGt" #-} stackOp2 g_verylow Expr.gt
          OpSlt -> {-# SCC "OpSlt" #-} stackOp2 g_verylow Expr.slt
          OpSgt -> {-# SCC "OpSgt" #-} stackOp2 g_verylow Expr.sgt
  
          OpEq -> {-# SCC "OpEq" #-} stackOp2 g_verylow Expr.eq
          OpIszero -> {-# SCC "OpIszero" #-} stackOp1 g_verylow Expr.iszero
  
          OpAnd -> {-# SCC "OpAnd" #-} stackOp2 g_verylow Expr.and
          OpOr -> {-# SCC "OpOr" #-} stackOp2 g_verylow Expr.or
          OpXor -> {-# SCC "OpXor" #-} stackOp2 g_verylow Expr.xor
          OpNot -> {-# SCC "OpNot" #-} stackOp1 g_verylow Expr.not
  
          OpByte -> {-# SCC "OpByte" #-} stackOp2 g_verylow (\i w -> Expr.padByte $ Expr.indexWord i w)
  
          OpShl -> {-# SCC "OpShl" #-} stackOp2 g_verylow Expr.shl
          OpShr -> {-# SCC "OpShr" #-} stackOp2 g_verylow Expr.shr
          OpSar -> {-# SCC "OpSar" #-} stackOp2 g_verylow Expr.sar
  
          -- more accurately referred to as KECCAK
          OpSha3 -> {-# SCC "OpSha3" #-}
            case stk of
              xOffset:xSize:xs ->
                burnSha3 xSize $
                  accessMemoryRange xOffset xSize $ do
                    hash <- readMemory xOffset xSize >>= \case
                      orig@(ConcreteBuf bs) ->
                        whenSymbolicElse
                          (pure $ Keccak orig)
                          (do
                            let kc = keccak' bs
                            modifying #keccakPreImgs (insert (bs, kc))
                            pure $ Lit kc
                          )
                      buf -> pure $ Keccak buf
                    next
                    assign' (#state % #stack) (hash : xs)
              _ -> underrun
  
          OpAddress -> {-# SCC "OpAddress" #-}
            limitStack 1 $
              burn g_base (next >> pushAddr self)
  
          OpBalance -> {-# SCC "OpBalance" #-}
            case stk of
              x:xs -> forceAddr x (freshVarFallback xs) $ \a ->
                accessAndBurn a $
                  fetchAccountWithFallback a (freshVarFallback xs) $ \c -> do
                    next
                    assign' (#state % #stack) xs
                    pushSym c.balance
              [] -> underrun
  
          OpOrigin -> {-# SCC "OpOrigin" #-}
            limitStack 1 . burn g_base $
              next >> pushAddr vm.tx.origin
  
          OpCaller -> {-# SCC "OpCaller" #-}
            limitStack 1 . burn g_base $
              next >> pushAddr vm.state.caller
  
          OpCallvalue -> {-# SCC "OpCallvalue" #-}
            limitStack 1 . burn g_base $
              next >> pushSym vm.state.callvalue
  
          OpCalldataload -> {-# SCC "OpCalldataload" #-} stackOp1 g_verylow $
            \ind -> Expr.readWord ind vm.state.calldata
  
          OpCalldatasize -> {-# SCC "OpCalldatasize" #-}
            limitStack 1 . burn g_base $
              next >> pushSym (bufLength vm.state.calldata)
  
          OpCalldatacopy -> {-# SCC "OpCalldatacopy" #-}
            case stk of
              xTo:xFrom:xSize:xs ->
                burnCalldatacopy xSize $
                  accessMemoryRange xTo xSize $ do
                    next
                    assign' (#state % #stack) xs
                    copyBytesToMemory vm.state.calldata xSize xFrom xTo
              _ -> underrun
  
          OpCodesize -> {-# SCC "OpCodesize" #-}
            limitStack 1 . burn g_base $
              next >> pushSym (codelen vm.state.code)
  
          OpCodecopy -> {-# SCC "OpCodecopy" #-}
            case stk of
              memOffset:codeOffset:n:xs ->
                burnCodecopy n $ do
                  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"
              _ -> underrun
  
          OpGasprice -> {-# SCC "OpGasprice" #-}
            limitStack 1 . burn g_base $
              next >> push vm.tx.gasprice
  
          OpExtcodesize -> {-# SCC "OpExtcodesize" #-}
            case stk of
              x':xs -> forceAddr x' (freshVarFallback xs) $ \x -> do
                let impl = accessAndBurn x $
                             fetchAccountWithFallback x (freshVarFallback xs) $ \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 -> {-# SCC "OpExtcodecopy" #-}
            case stk of
              extAccount':memOffset:codeOffset:codeSize:xs ->
                forceAddr extAccount' (unexpectedSymArgW "EXTCODECOPY") $ \extAccount -> do
                  burnExtcodecopy extAccount codeSize $
                    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 -> unexpectedSymArg "Cannot copy from unknown code at" [extAccount]
              _ -> underrun
  
          OpReturndatasize -> {-# SCC "OpReturndatasize" #-}
            limitStack 1 . burn g_base $
              next >> pushSym (bufLength vm.state.returndata)
  
          OpReturndatacopy -> {-# SCC "OpReturndatacopy" #-}
            case stk of
              xTo:xFrom:xSize:xs ->
                burnReturndatacopy xSize $
                  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, xSize) of
                      (Lit f, Lit l, Lit sz) ->
                        jump $ l < f + sz || f + sz < f
                      _ -> do
                        let oob = Expr.lt (bufLength vm.state.returndata) (Expr.add xFrom xSize)
                            overflow = Expr.lt (Expr.add xFrom xSize) (xFrom)
                        branch conf.maxDepth (Expr.or oob overflow) jump
              _ -> underrun
  
          OpExtcodehash -> {-# SCC "OpExtcodehash" #-}
            case stk of
              x':xs -> forceAddr x' (freshVarFallback xs) $ \x ->
                accessAndBurn x $ do
                  fetchAccountWithFallback x (freshVarFallback xs) $ \c -> do
                     next
                     assign' (#state % #stack) xs
                     if accountEmpty c
                       then push (W256 0)
                       else case view bytecode c of
                              Just b -> pushSym $ keccak b
                              Nothing -> pushSym $ CodeHash x
              [] ->
                underrun
  
          OpBlockhash -> {-# SCC "OpBlockhash" #-} do
            stackOp1 g_blockhash $ \case
              Lit i -> case vm.block.number of
                Lit vmBlockNumber ->
                  if i + 256 < vmBlockNumber || i >= vmBlockNumber
                  -- blockhash is 0 if block is too old or too new as per EVM spec
                  then Lit 0
                  -- We adopt the fake block hash scheme of the VMTests,
                  -- so that blockhash(i) is the hash of i as decimal ASCII.
                  else fakeBlockHash i
                -- For symbolic block numbers, we don't know if it's too old or too new,
                -- so we return fake block hash
                _ -> fakeBlockHash i
              i -> BlockHash i
              where
                fakeBlockHash i = (into i :: Integer) & show & Char8.pack & keccak' & Lit
  
          OpCoinbase -> {-# SCC "OpCoinbase" #-}
            limitStack 1 . burn g_base $
              next >> pushAddr vm.block.coinbase
  
          OpTimestamp -> {-# SCC "OpTimestamp" #-}
            limitStack 1 . burn g_base $
              next >> pushSym vm.block.timestamp
  
          OpNumber -> {-# SCC "OpNumber" #-}
            limitStack 1 . burn g_base $
              next >> pushSym vm.block.number
  
          OpPrevRandao -> {-# SCC "OpPrevRandao" #-} do
            limitStack 1 . burn g_base $
              next >> push vm.block.prevRandao
  
          OpGaslimit -> {-# SCC "OpGaslimit" #-}
            limitStack 1 . burn g_base $
              next >> push (into vm.block.gaslimit)
  
          OpChainid -> {-# SCC "OpChainid" #-}
            limitStack 1 . burn g_base $
              next >> push vm.env.chainId
  
          OpSelfbalance -> {-# SCC "OpSelfbalance" #-}
            limitStack 1 . burn g_low $
              next >> pushSym this.balance
  
          OpBaseFee -> {-# SCC "OpBaseFee" #-}
            limitStack 1 . burn g_base $
              next >> push vm.block.baseFee
  
          OpBlobhash -> {-# SCC "OpBlobhash" #-}
            stackOp1 g_verylow $ \_ -> Lit 0
  
          OpBlobBaseFee -> {-# SCC "OpBlobBaseFee" #-}
            limitStack 1 . burn g_base $
              next >> push 0
  
          OpPop -> {-# SCC "OpPop" #-}
            case stk of
              _:xs -> burn g_base (next >> assign' (#state % #stack) xs)
              _    -> underrun
  
          OpMload -> {-# SCC "OpMload" #-}
            case stk of
              x:xs ->
                burn g_verylow $
                  accessMemoryWord x $ do
                    next
                    buf <- readMemory x (Lit 32)
                    let w = Expr.readWordFromBytes (Lit 0) buf
                    assign' (#state % #stack) (w : xs)
              _ -> underrun
  
  
          OpMcopy -> {-# SCC "OpMcopy" #-}
            case stk of
              dstOff:srcOff:sz:xs ->  do
                case sz of
                  Lit sz' -> do
                    let words_copied = (sz' + 31) `div` 32
                    let g_mcopy = 3*words_copied -- memory access cost is part of accessMemoryRange
                    burn (g_verylow + (unsafeInto g_mcopy)) $
                      accessMemoryRange srcOff sz $ accessMemoryRange dstOff sz $ do
                        next
                        mcopy sz srcOff dstOff
                  _ -> do
                    -- symbolic, ignore gas
                    next
                    mcopy sz srcOff dstOff
                assign' (#state % #stack) xs
              _ -> underrun
              where
              mcopy sz srcOff dstOff = do
                    m <- gets (.state.memory)
                    case m of
                      ConcreteMemory _ -> do
                        buf <- readMemory srcOff sz
                        copyBytesToMemory buf sz (Lit 0) dstOff
                      SymbolicMemory mem -> do
                        assign (#state % #memory) (SymbolicMemory $ copySlice srcOff dstOff sz mem mem)
  
          OpMstore -> {-# SCC "OpMstore" #-}
            case stk of
              x:y:xs ->
                burn g_verylow $
                  accessMemoryWord x $ do
                    next
                    gets (.state.memory) >>= \case
                      ConcreteMemory mem -> do
                        case y of
                          Lit w ->
                            copyBytesToMemory (ConcreteBuf (word256Bytes w)) (Lit 32) (Lit 0) x
                          _ -> do
                            -- copy out and move to symbolic memory
                            buf <- freezeMemory mem
                            assign (#state % #memory) (SymbolicMemory $ writeWord x y buf)
                      SymbolicMemory mem ->
                        assign (#state % #memory) (SymbolicMemory $ writeWord x y mem)
                    assign' (#state % #stack) xs
              _ -> underrun
  
          OpMstore8 -> {-# SCC "OpMstore8" #-}
            case stk of
              x:y:xs ->
                burn g_verylow $
                  accessMemoryRange x (Lit 1) $ do
                    let yByte = indexWord (Lit 31) y
                    next
                    gets (.state.memory) >>= \case
                      ConcreteMemory mem -> do
                        case yByte of
                          LitByte byte ->
                            copyBytesToMemory (ConcreteBuf (BS.pack [byte])) (Lit 1) (Lit 0) x
                          _ -> do
                            -- copy out and move to symbolic memory
                            buf <- freezeMemory mem
                            assign (#state % #memory) (SymbolicMemory $ writeByte x yByte buf)
                      SymbolicMemory mem ->
                        assign (#state % #memory) (SymbolicMemory $ writeByte x yByte mem)
  
                    assign' (#state % #stack) xs
              _ -> underrun
  
          OpSload -> {-# SCC "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 -> {-# SCC "OpSstore" #-}
            notStatic $
            case stk of
              x:new:xs ->
                accessStorage self x $ \current -> do
                  ensureGas g_callstipend $ do
                    let
                      original =
                        case Expr.concKeccakSimpExpr $ SLoad x this.origStorage of
                          Lit v -> v
                          _ -> 0
                      storage_cost =
                        case (maybeLitWordSimp current, maybeLitWordSimp 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 (maybeLitWordSimp current, maybeLitWordSimp 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
  
          OpTload -> {-# SCC "OpTload" #-}
            case stk of
              x:xs -> do
                burn g_warm_storage_read $
                  accessTStorage self x $ \y -> do
                    next
                    assign' (#state % #stack) (y:xs)
              _ -> underrun
  
          OpTstore -> {-# SCC "OpTstore" #-}
            notStatic $
            case stk of
              x:new:xs ->
                burn g_sload $ do
                  next
                  modifying (#env % #contracts % ix self % #tStorage) (writeStorage x new)
                  assign' (#state % #stack) xs
              _ -> underrun
  
          OpJump -> {-# SCC "OpJump" #-}
            case stk of
              x:xs ->
                burn g_mid $ forceConcreteLimitSz x 2 "JUMP: symbolic jumpdest" $ \x' ->
                  case tryInto x' of
                    Left _ -> vmError BadJumpDestination
                    Right i -> checkJump i xs
              _ -> underrun
  
          OpJumpi -> {-# SCC "OpJumpi" #-}
            case stk of
              x:y:xs -> forceConcreteLimitSz x 2 "JUMPI: symbolic jumpdest" $ \x' ->
                burn g_high $
                  let jump :: Bool -> EVM t s ()
                      jump False = assign' (#state % #stack) xs >> next
                      jump _    = case tryInto x' of
                        Left _ -> vmError BadJumpDestination
                        Right i -> checkJump i xs
                  in branch conf.maxDepth y jump
              _ -> underrun
  
          OpPc -> {-# SCC "OpPc" #-}
            limitStack 1 . burn g_base $
              next >> push (unsafeInto vm.state.pc)
  
          OpMsize -> {-# SCC "OpMsize" #-}
            limitStack 1 . burn g_base $
              next >> push (into vm.state.memorySize)
  
          OpGas -> {-# SCC "OpGas" #-}
            limitStack 1 . burn g_base $
              next >> pushGas
  
          OpJumpdest -> {-# SCC "OpJumpdest" #-} burn g_jumpdest next
  
          OpExp -> {-# SCC "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 ->
                burnExp exponent $ do
                  next
                  assign' (#state % #stack) $ Expr.exp base exponent : xs
              _ -> underrun
  
          OpSignextend -> {-# SCC "OpSignextend" #-} stackOp2 g_low Expr.sex
  
          OpCreate -> {-# SCC "OpCreate" #-}
            notStatic $
            case stk of
              xValue:xOffset:xSize:xs ->
                accessMemoryRange xOffset xSize $ do
                  availableGas <- use (#state % #gas)
                  let (cost, gas') = costOfCreate fees availableGas xSize False
  
                  -- handle `prank`
                  let from' = fromMaybe self vm.state.overrideCaller
                  resetCaller <- use (#state % #resetCaller)
                  when resetCaller $ do
                    assign (#state % #overrideCaller) Nothing
                    assign (#state % #resetCaller) False
  
                  touchAddress from'
                  nonce <- zoom (#env % #contracts) $ do
                    contr <- use (at from')
                    pure $ (\c -> c.nonce) =<< contr
  
                  newAddr <- createAddress from' nonce
                  _ <- accessAccountForGas newAddr
                  burn' cost $ do
                    initCode <- readMemory xOffset xSize
                    create from' this xSize gas' xValue xs newAddr initCode
              _ -> underrun
  
          OpCall -> {-# SCC "OpCall" #-}
            case stk of
              xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
                branch conf.maxDepth (Expr.gt xValue (Lit 0)) $ \gt0 -> do
                  let addrFallback = if conf.promiseNoReent then const fallback
                                     else unexpectedSymArgW "unable to determine a call target"
                  (if gt0 then notStatic else id) $
                    forceAddr xTo' addrFallback $ \xTo ->
                      case gasTryFrom xGas of
                        Left _ -> vmError IllegalOverflow
                        Right gas -> do
                          overrideC <- use $ #state % #overrideCaller
                          let delegateFallback = if conf.promiseNoReent then const fallback
                                                 else unknownCode
                          delegateCall this gas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs delegateFallback $
                            \callee -> do
                              let from' = fromMaybe self overrideC
                              zoom #state $ do
                                assign #callvalue xValue
                                assign #caller from'
                                assign #contract callee
                              touchAccount from'
                              touchAccount callee
                              transfer from' callee xValue
                where fallback = freshBufFallback xs
              _ -> underrun
  
          OpCallcode -> {-# SCC "OpCallcode" #-}
            case stk of
              xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
                forceAddr xTo' (unexpectedSymArgW "unable to determine a call target") $ \xTo ->
                  case gasTryFrom xGas of
                    Left _ -> vmError IllegalOverflow
                    Right gas -> do
                      overrideC <- use $ #state % #overrideCaller
                      delegateCall this gas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs unknownCode $ \_ -> do
                        zoom #state $ do
                          assign #callvalue xValue
                          assign #caller $ fromMaybe self overrideC
                        touchAccount self
              _ -> underrun
  
          OpReturn -> {-# SCC "OpReturn" #-}
            case stk of
              xOffset:xSize:_ ->
                accessMemoryRange xOffset xSize $ do
                  output <- readMemory xOffset xSize
                  let
                    codesize = fromMaybe (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data")
                                 . maybeLitWordSimp . 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 conf.maxDepth (Expr.eqByte y (LitByte 0xef)) $ \case
                            True -> frameErrored
                            False -> frameReturned
                  else
                     finishFrame (FrameReturned output)
              _ -> underrun
  
          OpDelegatecall -> {-# SCC "OpDelegatecall" #-}
            case stk of
              xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
                forceAddr xTo (const $ unexpectedSymArg "unable to determine a call target" [xTo]) $ \xTo' ->
                    case gasTryFrom xGas of
                      Left _ -> vmError IllegalOverflow
                      Right gas ->
                        -- NOTE: we don't update overrideCaller in this case because
                        -- forge-std doesn't. see: https://github.com/foundry-rs/foundry/pull/8863
                        delegateCall this gas xTo' self (Lit 0) xInOffset xInSize xOutOffset xOutSize xs unknownCode $
                          \_ -> touchAccount self
              _ -> underrun
  
          OpCreate2 -> {-# SCC "OpCreate2" #-} notStatic $
            case stk of
              xValue:xOffset:xSize:xSalt':xs ->
                forceConcrete xSalt' "CREATE2" $ \(xSalt) ->
                  accessMemoryRange xOffset xSize $ do
                    availableGas <- use (#state % #gas)
                    buf <- readMemory xOffset xSize
                    forceConcreteBuf buf "CREATE2" $
                      \initCode -> do
                        -- handle `prank`
                        let from' = fromMaybe self vm.state.overrideCaller
                        resetCaller <- use (#state % #resetCaller)
                        when resetCaller $ do
                          assign (#state % #overrideCaller) Nothing
                          assign (#state % #resetCaller) False
  
                        touchAddress from'
  
                        let (cost, gas') = costOfCreate fees availableGas xSize True
                        newAddr <- create2Address self xSalt initCode
                        _ <- accessAccountForGas newAddr
                        burn' cost $
                          create from' this xSize gas' xValue xs newAddr (ConcreteBuf initCode)
              _ -> underrun
  
          OpStaticcall -> {-# SCC "OpStaticcall" #-}
            case stk of
              xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
                forceAddr xTo (const fallback) $ \xTo' -> case gasTryFrom xGas of
                  Left _ -> vmError IllegalOverflow
                  Right gas -> do
                    overrideC <- use $ #state % #overrideCaller
                    delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs (const fallback) $
                      \callee -> do
                        zoom #state $ do
                          assign #callvalue (Lit 0)
                          assign #caller $ fromMaybe self overrideC
                          assign #contract callee
                          assign #static True
                        touchAccount self
                        touchAccount callee
                  where
                    fallback = freshBufFallback xs
              _ -> underrun
  
          OpSelfdestruct -> {-# SCC "OpSelfdestruct" #-}
            notStatic $
            case stk of
              [] -> underrun
              (xTo':_) -> forceAddr xTo' (unexpectedSymArgW "SELFDESTRUCT") $ \case
                xTo@(LitAddr _) -> do
                  cc <- gets (.tx.subState.createdContracts)
                  let createdThisTr = self `member` cc
                  acc <- accessAccountForGas xTo
                  let cost = if acc then 0 else g_cold_account_access
                      funds = this.balance
                      recipientExists = accountExists xTo vm
                  branch conf.maxDepth (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
                      when (createdThisTr || isCreation this.code) $ do
                        selfdestruct self
                      touchAccount xTo
  
                      if hasFunds
                      then fetchAccount xTo $ \_ -> do
                        when (createdThisTr || xTo /= self) $ do
                          #env % #contracts % ix xTo % #balance %= (Expr.add funds)
                          assign (#env % #contracts % ix self % #balance) (Lit 0)
                        doStop
                      else
                        doStop
                a -> unexpectedSymArg "trying to self destruct to a symbolic address" [a]
  
          OpRevert -> {-# SCC "OpRevert" #-}
            case stk of
              xOffset:xSize:_ ->
                accessMemoryRange xOffset xSize $ do
                  output <- readMemory xOffset xSize
                  finishFrame (FrameReverted output)
              _ -> underrun
  
          OpUnknown xxx -> {-# SCC "OpUnknown" #-} vmError $ UnrecognizedOpcode xxx
  
  transfer :: (VMOps t, ?conf::Config) => Expr EAddr -> Expr EAddr -> Expr EWord -> EVM t s ()
  transfer _ _ (Lit 0) = pure ()
  transfer src dst val = do
    sb <- preuse $ #env % #contracts % ix src % #balance
    db <- preuse $ #env % #contracts % ix dst % #balance
    case (sb, db) of
      -- both sender and recipient in state
      (Just srcBal, Just _) ->
        branch (?conf).maxDepth (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
            touchAddress src
            transfer src dst val
          SymAddr _ -> unexpectedSymArg "Attempting to transfer eth from a symbolic address that is not present in the state" [src]
          GVar _ -> internalError "Unexpected GVar"
      -- recipient not in state
      (_ , Nothing) -> do
        case dst of
          LitAddr _ -> do
            touchAddress dst
            transfer src dst val
          SymAddr _ -> unexpectedSymArg "Attempting to transfer eth to a symbolic address that is not present in the state" [dst]
          GVar _ -> internalError "Unexpected GVar"
  
  -- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.
  callChecks
    :: forall (t :: VMType) s. (?op :: Word8, ?conf :: Config, VMOps t)
    => Contract
    -> Gas t
    -> Expr EAddr
    -> Expr EAddr
    -> Expr EWord
    -> Expr EWord
    -> Expr EWord
    -> Expr EWord
    -> Expr EWord
    -> [Expr EWord]
    -- continuation with gas available for call
    -> (Gas t -> EVM t s ())
    -> EVM t 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
        let from = fromMaybe vm.state.contract vm.state.overrideCaller
        fromBal <- preuse $ #env % #contracts % ix from % #balance
        costOfCall fees recipientExists xValue availableGas xGas xTo $ \cost gas' -> do
          let checkCallDepth =
                if length vm.frames >= 1024
                then do
                  assign' (#state % #stack) (Lit 0 : xs)
                  assign (#state % #returndata) mempty
                  pushTrace $ ErrorTrace CallDepthLimitReached
                  next
                else continue (toGas gas')
          case (fromBal, xValue) of
            -- we're not transferring any value, and can skip the balance check
            (_, Lit 0) -> burn (cost - gas') checkCallDepth
  
            -- from is in the state, we check if they have enough balance
            (Just fb, _) -> do
              burn (cost - gas') $
                branch (?conf).maxDepth (Expr.gt xValue fb) $ \case
                  True -> do
                    assign' (#state % #stack) (Lit 0 : xs)
                    assign (#state % #returndata) mempty
                    pushTrace $ ErrorTrace (BalanceTooLow xValue this.balance)
                    next
                  False -> checkCallDepth
  
            -- from is not in the state, we insert it if safe to do so and run the checks again
            (Nothing, _) -> case from of
              LitAddr _ -> do
                -- insert an entry in the state
                let contract = case vm.config.baseState of
                      AbstractBase -> unknownContract from
                      EmptyBase -> emptyContract
                (#env % #contracts) %= (Map.insert from contract)
                -- run callChecks again
                callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue
  
              -- adding a symbolic address into the state here would be unsound (due to potential aliasing)
              SymAddr _ -> unexpectedSymArg "Attempting to transfer eth from a symbolic address that is not present in the state" [from]
              GVar _ -> internalError "Unexpected GVar"
  
  precompiledContract
    :: (?conf :: Config, ?op :: Word8, VMOps t)
    => Contract
    -> Gas t
    -> Addr
    -> Addr
    -> Expr EWord
    -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
    -> [Expr EWord]
    -> EVM t 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)
        result' <- use #result
        case result' of
          Nothing -> case stk of
            x:_ -> case maybeLitWordSimp x of
              Just 0 ->
                pure ()
              Just 1 ->
                fetchAccount (LitAddr recipient) $ \_ -> do
                  touchAccount self
                  touchAccount (LitAddr recipient)
                  transfer self (LitAddr recipient) xValue
              _ -> unexpectedSymArg "unexpected return value from precompile" [x]
            _ -> underrun
          _ -> pure ()
  
  executePrecompile
    :: (?op :: Word8, VMOps t)
    => Addr
    -> Gas t -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr EWord]
    -> EVM t s ()
  executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  = do
    vm <- get
    input <- readMemory inOffset inSize
    let fees = vm.block.schedule
        cost = costOfPrecompile fees preCompileAddr input
        notImplemented = whenSymbolicElse
          (partial $ PrecompileMissing {pc = vm.state.pc, addr = vm.state.contract, preAddr = preCompileAddr})
          (vmError $ NonexistentPrecompile preCompileAddr)
        precompileFail = burn' (subGas gasCap cost) $ do
                           assign' (#state % #stack) (Lit 0 : xs)
                           pushTrace $ ErrorTrace PrecompileFailure
                           next
    if not (enoughGas 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) outSize (Lit 0) 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 outSize (Lit 0) 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 outSize (Lit 0) outOffset
            next
  
        -- IDENTITY
        0x4 -> do
            assign' (#state % #stack) (Lit 1 : xs)
            assign (#state % #returndata) input
            copyCallBytesToMemory input outSize 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 outSize (Lit 0) 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 outSize (Lit 0) 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 outSize (Lit 0) 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 outSize (Lit 0) 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 outSize (Lit 0) 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 t s -> CodeLocation
  getCodeLocation vm = (vm.state.contract, vm.state.pc)
  
  query :: Query t s -> EVM t s ()
  query q = assign #result $ Just $ HandleEffect (Query q)
  
  runBoth :: Maybe Int -> Int -> RunBoth s -> EVM Symbolic s ()
  runBoth depthLimit exploreDepth c = do
    if (isNothing depthLimit || (exploreDepth < fromJust depthLimit)) then do
      assign #result $ Just $ HandleEffect (RunBoth c)
    else do
      vm <- get
      assign #result $ Just $ Unfinished (BranchTooDeep {pc = vm.state.pc, addr = vm.state.contract})
  
  runAll :: Maybe Int -> Int -> RunAll s -> EVM Symbolic s ()
  runAll depthLimit exploreDepth c = do
    if (isNothing depthLimit || (exploreDepth < fromJust depthLimit)) then do
      assign #result $ Just $ HandleEffect (RunAll c)
    else do
      vm <- get
      assign #result $ Just $ Unfinished (BranchTooDeep {pc = vm.state.pc, addr = vm.state.contract})
  
  fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
  fetchAccount addr continue =
    let fallback = unexpectedSymArgW "trying to access a symbolic address that isn't already present in storage"
    in fetchAccountWithFallback addr fallback continue
  
  -- | Construct RPC Query and halt execution until resolved
  fetchAccountWithFallback :: VMOps t => Expr EAddr -> (Expr EAddr -> EVM t s ()) -> (Contract -> EVM t s ()) -> EVM t s ()
  fetchAccountWithFallback addr fallback continue =
    use (#env % #contracts % at addr) >>= \case
      Just c -> continue c
      Nothing -> case addr of
        SymAddr _ -> fallback addr
        LitAddr a -> do
          base <- use (#config % #baseState)
          assign (#result) . Just . HandleEffect . Query $
            PleaseFetchContract a base $ \c -> do
              assign (#env % #contracts % at addr) (Just c)
              assign #result Nothing
              continue c
        GVar _ -> internalError "Unexpected GVar"
  
  accessStorage :: forall s t . (?conf :: Config, VMOps t, Typeable t) => Expr EAddr
    -> Expr EWord
    -> (Expr EWord -> EVM t s ())
    -> EVM t s ()
  accessStorage addr slot continue = do
    let slotConc = Expr.concKeccakSimpExpr slot
    use (#env % #contracts % at addr) >>= \case
      Just c ->
        -- Try first without concretization. Then if we get a Just, with concretization
        -- if both give a Just, should we `continue`.
        -- --> This is because readStorage can do smart rewrites, but only in case
        --     the expression is of a particular format, which can be destroyed by simplification.
        --     However, without concretization, it may not find things that are actually in the storage
        case readStorage slot c.storage of
          Just x -> case readStorage slotConc c.storage of
            Just (Lit _) -> continue x
            Just _ | not c.external -> continue x
            _ -> rpcCall c slotConc
          Nothing -> rpcCall c slotConc
      Nothing ->
        fetchAccount addr $ \_ -> accessStorage addr slot continue
    where
        rpcCall c slotConc = fetchAccount addr $ \_ ->
          if c.external
          then forceConcreteAddr addr "cannot read storage from symbolic addresses via rpc" $ \addr' ->
            forceConcrete slotConc "cannot read symbolic slots via RPC" $ \slot' -> do
              use (#env % #contracts % at (LitAddr addr')) >>= \case
                Nothing -> internalError $ "contract addr " <> show addr' <> " marked external not found in cache"
                -- At this point, we know the contract is external and the underlying storage
                -- is concrete. Check if the slot has already been fetched
                Just contr -> if concStoreContains (Lit slot') contr.storage
                  then continue $ SLoad (Lit slot') contr.storage
                  else mkQuery addr' slot'
          else do
            -- Symbolic address that cannot be cajoled/solved into a concrete one
            -- We cannot query the underlying storage, as we don't know which one to query
            -- So we store and return 0, as it is the only sound option
            modifying (#env % #contracts % ix addr % #storage) (writeStorage slot (Lit 0))
            continue $ Lit 0
        mkQuery :: Addr -> W256 -> EVM t s ()
        mkQuery a s = query $ PleaseFetchSlot a s $ \x -> do
          modifying (#env % #contracts % ix (LitAddr a) % #storage) (writeStorage (Lit s) (Lit x))
          assign #result Nothing
          continue $ Lit x
  
  accessTStorage
    :: VMOps t => Expr EAddr
    -> Expr EWord
    -> (Expr EWord -> EVM t s ())
    -> EVM t s ()
  accessTStorage addr slot continue = do
    let slotConc = Expr.concKeccakSimpExpr slot
    use (#env % #contracts % at addr) >>= \case
      Just c ->
        -- Try first without concretization. Then if we get a Just, with concretization
        -- See `accessStorage` for more details
        case readStorage slot c.tStorage of
          Just x -> case readStorage slotConc c.tStorage of
            Just _ -> continue x
            Nothing -> continue $ Lit 0
          Nothing -> continue $ Lit 0
      Nothing ->
        fetchAccount addr $ \_ ->
          accessTStorage addr slot continue
  
  clearTStorages :: EVM t s ()
  clearTStorages = (#env % #contracts) %= fmap (\c -> c { tStorage = ConcreteStore mempty } :: Contract)
  
  accountExists :: Expr EAddr -> VM t 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
  
  -- Adds constraints such that two symbolic addresses cannot alias each other
  -- and symbolic addresses cannot alias concrete addresses
  addAliasConstraints :: EVM t s ()
  addAliasConstraints = do
    vm <- get
    let addrConstr = noClash $ Map.keys vm.env.contracts
    modifying #constraints ((++) addrConstr)
    where
      noClash addrs = [a ./= b | a <- addrs, b <- addrs, Expr.isSymAddr b, a < b]
  
  -- * How to finalize a transaction
  finalize :: VMOps t => EVM t s ()
  finalize = do
    let
      revertContracts  = use (#tx % #txReversion) >>= assign (#env % #contracts)
      revertSubstate   = assign (#tx % #subState) (SubState mempty mempty mempty mempty mempty mempty)
  
    addAliasConstraints
    use #result >>= \case
      Just (VMFailure (Revert _)) -> do
        revertContracts
        revertSubstate
      Just (VMFailure _) -> do
        -- burn remaining gas
        assign (#state % #gas) initialGas
        revertContracts
        revertSubstate
      Just (VMSuccess output) -> do
        clearTStorages
        -- deposit the code from a creation tx
        creation <- use (#tx % #isCreate)
        createe  <- use (#state % #contract)
        createeExists <- (Map.member createe) <$> use (#env % #contracts)
        when (creation && createeExists) $
          case output of
            ConcreteBuf bs -> replaceCode createe (RuntimeCode (ConcreteRuntimeCode bs))
            _ ->
              case Expr.toList output of
                Nothing -> unexpectedSymArg "runtime code cannot have an abstract length" [output]
                Just ops -> replaceCode createe (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
  
    payRefunds
  
    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 t 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 :: VMOps t => Int -> EVM (t :: VMType) s () -> EVM t s ()
  limitStack n continue = do
    stk <- use (#state % #stack)
    if length stk + n > 1024
      then vmError StackLimitExceeded
      else continue
  
  notStatic :: VMOps t => EVM t s () -> EVM t s ()
  notStatic continue = do
    bad <- use (#state % #static)
    if bad
      then vmError StateChangeWhileStatic
      else continue
  
  -- Ensures the account `addr` exists on the VM environment.
  -- Useful when `addr` needs to e.g. keep a eth balance or
  -- be the source of contract deployments via pranks
  touchAddress :: VMOps t => Expr EAddr -> EVM t s ()
  touchAddress addr = do
    baseState <- use (#config % #baseState)
    let mkc = case baseState of
                AbstractBase -> unknownContract
                EmptyBase -> const emptyContract
    (#env % #contracts) %= (Map.insertWith (\_ e -> e) addr (mkc addr))
  
  onlyDeployed :: forall t s . (?conf :: Config, VMOps t, Typeable t) =>
    Expr EWord
    -> (Expr EWord -> EVM t s ())
    -> (Expr EAddr -> EVM t s ())
    -> EVM t s ()
  onlyDeployed addrExpr fallback continue = do
      vm <- get
      if not (?conf.onlyDeployed) then fallback addrExpr
      else case eqT @t @Symbolic of
        Just Refl -> do
          let deployedAddrs = map forceEAddrToEWord $ mapMaybe (codeMustExist vm) $ Map.keys vm.env.contracts
          runAll (?conf.maxDepth) vm.exploreDepth $ PleaseRunAll addrExpr deployedAddrs runAllPaths
        _ -> internalError "Unknown address in Concrete mode"
    where
      codeMustExist :: (VM t s) -> Expr EAddr -> Maybe (Expr EAddr)
      codeMustExist vm addr = do
        contr <- Map.lookup addr vm.env.contracts
        case contr.code of
          RuntimeCode (ConcreteRuntimeCode _) -> Just addr
          _ -> Nothing
      runAllPaths val = do
          assign #result Nothing
          pushTo #constraints $ Expr.simplifyProp (addrExpr .== val)
          continue (forceEWordToEAddr val)
  
  forceAddr :: forall t s . (?conf :: Config, VMOps t, Typeable t) =>
    Expr EWord
    -> (Expr EWord -> EVM t s ())
    -> (Expr EAddr -> EVM t s ())
    -> EVM t s ()
  forceAddr addrExpr fallback continue = case wordToAddr addrExpr of
    Nothing -> manySolutions (?conf).maxDepth addrExpr 20 $ \case
      Just sol -> continue $ LitAddr (truncateToAddr sol)
      Nothing -> onlyDeployed addrExpr fallback continue
    Just c -> continue c
  
  
  unexpectedSymArg :: (Typeable a, VMOps t) => String -> [Expr a] -> EVM t s ()
  unexpectedSymArg msg n = do
    pc <- use (#state % #pc)
    state <- use #state
    let opName = getOpName state
    partial $ UnexpectedSymbolicArg pc state.contract opName msg (wrap n)
  
  unexpectedSymArgW :: (Typeable a, VMOps t) => String -> Expr a -> EVM t s ()
  unexpectedSymArgW msg n = unexpectedSymArg msg [n]
  
  unknownCode :: VMOps t => Expr EAddr -> EVM t s ()
  unknownCode n = unexpectedSymArg "call target has unknown code" [n]
  
  freshBufFallback :: (?conf :: Config, VMOps t, ?op :: Word8) => [Expr EWord] -> EVM t s ()
  freshBufFallback xs = do
    -- Reset caller if needed
    resetCaller <- use $ #state % #resetCaller
    when resetCaller $ assign (#state % #overrideCaller) Nothing
    -- overapproximate by returning a symbolic value
    freshVar <- use #freshVar
    assign #freshVar (freshVar + 1)
    let opName = pack $ show $ getOp ?op
    let freshVarExpr = Var (opName <> "-result-stack-fresh-" <> (pack . show) freshVar)
    modifying #constraints ((:) (PLEq freshVarExpr (Lit 1) ))
    let freshReturndataExpr = AbstractBuf (opName <> "-result-data-fresh-" <> (pack . show) freshVar)
    modifying #constraints ((:) (PLEq (bufLength freshReturndataExpr) (Lit (2 ^ ?conf.maxBufSize))))
    assign (#state % #returndata) freshReturndataExpr
    next >> assign' (#state % #stack) (freshVarExpr:xs)
  
  freshVarFallback:: (VMOps t, ?op :: Word8) => [Expr EWord] -> Expr a -> EVM t s ()
  freshVarFallback xs _ = do
    -- Reset caller if needed
    resetCaller <- use $ #state % #resetCaller
    when resetCaller $ assign (#state % #overrideCaller) Nothing
    -- overapproximate by returning a symbolic value
    freshVar <- use #freshVar
    assign #freshVar (freshVar + 1)
    let opName = pack $ show $ getOp ?op
    let freshVarExpr = Var (opName <> "-result-stack-fresh-" <> (pack . show) freshVar)
    next >> assign' (#state % #stack) (freshVarExpr:xs)
  
  forceConcrete :: (?conf :: Config, VMOps t) => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()
  forceConcrete n = forceConcreteLimitSz n 32
  
  forceConcreteLimitSz :: (?conf :: Config, VMOps t) => Expr EWord -> Int -> String -> (W256 -> EVM t s ()) -> EVM t s ()
  forceConcreteLimitSz n bytes msg continue = case maybeLitWordSimp n of
    Nothing -> manySolutions (?conf).maxDepth n bytes $ maybe fallback continue
    Just c -> continue c
    where fallback = unexpectedSymArg msg [n]
  
  forceConcreteAddr :: (?conf :: Config, VMOps t) => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()
  forceConcreteAddr n msg continue = case maybeLitAddrSimp n of
    Nothing -> manySolutions (?conf).maxDepth (WAddr n) 20 $ maybe fallback $ \c -> continue (truncateToAddr c)
    Just c -> continue c
    where fallback = unexpectedSymArg msg [n]
  
  forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s ()
  forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddrSimp n, maybeLitAddrSimp m) of
    (Just c, Just d) -> continue (c,d)
    _ -> unexpectedSymArg msg [n, m]
  
  forceConcrete2 :: VMOps t => (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s ()
  forceConcrete2 (n,m) msg continue = case (maybeLitWordSimp n, maybeLitWordSimp m) of
    (Just c, Just d) -> continue (c, d)
    _ -> unexpectedSymArg msg [n, m]
  
  forceConcreteBuf :: VMOps t => Expr Buf -> String -> (ByteString -> EVM t s ()) -> EVM t s ()
  forceConcreteBuf (ConcreteBuf b) _ continue = continue b
  forceConcreteBuf b msg _ = unexpectedSymArg msg [b]
  
  -- * Substate manipulation
  refund :: Word64 -> EVM t s ()
  refund n = do
    self <- use (#state % #contract)
    pushTo (#tx % #subState % #refunds) (self, n)
  
  unRefund :: Word64 -> EVM t 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 t s ()
  touchAccount = pushTo ((#tx % #subState) % #touchedAccounts)
  
  selfdestruct :: Expr EAddr -> EVM t s ()
  selfdestruct = pushTo ((#tx % #subState) % #selfdestructs)
  
  accessAndBurn :: VMOps t => Expr EAddr -> EVM t s () -> EVM t 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 t 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 t s Bool
  accessStorageForGas addr key = do
    accessedStrkeys <- use (#tx % #subState % #accessedStorageKeys)
    case maybeLitWordSimp key of
      Just litword -> do
        let accessed = member (addr, litword) accessedStrkeys
        assign (#tx % #subState % #accessedStorageKeys) (insert (addr, litword) accessedStrkeys)
        pure accessed
      _ -> pure 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
    :: forall t s . (?conf :: Config, ?op :: Word8, VMOps t, Typeable t)
    => Gas t -> (Expr EWord, Expr EWord) -> (Expr EWord, Expr EWord) -> [Expr EWord]
    -> EVM t s ()
  cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
    vm <- get
    input <- readMemory (Expr.add inOffset (Lit 4)) (Expr.sub inSize (Lit 4))
    calldata <- readMemory inOffset inSize
    abi <- readBytes 4 (Lit 0) <$> readMemory inOffset (Lit 4)
    let newContext = CallContext cheatCode cheatCode outOffset outSize (Lit 0) (maybeLitWordSimp abi) calldata vm.env.contracts vm.tx.subState
  
    pushTrace $ FrameTrace newContext
    next
    vm1 <- get
    burn' gas $ pushTo #frames $ Frame
                      { state = vm1.state { stack = xs }
                      , context = newContext
                      }
    case maybeLitWordSimp abi of
      -- 4-byte function selector
      Nothing -> manySolutions (?conf).maxDepth abi 4 $ \case
        Just concAbi -> runCheat concAbi input
        Nothing -> unexpectedSymArg "symbolic cheatcode selector" [abi]
      Just concAbi -> runCheat concAbi input
    where
      runCheat :: W256 -> Expr 'Buf -> EVM t s ()
      runCheat abi input =  do
        let abi' = unsafeInto abi
        case Map.lookup abi' cheatActions of
          Nothing -> do
            vm <- get
            whenSymbolicElse (partial $ CheatCodeMissing vm.state.pc vm.state.contract abi') (vmError $ BadCheatCode "Cannot understand cheatcode." abi')
          Just action -> action input
  
  type CheatAction t s = Expr Buf -> EVM t s ()
  
  cheatActions :: (?conf :: Config, VMOps t, Typeable t) => Map FunctionSelector (CheatAction t s)
  cheatActions = Map.fromList
    [ action "ffi(string[])" $
        \sig 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) -> toString a
                              _ -> "")
                            (V.toList strsV)
                    cont bs = continueOnce $ do
                      frameReturnBuf bs
                  in query (PleaseDoFFI cmd vm.osEnv cont)
                _ -> vmError (BadCheatCode "ffi(string[]) decoding of string failed" sig)
              _ -> vmError (BadCheatCode "ffi(string[]) parameter decoding failed" sig)
          else vmError $ BadCheatCode "ffi disabled: run again with --ffi if you want to allow tests to call external scripts" sig
  
    , action "warp(uint256)" $
        \sig input -> case decodeStaticArgs 0 1 input of
          [x]  -> do
            assign (#block % #timestamp) x
            doStop
          _ -> vmError (BadCheatCode "warp(uint256) parameter decoding failed" sig)
  
    , action "deal(address,uint256)" $
        \sig input -> case decodeStaticArgs 0 2 input of
          [a, amt] ->
            forceAddr a (unexpectedSymArgW "vm.deal: cannot decode target into an address") $ \usr ->
              fetchAccount usr $ \_ -> do
                assign (#env % #contracts % ix usr % #balance) amt
                doStop
          _ -> vmError (BadCheatCode "deal(address,uint256) parameter decoding failed" sig)
  
    , action "assume(bool)" $
        \sig input -> case decodeStaticArgs 0 1 input of
          [c] -> do
            modifying #constraints ((:) (PEq (Lit 1) c))
            doStop
          _ -> vmError (BadCheatCode "assume(bool) parameter decoding failed." sig)
  
    , action "roll(uint256)" $
        \sig input -> case decodeStaticArgs 0 1 input of
          [x] -> do
            assign (#block % #number) x
            doStop
          _ -> vmError (BadCheatCode "roll(uint256) parameter decoding failed" 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' $ \_ -> do
              modifying (#env % #contracts % ix a' % #storage) (writeStorage slot new)
              doStop
            _ -> vmError (BadCheatCode "store(address,bytes32,bytes32) issue, address provided may not be an address?" sig)
          _ -> vmError (BadCheatCode "store(address,bytes32,bytes32) parameter decoding failed" sig)
  
    , action "load(address,bytes32)" $
        \sig input -> case decodeStaticArgs 0 2 input of
          [a, slot] -> case wordToAddr a of
            Just a'@(LitAddr _) -> fetchAccount a' $ \_ ->
              accessStorage a' slot $ \res -> do
                let buf = writeWord (Lit 0) res (ConcreteBuf "")
                frameReturnExpr buf -- TODO reivew
            _ -> vmError (BadCheatCode "load(address,bytes32) issue, maybe the address provided is not correct?" sig)
          _ -> vmError (BadCheatCode "load(address,bytes32) parameter decoding failed" sig)
  
    , action "sign(uint256,bytes32)" $
        \sig 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' (into sk')
                  result = AbiTuple $
                    V.fromList
                      [ AbiUInt 8 $ into v
                      , AbiBytes 32 (word256Bytes r)
                      , AbiBytes 32 (word256Bytes s)
                      ]
              frameReturn result -- TODO ??
          _ -> vmError (BadCheatCode "sign(uint256,bytes32) parameter decoding failed" sig)
  
    , action "addr(uint256)" $
        \sig input -> case decodeStaticArgs 0 1 input of
          [sk] -> forceConcrete sk "cannot derive address for a symbolic key" $ \sk' -> do
            case EVM.Sign.deriveAddr $ into sk' of
              Nothing -> vmError (BadCheatCode "addr(uint256) could not derive address" sig)
              Just address -> do frameReturnBuf $ word256Bytes (into address) -- TODO ??
          _ -> vmError (BadCheatCode "addr(uint256) parameter decoding failed" sig)
  
    , action "prank(address)" $
        \sig input -> case decodeStaticArgs 0 1 input of
          [addr]  -> case wordToAddr addr of
            Just a -> do
              doStop
              assign (#state % #overrideCaller) (Just a)
              assign (#state % #resetCaller) True
            Nothing -> vmError (BadCheatCode "prank(address), could not decode address provided" sig)
          _ -> vmError (BadCheatCode "prank(address) parameter decoding failed" sig)
  
    , action "startPrank(address)" $
        \sig input -> case decodeStaticArgs 0 1 input of
          [addr]  -> case wordToAddr addr of
            Just a -> do
              doStop
              assign (#state % #overrideCaller) (Just a)
              assign (#state % #resetCaller) False
            Nothing -> vmError (BadCheatCode "startPrank(address), could not decode address provided" sig)
          _ -> vmError (BadCheatCode "startPrank(address) parameter decoding failed" sig)
  
    , action "stopPrank()" $
        \_ _ -> do
          doStop
          assign (#state % #overrideCaller) Nothing
          assign (#state % #resetCaller) False
  
    , action "createFork(string)" $
        \sig input -> case decodeBuf [AbiStringType] input of
          (CAbi valsArr,"") -> case valsArr of
            [AbiString bytes] -> do
              forkId <- length <$> gets (.forks)
              let urlOrAlias = Char8.unpack bytes
              modify' $ \vm -> vm { forks = vm.forks Seq.|> ForkState vm.env vm.block vm.pathsVisited urlOrAlias }
              frameReturn $ AbiUInt 256 (fromIntegral forkId)
            _ -> vmError (BadCheatCode "createFork(string) string provided may be incorrect?" sig)
          _ -> vmError (BadCheatCode "createFork(string) parameter decoding failed" sig)
  
    , action "selectFork(uint256)" $
        \sig input -> case decodeStaticArgs 0 1 input of
          [forkId] ->
            forceConcrete forkId "forkId of 'selectFork' must be concrete" $ \(fromIntegral -> forkId') -> do
              saved <- Seq.lookup forkId' <$> gets (.forks)
              case saved of
                Just forkState -> do
                  vm <- get
                  let contractAddr = vm.state.contract
                  let callerAddr = vm.state.caller
                  fetchAccount contractAddr $ \contractAcct -> fetchAccount callerAddr $ \callerAcct -> do
                    let
                      -- the current contract is persisted across forks
                      newContracts = Map.insert callerAddr callerAcct $
                                     Map.insert contractAddr contractAcct forkState.env.contracts
                      newEnv = (forkState.env :: Env) { contracts = newContracts }
  
                    when (vm.currentFork /= forkId') $ do
                      modify' $ \vm' -> vm'
                        { env = newEnv
                        , block = forkState.block
                        , forks = Seq.adjust' (\state -> (state :: ForkState)
                            { env = vm.env, block = vm.block, pathsVisited = vm.pathsVisited }
                          ) vm.currentFork  vm.forks
                        , currentFork = forkId'
                        }
                    doStop
                Nothing ->
                  vmError (NonexistentFork forkId')
          _ -> vmError (BadCheatCode "selectFork(uint256) parameter decoding failed" sig)
  
    , action "activeFork()" $
        \_ _ -> do
          vm <- get
          frameReturn $ AbiUInt 256 (fromIntegral vm.currentFork)
  
    , action "label(address,string)" $
        \sig input -> case decodeBuf [AbiAddressType, AbiStringType] input of
          (CAbi valsArr,"") -> case valsArr of
            [AbiAddress addr, AbiString label] -> do
              #labels %= Map.insert addr (decodeUtf8 label)
              doStop
            _ -> vmError (BadCheatCode "label(address,string) address decoding failed" sig)
          _ -> vmError (BadCheatCode "label(address,string) parameter decoding failed" sig)
  
    , action "setEnv(string,string)" $
        \sig input -> case decodeBuf [AbiStringType, AbiStringType] input of
          (CAbi valsArr,"") -> case valsArr of
            [AbiString variable, AbiString value] -> do
              let (varStr, varVal) = (toString variable, toString value)
              #osEnv %= Map.insert varStr varVal
              doStop
            _ -> vmError (BadCheatCode "setEnv(string,string) address decoding failed" sig)
          _ -> vmError (BadCheatCode "setEnv(string,string) parameter decoding failed" sig)
  
    -- Single-value environment read cheat actions
    , $(envReadSingleCheat "envBool(string)") AbiBool stringToBool
    , $(envReadSingleCheat "envUint(string)") (AbiUInt 256) stringToWord256
    , $(envReadSingleCheat "envInt(string)") (AbiInt 256) stringToInt256
    , $(envReadSingleCheat "envAddress(string)") AbiAddress stringToAddress
    , $(envReadSingleCheat "envBytes32(string)") (AbiBytes 32) stringToBytes32
    , $(envReadSingleCheat "envString(string)") (\x -> AbiTuple $ V.fromList [AbiString x]) stringToByteString
    , $(envReadSingleCheat "envBytes(bytes)") (\x -> AbiTuple $ V.fromList [AbiBytesDynamic x]) stringHexToByteString
  
    -- Multi-value environment read cheat actions
    , $(envReadMultipleCheat "envBool(string,string)" AbiBoolType) stringToBool
    , $(envReadMultipleCheat "envUint(string,string)" $ AbiUIntType 256) stringToWord256
    , $(envReadMultipleCheat "envInt(string,string)" $ AbiIntType 256) stringToInt256
    , $(envReadMultipleCheat "envAddress(string,string)" AbiAddressType) stringToAddress
    , $(envReadMultipleCheat "envBytes32(string,string)" $ AbiBytesType 32) stringToBytes32
    , $(envReadMultipleCheat "envString(string,string)" AbiStringType) stringToByteString
    , $(envReadMultipleCheat "envBytes(bytes,bytes)" AbiBytesDynamicType) stringHexToByteString
    , action "assertTrue(bool)" $ \sig input ->
        case decodeBuf [AbiBoolType] input of
          (CAbi [AbiBool True],"") -> doStop
          (CAbi [AbiBool False],"") -> frameRevert "assertion failed"
          (SAbi [eword],"") -> case (Expr.simplify (Expr.iszero eword)) of
            Lit 1 -> frameRevert "assertion failed"
            Lit 0 -> doStop
            ew -> branch (?conf).maxDepth ew $ \case
              True -> frameRevert "assertion failed"
              False -> doStop
          k -> vmError $ BadCheatCode ("assertTrue(bool) parameter decoding failed: " <> show k) sig
    , action "assertFalse(bool)" $ \sig input ->
        case decodeBuf [AbiBoolType] input of
          (CAbi [AbiBool False],"") -> doStop
          (CAbi [AbiBool True],"") -> frameRevert "assertion failed"
          (SAbi [eword],"") -> case (Expr.simplify (Expr.iszero eword)) of
            Lit 0 -> frameRevert "assertion failed"
            Lit 1 -> doStop
            ew -> branch (?conf).maxDepth ew $ \case
              False -> frameRevert "assertion failed"
              True -> doStop
          k -> vmError $ BadCheatCode ("assertFalse(bool) parameter decoding failed: " <> show k) sig
    , action "assertEq(bool,bool)"       $ assertEq AbiBoolType
    , action "assertEq(uint256,uint256)" $ assertEq (AbiUIntType 256)
    , action "assertEq(int256,int256)"   $ assertEq (AbiIntType 256)
    , action "assertEq(address,address)" $ assertEq AbiAddressType
    , action "assertEq(bytes32,bytes32)" $ assertEq (AbiBytesType 32)
    , action "assertEq(string,string)"   $ assertEq (AbiStringType)
    --
    , action "assertNotEq(bool,bool)"       $ assertNotEq AbiBoolType
    , action "assertNotEq(uint256,uint256)" $ assertNotEq (AbiUIntType 256)
    , action "assertNotEq(int256,int256)"   $ assertNotEq (AbiIntType 256)
    , action "assertNotEq(address,address)" $ assertNotEq AbiAddressType
    , action "assertNotEq(bytes32,bytes32)" $ assertNotEq (AbiBytesType 32)
    , action "assertNotEq(string,string)"   $ assertNotEq (AbiStringType)
    --
    , action "assertLt(uint256,uint256)" $ assertLt (AbiUIntType 256)
    , action "assertLt(int256,int256)"   $ assertSLt (AbiIntType 256)
    , action "assertLe(uint256,uint256)" $ assertLe (AbiUIntType 256)
    , action "assertLe(int256,int256)"   $ assertSLe (AbiIntType 256)
    , action "assertGt(uint256,uint256)" $ assertGt (AbiUIntType 256)
    , action "assertGt(int256,int256)"   $ assertSGt (AbiIntType 256)
    , action "assertGe(uint256,uint256)" $ assertGe (AbiUIntType 256)
    , action "assertGe(int256,int256)"   $ assertSGe (AbiIntType 256)
    --
    , action "toString(address)" $ toStringCheat AbiAddressType
    , action "toString(bool)"    $ toStringCheat AbiBoolType
    , action "toString(uint256)" $ toStringCheat (AbiUIntType 256)
    , action "toString(int256)"  $ toStringCheat (AbiIntType 256)
    , action "toString(bytes32)" $ toStringCheat (AbiBytesType 32)
    , action "toString(bytes)"   $ toStringCheat AbiBytesDynamicType
    ]
    where
      action s f = (abiKeccak s, f (abiKeccak s))
      either' v l r = either l r v
      frameReturn :: VMOps t => AbiValue -> EVM t s ()
      frameReturn v = frameReturnBuf $ encodeAbiValue v
      frameReturnBuf :: VMOps t => ByteString -> EVM t s ()
      frameReturnBuf buf = frameReturnExpr $ ConcreteBuf buf
      frameReturnExpr :: VMOps t => Expr Buf -> EVM t s ()
      frameReturnExpr e = finishFrame (FrameReturned e)
      frameRevert :: VMOps t => ByteString -> EVM t s ()
      frameRevert err = finishFrame (FrameReverted $ errorMsg err)
      errorMsg :: ByteString -> Expr Buf
      errorMsg err = ConcreteBuf $ selector "Error(string)" <> encodeAbiValue (AbiTuple $ V.fromList [AbiString err])
      continueOnce cont = do
        assign #result Nothing
        cont
      doStop = finishFrame (FrameReturned mempty)
      toString = unpack . decodeUtf8
      strip0x s = if "0x" `isPrefixOf` s then drop 2 s else s
      stringToBool :: String -> Either ByteString Bool
      stringToBool s = case s of
        "true" -> Right True
        "True" -> Right True
        "false" -> Right False
        "False" -> Right False
        _ -> Left "invalid value"
      stringToWord256 :: String -> Either ByteString Word256
      stringToWord256 s = maybeToEither "invalid W256 value" $ readMaybe s
      stringToInt256 :: String -> Either ByteString Int256
      stringToInt256 s = maybeToEither "invalid Int256 value" $ readMaybe s
      stringToAddress :: String -> Either ByteString Addr
      stringToAddress s = fmap Addr $ maybeToEither "invalid address value" $ readMaybe s
      stringToBytes32 :: String -> Either ByteString ByteString
      stringToBytes32 s = fmap word256Bytes $ maybeToEither "invalid bytes32 value" $ readMaybe s
      stringToByteString :: String -> Either ByteString ByteString
      stringToByteString = Right . Char8.pack
      stringHexToByteString :: String -> Either ByteString ByteString
      stringHexToByteString s = either (const $ Left "invalid bytes value") Right $ BS16.decodeBase16Untyped . Char8.pack . strip0x $ s
      paramDecodeErr abitype name abivals = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
        ")  parameter decoding failed. Error: " <> show abivals
      revertErr a b comp = frameRevert $ "assertion failed: " <>
        BS8.pack (show a) <> " " <> comp <> " " <> BS8.pack (show b)
      genAssert comp exprComp invComp name abitype sig input = do
        case decodeBuf [abitype, abitype] input of
          (CAbi [a, b],"") | a `comp` b -> doStop
          (CAbi [a, b],"")-> revertErr a b invComp
          (SAbi [ew1, ew2],"") -> case (Expr.simplify (Expr.iszero $ exprComp ew1 ew2)) of
            Lit 0 -> doStop
            Lit _ -> revertErr ew1 ew2 invComp
            ew -> branch (?conf).maxDepth ew $ \case
              False -> doStop
              True -> revertErr ew1 ew2 invComp
          abivals -> vmError (BadCheatCode (paramDecodeErr abitype name abivals) sig)
      assertEq =    genAssert (==) Expr.eq "!=" "assertEq"
      assertNotEq = genAssert (/=) (\a b -> Expr.iszero $ Expr.eq a b) "==" "assertNotEq"
      assertLt =    genAssert (<)  Expr.lt ">=" "assertLt"
      assertSLt =   genAssert (<)  Expr.slt ">=" "assertLt"
      assertGt =    genAssert (>)  Expr.gt "<=" "assertGt"
      assertSGt =   genAssert (>)  Expr.sgt "<=" "assertGt"
      assertLe =    genAssert (<=) Expr.leq ">" "assertLe"
      assertSLe =   genAssert (<=) (\a b -> Expr.iszero $ Expr.sgt a b) ">" "assertLe"
      assertGe =    genAssert (>=) Expr.geq "<" "assertGe"
      assertSGe =   genAssert (>=) (\a b -> Expr.iszero $ Expr.slt a b) "<" "assertGe"
      toStringCheat abitype sig input = do
        case decodeBuf [abitype] input of
          (CAbi [val],"") -> frameReturn $ AbiTuple $ V.fromList [AbiString $ Char8.pack $ show val]
          _ -> vmError (BadCheatCode ("toString parameter decoding failed for " <> show abitype) sig)
  
  -- * General call implementation ("delegateCall")
  -- note that the continuation is ignored in the precompile case
  delegateCall
    :: forall t s . (VMOps t, ?op :: Word8, ?conf :: Config, Typeable t)
    => Contract
    -> Gas t
    -> Expr EAddr
    -> Expr EAddr
    -> Expr EWord
    -> Expr EWord
    -> Expr EWord
    -> Expr EWord
    -> Expr EWord
    -> [Expr EWord]
    -> (Expr EAddr -> EVM t s ()) -- fallback
    -> (Expr EAddr -> EVM t s ()) -- continue
    -> EVM t s ()
  delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs fallback 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
        cheat gasGiven (xInOffset, xInSize) (xOutOffset, xOutSize) xs
    | otherwise =
        callChecks this gasGiven xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs $
          \xGas -> do
            resetCaller <- use $ #state % #resetCaller
            when resetCaller $ assign (#state % #overrideCaller) Nothing
            vm0 <- get
            fetchAccountWithFallback xTo (betterFallback xGas vm0) $ \target -> case target.code of
                UnknownCode _ -> betterFallback xGas vm0 xTo
                _ -> actualCall target xTo xGas vm0
    where
      betterFallback :: Gas t -> (VM t s) -> Expr 'EAddr -> EVM t s ()
      betterFallback xGas vm0 addr = onlyDeployed (forceEAddrToEWord addr) (fallback . forceEWordToEAddr) $ \a -> do
          let target = fromJust $ Map.lookup a vm0.env.contracts
          actualCall target a xGas vm0
      actualCall target addr xGas vm0 = do
          burn' xGas $ do
            calldata <- readMemory xInOffset xInSize
            abi <- maybeLitWordSimp . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4)
            let newContext = CallContext
                              { target    = addr
                              , 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 <$> VS.Mutable.new 0
            zoom #state $ do
              assign #gas xGas
              assign #pc 0
              assign #code (clearInitCode target.code)
              assign #codeContract addr
              assign #stack mempty
              assign #memory newMemory
              assign #memorySize 0
              assign #returndata mempty
              assign #calldata calldata
              assign #overrideCaller Nothing
              assign #resetCaller False
            continue addr
  
  -- -- * 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 :: forall t s. (?op :: Word8, ?conf::Config, VMOps t)
    => Expr EAddr -> Contract
    -> Expr EWord -> Gas t -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM t s ()
  create self this xSize xGas xValue xs newAddr initCode = do
    vm0 <- get
    -- are we exceeding the max init code size
    if xSize > Lit (vm0.block.maxCodeSize * 2)
    then do
      assign' (#state % #stack) (Lit 0 : xs)
      assign (#state % #returndata) mempty
      vmError $ MaxInitCodeSizeExceeded (vm0.block.maxCodeSize * 2) xSize
    -- are we overflowing the nonce
    else if this.nonce == Just maxBound
    then do
      assign' (#state % #stack) (Lit 0 : xs)
      assign (#state % #returndata) mempty
      pushTrace $ ErrorTrace NonceOverflow
      next
    -- are we overflowing the stack
    else if length vm0.frames >= 1024
    then do
      assign' (#state % #stack) (Lit 0 : xs)
      assign (#state % #returndata) mempty
      pushTrace $ ErrorTrace CallDepthLimitReached
      next
    -- are we deploying to an address that already has a contract?
    -- note: the symbolic interpreter generates constraints ensuring that
    -- symbolic storage keys cannot alias other storage keys, making this check
    -- safe to perform statically
    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 (?conf).maxDepth (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 -> unexpectedSymArg "initcode must have a concrete prefix" ([] :: [Expr EWord])
            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 Nothing -> AbstractStore a Nothing
                    SStore _ _ p -> resetStorage p
                    AbstractStore _ (Just _) -> internalError "unexpected logical store in EVM.hs"
                    GVar _  -> internalError "unexpected global variable"
  
              modifying (#env % #contracts % ix newAddr % #storage) resetStorage
              modifying (#env % #contracts % ix newAddr % #origStorage) resetStorage
              modifying (#tx % #subState % #createdContracts) (insert newAddr)
  
              transfer self newAddr xValue
  
              pushTrace (FrameTrace newContext)
              next
              vm1 <- get
              pushTo #frames $ Frame
                { context = newContext
                , state   = vm1.state { stack = xs }
                }
  
              state :: FrameState t s <- 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 constructor 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 t 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 t s ()
  replaceCodeOfSelf newCode = do
    vm <- get
    replaceCode vm.state.contract newCode
  
  resetState :: VMOps t => EVM t s ()
  resetState = do
    state <- lift blankState
    modify' $ \vm -> vm { result = Nothing, frames = [], state }
  
  -- * VM error implementation
  
  vmError :: VMOps t => EvmError -> EVM t s ()
  vmError e = finishFrame (FrameErrored e)
  
  wrap :: Typeable a => [Expr a] -> [SomeExpr]
  wrap = fmap SomeExpr
  
  underrun :: VMOps t => EVM t 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
  
  finishAllFramesAndStop :: VMOps t => EVM t s ()
  finishAllFramesAndStop = do
    vm <- get
    case vm.frames of
      [] -> finishFrame (FrameReturned mempty)
      _ -> do
        finishFrame (FrameReturned mempty)
        finishAllFramesAndStop
  
  -- | 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 :: VMOps t => FrameResult -> EVM t 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
          FrameReturned output -> ReturnTrace output nextFrame.context
          FrameReverted e -> ErrorTrace (Revert e)
          FrameErrored e -> ErrorTrace e
        -- Pop to the previous level of the debug trace stack.
        popTrace
  
        -- Pop the top frame.
        assign #frames remainingFrames
        -- Install the state of the frame to which we shall return.
        assign #state nextFrame.state
  
        -- 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 _ _ outOffset 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 oldVm
                push 1
  
              -- Case 2: Reverting during a call?
              FrameReverted output -> do
                revertContracts
                revertSubstate
                assign (#state % #returndata) output
                copyCallBytesToMemory output outSize outOffset
                reclaimRemainingGasAllowance oldVm
                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 oldVm
                      pushAddr createe
                case output of
                  ConcreteBuf bs ->
                    onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)
                  _ ->
                    case Expr.toList output of
                      Nothing -> partial $
                        UnexpectedSymbolicArg
                          oldVm.state.pc
                          oldVm.state.contract
                          (getOpName oldVm.state)
                          "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 oldVm
                push 0
  
              -- Case 6: Error during a creation?
              FrameErrored _ -> do
                revertContracts
                revertSubstate
                assign (#state % #returndata) mempty
                push 0
  
  
  -- * Memory helpers
  
  accessUnboundedMemoryRange
    :: VMOps t => Word64
    -> Word64
    -> EVM t s ()
    -> EVM t 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
    :: VMOps t
    => Expr EWord
    -> Expr EWord
    -> EVM t s ()
    -> EVM t s ()
  accessMemoryRange _ (Lit 0) continue = continue
  accessMemoryRange (Lit offs) (Lit sz) continue =
    case (,) <$> toWord64 offs <*> toWord64 sz of
      Nothing -> vmError IllegalOverflow
      Just (offs64, sz64) ->
        if offs64 + sz64 < sz64
          then vmError IllegalOverflow
          -- we need to limit these to <256MB because otherwise we could run out of memory
          -- in e.g. OpCalldatacopy and subsequent memory allocation when running with abstract gas.
          -- In these cases, the system would try to allocate a large (but <2**64 bytes) memory
          -- that leads to out-of-heap. Real-world scenarios cannot allocate 256MB of memory due to gas
          else if offs64 >= 0x0fffffff || sz64 >= 0x0fffffff
               then vmError IllegalOverflow
               else accessUnboundedMemoryRange offs64 sz64 continue
  -- we just ignore gas if we get symbolic inputs
  accessMemoryRange _ _ continue = continue
  
  accessMemoryWord
    :: VMOps t => Expr EWord -> EVM t s () -> EVM t s ()
  accessMemoryWord x = accessMemoryRange x (Lit 32)
  
  copyBytesToMemory
    :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM t 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 t s ()
  copyCallBytesToMemory bs size yOffset =
    copyBytesToMemory bs (Expr.min size (bufLength bs)) (Lit 0) yOffset
  
  readMemory :: Expr EWord -> Expr EWord -> EVM t 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 (VS.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 <- VS.freeze $ VS.Mutable.slice (unsafeInto offset) fromMemSize mem
              let dataFromMem = vectorToByteString 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 t s Trace
  withTraceLocation x = do
    vm <- get
    let this = fromJust $ currentContract vm
    pure Trace
      { tracedata = x
      , contract = this
      , opIx = fromMaybe 0 $ this.opIxMap VS.!? vm.state.pc
      }
  
  pushTrace :: TraceData -> EVM t s ()
  pushTrace x = do
    trace <- withTraceLocation x
    modifying #traces $
      \t -> Zipper.children $ Zipper.insert (Node trace []) t
  
  insertTrace :: TraceData -> EVM t s ()
  insertTrace x = do
    trace <- withTraceLocation x
    modifying #traces $
      \t -> Zipper.nextSpace $ Zipper.insert (Node trace []) t
  
  popTrace :: EVM t 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 t s -> Forest Trace
  traceForest vm = zipperRootForest vm.traces
  
  traceForest' :: Expr End -> Forest Trace
  traceForest' (Success _ (TraceContext f _ _) _ _) = f
  traceForest' (Partial _ (TraceContext f _ _) _) = f
  traceForest' (Failure _ (TraceContext f _ _) _) = f
  traceForest' (ITE {}) = internalError"Internal Error: ITE does not contain a trace"
  traceForest' (GVar {}) = internalError"Internal Error: Unexpected GVar"
  
  traceContext :: Expr End -> TraceContext
  traceContext (Success _ c _ _) = c
  traceContext (Partial _ c _) = c
  traceContext (Failure _ c _) = c
  traceContext (ITE {}) = internalError"Internal Error: ITE does not contain a trace"
  traceContext (GVar {}) = internalError"Internal Error: Unexpected GVar"
  
  traceTopLog :: [Expr Log] -> EVM t 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 t s ()
  push = pushSym . Lit
  
  pushSym :: Expr EWord -> EVM t s ()
  pushSym x = modifying' (#state % #stack) (x :)
  
  pushAddr :: Expr EAddr -> EVM t s ()
  pushAddr (LitAddr x) = modifying' (#state % #stack) (Lit (into x) :)
  pushAddr x@(SymAddr _) = modifying' (#state % #stack) (WAddr x :)
  pushAddr (GVar _) = internalError "Unexpected GVar"
  
  stackOp1
    :: (?op :: Word8, VMOps t)
    => Word64
    -> (Expr EWord -> Expr EWord)
    -> EVM t s ()
  stackOp1 cost f =
    use (#state % #stack) >>= \case
      x:xs ->
        burn cost $ do
          next
          let !y = f x
          assign' (#state % #stack) $ y : xs
      _ ->
        underrun
  
  stackOp2
    :: (?op :: Word8, VMOps t)
    => Word64
    -> (Expr EWord -> Expr EWord -> Expr EWord)
    -> EVM t s ()
  stackOp2 cost f =
    use (#state % #stack) >>= \case
      x:y:xs ->
        burn cost $ do
          next
          assign' (#state % #stack) $ f x y : xs
      _ ->
        underrun
  
  stackOp3
    :: (?op :: Word8, VMOps t)
    => Word64
    -> (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord)
    -> EVM t s ()
  stackOp3 cost f =
    use (#state % #stack) >>= \case
      x:y:z:xs ->
        burn cost $ do
        next
        assign' (#state % #stack) $ f x y z : xs
      _ ->
        underrun
  
  -- * Bytecode data functions
  
  checkJump :: VMOps t => Int -> [Expr EWord] -> EVM t s ()
  checkJump x xs = noJumpIntoInitData x $ do
    vm <- get
    case isValidJumpDest vm x of
      True -> do
        assign' (#state % #stack) xs
        assign' (#state % #pc) x
      False -> vmError BadJumpDestination
  
  -- fails with partial if we're trying to jump into the symbolic region of an `InitCode`
  noJumpIntoInitData :: VMOps t => Int -> EVM t s () -> EVM t 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 vm.state.contract idx
                        else cont
      -- we're not executing init code, so nothing to check here
      _ -> cont
  
  isValidJumpDest :: VM t 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 >>= maybeLitByteSimp
    in case op of
         Nothing -> False
         Just b -> 0x5b == b && (isJust $ contract.opIxMap VS.!? x)
           && (isJust $ contract.codeOps V.!? (contract.opIxMap VS.! x))
           && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap VS.! 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 -> VS.Vector Int
  mkOpIxMap (UnknownCode _) = internalError "Cannot build opIxMap for unknown code"
  mkOpIxMap (InitCode conc _)
    = VS.create $ VS.Mutable.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 >> VS.Mutable.write v i j)
          go v (1, !i, !j, !m) _ =
            {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> VS.Mutable.write v i j)
          go v (0, !i, !j, !m) _ =
            {- Other op. -}         (0,            i + 1, j + 1, m >> VS.Mutable.write v i j)
          go v (n, !i, !j, !m) _ =
            {- PUSH data. -}        (n - 1,        i + 1, j,     m >> VS.Mutable.write v i j)
  
  mkOpIxMap (RuntimeCode (ConcreteRuntimeCode ops)) =
    mkOpIxMap (InitCode ops mempty) -- a bit hacky
  
  mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))
    = VS.create $ VS.Mutable.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 maybeLitByteSimp x of
            Just x' -> if x' >= 0x60 && x' <= 0x7f
              -- start of PUSH op --
                       then (x' - 0x60 + 1, i + 1, j,     m >> VS.Mutable.write v i j)
              -- other data --
                       else (0,             i + 1, j + 1, m >> VS.Mutable.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 >> VS.Mutable.write v i j)
          go v (n, !i, !j, !m) _ =
            {- PUSH data. -}        (n - 1,        i + 1, j,     m >> VS.Mutable.write v i j)
  
  
  vmOp :: VM t 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") . maybeLitByteSimp $ xs' V.! i , V.toList $ V.drop i xs')
    in if (opslen code' < i)
       then Nothing
       else Just (readOp op pushdata)
  
  vmOpIx :: VM t s -> Maybe Int
  vmOpIx vm =
    do self <- currentContract vm
       self.opIxMap VS.!? vm.state.pc
  
  -- Maps operation indices 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") $ maybeLitByteSimp x
                j = opSize x'
            in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)
  
  -- * Gas cost calculation helpers
  
  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 t s CodeLocation
  codeloc = do
    vm <- get
    pure (vm.state.contract, vm.state.pc)
  
  createAddress :: Expr EAddr -> Maybe W64 -> EVM t 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 t s (Expr EAddr)
  create2Address (LitAddr a) s b = pure $ Concrete.create2Address a s b
  create2Address (SymAddr _) _ _ = freshSymAddr
  create2Address (GVar _) _ _ = internalError "Unexpected GVar"
  
  freshSymAddr :: EVM t 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 t s ()
  writeMemory memory offset buf = do
    memory' <- expandMemory (offset + BS.length buf)
    VS.iforM_ (byteStringToVector buf) $ \i v -> do
      VS.Mutable.unsafeWrite memory' (offset + i) v
    where
    expandMemory requiredSize = do
      let currentSize = VS.Mutable.length memory
      let toAlloc = requiredSize - currentSize
      if toAlloc > 0 then do
        -- As grow does a larger *copy* of the vector on a new place,
        -- we double the vector size to avoid the performance impact
        -- that would happen with repeated small expansion operations.
        let growthFactor = 2
        let targetSize = requiredSize * growthFactor
        -- Always grow at least 8k
        let toGrow = max 8192 $ targetSize - currentSize
        memory' <- VS.Mutable.grow memory toGrow
        assign (#state % #memory) (ConcreteMemory memory')
        pure memory'
      else
        pure memory
  
  freezeMemory :: MutableMemory s -> EVM t s (Expr Buf)
  freezeMemory memory =
    ConcreteBuf . vectorToByteString <$> VS.freeze memory
  
  
  instance VMOps Symbolic where
    burn' _ continue = continue
    burnExp _ continue = continue
    burnSha3 _ continue = continue
    burnCalldatacopy _ continue = continue
    burnCodecopy _ continue = continue
    burnExtcodecopy _ _ continue = continue
    burnReturndatacopy _ continue = continue
    burnLog _ _ continue = continue
  
    initialGas = ()
    ensureGas _ continue = continue
    gasTryFrom _ = Right ()
    costOfCreate _ _ _ _ = ((), ())
    costOfCall _ _ _ _ _ _ continue = continue 0 0
    reclaimRemainingGasAllowance _ = pure ()
    payRefunds = pure ()
    pushGas = do
      modifying (#env % #freshGasVals) (+ 1)
      n <- use (#env % #freshGasVals)
      pushSym $ Expr.Gas "" n
    enoughGas _ _ = True
    subGas _ _ = ()
    toGas _ = ()
    whenSymbolicElse a _ = a
  
    partial e = assign #result $ Just (Unfinished e)
    branch depthLimit cond continue = do
      loc <- codeloc
      pathconds <- use #constraints
      vm <- get
      query $ PleaseAskSMT cond pathconds (runBothPaths loc vm.exploreDepth)
      where
        condSimp = Expr.simplify cond
        condSimpConc = Expr.concKeccakSimpExpr condSimp
        runBothPaths loc _ (Case v) = do
          assign #result Nothing
          pushTo #constraints $ if v then Expr.simplifyProp (Lit 0 ./= condSimpConc)
                                     else Expr.simplifyProp (Lit 0 .== condSimpConc)
          (iteration, _) <- use (#iterations % at loc % non (0,[]))
          stack <- use (#state % #stack)
          assign (#pathsVisited % at (loc, iteration)) (Just v)
          assign (#iterations % at loc) (Just (iteration + 1, stack))
          continue v
        -- Both paths are possible; we ask for more input
        runBothPaths loc exploreDepth UnknownBranch =
          (runBoth depthLimit exploreDepth ) . PleaseRunBoth condSimp $ (runBothPaths loc exploreDepth) . Case
  
    -- numBytes allows us to specify how many bytes of the returned value is relevant
    -- if it's e.g.a JUMP, only 2 bytes can be relevant. This allows us to avoid
    -- getting solutions that are nonsensical
    manySolutions maxDepth ewordExpr numBytes continue = do
      pathconds <- use #constraints
      vm <- get
      query $ PleaseGetSols ewordExpr numBytes pathconds $ \case
        Just concVals -> do
          assign #result Nothing
          case concVals of
            -- zero solutions means that we are in a branch that's not possible
            -- so revert all frames and stop all execution on this branch
            [] -> finishAllFramesAndStop
            [val] -> do
              assign #result Nothing
              pushTo #constraints $ Expr.simplifyProp (ewordExpr .== (Lit val))
              continue $ Just val
            _ -> runAll maxDepth vm.exploreDepth $ PleaseRunAll ewordExpr (map Lit concVals) runAllPaths
        Nothing -> do
          assign #result Nothing
          continue Nothing
      where
        runAllPaths val = do
          assign #result Nothing
          pushTo #constraints $ Expr.simplifyProp (ewordExpr .== val)
          case val of
            Lit v -> continue $ Just v
            _ -> internalError "runAllPaths can only get concrete values here"
  
  instance VMOps Concrete where
    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)
  
    burnExp (forceLit -> exponent) continue = do
      FeeSchedule {..} <- gets (.block.schedule)
      let cost = if exponent == 0
            then g_exp
            else g_exp + g_expbyte * unsafeInto (ceilDiv (1 + log2 exponent) 8)
      burn cost continue
  
    burnSha3 (forceLit -> xSize) continue = do
      FeeSchedule {..} <- gets (.block.schedule)
      burn (g_sha3 + g_sha3word * ceilDiv (unsafeInto xSize) 32) continue
  
    burnCalldatacopy (forceLit -> xSize) continue = do
      FeeSchedule {..} <- gets (.block.schedule)
      burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) continue
  
    burnCodecopy (forceLit -> n) continue =
      case tryFrom n of
        Left _ -> vmError IllegalOverflow
        Right n' -> do
          FeeSchedule {..} <- gets (.block.schedule)
          if n' <= ( (maxBound :: Word64) - g_verylow ) `div` g_copy * 32 then
            burn (g_verylow + g_copy * ceilDiv (unsafeInto n) 32) continue
          else vmError IllegalOverflow
  
    burnExtcodecopy extAccount (forceLit -> codeSize) continue = do
      FeeSchedule {..} <- gets (.block.schedule)
      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) continue
  
    burnReturndatacopy (forceLit -> xSize) continue = do
      FeeSchedule {..} <- gets (.block.schedule)
      burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) continue
  
    burnLog (forceLit -> xSize) n continue = do
      case tryFrom xSize of
        Right sz -> do
          FeeSchedule {..} <- gets (.block.schedule)
          burn (g_log + g_logdata * sz + (into n) * g_logtopic) continue
        _ -> vmError IllegalOverflow
  
    initialGas = 0
  
    ensureGas amount continue = do
      availableGas <- use (#state % #gas)
  
      if availableGas <= amount then
        vmError (OutOfGas availableGas amount)
      else continue
  
    gasTryFrom (forceLit -> w256) =
      case tryFrom w256 of
        Left _ -> Left ()
        Right a -> Right a
  
    -- Gas cost of create, including hash cost if needed
    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 (forceLit size)) 32)
        initGas    = allButOne64th (availableGas - createCost)
  
    -- Gas cost function for CALL, transliterated from the Yellow Paper.
    costOfCall (FeeSchedule {..}) recipientExists (forceLit -> xValue) availableGas xGas target continue = 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
      let (cost, gas') = (c_gascap + c_extra, c_callgas)
      continue cost gas'
  
    -- When entering a call, the gas allowance is counted as burned
    -- in advance; this unburns the remainder and adds it to the
    -- parent frame.
    reclaimRemainingGasAllowance oldVm = do
      let remainingGas = oldVm.state.gas
      modifying #burned (subtract remainingGas)
      modifying (#state % #gas) (+ remainingGas)
  
    payRefunds = do
      -- 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)
  
    pushGas = do
      vm <- get
      push (into vm.state.gas)
  
    enoughGas cost gasCap = cost <= gasCap
    subGas gasCap cost = gasCap - cost
    toGas = id
    whenSymbolicElse _ a = a
    partial _ = internalError "won't happen during concrete exec"
    branch _ (forceLit -> cond) continue = continue (cond > 0)
    manySolutions _ _ _ = internalError "SMT solver should never be needed in concrete mode"
  
  -- Create symbolic VM from concrete VM
  symbolify :: VM Concrete s -> VM Symbolic s
  symbolify vm =
    vm { result = symbolifyResult <$> vm.result
       , state  = symbolifyFrameState vm.state
       , frames = symbolifyFrame <$> vm.frames
       , burned = ()
       }
  
  symbolifyFrameState :: FrameState Concrete s -> FrameState Symbolic s
  symbolifyFrameState state = state { gas = () }
  
  symbolifyFrame :: Frame Concrete s -> Frame Symbolic s
  symbolifyFrame frame = frame { state = symbolifyFrameState frame.state }
  
  symbolifyResult :: VMResult Concrete s -> VMResult Symbolic s
  symbolifyResult result =
    case result of
      HandleEffect _ -> internalError "shouldn't happen"
      VMFailure e -> VMFailure e
      VMSuccess b -> VMSuccess b
  
  
  burn :: VMOps t => Word64 -> EVM t s () -> EVM t s ()
  burn = burn' . toGas
  