{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImplicitParams #-}

module EVM where

import Prelude hiding (exponent)

import Optics.Core
import Optics.State
import Optics.State.Operators
import Optics.Zoom
import Optics.Operators.Unsafe

import EVM.ABI
import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord,
  writeByte, bufLength, indexWord, litAddr, readBytes, word256At, copySlice, wordToAddr)
import EVM.Expr qualified as Expr
import EVM.FeeSchedule (FeeSchedule (..))
import EVM.Op
import EVM.Precompiled qualified
import EVM.Solidity
import EVM.Types
import EVM.Types qualified as Expr (Expr(Gas))
import EVM.Sign qualified
import EVM.Concrete qualified as Concrete

import Control.Monad.ST (ST)
import Control.Monad.State.Strict hiding (state)
import Data.Bits (FiniteBits, countLeadingZeros, finiteBitSize)
import Data.ByteArray qualified as BA
import Data.ByteString (ByteString)
import Data.ByteString qualified as BS
import Data.ByteString.Lazy (fromStrict)
import Data.ByteString.Lazy qualified as LS
import Data.ByteString.Char8 qualified as Char8
import Data.Foldable (toList)
import Data.List (find)
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Maybe (fromMaybe, fromJust, isJust)
import Data.Set (insert, member, fromList)
import Data.Sequence (Seq)
import Data.Sequence qualified as Seq
import Data.Text (unpack, pack)
import Data.Text.Encoding (decodeUtf8)
import Data.Tree
import Data.Tree.Zipper qualified as Zipper
import Data.Typeable
import Data.Vector qualified as V
import Data.Vector.Storable qualified as SV
import Data.Vector.Storable.Mutable qualified as SV
import Data.Vector.Unboxed qualified as VUnboxed
import Data.Vector.Unboxed.Mutable qualified as VUnboxed.Mutable
import Data.Word (Word8, Word32, Word64)
import Witch (into, tryFrom, unsafeInto)

import Crypto.Hash (Digest, SHA256, RIPEMD160)
import Crypto.Hash qualified as Crypto
import Crypto.Number.ModArithmetic (expFast)

blankState :: VMOps t => ST s (FrameState t s)
blankState = do
  memory <- ConcreteMemory <$> VUnboxed.Mutable.new 0
  pure $ FrameState
    { contract     = LitAddr 0
    , codeContract = LitAddr 0
    , code         = RuntimeCode (ConcreteRuntimeCode "")
    , pc           = 0
    , stack        = mempty
    , memory
    , memorySize   = 0
    , calldata     = mempty
    , callvalue    = Lit 0
    , caller       = LitAddr 0
    , gas          = initialGas
    , returndata   = mempty
    , static       = False
    }

-- | An "external" view of a contract's bytecode, appropriate for
-- e.g. @EXTCODEHASH@.
bytecode :: Getter Contract (Maybe (Expr Buf))
bytecode = #code % to f
  where f (InitCode _ _) = Just mempty
        f (RuntimeCode (ConcreteRuntimeCode bs)) = Just $ ConcreteBuf bs
        f (RuntimeCode (SymbolicRuntimeCode ops)) = Just $ Expr.fromList ops
        f (UnknownCode _) = Nothing

-- * Data accessors

currentContract :: VM 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 <$> VUnboxed.Mutable.new 0
  pure $ VM
    { result = Nothing
    , frames = mempty
    , tx = TxState
      { gasprice = o.gasprice
      , gaslimit = o.gaslimit
      , priorityFee = o.priorityFee
      , origin = txorigin
      , toAddr = txtoAddr
      , value = o.value
      , substate = SubState mempty touched initialAccessedAddrs initialAccessedStorageKeys mempty
      , isCreate = o.create
      , txReversion = Map.fromList ((o.address,o.contract):o.otherContracts)
      }
    , logs = []
    , traces = Zipper.fromForest []
    , block = block
    , state = FrameState
      { pc = 0
      , stack = mempty
      , memory
      , memorySize = 0
      , code = o.contract.code
      , contract = o.address
      , codeContract = o.address
      , calldata = fst o.calldata
      , callvalue = o.value
      , caller = o.caller
      , gas = o.gas
      , returndata = mempty
      , static = False
      }
    , env = env
    , cache = cache
    , burned = initialGas
    , constraints = snd o.calldata
    , iterations = mempty
    , config = RuntimeConfig
      { allowFFI = o.allowFFI
      , overrideCaller = Nothing
      , baseState = o.baseState
      }
    , forks = Seq.singleton (ForkState env block cache "")
    , currentFork = 0
    }
    where
    env = Env
      { chainId = o.chainId
      , contracts = Map.fromList ((o.address,o.contract):o.otherContracts)
      , freshAddresses = 0
      , 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
      }
    cache = Cache mempty mempty

-- | Initialize an abstract contract with unknown code
unknownContract :: Expr EAddr -> Contract
unknownContract addr = Contract
  { code        = UnknownCode addr
  , storage     = 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
  , 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
  , 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))

-- | Executes the EVM one step
exec1 :: forall (t :: VMType) s. VMOps t => EVM t s ()
exec1 = do
  vm <- get

  let
    -- Convenient aliases
    stk  = vm.state.stack
    self = vm.state.contract
    this = fromMaybe (internalError "state contract") (Map.lookup self vm.env.contracts)

    fees@FeeSchedule {..} = vm.block.schedule

    doStop = finishFrame (FrameReturned mempty)

    litSelf = maybeLitAddr self

  if isJust litSelf && (fromJust litSelf) > 0x0 && (fromJust litSelf) <= 0x9 then do
    -- call to precompile
    let ?op = 0x00 -- dummy value
    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 -> partial $
               UnexpectedSymbolicArg vmx.state.pc "precompile returned a symbolic value" (wrap [e])
      _ ->
        underrun

  else if vm.state.pc >= opslen vm.state.code
    then doStop

    else do
      let ?op = case vm.state.code of
                  UnknownCode _ -> internalError "Cannot execute unknown code"
                  InitCode conc _ -> BS.index conc vm.state.pc
                  RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs vm.state.pc
                  RuntimeCode (SymbolicRuntimeCode ops) ->
                    fromMaybe (internalError "could not analyze symbolic code") $
                      maybeLitByte $ ops V.! vm.state.pc

      case getOp (?op) of

        OpPush0 -> do
          limitStack 1 $
            burn g_base $ do
              next
              pushSym (Lit 0)

        OpPush n' -> do
          let n = into n'
              !xs = case vm.state.code of
                UnknownCode _ -> internalError "Cannot execute unknown code"
                InitCode conc _ -> Lit $ word $ padRight n $ BS.take n (BS.drop (1 + vm.state.pc) conc)
                RuntimeCode (ConcreteRuntimeCode bs) -> Lit $ word $ BS.take n $ BS.drop (1 + vm.state.pc) bs
                RuntimeCode (SymbolicRuntimeCode ops) ->
                  let bytes = V.take n $ V.drop (1 + vm.state.pc) ops
                  in readWord (Lit 0) $ Expr.fromList $ padLeft' 32 bytes
          limitStack 1 $
            burn g_verylow $ do
              next
              pushSym xs

        OpDup i ->
          case preview (ix (into i - 1)) stk of
            Nothing -> underrun
            Just y ->
              limitStack 1 $
                burn g_verylow $ do
                  next
                  pushSym y

        OpSwap i ->
          if length stk < (into i) + 1
            then underrun
            else
              burn g_verylow $ do
                next
                zoom (#state % #stack) $ do
                  assign (ix 0) (stk ^?! ix (into i))
                  assign (ix (into i)) (stk ^?! ix 0)

        OpLog n ->
          notStatic $
          case stk of
            (xOffset:xSize:xs) ->
              if length xs < (into n)
              then underrun
              else 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 -> doStop

        OpAdd -> stackOp2 g_verylow Expr.add
        OpMul -> stackOp2 g_low Expr.mul
        OpSub -> stackOp2 g_verylow Expr.sub

        OpDiv -> stackOp2 g_low Expr.div

        OpSdiv -> stackOp2 g_low Expr.sdiv

        OpMod -> stackOp2 g_low Expr.mod

        OpSmod -> stackOp2 g_low Expr.smod
        OpAddmod -> stackOp3 g_mid Expr.addmod
        OpMulmod -> stackOp3 g_mid Expr.mulmod

        OpLt -> stackOp2 g_verylow Expr.lt
        OpGt -> stackOp2 g_verylow Expr.gt
        OpSlt -> stackOp2 g_verylow Expr.slt
        OpSgt -> stackOp2 g_verylow Expr.sgt

        OpEq -> stackOp2 g_verylow Expr.eq
        OpIszero -> stackOp1 g_verylow Expr.iszero

        OpAnd -> stackOp2 g_verylow Expr.and
        OpOr -> stackOp2 g_verylow Expr.or
        OpXor -> stackOp2 g_verylow Expr.xor
        OpNot -> stackOp1 g_verylow Expr.not

        OpByte -> stackOp2 g_verylow (\i w -> Expr.padByte $ Expr.indexWord i w)

        OpShl -> stackOp2 g_verylow Expr.shl
        OpShr -> stackOp2 g_verylow Expr.shr
        OpSar -> stackOp2 g_verylow Expr.sar

        -- more accurately referred to as KECCAK
        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)
                        (pure $ Lit (keccak' bs))
                    buf -> pure $ Keccak buf
                  next
                  assign (#state % #stack) (hash : xs)
            _ -> underrun

        OpAddress ->
          limitStack 1 $
            burn g_base (next >> pushAddr self)

        OpBalance ->
          case stk of
            x:xs -> forceAddr x "BALANCE" $ \a ->
              accessAndBurn a $
                fetchAccount a $ \c -> do
                  next
                  assign (#state % #stack) xs
                  pushSym c.balance
            [] ->
              underrun

        OpOrigin ->
          limitStack 1 . burn g_base $
            next >> pushAddr vm.tx.origin

        OpCaller ->
          limitStack 1 . burn g_base $
            next >> pushAddr vm.state.caller

        OpCallvalue ->
          limitStack 1 . burn g_base $
            next >> pushSym vm.state.callvalue

        OpCalldataload -> stackOp1 g_verylow $
          \ind -> Expr.readWord ind vm.state.calldata

        OpCalldatasize ->
          limitStack 1 . burn g_base $
            next >> pushSym (bufLength vm.state.calldata)

        OpCalldatacopy ->
          case stk of
            xTo:xFrom:xSize:xs ->
              burnCalldatacopy xSize $
                accessMemoryRange xTo xSize $ do
                  next
                  assign (#state % #stack) xs
                  copyBytesToMemory vm.state.calldata xSize xFrom xTo
            _ -> underrun

        OpCodesize ->
          limitStack 1 . burn g_base $
            next >> pushSym (codelen vm.state.code)

        OpCodecopy ->
          case stk of
            memOffset:codeOffset:n:xs ->
              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 ->
          limitStack 1 . burn g_base $
            next >> push vm.tx.gasprice

        OpExtcodesize ->
          case stk of
            x':xs -> forceAddr x' "EXTCODESIZE" $ \x -> do
              let impl = accessAndBurn x $
                           fetchAccount x $ \c -> do
                             next
                             assign (#state % #stack) xs
                             case view bytecode c of
                               Just b -> pushSym (bufLength b)
                               Nothing -> pushSym $ CodeSize x
              case x of
                a@(LitAddr _) -> if a == cheatCode
                  then do
                    next
                    assign (#state % #stack) xs
                    pushSym (Lit 1)
                  else impl
                _ -> impl
            [] ->
              underrun

        OpExtcodecopy ->
          case stk of
            extAccount':memOffset:codeOffset:codeSize:xs ->
              forceAddr extAccount' "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 -> do
                          pc <- use (#state % #pc)
                          partial $ UnexpectedSymbolicArg pc "Cannot copy from unknown code at" (wrap [extAccount])
            _ -> underrun

        OpReturndatasize ->
          limitStack 1 . burn g_base $
            next >> pushSym (bufLength vm.state.returndata)

        OpReturndatacopy ->
          case stk of
            xTo:xFrom:xSize:xs ->
              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 (Expr.or oob overflow) jump
            _ -> underrun

        OpExtcodehash ->
          case stk of
            x':xs -> forceAddr x' "EXTCODEHASH" $ \x ->
              accessAndBurn x $ do
                next
                assign (#state % #stack) xs
                fetchAccount x $ \c ->
                   if accountEmpty c
                     then push (W256 0)
                     else case view bytecode c of
                            Just b -> pushSym $ keccak b
                            Nothing -> pushSym $ CodeHash x
            [] ->
              underrun

        OpBlockhash -> do
          -- We adopt the fake block hash scheme of the VMTests,
          -- so that blockhash(i) is the hash of i as decimal ASCII.
          stackOp1 g_blockhash $ \case
            Lit i -> if i + 256 < vm.block.number || i >= vm.block.number
                     then Lit 0
                     else (into i :: Integer) & show & Char8.pack & keccak' & Lit
            i -> BlockHash i

        OpCoinbase ->
          limitStack 1 . burn g_base $
            next >> pushAddr vm.block.coinbase

        OpTimestamp ->
          limitStack 1 . burn g_base $
            next >> pushSym vm.block.timestamp

        OpNumber ->
          limitStack 1 . burn g_base $
            next >> push vm.block.number

        OpPrevRandao -> do
          limitStack 1 . burn g_base $
            next >> push vm.block.prevRandao

        OpGaslimit ->
          limitStack 1 . burn g_base $
            next >> push (into vm.block.gaslimit)

        OpChainid ->
          limitStack 1 . burn g_base $
            next >> push vm.env.chainId

        OpSelfbalance ->
          limitStack 1 . burn g_low $
            next >> pushSym this.balance

        OpBaseFee ->
          limitStack 1 . burn g_base $
            next >> push vm.block.baseFee

        OpPop ->
          case stk of
            _:xs -> burn g_base (next >> assign (#state % #stack) xs)
            _    -> underrun

        OpMload ->
          case stk of
            x:xs ->
              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

        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 ->
          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 ->
          case stk of
            x:xs -> do
              acc <- accessStorageForGas self x
              let cost = if acc then g_warm_storage_read else g_cold_sload
              burn cost $
                accessStorage self x $ \y -> do
                  next
                  assign (#state % #stack) (y:xs)
            _ -> underrun

        OpSstore ->
          notStatic $
          case stk of
            x:new:xs ->
              accessStorage self x $ \current -> do
                ensureGas g_callstipend $ do
                  let
                    original =
                      case Expr.concKeccakSimpExpr $ SLoad x this.origStorage of
                        Lit v -> v
                        _ -> 0
                    storage_cost =
                      case (maybeLitWord current, maybeLitWord new) of
                        (Just current', Just new') ->
                           if (current' == new') then g_sload
                           else if (current' == original) && (original == 0) then g_sset
                           else if (current' == original) then g_sreset
                           else g_sload

                        -- if any of the arguments are symbolic,
                        -- assume worst case scenario
                        _-> g_sset

                  acc <- accessStorageForGas self x
                  let cold_storage_cost = if acc then 0 else g_cold_sload
                  burn (storage_cost + cold_storage_cost) $ do
                    next
                    assign (#state % #stack) xs
                    modifying (#env % #contracts % ix self % #storage) (writeStorage x new)

                    case (maybeLitWord current, maybeLitWord new) of
                       (Just current', Just new') ->
                          unless (current' == new') $
                            if current' == original then
                              when (original /= 0 && new' == 0) $
                                refund (g_sreset + g_access_list_storage_key)
                            else do
                              when (original /= 0) $
                                if current' == 0
                                then unRefund (g_sreset + g_access_list_storage_key)
                                else when (new' == 0) $ refund (g_sreset + g_access_list_storage_key)
                              when (original == new') $
                                if original == 0
                                then refund (g_sset - g_sload)
                                else refund (g_sreset - g_sload)
                       -- if any of the arguments are symbolic,
                       -- don't change the refund counter
                       _ -> noop
            _ -> underrun

        OpJump ->
          case stk of
            x:xs ->
              burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' ->
                case toInt x' of
                  Nothing -> vmError BadJumpDestination
                  Just i -> checkJump i xs
            _ -> underrun

        OpJumpi ->
          case stk of
            x:y:xs -> forceConcrete x "JUMPI: symbolic jumpdest" $ \x' ->
              burn g_high $
                let jump :: Bool -> EVM t s ()
                    jump False = assign (#state % #stack) xs >> next
                    jump _    = case toInt x' of
                      Nothing -> vmError BadJumpDestination
                      Just i -> checkJump i xs
                in branch y jump
            _ -> underrun

        OpPc ->
          limitStack 1 . burn g_base $
            next >> push (unsafeInto vm.state.pc)

        OpMsize ->
          limitStack 1 . burn g_base $
            next >> push (into vm.state.memorySize)

        OpGas ->
          limitStack 1 . burn g_base $
            next >> pushGas

        OpJumpdest -> burn g_jumpdest next

        OpExp ->
          -- NOTE: this can be done symbolically using unrolling like this:
          --       https://hackage.haskell.org/package/sbv-9.0/docs/src/Data.SBV.Core.Model.html#.%5E
          --       However, it requires symbolic gas, since the gas depends on the exponent
          case stk of
            base:exponent:xs ->
              burnExp exponent $ do
                next
                (#state % #stack) .= Expr.exp base exponent : xs
            _ -> underrun

        OpSignextend -> stackOp2 g_low Expr.sex

        OpCreate ->
          notStatic $
          case stk of
            xValue:xOffset:xSize:xs ->
              accessMemoryRange xOffset xSize $ do
                availableGas <- use (#state % #gas)
                let
                  (cost, gas') = costOfCreate fees availableGas xSize False
                newAddr <- createAddress self this.nonce
                _ <- accessAccountForGas newAddr
                burn' cost $ do
                  initCode <- readMemory xOffset xSize
                  create self this xSize gas' xValue xs newAddr initCode
            _ -> underrun

        OpCall ->
          case stk of
            xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
              branch (Expr.gt xValue (Lit 0)) $ \gt0 -> do
                (if gt0 then notStatic else id) $
                  forceAddr xTo' "unable to determine a call target" $ \xTo ->
                    case gasTryFrom xGas of
                      Left _ -> vmError IllegalOverflow
                      Right gas ->
                        delegateCall this gas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $
                          \callee -> do
                            let from' = fromMaybe self vm.config.overrideCaller
                            zoom #state $ do
                              assign #callvalue xValue
                              assign #caller from'
                              assign #contract callee
                            assign (#config % #overrideCaller) Nothing
                            touchAccount from'
                            touchAccount callee
                            transfer from' callee xValue
            _ ->
              underrun

        OpCallcode ->
          case stk of
            xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
              forceAddr xTo' "unable to determine a call target" $ \xTo ->
                case gasTryFrom xGas of
                  Left _ -> vmError IllegalOverflow
                  Right gas ->
                    delegateCall this gas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do
                      zoom #state $ do
                        assign #callvalue xValue
                        assign #caller $ fromMaybe self vm.config.overrideCaller
                      assign (#config % #overrideCaller) Nothing
                      touchAccount self
            _ ->
              underrun

        OpReturn ->
          case stk of
            xOffset:xSize:_ ->
              accessMemoryRange xOffset xSize $ do
                output <- readMemory xOffset xSize
                let
                  codesize = fromMaybe (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data")
                               . maybeLitWord . bufLength $ output
                  maxsize = vm.block.maxCodeSize
                  creation = case vm.frames of
                    [] -> vm.tx.isCreate
                    frame:_ -> case frame.context of
                       CreationContext {} -> True
                       CallContext {} -> False
                if creation
                then
                  if codesize > maxsize
                  then
                    finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))
                  else do
                    let frameReturned = burn (g_codedeposit * unsafeInto codesize) $
                                          finishFrame (FrameReturned output)
                        frameErrored = finishFrame $ FrameErrored InvalidFormat
                    case readByte (Lit 0) output of
                      LitByte 0xef -> frameErrored
                      LitByte _ -> frameReturned
                      y -> branch (Expr.eqByte y (LitByte 0xef)) $ \case
                          True -> frameErrored
                          False -> frameReturned
                else
                   finishFrame (FrameReturned output)
            _ -> underrun

        OpDelegatecall ->
          case stk of
            xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
              case wordToAddr xTo of
                Nothing -> do
                  loc <- codeloc
                  let msg = "Unable to determine a call target"
                  partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]
                Just xTo' ->
                  case gasTryFrom xGas of
                    Left _ -> vmError IllegalOverflow
                    Right gas ->
                      delegateCall this gas xTo' self (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $
                        \_ -> touchAccount self
            _ -> underrun

        OpCreate2 -> notStatic $
          case stk of
            xValue:xOffset:xSize:xSalt':xs ->
              forceConcrete xSalt' "CREATE2" $ \(xSalt) ->
                accessMemoryRange xOffset xSize $ do
                  availableGas <- use (#state % #gas)
                  buf <- readMemory xOffset xSize
                  forceConcreteBuf buf "CREATE2" $
                    \initCode -> do
                      let
                        (cost, gas') = costOfCreate fees availableGas xSize True
                      newAddr <- create2Address self xSalt initCode
                      _ <- accessAccountForGas newAddr
                      burn' cost $
                        create self this xSize gas' xValue xs newAddr (ConcreteBuf initCode)
            _ -> underrun

        OpStaticcall ->
          case stk of
            xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
              case wordToAddr xTo of
                Nothing -> do
                  loc <- codeloc
                  let msg = "Unable to determine a call target"
                  partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]
                Just xTo' ->
                  case gasTryFrom xGas of
                    Left _ -> vmError IllegalOverflow
                    Right gas ->
                      delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $
                        \callee -> do
                          zoom #state $ do
                            assign #callvalue (Lit 0)
                            assign #caller $ fromMaybe self (vm.config.overrideCaller)
                            assign #contract callee
                            assign #static True
                          assign (#config % #overrideCaller) Nothing
                          touchAccount self
                          touchAccount callee
            _ ->
              underrun

        OpSelfdestruct ->
          notStatic $
          case stk of
            [] -> underrun
            (xTo':_) -> forceAddr xTo' "SELFDESTRUCT" $ \case
              xTo@(LitAddr _) -> do
                acc <- accessAccountForGas xTo
                let cost = if acc then 0 else g_cold_account_access
                    funds = this.balance
                    recipientExists = accountExists xTo vm
                branch (Expr.iszero $ Expr.eq funds (Lit 0)) $ \hasFunds -> do
                  let c_new = if (not recipientExists) && hasFunds
                              then g_selfdestruct_newaccount
                              else 0
                  burn (g_selfdestruct + c_new + cost) $ do
                    selfdestruct self
                    touchAccount xTo

                    if hasFunds
                    then fetchAccount xTo $ \_ -> do
                           #env % #contracts % ix xTo % #balance %= (Expr.add funds)
                           assign (#env % #contracts % ix self % #balance) (Lit 0)
                           doStop
                    else do
                      doStop
              a -> do
                pc <- use (#state % #pc)
                partial $ UnexpectedSymbolicArg pc "trying to self destruct to a symbolic address" (wrap [a])

        OpRevert ->
          case stk of
            xOffset:xSize:_ ->
              accessMemoryRange xOffset xSize $ do
                output <- readMemory xOffset xSize
                finishFrame (FrameReverted output)
            _ -> underrun

        OpUnknown xxx ->
          vmError $ UnrecognizedOpcode xxx

transfer :: VMOps t => 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
  baseState <- use (#config % #baseState)
  let mkc = case baseState of
              AbstractBase -> unknownContract
              EmptyBase -> const emptyContract
  case (sb, db) of
    -- both sender and recipient in state
    (Just srcBal, Just _) ->
      branch (Expr.gt val srcBal) $ \case
        True -> vmError $ BalanceTooLow val srcBal
        False -> do
          (#env % #contracts % ix src % #balance) %= (`Expr.sub` val)
          (#env % #contracts % ix dst % #balance) %= (`Expr.add` val)
    -- sender not in state
    (Nothing, Just _) -> do
      case src of
        LitAddr _ -> do
          (#env % #contracts) %= (Map.insert src (mkc src))
          transfer src dst val
        SymAddr _ -> do
          pc <- use (#state % #pc)
          partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth from a symbolic address that is not present in the state" (wrap [src])
        GVar _ -> internalError "Unexpected GVar"
    -- recipient not in state
    (_ , Nothing) -> do
      case dst of
        LitAddr _ -> do
          (#env % #contracts) %= (Map.insert dst (mkc dst))
          transfer src dst val
        SymAddr _ -> do
          pc <- use (#state % #pc)
          partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth to a symbolic address that is not present in the state" (wrap [dst])
        GVar _ -> internalError "Unexpected GVar"

-- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.
callChecks
  :: forall (t :: VMType) s. (?op :: Word8, 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.config.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 (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 _ -> do
              pc <- use (#state % #pc)
              partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth from a symbolic address that is not present in the state" (wrap [from])
            GVar _ -> internalError "Unexpected GVar"




precompiledContract
  :: (?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)
      pc' <- use (#state % #pc)
      result' <- use #result
      case result' of
        Nothing -> case stk of
          x:_ -> case maybeLitWord x of
            Just 0 ->
              pure ()
            Just 1 ->
              fetchAccount (LitAddr recipient) $ \_ -> do
                touchAccount self
                touchAccount (LitAddr recipient)
                transfer self (LitAddr recipient) xValue
            _ -> partial $
                   UnexpectedSymbolicArg pc' "unexpected return value from precompile" (wrap [x])
          _ -> underrun
        _ -> pure ()

executePrecompile
  :: (?op :: Word8, 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 = internalError $ "precompile at address " <> show preCompileAddr <> " not yet implemented"
      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 = assign #result . Just . HandleEffect . Query

choose :: Choose s -> EVM Symbolic s ()
choose = assign #result . Just . HandleEffect . Choose

-- | Construct RPC Query and halt execution until resolved
fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
fetchAccount addr continue =
  use (#env % #contracts % at addr) >>= \case
    Just c -> continue c
    Nothing -> case addr of
      SymAddr _ -> do
        pc <- use (#state % #pc)
        partial $ UnexpectedSymbolicArg pc "trying to access a symbolic address that isn't already present in storage" (wrap [addr])
      LitAddr a -> do
        use (#cache % #fetched % at a) >>= \case
          Just c -> do
            assign (#env % #contracts % at addr) (Just c)
            continue c
          Nothing -> do
            base <- use (#config % #baseState)
            assign (#result) . Just . HandleEffect . Query $
              PleaseFetchContract a base
                (\c -> do assign (#cache % #fetched % at a) (Just c)
                          assign (#env % #contracts % at addr) (Just c)
                          assign #result Nothing
                          continue c)
      GVar _ -> internalError "Unexpected GVar"

accessStorage
  :: VMOps 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 _ -> continue x
          Nothing -> rpcCall c slotConc
        Nothing -> rpcCall c slotConc
    Nothing ->
      fetchAccount addr $ \_ ->
        accessStorage addr slot continue
  where
      rpcCall c slotConc = 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
            -- check if the slot is cached
            contract <- preuse (#cache % #fetched % ix addr')
            case contract of
              Nothing -> internalError "contract marked external not found in cache"
              Just fetched -> case readStorage (Lit slot') fetched.storage of
                          Nothing -> mkQuery addr' slot'
                          Just val -> continue val
        else do
          modifying (#env % #contracts % ix addr % #storage) (writeStorage slot (Lit 0))
          continue $ Lit 0
      mkQuery a s = query $
        PleaseFetchSlot a s
          (\x -> do
              modifying (#cache % #fetched % ix a % #storage) (writeStorage (Lit s) (Lit x))
              modifying (#env % #contracts % ix (LitAddr a) % #storage) (writeStorage (Lit s) (Lit x))
              assign #result Nothing
              continue (Lit x))

accountExists :: Expr EAddr -> VM 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

-- * 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)

  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
      -- deposit the code from a creation tx
      pc' <- use (#state % #pc)
      creation <- use (#tx % #isCreate)
      createe  <- use (#state % #contract)
      createeExists <- (Map.member createe) <$> use (#env % #contracts)
      let onContractCode contractCode =
            when (creation && createeExists) $ replaceCode createe contractCode
      case output of
        ConcreteBuf bs ->
          onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)
        _ ->
          case Expr.toList output of
            Nothing ->
              partial $
                UnexpectedSymbolicArg pc' "runtime code cannot have an abstract length" (wrap [output])
            Just ops ->
              onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)
    _ ->
      internalError "Finalising an unfinished tx."

  -- compute and pay the refund to the caller and the
  -- corresponding payment to the miner
  block <- use #block

  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

forceAddr :: VMOps t => Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s ()
forceAddr n msg continue = case wordToAddr n of
  Nothing -> do
    vm <- get
    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])
  Just c -> continue c

forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()
forceConcrete n msg continue = case maybeLitWord n of
  Nothing -> do
    vm <- get
    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])
  Just c -> continue c

forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()
forceConcreteAddr n msg continue = case maybeLitAddr n of
  Nothing -> do
    vm <- get
    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])
  Just c -> continue c

forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s ()
forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddr n, maybeLitAddr m) of
  (Just c, Just d) -> continue (c,d)
  _ -> do
    vm <- get
    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])

forceConcrete2 :: VMOps t => (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s ()
forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of
  (Just c, Just d) -> continue (c, d)
  _ -> do
    vm <- get
    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])

forceConcreteBuf :: VMOps t => Expr Buf -> String -> (ByteString -> EVM t s ()) -> EVM t s ()
forceConcreteBuf (ConcreteBuf b) _ continue = continue b
forceConcreteBuf b msg _ = do
    vm <- get
    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [b])

-- * Substate manipulation
refund :: Word64 -> EVM 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 maybeLitWord 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
  :: (?op :: Word8, VMOps t)
  => (Expr EWord, Expr EWord) -> (Expr EWord, Expr EWord)
  -> EVM t s ()
cheat (inOffset, inSize) (outOffset, outSize) = do
  vm <- get
  input <- readMemory (Expr.add inOffset (Lit 4)) (Expr.sub inSize (Lit 4))
  abi <- readBytes 4 (Lit 0) <$> readMemory inOffset (Lit 4)
  pushTrace $ FrameTrace (CallContext cheatCode cheatCode inOffset inSize (Lit 0) (maybeLitWord abi) input vm.env.contracts vm.tx.substate)
  case maybeLitWord abi of
    Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc "symbolic cheatcode selector" (wrap [abi])
    Just (unsafeInto -> abi') ->
      case Map.lookup abi' cheatActions of
        Nothing ->
          vmError (BadCheatCode abi')
        Just action -> do
            action outOffset outSize input
            popTrace
            next
            push 1

type CheatAction t s = Expr EWord -> Expr EWord -> Expr Buf -> EVM t s ()

cheatActions :: VMOps t => Map FunctionSelector (CheatAction t s)
cheatActions =
  Map.fromList
    [ action "ffi(string[])" $
        \sig outOffset outSize input -> do
          vm <- get
          if vm.config.allowFFI then
            case decodeBuf [AbiArrayDynamicType AbiStringType] input of
              CAbi valsArr -> case valsArr of
                [AbiArrayDynamic AbiStringType strsV] ->
                  let
                    cmd = fmap
                            (\case
                              (AbiString a) -> unpack $ decodeUtf8 a
                              _ -> "")
                            (V.toList strsV)
                    cont bs = do
                      let encoded = ConcreteBuf bs
                      assign (#state % #returndata) encoded
                      copyBytesToMemory encoded outSize (Lit 0) outOffset
                      assign #result Nothing
                  in query (PleaseDoFFI cmd cont)
                _ -> vmError (BadCheatCode sig)
              _ -> vmError (BadCheatCode sig)
          else
            let msg = "ffi disabled: run again with --ffi if you want to allow tests to call external scripts"
            in partial $ UnexpectedSymbolicArg vm.state.pc msg [],

      action "warp(uint256)" $
        \sig _ _ input -> case decodeStaticArgs 0 1 input of
          [x]  -> assign (#block % #timestamp) x
          _ -> vmError (BadCheatCode sig),

      action "deal(address,uint256)" $
        \sig _ _ input -> case decodeStaticArgs 0 2 input of
          [a, amt] ->
            forceAddr a "vm.deal: cannot decode target into an address" $ \usr ->
              fetchAccount usr $ \_ -> do
                assign (#env % #contracts % ix usr % #balance) amt
          _ -> vmError (BadCheatCode sig),

      action "assume(bool)" $
        \sig _ _ input -> case decodeStaticArgs 0 1 input of
          [c] -> modifying #constraints ((:) (PEq c (Lit 1)))
          _ -> vmError (BadCheatCode sig),

      action "roll(uint256)" $
        \sig _ _ input -> case decodeStaticArgs 0 1 input of
          [x] -> forceConcrete x "cannot roll to a symbolic block number" (assign (#block % #number))
          _ -> vmError (BadCheatCode sig),

      action "store(address,bytes32,bytes32)" $
        \sig _ _ input -> case decodeStaticArgs 0 3 input of
          [a, slot, new] -> case wordToAddr a of
            Just a'@(LitAddr _) -> fetchAccount a' $ \_ ->
              modifying (#env % #contracts % ix a' % #storage) (writeStorage slot new)
            _ -> vmError (BadCheatCode sig)
          _ -> vmError (BadCheatCode sig),

      action "load(address,bytes32)" $
        \sig outOffset _ input -> case decodeStaticArgs 0 2 input of
          [a, slot] -> case wordToAddr a of
            Just a'@(LitAddr _) -> fetchAccount a' $ \_ ->
              accessStorage a' slot $ \res -> do
                assign (#state % #returndata % word256At (Lit 0)) res
                let buf = writeWord (Lit 0) res (ConcreteBuf "")
                copyBytesToMemory buf (Lit 32) (Lit 0) outOffset
            _ -> vmError (BadCheatCode sig)
          _ -> vmError (BadCheatCode sig),

      action "sign(uint256,bytes32)" $
        \sig outOffset _ input -> case decodeStaticArgs 0 2 input of
          [sk, hash] ->
            forceConcrete2 (sk, hash) "cannot sign symbolic data" $ \(sk', hash') -> do
              let (v,r,s) = EVM.Sign.sign hash' (into sk')
                  encoded = encodeAbiValue $
                    AbiTuple (V.fromList
                      [ AbiUInt 8 $ into v
                      , AbiBytes 32 (word256Bytes r)
                      , AbiBytes 32 (word256Bytes s)
                      ])
              assign (#state % #returndata) (ConcreteBuf encoded)
              copyBytesToMemory (ConcreteBuf encoded) (Lit . unsafeInto . BS.length $ encoded) (Lit 0) outOffset
          _ -> vmError (BadCheatCode sig),

      action "addr(uint256)" $
        \sig outOffset _ input -> case decodeStaticArgs 0 1 input of
          [sk] -> forceConcrete sk "cannot derive address for a symbolic key" $ \sk' -> do
            let a = EVM.Sign.deriveAddr $ into sk'
            case a of
              Nothing -> vmError (BadCheatCode sig)
              Just address -> do
                let expAddr = litAddr address
                assign (#state % #returndata % word256At (Lit 0)) expAddr
                let buf = ConcreteBuf $ word256Bytes (into address)
                copyBytesToMemory buf (Lit 32) (Lit 0) outOffset
          _ -> vmError (BadCheatCode sig),

      action "prank(address)" $
        \sig _ _ input -> case decodeStaticArgs 0 1 input of
          [addr]  -> case wordToAddr addr of
            Just a -> assign (#config % #overrideCaller) (Just a)
            Nothing -> vmError (BadCheatCode sig)
          _ -> vmError (BadCheatCode sig),

      action "createFork(string)" $
        \sig outOffset _ 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.cache urlOrAlias }
              let encoded = encodeAbiValue $ AbiUInt 256 (fromIntegral forkId)
              assign (#state % #returndata) (ConcreteBuf encoded)
              copyBytesToMemory (ConcreteBuf encoded) (Lit . unsafeInto . BS.length $ encoded) (Lit 0) outOffset
            _ -> vmError (BadCheatCode sig)
          _ -> vmError (BadCheatCode sig),

      action "selectFork(uint256)" $
        \sig _ _ input -> case decodeStaticArgs 0 1 input of
          [forkId] ->
            forceConcrete forkId "forkId 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, cache = vm.cache }
                          ) vm.currentFork  vm.forks
                        , currentFork = forkId'
                        }
                Nothing ->
                  vmError (NonexistentFork forkId')
          _ -> vmError (BadCheatCode sig),

      action "activeFork()" $
        \_ outOffset _ _ -> do
          vm <- get
          let encoded = encodeAbiValue $ AbiUInt 256 (fromIntegral vm.currentFork)
          assign (#state % #returndata) (ConcreteBuf encoded)
          copyBytesToMemory (ConcreteBuf encoded) (Lit . unsafeInto . BS.length $ encoded) (Lit 0) outOffset
    ]
  where
    action s f = (abiKeccak s, f (abiKeccak s))

-- * General call implementation ("delegateCall")
-- note that the continuation is ignored in the precompile case
delegateCall
  :: (VMOps t, ?op :: Word8)
  => Contract
  -> Gas t
  -> Expr EAddr
  -> Expr EAddr
  -> Expr EWord
  -> Expr EWord
  -> Expr EWord
  -> Expr EWord
  -> Expr EWord
  -> [Expr EWord]
  -> (Expr EAddr -> EVM t s ())
  -> EVM t s ()
delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue
  | isPrecompileAddr xTo
      = forceConcreteAddr2 (xTo, xContext) "Cannot call precompile with symbolic addresses" $
          \(xTo', xContext') ->
            precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs
  | xTo == cheatCode = do
      assign (#state % #stack) xs
      cheat (xInOffset, xInSize) (xOutOffset, xOutSize)
  | otherwise =
      callChecks this gasGiven xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs $
        \xGas -> do
          vm0 <- get
          fetchAccount xTo $ \target -> case target.code of
              UnknownCode _ -> do
                pc <- use (#state % #pc)
                partial $ UnexpectedSymbolicArg pc "call target has unknown code" (wrap [xTo])
              _ -> do
                burn' xGas $ do
                  calldata <- readMemory xInOffset xInSize
                  abi <- maybeLitWord . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4)
                  let newContext = CallContext
                                    { target    = xTo
                                    , context   = xContext
                                    , offset    = xOutOffset
                                    , size      = xOutSize
                                    , codehash  = target.codehash
                                    , callreversion = vm0.env.contracts
                                    , subState  = vm0.tx.substate
                                    , abi
                                    , calldata
                                    }
                  pushTrace (FrameTrace newContext)
                  next
                  vm1 <- get

                  pushTo #frames $ Frame
                    { state = vm1.state { stack = xs }
                    , context = newContext
                    }

                  let clearInitCode = \case
                        (InitCode _ _) -> InitCode mempty mempty
                        a -> a

                  newMemory <- ConcreteMemory <$> VUnboxed.Mutable.new 0
                  zoom #state $ do
                    assign #gas xGas
                    assign #pc 0
                    assign #code (clearInitCode target.code)
                    assign #codeContract xTo
                    assign #stack mempty
                    assign #memory newMemory
                    assign #memorySize 0
                    assign #returndata mempty
                    assign #calldata calldata
                  continue xTo

-- -- * Contract creation

-- EIP 684
collision :: Maybe Contract -> Bool
collision c' = case c' of
  Just c -> c.nonce /= Just 0 || case c.code of
    RuntimeCode (ConcreteRuntimeCode "") -> False
    RuntimeCode (SymbolicRuntimeCode b) -> not $ null b
    _ -> True
  Nothing -> False

create :: forall t s. (?op :: Word8, 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
  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
  else if this.nonce == Just maxBound
  then do
    assign (#state % #stack) (Lit 0 : xs)
    assign (#state % #returndata) mempty
    pushTrace $ ErrorTrace NonceOverflow
    next
  else if length vm0.frames >= 1024
  then do
    assign (#state % #stack) (Lit 0 : xs)
    assign (#state % #returndata) mempty
    pushTrace $ ErrorTrace CallDepthLimitReached
    next
  else if collision $ Map.lookup newAddr vm0.env.contracts
  then burn' xGas $ do
    assign (#state % #stack) (Lit 0 : xs)
    assign (#state % #returndata) mempty
    modifying (#env % #contracts % ix self % #nonce) (fmap ((+) 1))
    next
  -- do we have enough balance
  else branch (Expr.gt xValue this.balance) $ \case
      True -> do
        assign (#state % #stack) (Lit 0 : xs)
        assign (#state % #returndata) mempty
        pushTrace $ ErrorTrace $ BalanceTooLow xValue this.balance
        next
        touchAccount self
        touchAccount newAddr
      -- are we overflowing the nonce
      False -> burn' xGas $ do
        case parseInitCode initCode of
          Nothing ->
            partial $ UnexpectedSymbolicArg vm0.state.pc "initcode must have a concrete prefix" []
          Just c -> do
            let
              newContract = initialContract c
              newContext  =
                CreationContext { address   = newAddr
                                , codehash  = newContract.codehash
                                , createreversion = vm0.env.contracts
                                , substate  = vm0.tx.substate
                                }

            zoom (#env % #contracts) $ do
              oldAcc <- use (at newAddr)
              let oldBal = maybe (Lit 0) (.balance) oldAcc

              assign (at newAddr) (Just (newContract & #balance .~ oldBal))
              modifying (ix self % #nonce) (fmap ((+) 1))

            let
              resetStorage :: Expr Storage -> Expr Storage
              resetStorage = \case
                  ConcreteStore _ -> ConcreteStore mempty
                  AbstractStore a 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

            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

-- | 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
          FrameErrored e ->
            ErrorTrace e
          FrameReverted e ->
            ErrorTrace (Revert e)
          FrameReturned output ->
            ReturnTrace output nextFrame.context
      -- Pop to the previous level of the debug trace stack.
      popTrace

      -- Pop the top frame.
      assign #frames remainingFrames
      -- Install the state of the frame to which we shall return.
      assign #state nextFrame.state

      -- 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
                        "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 (VUnboxed.Mutable.length mem)
          if size > Expr.maxBytes ||
             offset + size > Expr.maxBytes ||
             offset >= into memSize then
            -- reads past memory are all zeros
            pure $ ConcreteBuf $ BS.replicate (unsafeInto size) 0
          else do
            let pastEnd = (unsafeInto offset + unsafeInto size) - unsafeInto memSize
            let fromMemSize = if pastEnd > 0 then unsafeInto size - pastEnd else unsafeInto size

            buf <- VUnboxed.freeze $ VUnboxed.Mutable.slice (unsafeInto offset) fromMemSize mem
            let dataFromMem = BS.pack $ VUnboxed.toList buf
            pure $ ConcreteBuf $ dataFromMem <> BS.replicate pastEnd 0
        _ -> do
          buf <- freezeMemory mem
          pure $ copySlice offset' (Lit 0) size' buf mempty
    SymbolicMemory mem ->
      pure $ copySlice offset' (Lit 0) size' mem mempty

-- * Tracing

withTraceLocation :: TraceData -> EVM t s Trace
withTraceLocation x = do
  vm <- get
  let this = fromJust $ currentContract vm
  pure Trace
    { tracedata = x
    , contract = this
    , opIx = fromMaybe 0 $ this.opIxMap SV.!? vm.state.pc
    }

pushTrace :: TraceData -> EVM 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 _ (Traces f _) _ _) = f
traceForest' (Partial _ (Traces f _) _) = f
traceForest' (Failure _ (Traces f _) _) = f
traceForest' (ITE {}) = internalError"Internal Error: ITE does not contain a trace"
traceForest' (GVar {}) = internalError"Internal Error: Unexpected GVar"

traceContext :: Expr End -> Map (Expr EAddr) Contract
traceContext (Success _ (Traces _ c) _ _) = c
traceContext (Partial _ (Traces _ c) _) = c
traceContext (Failure _ (Traces _ c) _) = c
traceContext (ITE {}) = internalError"Internal Error: ITE does not contain a trace"
traceContext (GVar {}) = internalError"Internal Error: Unexpected GVar"

traceTopLog :: [Expr Log] -> EVM 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 = #state % #stack %= (x :)

pushAddr :: Expr EAddr -> EVM t s ()
pushAddr (LitAddr x) = #state % #stack %= (Lit (into x) :)
pushAddr x@(SymAddr _) = #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
        #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
        #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
      (#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
      #state % #stack .= xs
      #state % #pc .= x
    False -> vmError BadJumpDestination

-- fails with partial if we're trying to jump into the symbolic region of an `InitCode`
noJumpIntoInitData :: 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 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 >>= maybeLitByte
  in case op of
       Nothing -> False
       Just b -> 0x5b == b && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap SV.! x))

opSize :: Word8 -> Int
opSize x | x >= 0x60 && x <= 0x7f = into x - 0x60 + 2
opSize _                          = 1

--  i of the resulting vector contains the operation index for
-- the program counter value i.  This is needed because source map
-- entries are per operation, not per byte.
mkOpIxMap :: ContractCode -> SV.Vector Int
mkOpIxMap (UnknownCode _) = internalError "Cannot build opIxMap for unknown code"
mkOpIxMap (InitCode conc _)
  = SV.create $ SV.new (BS.length conc) >>= \v ->
      -- Loop over the byte string accumulating a vector-mutating action.
      -- This is somewhat obfuscated, but should be fast.
      let (_, _, _, m) = BS.foldl' (go v) (0 :: Word8, 0, 0, pure ()) conc
      in m >> pure v
      where
        -- concrete case
        go v (0, !i, !j, !m) x | x >= 0x60 && x <= 0x7f =
          {- Start of PUSH op. -} (x - 0x60 + 1, i + 1, j,     m >> SV.write v i j)
        go v (1, !i, !j, !m) _ =
          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> SV.write v i j)
        go v (0, !i, !j, !m) _ =
          {- Other op. -}         (0,            i + 1, j + 1, m >> SV.write v i j)
        go v (n, !i, !j, !m) _ =
          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)

mkOpIxMap (RuntimeCode (ConcreteRuntimeCode ops)) =
  mkOpIxMap (InitCode ops mempty) -- a bit hacky

mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))
  = SV.create $ SV.new (length ops) >>= \v ->
      let (_, _, _, m) = foldl (go v) (0, 0, 0, pure ()) (stripBytecodeMetadataSym $ V.toList ops)
      in m >> pure v
      where
        go v (0, !i, !j, !m) x = case maybeLitByte x of
          Just x' -> if x' >= 0x60 && x' <= 0x7f
            -- start of PUSH op --
                     then (x' - 0x60 + 1, i + 1, j,     m >> SV.write v i j)
            -- other data --
                     else (0,             i + 1, j + 1, m >> SV.write v i j)
          _ -> internalError $ "cannot analyze symbolic code:\nx: " <> show x <> " i: " <> show i <> " j: " <> show j

        go v (1, !i, !j, !m) _ =
          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> SV.write v i j)
        go v (n, !i, !j, !m) _ =
          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)


vmOp :: VM 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") . maybeLitByte $ 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 SV.!? 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") $ maybeLitByte 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)
  mapM_ (uncurry (VUnboxed.Mutable.write memory'))
        (zip [offset..] (BS.unpack buf))
  where
  expandMemory targetSize = do
    let toAlloc = targetSize - VUnboxed.Mutable.length memory
    if toAlloc > 0 then do
      memory' <- VUnboxed.Mutable.grow memory toAlloc
      assign (#state % #memory) (ConcreteMemory memory')
      pure memory'
    else
      pure memory

freezeMemory :: MutableMemory s -> EVM t s (Expr Buf)
freezeMemory memory =
  ConcreteBuf . BS.pack . VUnboxed.toList <$> VUnboxed.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 cond continue = do
    loc <- codeloc
    pathconds <- use #constraints
    query $ PleaseAskSMT cond pathconds (choosePath loc)
    where
      condSimp = Expr.simplify cond
      condSimpConc = Expr.concKeccakSimpExpr condSimp
      choosePath loc (Case v) = do
        assign #result Nothing
        pushTo #constraints $ if v then Expr.simplifyProp (condSimpConc ./= Lit 0)
                                   else Expr.simplifyProp (condSimpConc .== Lit 0)
        (iteration, _) <- use (#iterations % at loc % non (0,[]))
        stack <- use (#state % #stack)
        assign (#cache % #path % at (loc, iteration)) (Just v)
        assign (#iterations % at loc) (Just (iteration + 1, stack))
        continue v
      -- Both paths are possible; we ask for more input
      choosePath loc Unknown =
        choose . PleaseChoosePath condSimp $ choosePath loc . Case

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)

-- 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

forceLit :: Expr EWord -> W256
forceLit (Lit w) = w
forceLit _ = internalError "concrete vm, shouldn't ever happen"

burn :: VMOps t => Word64 -> EVM t s () -> EVM t s ()
burn = burn' . toGas