content: {-# Language ImplicitParams #-}
  {-# Language ConstraintKinds #-}
  {-# Language FlexibleInstances #-}
  {-# Language DataKinds #-}
  {-# Language GADTs #-}
  {-# Language RecordWildCards #-}
  {-# Language ScopedTypeVariables #-}
  {-# Language StandaloneDeriving #-}
  {-# Language StrictData #-}
  {-# Language TemplateHaskell #-}
  {-# Language TypeOperators #-}
  {-# Language ViewPatterns #-}
  
  module EVM where
  
  import Prelude hiding (log, Word, exponent, GT, LT)
  
  import Data.SBV hiding (Word, output, Unknown)
  import Data.Proxy (Proxy(..))
  import Data.Text (unpack)
  import Data.Text.Encoding (decodeUtf8, encodeUtf8)
  import qualified Data.Vector as V
  import EVM.ABI
  import EVM.Types
  import EVM.Solidity
  import EVM.Concrete (createAddress, wordValue, keccakBlob, create2Address, readMemoryWord)
  import EVM.Symbolic
  import EVM.Op
  import EVM.FeeSchedule (FeeSchedule (..))
  import Options.Generic as Options
  import qualified EVM.Precompiled
  
  import Control.Lens hiding (op, (:<), (|>), (.>))
  import Control.Monad.State.Strict hiding (state)
  
  import Data.ByteString              (ByteString)
  import Data.ByteString.Lazy         (fromStrict)
  import Data.Map.Strict              (Map)
  import Data.Set                     (Set, insert, member, fromList)
  import Data.Maybe                   (fromMaybe)
  import Data.Sequence                (Seq)
  import Data.Vector.Storable         (Vector)
  import Data.Foldable                (toList)
  
  import Data.Tree
  import Data.List (find)
  
  import qualified Data.ByteString      as BS
  import qualified Data.ByteString.Lazy as LS
  import qualified Data.ByteString.Char8 as Char8
  import qualified Data.ByteArray       as BA
  import qualified Data.Map.Strict      as Map
  import qualified Data.Sequence        as Seq
  import qualified Data.Tree.Zipper     as Zipper
  import qualified Data.Vector          as V
  import qualified Data.Vector.Storable as Vector
  import qualified Data.Vector.Storable.Mutable as Vector
  
  import qualified Data.Vector as RegularVector
  
  import Crypto.Number.ModArithmetic (expFast)
  import qualified Crypto.Hash as Crypto
  import Crypto.Hash (Digest, SHA256, RIPEMD160, digestFromByteString)
  import Crypto.PubKey.ECC.ECDSA (signDigestWith, PrivateKey(..), Signature(..))
  import Crypto.PubKey.ECC.Types (getCurveByName, CurveName(..), Point(..))
  import Crypto.PubKey.ECC.Generate (generateQ)
  
  -- * Data types
  
  -- | EVM failure modes
  data Error
    = BalanceTooLow Word Word
    | UnrecognizedOpcode Word8
    | SelfDestruction
    | StackUnderrun
    | BadJumpDestination
    | Revert ByteString
    | OutOfGas Word Word
    | BadCheatCode (Maybe Word32)
    | StackLimitExceeded
    | IllegalOverflow
    | Query Query
    | Choose Choose
    | StateChangeWhileStatic
    | InvalidMemoryAccess
    | CallDepthLimitReached
    | MaxCodeSizeExceeded Word Word
    | InvalidFormat
    | PrecompileFailure
    | UnexpectedSymbolicArg
    | DeadPath
    | NotUnique Whiff
    | SMTTimeout
    | FFI AbiVals
  deriving instance Show Error
  
  -- | The possible result states of a VM
  data VMResult
    = VMFailure Error -- ^ An operation failed
    | VMSuccess Buffer -- ^ Reached STOP, RETURN, or end-of-code
  
  deriving instance Show VMResult
  
  -- | The state of a stepwise EVM execution
  data VM = VM
    { _result         :: Maybe VMResult
    , _state          :: FrameState
    , _frames         :: [Frame]
    , _env            :: Env
    , _block          :: Block
    , _tx             :: TxState
    , _logs           :: Seq Log
    , _traces         :: Zipper.TreePos Zipper.Empty Trace
    , _cache          :: Cache
    , _burned         :: Word
    , _constraints    :: [(SBool, Whiff)]
    , _iterations     :: Map CodeLocation Int
    , _allowFFI       :: Bool
    }
    deriving (Show)
  
  data Trace = Trace
    { _traceOpIx     :: Int
    , _traceContract :: Contract
    , _traceData     :: TraceData
    }
    deriving (Show)
  
  data TraceData
    = EventTrace Log
    | FrameTrace FrameContext
    | QueryTrace Query
    | ErrorTrace Error
    | EntryTrace Text
    | ReturnTrace Buffer FrameContext
    deriving (Show)
  
  -- | Queries halt execution until resolved through RPC calls or SMT queries
  data Query where
    PleaseFetchContract :: Addr -> StorageModel -> (Contract -> EVM ()) -> Query
    PleaseMakeUnique    :: SymVal a => SBV a -> [SBool] -> (IsUnique a -> EVM ()) -> Query
    PleaseFetchSlot     :: Addr -> Word -> (Word -> EVM ()) -> Query
    PleaseAskSMT        :: SBool -> [SBool] -> (BranchCondition -> EVM ()) -> Query
    PleaseDoFFI         :: [String] -> (ByteString -> EVM ()) -> Query
  
  data Choose where
    PleaseChoosePath    :: Whiff -> (Bool -> EVM ()) -> Choose
  
  instance Show Query where
    showsPrec _ = \case
      PleaseFetchContract addr _ _ ->
        (("<EVM.Query: fetch contract " ++ show addr ++ ">") ++)
      PleaseFetchSlot addr slot _ ->
        (("<EVM.Query: fetch slot "
          ++ show slot ++ " for "
          ++ show addr ++ ">") ++)
      PleaseAskSMT condition constraints _ ->
        (("<EVM.Query: ask SMT about "
          ++ show condition ++ " in context "
          ++ show constraints ++ ">") ++)
      PleaseMakeUnique val constraints _ ->
        (("<EVM.Query: make value "
          ++ show val ++ " unique in context "
          ++ show constraints ++ ">") ++)
      PleaseDoFFI cmd _ ->
        (("<EVM.Query: do ffi: " ++ (show cmd)) ++)
  
  instance Show Choose where
    showsPrec _ = \case
      PleaseChoosePath _ _ ->
        (("<EVM.Choice: waiting for user to select path (0,1)") ++)
  
  -- | Alias for the type of e.g. @exec1@.
  type EVM a = State VM a
  
  type CodeLocation = (Addr, Int)
  
  -- | The possible return values of a SMT query
  data BranchCondition = Case Bool | Unknown | Inconsistent
    deriving Show
  
  -- | The possible return values of a `is unique` SMT query
  data IsUnique a = Unique a | Multiple | InconsistentU | TimeoutU
    deriving Show
  
  -- | The cache is data that can be persisted for efficiency:
  -- any expensive query that is constant at least within a block.
  data Cache = Cache
    { _fetched :: Map Addr Contract,
      _path :: Map (CodeLocation, Int) Bool
    } deriving Show
  
  -- | A way to specify an initial VM state
  data VMOpts = VMOpts
    { vmoptContract :: Contract
    , vmoptCalldata :: (Buffer, SymWord)
    , vmoptValue :: SymWord
    , vmoptPriorityFee :: W256
    , vmoptAddress :: Addr
    , vmoptCaller :: SAddr
    , vmoptOrigin :: Addr
    , vmoptGas :: W256
    , vmoptGaslimit :: W256
    , vmoptNumber :: W256
    , vmoptTimestamp :: SymWord
    , vmoptCoinbase :: Addr
    , vmoptDifficulty :: W256
    , vmoptMaxCodeSize :: W256
    , vmoptBlockGaslimit :: W256
    , vmoptGasprice :: W256
    , vmoptBaseFee :: W256
    , vmoptSchedule :: FeeSchedule Integer
    , vmoptChainId :: W256
    , vmoptCreate :: Bool
    , vmoptStorageModel :: StorageModel
    , vmoptTxAccessList :: Map Addr [W256]
    , vmoptAllowFFI :: Bool
    } deriving Show
  
  -- | A log entry
  data Log = Log Addr Buffer [SymWord]
    deriving (Show)
  
  -- | An entry in the VM's "call/create stack"
  data Frame = Frame
    { _frameContext   :: FrameContext
    , _frameState     :: FrameState
    }
    deriving (Show)
  
  -- | Call/create info
  data FrameContext
    = CreationContext
      { creationContextAddress   :: Addr
      , creationContextCodehash  :: W256
      , creationContextReversion :: Map Addr Contract
      , creationContextSubstate  :: SubState
      }
    | CallContext
      { callContextTarget    :: Addr
      , callContextContext   :: Addr
      , callContextOffset    :: Word
      , callContextSize      :: Word
      , callContextCodehash  :: W256
      , callContextAbi       :: Maybe Word
      , callContextData      :: Buffer
      , callContextReversion :: Map Addr Contract
      , callContextSubState  :: SubState
      }
    deriving (Show)
  
  -- | The "registers" of the VM along with memory and data stack
  data FrameState = FrameState
    { _contract     :: Addr
    , _codeContract :: Addr
    , _code         :: Buffer
    , _pc           :: Int
    , _stack        :: [SymWord]
    , _memory       :: Buffer
    , _memorySize   :: Int
    , _calldata     :: (Buffer, SymWord)
    , _callvalue    :: SymWord
    , _caller       :: SAddr
    , _gas          :: Word
    , _returndata   :: Buffer
    , _static       :: Bool
    }
    deriving (Show)
  
  -- | The state that spans a whole transaction
  data TxState = TxState
    { _gasprice            :: Word
    , _txgaslimit          :: Word
    , _txPriorityFee       :: Word
    , _origin              :: Addr
    , _toAddr              :: Addr
    , _value               :: SymWord
    , _substate            :: SubState
    , _isCreate            :: Bool
    , _txReversion         :: Map Addr Contract
    }
    deriving (Show)
  
  -- | The "accrued substate" across a transaction
  data SubState = SubState
    { _selfdestructs   :: [Addr]
    , _touchedAccounts :: [Addr]
    , _accessedAddresses :: Set Addr
    , _accessedStorageKeys :: Set (Addr, W256)
    , _refunds         :: [(Addr, Integer)]
    -- in principle we should include logs here, but do not for now
    }
    deriving (Show)
  
  -- | A contract is either in creation (running its "constructor") or
  -- post-creation, and code in these two modes is treated differently
  -- by instructions like @EXTCODEHASH@, so we distinguish these two
  -- code types.
  data ContractCode
    = InitCode Buffer     -- ^ "Constructor" code, during contract creation
    | RuntimeCode Buffer  -- ^ "Instance" code, after contract creation
    deriving (Show)
  
  -- runtime err when used for symbolic code
  instance Eq ContractCode where
    (InitCode x) == (InitCode y) = forceBuffer x == forceBuffer y
    (RuntimeCode x) == (RuntimeCode y) = forceBuffer x == forceBuffer y
    _ == _ = False
  
  -- runtime err when used for symbolic code
  instance Ord ContractCode where
    compare x y = compare (forceBuffer (buf x)) (forceBuffer (buf y))
      where buf (InitCode z) = z
            buf (RuntimeCode z) = z
  
  -- | A contract can either have concrete or symbolic storage
  -- depending on what type of execution we are doing
  data Storage
    = Concrete (Map Word SymWord)
    | Symbolic [(SymWord, SymWord)] (SArray (WordN 256) (WordN 256))
    deriving (Show)
  
  -- to allow for Eq Contract (which useful for debugging vmtests)
  -- we mock an instance of Eq for symbolic storage.
  -- It should not (cannot) be used though.
  instance Eq Storage where
    (==) (Concrete a) (Concrete b) = fmap forceLit a == fmap forceLit b
    (==) (Symbolic _ _) (Concrete _) = False
    (==) (Concrete _) (Symbolic _ _) = False
    (==) _ _ = error "do not compare two symbolic arrays like this!"
  
  -- | The state of a contract
  data Contract = Contract
    { _contractcode :: ContractCode
    , _storage      :: Storage
    , _balance      :: Word
    , _nonce        :: Word
    , _codehash     :: W256
    , _opIxMap      :: Vector Int
    , _codeOps      :: RegularVector.Vector (Int, Op)
    , _external     :: Bool
    , _origStorage  :: Map Word Word
    }
  
  deriving instance Show Contract
  
  -- | When doing symbolic execution, we have three different
  -- ways to model the storage of contracts. This determines
  -- not only the initial contract storage model but also how
  -- RPC or state fetched contracts will be modeled.
  data StorageModel
    = ConcreteS    -- ^ Uses `Concrete` Storage. Reading / Writing from abstract
                   -- locations causes a runtime failure. Can be nicely combined with RPC.
  
    | SymbolicS    -- ^ Uses `Symbolic` Storage. Reading / Writing never reaches RPC,
                   -- but always done using an SMT array with no default value.
  
    | InitialS     -- ^ Uses `Symbolic` Storage. Reading / Writing never reaches RPC,
                   -- but always done using an SMT array with 0 as the default value.
  
    deriving (Read, Show)
  
  instance ParseField StorageModel
  
  -- | Various environmental data
  data Env = Env
    { _contracts    :: Map Addr Contract
    , _chainId      :: Word
    , _storageModel :: StorageModel
    , _sha3Crack    :: Map Word ByteString
    , _keccakUsed   :: [([SWord 8], SWord 256)]
    }
    deriving (Show)
  
  
  -- | Data about the block
  data Block = Block
    { _coinbase    :: Addr
    , _timestamp   :: SymWord
    , _number      :: Word
    , _difficulty  :: Word
    , _gaslimit    :: Word
    , _baseFee     :: Word
    , _maxCodeSize :: Word
    , _schedule    :: FeeSchedule Integer
    } deriving Show
  
  blankState :: FrameState
  blankState = FrameState
    { _contract     = 0
    , _codeContract = 0
    , _code         = mempty
    , _pc           = 0
    , _stack        = mempty
    , _memory       = mempty
    , _memorySize   = 0
    , _calldata     = (mempty, 0)
    , _callvalue    = 0
    , _caller       = 0
    , _gas          = 0
    , _returndata   = mempty
    , _static       = False
    }
  
  makeLenses ''FrameState
  makeLenses ''Frame
  makeLenses ''Block
  makeLenses ''TxState
  makeLenses ''SubState
  makeLenses ''Contract
  makeLenses ''Env
  makeLenses ''Cache
  makeLenses ''Trace
  makeLenses ''VM
  
  -- | An "external" view of a contract's bytecode, appropriate for
  -- e.g. @EXTCODEHASH@.
  bytecode :: Getter Contract Buffer
  bytecode = contractcode . to f
    where f (InitCode _)    = mempty
          f (RuntimeCode b) = b
  
  instance Semigroup Cache where
    a <> b = Cache
      { _fetched = Map.unionWith unifyCachedContract (view fetched a) (view fetched b)
      , _path = mappend (view path a) (view path b)
      }
  
  -- only intended for use in Cache merges, where we expect
  -- everything to be Concrete
  unifyCachedContract :: Contract -> Contract -> Contract
  unifyCachedContract a b = a & set storage merged
    where merged = case (view storage a, view storage b) of
                     (Concrete sa, Concrete sb) ->
                       Concrete (mappend sa sb)
                     _ ->
                       view storage a
  
  instance Monoid Cache where
    mempty = Cache { _fetched = mempty,
                     _path = mempty
                   }
  
  -- * Data accessors
  
  currentContract :: VM -> Maybe Contract
  currentContract vm =
    view (env . contracts . at (view (state . codeContract) vm)) vm
  
  -- * Data constructors
  
  makeVm :: VMOpts -> VM
  makeVm o =
    let txaccessList = vmoptTxAccessList o
        txorigin = vmoptOrigin o
        txtoAddr = vmoptAddress o
        initialAccessedAddrs = fromList $ [txorigin, txtoAddr] ++ [1..9] ++ (Map.keys txaccessList)
        initialAccessedStorageKeys = fromList $ foldMap (uncurry (map . (,))) (Map.toList txaccessList)
        touched = if vmoptCreate o then [txorigin] else [txorigin, txtoAddr]
    in
    VM
    { _result = Nothing
    , _frames = mempty
    , _tx = TxState
      { _gasprice = w256 $ vmoptGasprice o
      , _txgaslimit = w256 $ vmoptGaslimit o
      , _txPriorityFee = w256 $ vmoptPriorityFee o
      , _origin = txorigin
      , _toAddr = txtoAddr
      , _value = vmoptValue o
      , _substate = SubState mempty touched initialAccessedAddrs initialAccessedStorageKeys mempty
      --, _accessList = txaccessList
      , _isCreate = vmoptCreate o
      , _txReversion = Map.fromList
        [(vmoptAddress o, vmoptContract o)]
      }
    , _logs = mempty
    , _traces = Zipper.fromForest []
    , _block = Block
      { _coinbase = vmoptCoinbase o
      , _timestamp = vmoptTimestamp o
      , _number = w256 $ vmoptNumber o
      , _difficulty = w256 $ vmoptDifficulty o
      , _maxCodeSize = w256 $ vmoptMaxCodeSize o
      , _gaslimit = w256 $ vmoptBlockGaslimit o
      , _baseFee = w256 $ vmoptBaseFee o
      , _schedule = vmoptSchedule o
      }
    , _state = FrameState
      { _pc = 0
      , _stack = mempty
      , _memory = mempty
      , _memorySize = 0
      , _code = theCode
      , _contract = vmoptAddress o
      , _codeContract = vmoptAddress o
      , _calldata = vmoptCalldata o
      , _callvalue = vmoptValue o
      , _caller = vmoptCaller o
      , _gas = w256 $ vmoptGas o
      , _returndata = mempty
      , _static = False
      }
    , _env = Env
      { _sha3Crack = mempty
      , _chainId = w256 $ vmoptChainId o
      , _contracts = Map.fromList
        [(vmoptAddress o, vmoptContract o)]
      , _keccakUsed = mempty
      , _storageModel = vmoptStorageModel o
      }
    , _cache = Cache mempty mempty
    , _burned = 0
    , _constraints = []
    , _iterations = mempty
    , _allowFFI = vmoptAllowFFI o
    } where theCode = case _contractcode (vmoptContract o) of
              InitCode b    -> b
              RuntimeCode b -> b
  
  -- | Initialize empty contract with given code
  initialContract :: ContractCode -> Contract
  initialContract theContractCode = Contract
    { _contractcode = theContractCode
    , _codehash =
      case theCode of
        ConcreteBuffer b -> keccak (stripBytecodeMetadata b)
        SymbolicBuffer _ -> 0
  
    , _storage  = Concrete mempty
    , _balance  = 0
    , _nonce    = if creation then 1 else 0
    , _opIxMap  = mkOpIxMap theCode
    , _codeOps  = mkCodeOps theCode
    , _external = False
    , _origStorage = mempty
    } where
        (creation, theCode) = case theContractCode of
              InitCode b    -> (True, b)
              RuntimeCode b -> (False, b)
  
  contractWithStore :: ContractCode -> Storage -> Contract
  contractWithStore theContractCode store =
    initialContract theContractCode & set storage store
  
  -- * Opcode dispatch (exec1)
  
  -- | Update program counter
  next :: (?op :: Word8) => EVM ()
  next = modifying (state . pc) (+ (opSize ?op))
  
  -- | Executes the EVM one step
  exec1 :: EVM ()
  exec1 = do
    vm <- get
  
    let
      -- Convenience function to access parts of the current VM state.
      -- Arcane type signature needed to avoid monomorphism restriction.
      the :: (b -> VM -> Const a VM) -> ((a -> Const a a) -> b) -> a
      the f g = view (f . g) vm
  
      -- Convenient aliases
      mem  = the state memory
      stk  = the state stack
      self = the state contract
      this = fromMaybe (error "internal error: state contract") (preview (ix self) (the env contracts))
  
      fees@FeeSchedule {..} = the block schedule
  
      doStop = finishFrame (FrameReturned mempty)
  
    if self > 0x0 && self <= 0x9 then do
      -- call to precompile
      let ?op = 0x00 -- dummy value
      let
        calldatasize = snd (the state calldata)
      case maybeLitWord calldatasize of
          Nothing -> vmError UnexpectedSymbolicArg
          Just calldatasize' -> do
            copyBytesToMemory (fst $ the state calldata) (num calldatasize') 0 0
            executePrecompile self (num $ the state gas) 0 (num calldatasize') 0 0 []
            vmx <- get
            case view (state.stack) vmx of
              (x:_) -> case maybeLitWord x of
                Just 0 -> do
                  fetchAccount self $ \_ -> do
                    touchAccount self
                    vmError PrecompileFailure
                Just _ ->
                  fetchAccount self $ \_ -> do
                    touchAccount self
                    out <- use (state . returndata)
                    finishFrame (FrameReturned out)
                Nothing -> vmError UnexpectedSymbolicArg
              _ ->
                underrun
  
    else if the state pc >= len (the state code)
      then doStop
  
      else do
        let ?op = fromMaybe (error "could not analyze symbolic code") $ unliteral $ EVM.Symbolic.index (the state pc) (the state code)
  
        case ?op of
  
          -- op: PUSH
          x | x >= 0x60 && x <= 0x7f -> do
            let !n = num x - 0x60 + 1
                !xs = case the state code of
                        ConcreteBuffer b -> w256lit $ word $ padRight n $ BS.take n (BS.drop (1 + the state pc) b)
                        SymbolicBuffer b -> readSWord' 0 $ padLeft' 32 $ take n $ drop (1 + the state pc) b
            limitStack 1 $
              burn g_verylow $ do
                next
                pushSym xs
  
          -- op: DUP
          x | x >= 0x80 && x <= 0x8f -> do
            let !i = x - 0x80 + 1
            case preview (ix (num i - 1)) stk of
              Nothing -> underrun
              Just y ->
                limitStack 1 $
                  burn g_verylow $ do
                    next
                    pushSym y
  
          -- op: SWAP
          x | x >= 0x90 && x <= 0x9f -> do
            let i = num (x - 0x90 + 1)
            if length stk < i + 1
              then underrun
              else
                burn g_verylow $ do
                  next
                  zoom (state . stack) $ do
                    assign (ix 0) (stk ^?! ix i)
                    assign (ix i) (stk ^?! ix 0)
  
          -- op: LOG
          x | x >= 0xa0 && x <= 0xa4 ->
            notStatic $
            let n = (num x - 0xa0) in
            case stk of
              (xOffset':xSize':xs) ->
                if length xs < n
                then underrun
                else
                  forceConcrete2 (xOffset', xSize') $ \(xOffset, xSize) -> do
                      let (topics, xs') = splitAt n xs
                          bytes         = readMemory (num xOffset) (num xSize) vm
                          log           = Log self bytes topics
  
                      burn (g_log + g_logdata * (num xSize) + num n * g_logtopic) $
                        accessMemoryRange fees xOffset xSize $ do
                          traceLog log
                          next
                          assign (state . stack) xs'
                          pushToSequence logs log
              _ ->
                underrun
  
          -- op: STOP
          0x00 -> doStop
  
          -- op: ADD
          0x01 -> stackOp2 (const g_verylow) (uncurry (+))
          -- op: MUL
          0x02 -> stackOp2 (const g_low) (uncurry (*))
          -- op: SUB
          0x03 -> stackOp2 (const g_verylow) (uncurry (-))
  
          -- op: DIV
          0x04 -> stackOp2 (const g_low) (uncurry (sDiv))
  
          -- op: SDIV
          0x05 ->
            stackOp2 (const g_low) (uncurry sdiv)
  
          -- op: MOD
          0x06 -> stackOp2 (const g_low) $ \(S a x, S b y) -> S (ITE (IsZero b) (Literal 0) (Mod a b)) (ite (y .== 0) 0 (x `sMod` y))
  
          -- op: SMOD
          0x07 -> stackOp2 (const g_low) $ uncurry smod
          -- op: ADDMOD
          0x08 -> stackOp3 (const g_mid) (\(x, y, z) -> addmod x y z)
          -- op: MULMOD
          0x09 -> stackOp3 (const g_mid) (\(x, y, z) -> mulmod x y z)
  
          -- op: LT
          0x10 -> stackOp2 (const g_verylow) $ \(S a x, S b y) -> iteWhiff (LT a b) (x .< y) 1 0
          -- op: GT
          0x11 -> stackOp2 (const g_verylow) $ \(S a x, S b y) -> iteWhiff (GT a b) (x .> y) 1 0
          -- op: SLT
          0x12 -> stackOp2 (const g_verylow) $ uncurry slt
          -- op: SGT
          0x13 -> stackOp2 (const g_verylow) $ uncurry sgt
  
          -- op: EQ
          0x14 -> stackOp2 (const g_verylow) $ \(S a x, S b y) -> iteWhiff (Eq a b) (x .== y) 1 0
          -- op: ISZERO
          0x15 -> stackOp1 (const g_verylow) $ \(S a x) -> iteWhiff (IsZero a) (x .== 0) 1 0
  
          -- op: AND
          0x16 -> stackOp2 (const g_verylow) $ uncurry (.&.)
          -- op: OR
          0x17 -> stackOp2 (const g_verylow) $ uncurry (.|.)
          -- op: XOR
          0x18 -> stackOp2 (const g_verylow) $ uncurry xor
          -- op: NOT
          0x19 -> stackOp1 (const g_verylow) complement
  
          -- op: BYTE
          0x1a -> stackOp2 (const g_verylow) $ \case
            (n, _) | (forceLit n) >= 32 -> 0
            (n, x) | otherwise          -> 0xff .&. shiftR x (8 * (31 - num (forceLit n)))
  
          -- op: SHL
          0x1b -> stackOp2 (const g_verylow) $ \((S a n), (S b x)) -> S (SHL b a) $ sShiftLeft x n
          -- op: SHR
          0x1c -> stackOp2 (const g_verylow) $ \((S a n), (S b x)) -> S (SHR b a) $ sShiftRight x n
          -- op: SAR
          0x1d -> stackOp2 (const g_verylow) $ \((S a n), (S b x)) -> S (SAR b a) $ sSignedShiftArithRight x n
  
          -- op: SHA3
          -- more accurately refered to as KECCAK
          0x20 ->
            case stk of
              (xOffset' : xSize' : xs) ->
                forceConcrete xOffset' $
                  \xOffset -> forceConcrete xSize' $ \xSize ->
                    burn (g_sha3 + g_sha3word * ceilDiv (num xSize) 32) $
                      accessMemoryRange fees xOffset xSize $ do
                        (hash@(S _ hash'), invMap, bytes) <- case readMemory xOffset xSize vm of
                                           ConcreteBuffer bs -> do
                                             pure (litWord $ keccakBlob bs, Map.singleton (keccakBlob bs) bs, litBytes bs)
                                           SymbolicBuffer bs -> do
                                             let hash' = symkeccak' bs
                                             return (S (FromKeccak $ SymbolicBuffer bs) hash', mempty, bs)
  
                        -- Although we would like to simply assert that the uninterpreted function symkeccak'
                        -- is injective, this proves to cause a lot of concern for our smt solvers, probably
                        -- due to the introduction of universal quantifiers into the queries.
  
                        -- Instead, we keep track of all of the particular invocations of symkeccak' we see
                        -- (similarly to sha3Crack), and simply assert that injectivity holds for these
                        -- particular invocations.
                        --
                        -- We additionally make the probabalisitc assumption that the output of symkeccak'
                        -- is greater than 100. This lets us avoid having to reason about storage collisions
                        -- between mappings and "normal" slots
  
                        let previousUsed = view (env . keccakUsed) vm
                        env . keccakUsed <>= [(bytes, hash')]
                        constraints <>= (hash' .> 100, Todo "probabilistic keccak assumption" []):
                          (fmap (\(preimage, image) ->
                            -- keccak is a function
                            ((preimage .== bytes .=> image .== hash') .&&
                            -- which is injective
                            (image .== hash' .=> preimage .== bytes), Todo "injective keccak assumption" []))
                           previousUsed)
  
                        next
                        assign (state . stack) (hash : xs)
                        (env . sha3Crack) <>= invMap
              _ -> underrun
  
          -- op: ADDRESS
          0x30 ->
            limitStack 1 $
              burn g_base (next >> push (num self))
  
          -- op: BALANCE
          0x31 ->
            case stk of
              (x':xs) -> forceConcrete x' $ \x ->
                accessAndBurn (num x) $
                  fetchAccount (num x) $ \c -> do
                    next
                    assign (state . stack) xs
                    push (view balance c)
              [] ->
                underrun
  
          -- op: ORIGIN
          0x32 ->
            limitStack 1 . burn g_base $
              next >> push (num (the tx origin))
  
          -- op: CALLER
          0x33 ->
            limitStack 1 . burn g_base $
              let toSymWord :: SAddr -> SymWord
                  toSymWord (SAddr x) = case unliteral x of
                    Just s -> litWord $ num s
                    Nothing -> var "CALLER" $ sFromIntegral x
              in next >> pushSym (toSymWord (the state caller))
  
          -- op: CALLVALUE
          0x34 ->
            limitStack 1 . burn g_base $
              next >> pushSym (the state callvalue)
  
          -- op: CALLDATALOAD
          0x35 -> stackOp1 (const g_verylow) $
            \ind -> uncurry (readSWordWithBound ind) (the state calldata)
  
          -- op: CALLDATASIZE
          0x36 ->
            limitStack 1 . burn g_base $
              next >> pushSym (snd (the state calldata))
  
          -- op: CALLDATACOPY
          0x37 ->
            case stk of
              (xTo' : xFrom' : xSize' : xs) -> forceConcrete3 (xTo',xFrom',xSize') $ \(xTo,xFrom,xSize) ->
                burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $
                  accessUnboundedMemoryRange fees xTo xSize $ do
                    next
                    assign (state . stack) xs
                    case the state calldata of
                      (SymbolicBuffer cd, (S _ cdlen)) -> copyBytesToMemory (SymbolicBuffer [ite (i .<= cdlen) x 0 | (x, i) <- zip cd [1..]]) xSize xFrom xTo
                      -- when calldata is concrete,
                      -- the bound should always be equal to the bytestring length
                      (cd, _) -> copyBytesToMemory cd xSize xFrom xTo
              _ -> underrun
  
          -- op: CODESIZE
          0x38 ->
            limitStack 1 . burn g_base $
              next >> push (num (len (the state code)))
  
          -- op: CODECOPY
          0x39 ->
            case stk of
              (memOffset' : codeOffset' : n' : xs) -> forceConcrete3 (memOffset',codeOffset',n') $ \(memOffset,codeOffset,n) -> do
                burn (g_verylow + g_copy * ceilDiv (num n) 32) $
                  accessUnboundedMemoryRange fees memOffset n $ do
                    next
                    assign (state . stack) xs
                    copyBytesToMemory (the state code)
                      n codeOffset memOffset
              _ -> underrun
  
          -- op: GASPRICE
          0x3a ->
            limitStack 1 . burn g_base $
              next >> push (the tx gasprice)
  
          -- op: EXTCODESIZE
          0x3b ->
            case stk of
              (x':xs) -> makeUnique x' $ \x ->
                if x == num cheatCode
                  then do
                    next
                    assign (state . stack) xs
                    push (w256 1)
                  else
                    accessAndBurn (num x) $
                      fetchAccount (num x) $ \c -> do
                        next
                        assign (state . stack) xs
                        push (num (len (view bytecode c)))
              [] ->
                underrun
  
          -- op: EXTCODECOPY
          0x3c ->
            case stk of
              ( extAccount'
                : memOffset'
                : codeOffset'
                : codeSize'
                : xs ) ->
                forceConcrete4 (extAccount', memOffset', codeOffset', codeSize') $
                  \(extAccount, memOffset, codeOffset, codeSize) -> do
                    acc <- accessAccountForGas (num extAccount)
                    let cost = if acc then g_warm_storage_read else g_cold_account_access
                    burn (cost + g_copy * ceilDiv (num codeSize) 32) $
                      accessUnboundedMemoryRange fees memOffset codeSize $
                        fetchAccount (num extAccount) $ \c -> do
                          next
                          assign (state . stack) xs
                          copyBytesToMemory (view bytecode c)
                            codeSize codeOffset memOffset
              _ -> underrun
  
          -- op: RETURNDATASIZE
          0x3d ->
            limitStack 1 . burn g_base $
              next >> push (num $ len (the state returndata))
  
          -- op: RETURNDATACOPY
          0x3e ->
            case stk of
              (xTo' : xFrom' : xSize' :xs) -> forceConcrete3 (xTo', xFrom', xSize') $
                \(xTo, xFrom, xSize) ->
                  burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $
                    accessUnboundedMemoryRange fees xTo xSize $ do
                      next
                      assign (state . stack) xs
                      if num (len (the state returndata)) < xFrom + xSize || xFrom + xSize < xFrom
                      then vmError InvalidMemoryAccess
                      else copyBytesToMemory (the state returndata) xSize xFrom xTo
              _ -> underrun
  
          -- op: EXTCODEHASH
          0x3f ->
            case stk of
              (x':xs) -> forceConcrete x' $ \x ->
                accessAndBurn (num x) $ do
                  next
                  assign (state . stack) xs
                  fetchAccount (num x) $ \c ->
                     if accountEmpty c
                       then push (num (0 :: Int))
                       else case view bytecode c of
                             ConcreteBuffer b -> push (num (keccak b))
                             b'@(SymbolicBuffer b) -> pushSym (S (FromKeccak b') $ symkeccak' b)
              [] ->
                underrun
  
          -- op: BLOCKHASH
          0x40 -> do
            -- We adopt the fake block hash scheme of the VMTests,
            -- so that blockhash(i) is the hash of i as decimal ASCII.
            stackOp1 (const g_blockhash) $
              \(forceLit -> i) ->
                if i + 256 < the block number || i >= the block number
                then 0
                else
                  (num i :: Integer)
                    & show & Char8.pack & keccak & num
  
          -- op: COINBASE
          0x41 ->
            limitStack 1 . burn g_base $
              next >> push (num (the block coinbase))
  
          -- op: TIMESTAMP
          0x42 ->
            limitStack 1 . burn g_base $
              next >> pushSym (the block timestamp)
  
          -- op: NUMBER
          0x43 ->
            limitStack 1 . burn g_base $
              next >> push (the block number)
  
          -- op: DIFFICULTY
          0x44 ->
            limitStack 1 . burn g_base $
              next >> push (the block difficulty)
  
          -- op: GASLIMIT
          0x45 ->
            limitStack 1 . burn g_base $
              next >> push (the block gaslimit)
  
          -- op: CHAINID
          0x46 ->
            limitStack 1 . burn g_base $
              next >> push (the env chainId)
  
          -- op: SELFBALANCE
          0x47 ->
            limitStack 1 . burn g_low $
              next >> push (view balance this)
  
          -- op: BASEFEE
          0x48 ->
            limitStack 1 . burn g_base $
              next >> push (the block baseFee)
  
          -- op: POP
          0x50 ->
            case stk of
              (_:xs) -> burn g_base (next >> assign (state . stack) xs)
              _      -> underrun
  
          -- op: MLOAD
          0x51 ->
            case stk of
              (x':xs) -> forceConcrete x' $ \x ->
                burn g_verylow $
                  accessMemoryWord fees x $ do
                    next
                    assign (state . stack) (view (word256At (num x)) mem : xs)
              _ -> underrun
  
          -- op: MSTORE
          0x52 ->
            case stk of
              (x':y:xs) -> forceConcrete x' $ \x ->
                burn g_verylow $
                  accessMemoryWord fees x $ do
                    next
                    assign (state . memory . word256At (num x)) y
                    assign (state . stack) xs
              _ -> underrun
  
          -- op: MSTORE8
          0x53 ->
            case stk of
              (x':(S _ y):xs) -> forceConcrete x' $ \x ->
                burn g_verylow $
                  accessMemoryRange fees x 1 $ do
                    let yByte = bvExtract (Proxy :: Proxy 7) (Proxy :: Proxy 0) y
                    next
                    modifying (state . memory) (setMemoryByte x yByte)
                    assign (state . stack) xs
              _ -> underrun
  
          -- op: SLOAD
          0x54 ->
            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
  
          -- op: SSTORE
          0x55 ->
            notStatic $
            case stk of
              (x:new:xs) ->
                accessStorage self x $ \current -> do
                  availableGas <- use (state . gas)
  
                  if num availableGas <= g_callstipend
                    then finishFrame (FrameErrored (OutOfGas availableGas (num g_callstipend)))
                    else do
                      let original = case view storage this of
                                    Concrete _ -> fromMaybe 0 (Map.lookup (forceLit x) (view origStorage this))
                                    Symbolic _ _ -> 0 -- we don't use this value anywhere anyway
                          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 new' == 0
                                          then refund (g_sreset + g_access_list_storage_key)
                                          else unRefund (g_sreset + g_access_list_storage_key)
                                        when (original == new') $
                                          if original == 0
                                          then refund (g_sset - g_sload)
                                          else refund (g_sreset - g_sload)
                           -- if any of the arguments are symbolic,
                           -- don't change the refund counter
                           _ -> noop
              _ -> underrun
  
          -- op: JUMP
          0x56 ->
            case stk of
              (x:xs) ->
                burn g_mid $ forceConcrete x $ \x' ->
                  checkJump x' xs
              _ -> underrun
  
          -- op: JUMPI
          0x57 -> do
            case stk of
              (x:y@(S w _):xs) -> forceConcrete x $ \x' ->
                  burn g_high $
                    let jump :: Bool -> EVM ()
                        jump True = assign (state . stack) xs >> next
                        jump _    = checkJump x' xs
                    in case maybeLitWord y of
                        Just y' -> jump (0 == y')
                        -- if the jump condition is symbolic, an smt query has to be made.
                        Nothing -> askSMT (self, the state pc) (0 .== y, IsZero w) jump
              _ -> underrun
  
          -- op: PC
          0x58 ->
            limitStack 1 . burn g_base $
              next >> push (num (the state pc))
  
          -- op: MSIZE
          0x59 ->
            limitStack 1 . burn g_base $
              next >> push (num (the state memorySize))
  
          -- op: GAS
          0x5a ->
            limitStack 1 . burn g_base $
              next >> push (the state gas - num g_base)
  
          -- op: JUMPDEST
          0x5b -> burn g_jumpdest next
  
          -- op: EXP
          0x0a ->
            let cost (_ ,(forceLit -> exponent)) =
                  if exponent == 0
                  then g_exp
                  else g_exp + g_expbyte * num (ceilDiv (1 + log2 exponent) 8)
            in stackOp2 cost $ \((S a x),(S b y)) -> S (Exp a b) (x .^ y)
  
          -- op: SIGNEXTEND
          0x0b ->
            stackOp2 (const g_low) $ \((forceLit -> bytes), w@(S a x)) ->
              if bytes >= 32 then w
              else let n = num bytes * 8 + 7 in
                S (Todo "signextend" [a]) $ ite (sTestBit x n)
                                            (x .|. complement (bit n - 1))
                                            (x .&. (bit n - 1))
  
          -- op: CREATE
          0xf0 ->
            notStatic $
            case stk of
              (xValue' : xOffset' : xSize' : xs) -> forceConcrete3 (xValue', xOffset', xSize') $
                \(xValue, xOffset, xSize) -> do
                  accessMemoryRange fees xOffset xSize $ do
                    availableGas <- use (state . gas)
                    let
                      newAddr = createAddress self (wordValue (view nonce this))
                      (cost, gas') = costOfCreate fees availableGas 0
                    _ <- accessAccountForGas newAddr
                    burn (cost - gas') $
                      let initCode = readMemory (num xOffset) (num xSize) vm
                      in create self this (num gas') xValue xs newAddr initCode
              _ -> underrun
  
          -- op: CALL
          0xf1 ->
            case stk of
              ( xGas'
                : S _ xTo
                : (forceLit -> xValue)
                : xInOffset'
                : xInSize'
                : xOutOffset'
                : xOutSize'
                : xs
               ) -> forceConcrete5 (xGas',xInOffset', xInSize', xOutOffset', xOutSize') $
                \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->
                  (if xValue > 0 then notStatic else id) $
                    let target = SAddr $ sFromIntegral xTo in
                    delegateCall this xGas target target xValue xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do
                      zoom state $ do
                        assign callvalue (litWord xValue)
                        assign caller (litAddr self)
                        assign contract callee
                      transfer self callee xValue
                      touchAccount self
                      touchAccount callee
              _ ->
                underrun
  
          -- op: CALLCODE
          0xf2 ->
            case stk of
              ( xGas'
                : S _ xTo'
                : (forceLit -> xValue)
                : xInOffset'
                : xInSize'
                : xOutOffset'
                : xOutSize'
                : xs
                ) -> forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') $
                  \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->
                    let target = SAddr $ sFromIntegral xTo' in
                    delegateCall this xGas target (litAddr self) xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do
                      zoom state $ do
                        assign callvalue (litWord xValue)
                        assign caller (litAddr self)
                      touchAccount self
              _ ->
                underrun
  
          -- op: RETURN
          0xf3 ->
            case stk of
              (xOffset' : xSize' :_) -> forceConcrete2 (xOffset', xSize') $ \(xOffset, xSize) ->
                accessMemoryRange fees xOffset xSize $ do
                  let
                    output = readMemory xOffset xSize vm
                    codesize = num (len output)
                    maxsize = the block maxCodeSize
                    creation = case view frames vm of
                      [] -> the tx isCreate
                      frame:_ -> case view frameContext frame of
                         CreationContext {} -> True
                         CallContext {} -> False
                  if creation
                  then
                    if codesize > maxsize
                    then
                      finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))
                    else
                      if isConcretely (readByteOrZero 0 output) ((==) 0xef)
                      then finishFrame $ FrameErrored InvalidFormat
                      else do
                        burn (g_codedeposit * num codesize) $
                          finishFrame (FrameReturned output)
                  else
                     finishFrame (FrameReturned output)
              _ -> underrun
  
          -- op: DELEGATECALL
          0xf4 ->
            case stk of
              (xGas'
               :S _ xTo
               :xInOffset'
               :xInSize'
               :xOutOffset'
               :xOutSize'
               :xs) -> forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') $
                \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->
                  let target = SAddr $ sFromIntegral xTo in
                  delegateCall this xGas target (litAddr self) 0 xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do
                    touchAccount self
              _ -> underrun
  
          -- op: CREATE2
          0xf5 -> notStatic $
            case stk of
              (xValue'
               :xOffset'
               :xSize'
               :xSalt'
               :xs) -> forceConcrete4 (xValue', xOffset', xSize', xSalt') $
                \(xValue, xOffset, xSize, xSalt) ->
                  accessMemoryRange fees xOffset xSize $ do
                    availableGas <- use (state . gas)
  
                    forceConcreteBuffer (readMemory (num xOffset) (num xSize) vm) $ \initCode -> do
                     let
                      newAddr  = create2Address self (num xSalt) initCode
                      (cost, gas') = costOfCreate fees availableGas xSize
                     _ <- accessAccountForGas newAddr
                     burn (cost - gas') $
                      create self this (num gas') xValue xs newAddr (ConcreteBuffer initCode)
              _ -> underrun
  
          -- op: STATICCALL
          0xfa ->
            case stk of
              (xGas'
               :S _ xTo
               :xInOffset'
               :xInSize'
               :xOutOffset'
               :xOutSize'
               :xs) -> forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') $
                \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) -> do
                  let target = SAddr $ sFromIntegral xTo
                  delegateCall this xGas target target 0 xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do
                    zoom state $ do
                      assign callvalue 0
                      assign caller (litAddr self)
                      assign contract callee
                      assign static True
                    touchAccount self
                    touchAccount callee
              _ ->
                underrun
  
          -- op: SELFDESTRUCT
          0xff ->
            notStatic $
            case stk of
              [] -> underrun
              (xTo':_) -> forceConcrete xTo' $ \(num -> xTo) -> do
                acc <- accessAccountForGas (num xTo)
                let cost = if acc then 0 else g_cold_account_access
                    funds = view balance this
                    recipientExists = accountExists xTo vm
                    c_new = if not recipientExists && funds /= 0
                            then num g_selfdestruct_newaccount
                            else 0
                burn (g_selfdestruct + c_new + cost) $ do
                     selfdestruct self
                     touchAccount xTo
  
                     if funds /= 0
                     then fetchAccount xTo $ \_ -> do
                            env . contracts . ix xTo . balance += funds
                            assign (env . contracts . ix self . balance) 0
                            doStop
                     else doStop
  
          -- op: REVERT
          0xfd ->
            case stk of
              (xOffset':xSize':_) -> forceConcrete2 (xOffset', xSize') $ \(xOffset, xSize) ->
                accessMemoryRange fees xOffset xSize $ do
                  let output = readMemory xOffset xSize vm
                  finishFrame (FrameReverted output)
              _ -> underrun
  
          xxx ->
            vmError (UnrecognizedOpcode xxx)
  
  transfer :: Addr -> Addr -> Word -> EVM ()
  transfer xFrom xTo xValue =
    zoom (env . contracts) $ do
      ix xFrom . balance -= xValue
      ix xTo  . balance += xValue
  
  -- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.
  callChecks
    :: (?op :: Word8)
    => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord]
     -- continuation with gas available for call
    -> (Integer -> EVM ())
    -> EVM ()
  callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue = do
    vm <- get
    let fees = view (block . schedule) vm
    accessMemoryRange fees xInOffset xInSize $
      accessMemoryRange fees xOutOffset xOutSize $ do
        availableGas <- use (state . gas)
        let recipientExists = accountExists xContext vm
        (cost, gas') <- costOfCall fees recipientExists xValue availableGas xGas xTo
        burn (cost - gas') $ do
          if xValue > view balance this
          then do
            assign (state . stack) (0 : xs)
            assign (state . returndata) mempty
            pushTrace $ ErrorTrace $ BalanceTooLow xValue (view balance this)
            next
          else if length (view frames vm) >= 1024
               then do
                 assign (state . stack) (0 : xs)
                 assign (state . returndata) mempty
                 pushTrace $ ErrorTrace CallDepthLimitReached
                 next
               else continue gas'
  
  precompiledContract
    :: (?op :: Word8)
    => Contract
    -> Word
    -> Addr
    -> Addr
    -> Word
    -> Word -> Word -> Word -> Word
    -> [SymWord]
    -> EVM ()
  precompiledContract this xGas precompileAddr recipient xValue inOffset inSize outOffset outSize xs =
    callChecks this xGas recipient precompileAddr xValue inOffset inSize outOffset outSize xs $ \gas' ->
    do
      executePrecompile precompileAddr gas' inOffset inSize outOffset outSize xs
      self <- use (state . contract)
      stk <- use (state . stack)
      case stk of
        (x:_) -> case maybeLitWord x of
          Just 0 ->
            return ()
          Just 1 ->
            fetchAccount recipient $ \_ -> do
  
            transfer self recipient xValue
            touchAccount self
            touchAccount recipient
          _ -> vmError UnexpectedSymbolicArg
        _ -> underrun
  
  executePrecompile
    :: (?op :: Word8)
    => Addr
    -> Integer -> Word -> Word -> Word -> Word -> [SymWord]
    -> EVM ()
  executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  = do
    vm <- get
    let input = readMemory (num inOffset) (num inSize) vm
        fees = view (block . schedule) vm
        cost = costOfPrecompile fees preCompileAddr input
        notImplemented = error $ "precompile at address " <> show preCompileAddr <> " not yet implemented"
        precompileFail = burn (num gasCap - cost) $ do
                           assign (state . stack) (0 : xs)
                           pushTrace $ ErrorTrace PrecompileFailure
                           next
    if cost > num gasCap then
      burn (num gasCap) $ do
        assign (state . stack) (0 : xs)
        next
    else
      burn cost $
        case preCompileAddr of
          -- ECRECOVER
          0x1 ->
           -- TODO: support symbolic variant
           forceConcreteBuffer input $ \input' ->
            case EVM.Precompiled.execute 0x1 (truncpadlit 128 input') 32 of
              Nothing -> do
                -- return no output for invalid signature
                assign (state . stack) (1 : xs)
                assign (state . returndata) mempty
                next
              Just output -> do
                assign (state . stack) (1 : xs)
                assign (state . returndata) (ConcreteBuffer output)
                copyBytesToMemory (ConcreteBuffer output) outSize 0 outOffset
                next
  
          -- SHA2-256
          0x2 ->
            let
              hash = case input of
                       ConcreteBuffer input' -> ConcreteBuffer $ BS.pack $ BA.unpack (Crypto.hash input' :: Digest SHA256)
                       SymbolicBuffer input' -> SymbolicBuffer $ symSHA256 input'
            in do
              assign (state . stack) (1 : xs)
              assign (state . returndata) hash
              copyBytesToMemory hash outSize 0 outOffset
              next
  
          -- RIPEMD-160
          0x3 ->
           -- TODO: support symbolic variant
           forceConcreteBuffer input $ \input' ->
  
            let
              padding = BS.pack $ replicate 12 0
              hash' = BS.pack $ BA.unpack (Crypto.hash input' :: Digest RIPEMD160)
              hash  = ConcreteBuffer $ padding <> hash'
            in do
              assign (state . stack) (1 : xs)
              assign (state . returndata) hash
              copyBytesToMemory hash outSize 0 outOffset
              next
  
          -- IDENTITY
          0x4 -> do
              assign (state . stack) (1 : xs)
              assign (state . returndata) input
              copyCallBytesToMemory input outSize 0 outOffset
              next
  
          -- MODEXP
          0x5 ->
           -- TODO: support symbolic variant
           forceConcreteBuffer input $ \input' ->
  
            let
              (lenb, lene, lenm) = parseModexpLength input'
  
              output = ConcreteBuffer $
                if isZero (96 + lenb + lene) lenm input'
                then truncpadlit (num lenm) (asBE (0 :: Int))
                else
                  let
                    b = asInteger $ lazySlice 96 lenb input'
                    e = asInteger $ lazySlice (96 + lenb) lene input'
                    m = asInteger $ lazySlice (96 + lenb + lene) lenm input'
                  in
                    padLeft (num lenm) (asBE (expFast b e m))
            in do
              assign (state . stack) (1 : xs)
              assign (state . returndata) output
              copyBytesToMemory output outSize 0 outOffset
              next
  
          -- ECADD
          0x6 ->
           -- TODO: support symbolic variant
           forceConcreteBuffer input $ \input' ->
             case EVM.Precompiled.execute 0x6 (truncpadlit 128 input') 64 of
            Nothing -> precompileFail
            Just output -> do
              let truncpaddedOutput = ConcreteBuffer $ truncpadlit 64 output
              assign (state . stack) (1 : xs)
              assign (state . returndata) truncpaddedOutput
              copyBytesToMemory truncpaddedOutput outSize 0 outOffset
              next
  
          -- ECMUL
          0x7 ->
           -- TODO: support symbolic variant
           forceConcreteBuffer input $ \input' ->
  
            case EVM.Precompiled.execute 0x7 (truncpadlit 96 input') 64 of
            Nothing -> precompileFail
            Just output -> do
              let truncpaddedOutput = ConcreteBuffer $ truncpadlit 64 output
              assign (state . stack) (1 : xs)
              assign (state . returndata) truncpaddedOutput
              copyBytesToMemory truncpaddedOutput outSize 0 outOffset
              next
  
          -- ECPAIRING
          0x8 ->
           -- TODO: support symbolic variant
           forceConcreteBuffer input $ \input' ->
  
            case EVM.Precompiled.execute 0x8 input' 32 of
            Nothing -> precompileFail
            Just output -> do
              let truncpaddedOutput = ConcreteBuffer $ truncpadlit 32 output
              assign (state . stack) (1 : xs)
              assign (state . returndata) truncpaddedOutput
              copyBytesToMemory truncpaddedOutput outSize 0 outOffset
              next
  
          -- BLAKE2
          0x9 ->
           -- TODO: support symbolic variant
           forceConcreteBuffer input $ \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 = ConcreteBuffer $ truncpadlit 64 output
                  assign (state . stack) (1 : xs)
                  assign (state . returndata) truncpaddedOutput
                  copyBytesToMemory truncpaddedOutput outSize 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 :: Word -> Word -> ByteString -> LS.ByteString
  lazySlice offset size bs =
    let bs' = LS.take (num size) (LS.drop (num offset) (fromStrict bs))
    in bs' <> LS.replicate ((num size) - LS.length bs') 0
  
  parseModexpLength :: ByteString -> (Word, Word, Word)
  parseModexpLength input =
    let lenb = w256 $ word $ LS.toStrict $ lazySlice  0 32 input
        lene = w256 $ word $ LS.toStrict $ lazySlice 32 64 input
        lenm = w256 $ 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 :: Word -> Word -> ByteString -> Bool
  isZero offset size bs =
    LS.all (== 0) $
      LS.take (num size) $
        LS.drop (num offset) $
          fromStrict bs
  
  asInteger :: LS.ByteString -> Integer
  asInteger xs = if xs == mempty then 0
    else 256 * asInteger (LS.init xs)
        + num (LS.last xs)
  
  -- * Opcode helper actions
  
  noop :: Monad m => m ()
  noop = pure ()
  
  pushTo :: MonadState s m => ASetter s s [a] [a] -> a -> m ()
  pushTo f x = f %= (x :)
  
  pushToSequence :: MonadState s m => ASetter s s (Seq a) (Seq a) -> a -> m ()
  pushToSequence f x = f %= (Seq.|> x)
  
  getCodeLocation :: VM -> CodeLocation
  getCodeLocation vm = (view (state . contract) vm, view (state . pc) vm)
  
  -- | Ask the SMT solver to provide a concrete model for val iff a unique model exists
  makeUnique :: SymWord -> (Word -> EVM ()) -> EVM ()
  makeUnique sw@(S w val) cont = case maybeLitWord sw of
    Nothing -> do
      conditions <- use constraints
      assign result . Just . VMFailure . Query $ PleaseMakeUnique val (fst <$> conditions) $ \case
        Unique a -> do
          assign result Nothing
          cont (C w $ fromSizzle a)
        InconsistentU -> vmError DeadPath
        TimeoutU -> vmError SMTTimeout
        Multiple -> vmError $ NotUnique w
    Just a -> cont a
  
  -- | Construct SMT Query and halt execution until resolved
  askSMT :: CodeLocation -> (SBool, Whiff) -> (Bool -> EVM ()) -> EVM ()
  askSMT codeloc (condition, whiff) continue = do
    -- We keep track of how many times we have come across this particular
    -- (contract, pc) combination in the `iteration` mapping.
    iteration <- use (iterations . at codeloc . non 0)
  
    -- If we are backstepping, the result of this query should be cached
    -- already. So we first check the cache to see if the result is known
    use (cache . path . at (codeloc, iteration)) >>= \case
       -- If the query has been done already, select path or select the only available
       Just w -> choosePath (Case w)
       -- If this is a new query, run the query, cache the result
       -- increment the iterations and select appropriate path
       Nothing -> do pathconds <- use constraints
                     assign result . Just . VMFailure . Query $ PleaseAskSMT
                       condition' (fst <$> pathconds) choosePath
  
     where condition' = simplifyCondition condition whiff
  
           choosePath :: BranchCondition -> EVM ()
           -- Only one path is possible
           choosePath (Case v) = do assign result Nothing
                                    pushTo constraints $ if v then (condition', whiff) else (sNot condition', IsZero whiff)
                                    iteration <- use (iterations . at codeloc . non 0)
                                    assign (cache . path . at (codeloc, iteration)) (Just v)
                                    assign (iterations . at codeloc) (Just (iteration + 1))
                                    continue v
           -- Both paths are possible; we ask for more input
           choosePath Unknown = assign result . Just . VMFailure . Choose . PleaseChoosePath whiff $ choosePath . Case
           -- None of the paths are possible; fail this branch
           choosePath Inconsistent = vmError DeadPath
  
  -- | Construct RPC Query and halt execution until resolved
  fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM ()
  fetchAccount addr continue =
    use (env . contracts . at addr) >>= \case
      Just c -> continue c
      Nothing ->
        use (cache . fetched . at addr) >>= \case
          Just c -> do
            assign (env . contracts . at addr) (Just c)
            continue c
          Nothing -> do
            model <- use (env . storageModel)
            assign result . Just . VMFailure $ Query $
              PleaseFetchContract addr model
                (\c -> do assign (cache . fetched . at addr) (Just c)
                          assign (env . contracts . at addr) (Just c)
                          assign result Nothing
                          continue c)
  
  readStorage :: Storage -> SymWord -> Maybe (SymWord)
  readStorage (Symbolic _ s) (S w loc) = Just $ S (FromStorage w s) $ readArray s loc
  readStorage (Concrete s) loc = Map.lookup (forceLit loc) s
  
  writeStorage :: SymWord -> SymWord -> Storage -> Storage
  writeStorage k@(S _ loc) v@(S _ val) (Symbolic xs s) = Symbolic ((k,v):xs) (writeArray s loc val)
  writeStorage loc val (Concrete s) = Concrete (Map.insert (forceLit loc) val s)
  
  accessStorage
    :: Addr                -- ^ Contract address
    -> SymWord             -- ^ Storage slot key
    -> (SymWord -> EVM ()) -- ^ Continuation
    -> EVM ()
  accessStorage addr slot continue =
    use (env . contracts . at addr) >>= \case
      Just c ->
        case readStorage (view storage c) slot of
          -- Notice that if storage is symbolic, we always continue straight away
          Just x ->
            continue x
          Nothing ->
            if view external c
            then
              -- check if the slot is cached
              use (cache . fetched . at addr) >>= \case
                Nothing -> mkQuery
                Just cachedContract ->
                  maybe mkQuery continue (readStorage (view storage cachedContract) slot)
            else do
              modifying (env . contracts . ix addr . storage) (writeStorage slot 0)
              continue 0
      Nothing ->
        fetchAccount addr $ \_ ->
          accessStorage addr slot continue
    where
        mkQuery = assign result . Just . VMFailure . Query $
                    PleaseFetchSlot addr (forceLit slot)
                      (\(litWord -> x) -> do
                          modifying (cache . fetched . ix addr . storage) (writeStorage slot x)
                          modifying (env . contracts . ix addr . storage) (writeStorage slot x)
                          assign result Nothing
                          continue x)
  
  accountExists :: Addr -> VM -> Bool
  accountExists addr vm =
    case view (env . contracts . at addr) vm of
      Just c -> not (accountEmpty c)
      Nothing -> False
  
  -- EIP 161
  accountEmpty :: Contract -> Bool
  accountEmpty c =
    case view contractcode c of
      RuntimeCode b -> len b == 0
      _ -> False
    && (view nonce c == 0)
    && (view balance c == 0)
  
  -- * How to finalize a transaction
  finalize :: EVM ()
  finalize = do
    let
      revertContracts  = use (tx . txReversion) >>= assign (env . contracts)
      revertSubstate   = assign (tx . substate) (SubState mempty mempty mempty mempty mempty)
  
    use result >>= \case
      Nothing ->
        error "Finalising an unfinished tx."
      Just (VMFailure (Revert _)) -> do
        revertContracts
        revertSubstate
      Just (VMFailure _) -> do
        -- burn remaining gas
        assign (state . gas) 0
        revertContracts
        revertSubstate
      Just (VMSuccess output) -> do
        -- deposit the code from a creation tx
        creation <- use (tx . isCreate)
        createe  <- use (state . contract)
        createeExists <- (Map.member createe) <$> use (env . contracts)
  
        when (creation && createeExists) $ replaceCode createe (RuntimeCode output)
  
    -- compute and pay the refund to the caller and the
    -- corresponding payment to the miner
    txOrigin     <- use (tx . origin)
    sumRefunds   <- (sum . (snd <$>)) <$> (use (tx . substate . refunds))
    miner        <- use (block . coinbase)
    blockReward  <- num . r_block <$> (use (block . schedule))
    gasPrice     <- use (tx . gasprice)
    priorityFee  <- use (tx . txPriorityFee)
    gasLimit     <- use (tx . txgaslimit)
    gasRemaining <- use (state . gas)
  
    let
      gasUsed      = gasLimit - gasRemaining
      cappedRefund = min (quot gasUsed 5) (num sumRefunds)
      originPay    = (gasRemaining + cappedRefund) * gasPrice
  
      minerPay     = priorityFee * gasUsed
  
    modifying (env . contracts)
       (Map.adjust (over balance (+ originPay)) txOrigin)
    modifying (env . contracts)
       (Map.adjust (over balance (+ minerPay)) miner)
    touchAccount miner
  
    -- pay out the block reward, recreating the miner if necessary
    preuse (env . contracts . ix miner) >>= \case
      Nothing -> modifying (env . contracts)
        (Map.insert miner (initialContract (EVM.RuntimeCode mempty)))
      Just _  -> noop
    modifying (env . contracts)
      (Map.adjust (over balance (+ blockReward)) miner)
  
    -- perform state trie clearing (EIP 161), of selfdestructs
    -- and touched accounts. addresses are cleared if they have
    --    a) selfdestructed, or
    --    b) been touched and
    --    c) are empty.
    -- (see Yellow Paper "Accrued Substate")
    --
    -- remove any destructed addresses
    destroyedAddresses <- use (tx . substate . selfdestructs)
    modifying (env . contracts)
      (Map.filterWithKey (\k _ -> (notElem k destroyedAddresses)))
    -- then, clear any remaining empty and touched addresses
    touchedAddresses <- use (tx . substate . touchedAccounts)
    modifying (env . contracts)
      (Map.filterWithKey
        (\k a -> not ((elem k touchedAddresses) && accountEmpty a)))
  
  -- | Loads the selected contract as the current contract to execute
  loadContract :: Addr -> EVM ()
  loadContract target =
    preuse (env . contracts . ix target . contractcode) >>=
      \case
        Nothing ->
          error "Call target doesn't exist"
        Just (InitCode targetCode) -> do
          assign (state . contract) target
          assign (state . code)     targetCode
          assign (state . codeContract) target
        Just (RuntimeCode targetCode) -> do
          assign (state . contract) target
          assign (state . code)     targetCode
          assign (state . codeContract) target
  
  limitStack :: Int -> EVM () -> EVM ()
  limitStack n continue = do
    stk <- use (state . stack)
    if length stk + n > 1024
      then vmError StackLimitExceeded
      else continue
  
  notStatic :: EVM () -> EVM ()
  notStatic continue = do
    bad <- use (state . static)
    if bad
      then vmError StateChangeWhileStatic
      else continue
  
  -- | Burn gas, failing if insufficient gas is available
  -- We use the `Integer` type to avoid overflows in intermediate
  -- calculations and throw if the value won't fit into a uint64
  burn :: Integer -> EVM () -> EVM ()
  burn n' continue =
    if n' > (2 :: Integer) ^ (64 :: Integer) - 1
    then vmError IllegalOverflow
    else do
      let n = num n'
      available <- use (state . gas)
      if n <= available
        then do
          state . gas -= n
          burned += n
          continue
        else
          vmError (OutOfGas available n)
  
  forceConcreteAddr :: SAddr -> (Addr -> EVM ()) -> EVM ()
  forceConcreteAddr n continue = case maybeLitAddr n of
    Nothing -> vmError UnexpectedSymbolicArg
    Just c -> continue c
  
  forceConcrete :: SymWord -> (Word -> EVM ()) -> EVM ()
  forceConcrete n continue = case maybeLitWord n of
    Nothing -> vmError UnexpectedSymbolicArg
    Just c -> continue c
  
  forceConcrete2 :: (SymWord, SymWord) -> ((Word, Word) -> EVM ()) -> EVM ()
  forceConcrete2 (n,m) continue = case (maybeLitWord n, maybeLitWord m) of
    (Just c, Just d) -> continue (c, d)
    _ -> vmError UnexpectedSymbolicArg
  
  forceConcrete3 :: (SymWord, SymWord, SymWord) -> ((Word, Word, Word) -> EVM ()) -> EVM ()
  forceConcrete3 (k,n,m) continue = case (maybeLitWord k, maybeLitWord n, maybeLitWord m) of
    (Just c, Just d, Just f) -> continue (c, d, f)
    _ -> vmError UnexpectedSymbolicArg
  
  forceConcrete4 :: (SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word) -> EVM ()) -> EVM ()
  forceConcrete4 (k,l,n,m) continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord n, maybeLitWord m) of
    (Just b, Just c, Just d, Just f) -> continue (b, c, d, f)
    _ -> vmError UnexpectedSymbolicArg
  
  forceConcrete5 :: (SymWord, SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word, Word) -> EVM ()) -> EVM ()
  forceConcrete5 (k,l,m,n,o) continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o) of
    (Just a, Just b, Just c, Just d, Just e) -> continue (a, b, c, d, e)
    _ -> vmError UnexpectedSymbolicArg
  
  forceConcrete6 :: (SymWord, SymWord, SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word, Word, Word) -> EVM ()) -> EVM ()
  forceConcrete6 (k,l,m,n,o,p) continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o, maybeLitWord p) of
    (Just a, Just b, Just c, Just d, Just e, Just f) -> continue (a, b, c, d, e, f)
    _ -> vmError UnexpectedSymbolicArg
  
  forceConcreteBuffer :: Buffer -> (ByteString -> EVM ()) -> EVM ()
  forceConcreteBuffer (SymbolicBuffer b) continue = case maybeLitBytes b of
    Nothing -> vmError UnexpectedSymbolicArg
    Just bs -> continue bs
  forceConcreteBuffer (ConcreteBuffer b) continue = continue b
  
  -- * Substate manipulation
  refund :: Integer -> EVM ()
  refund n = do
    self <- use (state . contract)
    pushTo (tx . substate . refunds) (self, n)
  
  unRefund :: Integer -> EVM ()
  unRefund n = do
    self <- use (state . contract)
    refs <- use (tx . substate . refunds)
    assign (tx . substate . refunds)
      (filter (\(a,b) -> not (a == self && b == n)) refs)
  
  touchAccount :: Addr -> EVM()
  touchAccount = pushTo ((tx . substate) . touchedAccounts)
  
  selfdestruct :: Addr -> EVM()
  selfdestruct = pushTo ((tx . substate) . selfdestructs)
  
  accessAndBurn :: Addr -> EVM () -> EVM ()
  accessAndBurn x cont = do
    FeeSchedule {..} <- use ( block . schedule )
    acc <- accessAccountForGas x
    let cost = if acc then g_warm_storage_read else g_cold_account_access
    burn cost cont
  
  -- | returns a wrapped boolean- if true, this address has been touched before in the txn (warm gas cost as in EIP 2929)
  -- otherwise cold
  accessAccountForGas :: Addr -> EVM Bool
  accessAccountForGas addr = do
    accessedAddrs <- use (tx . substate . accessedAddresses)
    let accessed = member addr accessedAddrs
    assign (tx . substate . accessedAddresses) (insert addr accessedAddrs)
    return accessed
  
  -- | returns a wrapped boolean- if true, this slot has been touched before in the txn (warm gas cost as in EIP 2929)
  -- otherwise cold
  accessStorageForGas :: Addr -> SymWord -> EVM Bool
  accessStorageForGas addr key = do
    accessedStrkeys <- use (tx . substate . accessedStorageKeys)
    case maybeLitWord key of
      Just litword -> do
        let litword256 = wordValue litword
        let accessed = member (addr, litword256) accessedStrkeys
        assign (tx . substate . accessedStorageKeys) (insert (addr, litword256) accessedStrkeys)
        return accessed
      _ -> return False
  
  -- * Cheat codes
  
  -- The cheat code is 7109709ecfa91a80626ff3989d68f67f5b1dd12d.
  -- Call this address using one of the cheatActions below to do
  -- special things, e.g. changing the block timestamp. Beware that
  -- these are necessarily hevm specific.
  cheatCode :: Addr
  cheatCode = num (keccak "hevm cheat code")
  
  cheat
    :: (?op :: Word8)
    => (Word, Word) -> (Word, Word)
    -> EVM ()
  cheat (inOffset, inSize) (outOffset, outSize) = do
    mem <- use (state . memory)
    vm <- get
    let
      abi = readMemoryWord32 inOffset mem
      input = readMemory (inOffset + 4) (inSize - 4) vm
    case fromSized <$> unliteral abi of
      Nothing -> vmError UnexpectedSymbolicArg
      Just abi' ->
        case Map.lookup abi' cheatActions of
          Nothing ->
            vmError (BadCheatCode (Just abi'))
          Just action -> do
              action outOffset outSize input
              next
              push 1
  
  type CheatAction = Word -> Word -> Buffer -> EVM ()
  
  cheatActions :: Map Word32 CheatAction
  cheatActions =
    Map.fromList
      [ action "ffi(string[])" $
          \sig outOffset outSize input -> do
            vm <- get
            if view EVM.allowFFI vm then
              case decodeBuffer [AbiArrayDynamicType AbiStringType] input of
                CAbi valsArr -> case valsArr of
                  [AbiArrayDynamic AbiStringType strsV] ->
                    let
                      cmd = (flip fmap) (V.toList strsV) (\case
                        (AbiString a) -> unpack $ decodeUtf8 a
                        _ -> "")
                      cont bs = do
                        let encoded = ConcreteBuffer bs
                        assign (state . returndata) encoded
                        copyBytesToMemory encoded outSize 0 outOffset
                        assign result Nothing
                    in assign result (Just . VMFailure . Query $ (PleaseDoFFI cmd cont))
                  _ -> vmError (BadCheatCode sig)
                _ -> vmError (BadCheatCode sig)
            else
              let msg = encodeUtf8 "ffi disabled: run again with --ffi if you want to allow tests to call external scripts"
              in vmError . Revert $ abiMethod "Error(string)" (AbiTuple . V.fromList $ [AbiString msg]),
  
        action "warp(uint256)" $
          \sig _ _ input -> case decodeStaticArgs input of
            [x]  -> assign (block . timestamp) x
            _ -> vmError (BadCheatCode sig),
  
        action "roll(uint256)" $
          \sig _ _ input -> case decodeStaticArgs input of
            [x] -> forceConcrete x (assign (block . number))
            _ -> vmError (BadCheatCode sig),
  
        action "store(address,bytes32,bytes32)" $
          \sig _ _ input -> case decodeStaticArgs input of
            [a, slot, new] ->
              makeUnique a $ \(C _ (num -> a')) ->
                fetchAccount a' $ \_ -> do
                  modifying (env . contracts . ix a' . storage) (writeStorage slot new)
            _ -> vmError (BadCheatCode sig),
  
        action "load(address,bytes32)" $
          \sig outOffset _ input -> case decodeStaticArgs input of
            [a, slot] ->
              makeUnique a $ \(C _ (num -> a'))->
                accessStorage a' slot $ \res -> do
                  assign (state . returndata . word256At 0) res
                  assign (state . memory . word256At outOffset) res
            _ -> vmError (BadCheatCode sig),
  
        action "sign(uint256,bytes32)" $
          \sig outOffset _ input -> case decodeStaticArgs input of
            [sk, hash] ->
              forceConcrete sk $ \sk' ->
                forceConcrete hash $ \(C _ hash') -> let
                  curve = getCurveByName SEC_p256k1
                  priv = PrivateKey curve (num sk')
                  digest = digestFromByteString (word256Bytes hash')
                in do
                  case digest of
                    Nothing -> vmError (BadCheatCode sig)
                    Just digest' -> do
                      let s = ethsign priv digest'
                          v = if (sign_s s) % 2 == 0 then 27 else 28
                          encoded = encodeAbiValue $
                            AbiTuple (RegularVector.fromList
                              [ AbiUInt 8 v
                              , AbiBytes 32 (word256Bytes . fromInteger $ sign_r s)
                              , AbiBytes 32 (word256Bytes . fromInteger $ sign_s s)
                              ])
                      assign (state . returndata) (ConcreteBuffer encoded)
                      copyBytesToMemory (ConcreteBuffer encoded) (num . BS.length $ encoded) 0 outOffset
            _ -> vmError (BadCheatCode sig),
  
        action "addr(uint256)" $
          \sig outOffset _ input -> case decodeStaticArgs input of
            [sk] -> forceConcrete sk $ \sk' -> let
                  curve = getCurveByName SEC_p256k1
                  pubPoint = generateQ curve (num sk')
                  encodeInt = encodeAbiValue . AbiUInt 256 . fromInteger
                in do
                  case pubPoint of
                    PointO -> do vmError (BadCheatCode sig)
                    Point x y -> do
                      -- See yellow paper #286
                      let
                        pub = BS.concat [ encodeInt x, encodeInt y ]
                        addr = w256lit . num . word256 . BS.drop 12 . BS.take 32 . keccakBytes $ pub
                      assign (state . returndata . word256At 0) addr
                      assign (state . memory . word256At outOffset) addr
            _ -> vmError (BadCheatCode sig)
  
      ]
    where
      action s f = (abiKeccak s, f (Just $ abiKeccak s))
  
  -- | Hack deterministic signing, totally insecure...
  ethsign :: PrivateKey -> Digest Crypto.Keccak_256 -> Signature
  ethsign sk digest = go 420
    where
      go k = case signDigestWith k sk digest of
         Nothing  -> go (k + 1)
         Just sig -> sig
  
  -- * General call implementation ("delegateCall")
  -- note that the continuation is ignored in the precompile case
  delegateCall
    :: (?op :: Word8)
    => Contract -> Word -> SAddr -> SAddr -> Word -> Word -> Word -> Word -> Word -> [SymWord]
    -> (Addr -> EVM ())
    -> EVM ()
  delegateCall this gasGiven (SAddr xTo) (SAddr xContext) xValue xInOffset xInSize xOutOffset xOutSize xs continue =
    makeUnique (S (Todo "xTo" []) $ sFromIntegral xTo) $ \(C _ (num -> xTo')) ->
      makeUnique (S (Todo "xcontext" []) $ sFromIntegral xContext) $ \(C _ (num -> xContext')) ->
        if xTo' > 0 && xTo' <= 9
        then precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs
        else if num xTo' == cheatCode then
          do
            assign (state . stack) xs
            cheat (xInOffset, xInSize) (xOutOffset, xOutSize)
        else
          callChecks this gasGiven xContext' xTo' xValue xInOffset xInSize xOutOffset xOutSize xs $
          \xGas -> do
            vm0 <- get
            fetchAccount xTo' $ \target ->
                  burn xGas $ do
                    let newContext = CallContext
                                      { callContextTarget    = xTo'
                                      , callContextContext   = xContext'
                                      , callContextOffset    = xOutOffset
                                      , callContextSize      = xOutSize
                                      , callContextCodehash  = view codehash target
                                      , callContextReversion = view (env . contracts) vm0
                                      , callContextSubState  = view (tx . substate) vm0
                                      , callContextAbi =
                                          if xInSize >= 4
                                          then case unliteral $ readMemoryWord32 xInOffset (view (state . memory) vm0)
                                               of Nothing -> Nothing
                                                  Just abi -> Just . w256 $ num abi
                                          else Nothing
                                      , callContextData = (readMemory (num xInOffset) (num xInSize) vm0)
                                      }
  
                    pushTrace (FrameTrace newContext)
                    next
                    vm1 <- get
  
                    pushTo frames $ Frame
                      { _frameState = (set stack xs) (view state vm1)
                      , _frameContext = newContext
                      }
  
                    zoom state $ do
                      assign gas (num xGas)
                      assign pc 0
                      assign code (view bytecode target)
                      assign codeContract xTo'
                      assign stack mempty
                      assign memory mempty
                      assign memorySize 0
                      assign returndata mempty
                      assign calldata (readMemory (num xInOffset) (num xInSize) vm0, w256lit (num xInSize))
  
                    continue xTo'
  
  -- -- * Contract creation
  
  -- EIP 684
  collision :: Maybe Contract -> Bool
  collision c' = case c' of
    Just c -> (view nonce c /= 0) || case view contractcode c of
      RuntimeCode b -> len b /= 0
      _ -> True
    Nothing -> False
  
  create :: (?op :: Word8)
    => Addr -> Contract
    -> Word -> Word -> [SymWord] -> Addr -> Buffer -> EVM ()
  create self this xGas' xValue xs newAddr initCode = do
    vm0 <- get
    let xGas = num xGas'
    if xValue > view balance this
    then do
      assign (state . stack) (0 : xs)
      assign (state . returndata) mempty
      pushTrace $ ErrorTrace $ BalanceTooLow xValue (view balance this)
      next
    else if length (view frames vm0) >= 1024
    then do
      assign (state . stack) (0 : xs)
      assign (state . returndata) mempty
      pushTrace $ ErrorTrace CallDepthLimitReached
      next
    else if collision $ view (env . contracts . at newAddr) vm0
    then burn xGas $ do
      assign (state . stack) (0 : xs)
      modifying (env . contracts . ix self . nonce) succ
      next
    else burn xGas $ do
      touchAccount self
      touchAccount newAddr
      let
        store = case view (env . storageModel) vm0 of
          ConcreteS -> Concrete mempty
          SymbolicS -> Symbolic [] $ sListArray 0 []
          InitialS  -> Symbolic [] $ sListArray 0 []
        newContract =
          initialContract (InitCode initCode) & set storage store
        newContext  =
          CreationContext { creationContextAddress   = newAddr
                          , creationContextCodehash  = view codehash newContract
                          , creationContextReversion = view (env . contracts) vm0
                          , creationContextSubstate  = view (tx . substate) vm0
                          }
  
      zoom (env . contracts) $ do
        oldAcc <- use (at newAddr)
        let oldBal = maybe 0 (view balance) oldAcc
  
        assign (at newAddr) (Just (newContract & balance .~ oldBal))
        modifying (ix self . nonce) succ
  
      transfer self newAddr xValue
  
      pushTrace (FrameTrace newContext)
      next
      vm1 <- get
      pushTo frames $ Frame
        { _frameContext = newContext
        , _frameState   = (set stack xs) (view state vm1)
        }
  
      assign state $
        blankState
          & set contract   newAddr
          & set codeContract newAddr
          & set code       initCode
          & set callvalue  (litWord xValue)
          & set caller     (litAddr self)
          & set gas        xGas'
  
  -- | Replace a contract's code, like when CREATE returns
  -- from the constructor code.
  replaceCode :: Addr -> ContractCode -> EVM ()
  replaceCode target newCode =
    zoom (env . contracts . at target) $
      get >>= \case
        Just now -> case (view contractcode now) of
          InitCode _ ->
            put . Just $
            initialContract newCode
            & set storage (view storage now)
            & set balance (view balance now)
            & set nonce   (view nonce now)
          RuntimeCode _ ->
            error ("internal error: can't replace code of deployed contract " <> show target)
        Nothing ->
          error "internal error: can't replace code of nonexistent contract"
  
  replaceCodeOfSelf :: ContractCode -> EVM ()
  replaceCodeOfSelf newCode = do
    vm <- get
    replaceCode (view (state . contract) vm) newCode
  
  resetState :: EVM ()
  resetState = do
    assign result Nothing
    assign frames []
    assign state  blankState
  
  
  -- * VM error implementation
  
  vmError :: Error -> EVM ()
  vmError e = finishFrame (FrameErrored e)
  
  underrun :: EVM ()
  underrun = vmError StackUnderrun
  
  -- | A stack frame can be popped in three ways.
  data FrameResult
    = FrameReturned Buffer -- ^ STOP, RETURN, or no more code
    | FrameReverted Buffer -- ^ REVERT
    | FrameErrored Error -- ^ Any other error
    deriving Show
  
  -- | This function defines how to pop the current stack frame in either of
  -- the ways specified by 'FrameResult'.
  --
  -- It also handles the case when the current stack frame is the only one;
  -- in this case, we set the final '_result' of the VM execution.
  finishFrame :: FrameResult -> EVM ()
  finishFrame how = do
    oldVm <- get
  
    case view frames oldVm of
      -- Is the current frame the only one?
      [] -> do
        case how of
            FrameReturned output -> assign result . Just $ VMSuccess output
            FrameReverted buffer -> forceConcreteBuffer buffer $ \out -> assign result . Just $ VMFailure (Revert out)
            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 (ConcreteBuffer output) ->
              ErrorTrace (Revert output)
            FrameReverted (SymbolicBuffer output) ->
              ErrorTrace (Revert (forceLitBytes output))
            FrameReturned output ->
              ReturnTrace output (view frameContext nextFrame)
        -- 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 (view frameState nextFrame)
  
        -- When entering a call, the gas allowance is counted as burned
        -- in advance; this unburns the remainder and adds it to the
        -- parent frame.
        let remainingGas = view (state . gas) oldVm
            reclaimRemainingGasAllowance = do
              modifying burned (subtract remainingGas)
              modifying (state . gas) (+ remainingGas)
  
            FeeSchedule {..} = view ( block . schedule ) oldVm
  
        -- Now dispatch on whether we were creating or calling,
        -- and whether we shall return, revert, or error (six cases).
        case view frameContext nextFrame of
  
          -- Were we calling?
          CallContext _ _ (num -> outOffset) (num -> outSize) _ _ _ reversion substate' -> do
  
            -- Excerpt K.1. from the yellow paper:
            -- K.1. Deletion of an Account Despite Out-of-gas.
            -- At block 2675119, in the transaction 0xcf416c536ec1a19ed1fb89e4ec7ffb3cf73aa413b3aa9b77d60e4fd81a4296ba,
            -- an account at address 0x03 was called and an out-of-gas occurred during the call.
            -- Against the equation (197), this added 0x03 in the set of touched addresses, and this transaction turned σ[0x03] into ∅.
  
            -- In other words, we special case address 0x03 and keep it in the set of touched accounts during revert
            touched <- use (tx . substate . touchedAccounts)
  
            let
              substate'' = over touchedAccounts (maybe id cons (find ((==) 3) touched)) substate'
              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 0 outOffset
                reclaimRemainingGasAllowance
                push 1
  
              -- Case 2: Reverting during a call?
              FrameReverted output -> do
                revertContracts
                revertSubstate
                assign (state . returndata) output
                copyCallBytesToMemory output outSize 0 outOffset
                reclaimRemainingGasAllowance
                push 0
  
              -- Case 3: Error during a call?
              FrameErrored _ -> do
                revertContracts
                revertSubstate
                assign (state . returndata) mempty
                push 0
          -- Or were we creating?
          CreationContext _ _ reversion substate' -> do
            creator <- use (state . contract)
            let
              createe = view (state . contract) oldVm
              revertContracts = assign (env . contracts) reversion'
              revertSubstate  = assign (tx . substate) substate'
  
              -- persist the nonce through the reversion
              reversion' = (Map.adjust (over nonce (+ 1)) creator) reversion
  
            case how of
              -- Case 4: Returning during a creation?
              FrameReturned output -> do
                  replaceCode createe (RuntimeCode output)
                  assign (state . returndata) mempty
                  reclaimRemainingGasAllowance
                  push (num createe)
  
              -- Case 5: Reverting during a creation?
              FrameReverted output -> do
                revertContracts
                revertSubstate
                assign (state . returndata) output
                reclaimRemainingGasAllowance
                push 0
  
              -- Case 6: Error during a creation?
              FrameErrored _ -> do
                revertContracts
                revertSubstate
                assign (state . returndata) mempty
                push 0
  
  
  -- * Memory helpers
  
  accessUnboundedMemoryRange
    :: FeeSchedule Integer
    -> Word
    -> Word
    -> EVM ()
    -> EVM ()
  accessUnboundedMemoryRange _ _ 0 continue = continue
  accessUnboundedMemoryRange fees f l continue = do
    m0 <- num <$> use (state . memorySize)
    do
      let m1 = 32 * ceilDiv (max m0 (num f + num l)) 32
      burn (memoryCost fees m1 - memoryCost fees m0) $ do
        assign (state . memorySize) (num m1)
        continue
  
  accessMemoryRange
    :: FeeSchedule Integer
    -> Word
    -> Word
    -> EVM ()
    -> EVM ()
  accessMemoryRange _ _ 0 continue = continue
  accessMemoryRange fees f l continue =
    if f + l < l
      then vmError IllegalOverflow
      else accessUnboundedMemoryRange fees f l continue
  
  accessMemoryWord
    :: FeeSchedule Integer -> Word -> EVM () -> EVM ()
  accessMemoryWord fees x = accessMemoryRange fees x 32
  
  copyBytesToMemory
    :: Buffer -> Word -> Word -> Word -> EVM ()
  copyBytesToMemory bs size xOffset yOffset =
    if size == 0 then noop
    else do
      mem <- use (state . memory)
      assign (state . memory) $
        writeMemory bs size xOffset yOffset mem
  
  copyCallBytesToMemory
    :: Buffer -> Word -> Word -> Word -> EVM ()
  copyCallBytesToMemory bs size xOffset yOffset =
    if size == 0 then noop
    else do
      mem <- use (state . memory)
      assign (state . memory) $
        writeMemory bs (min size (num (len bs))) xOffset yOffset mem
  
  readMemory :: Word -> Word -> VM -> Buffer
  readMemory offset size vm = sliceWithZero (num offset) (num size) (view (state . memory) vm)
  
  word256At
    :: Functor f
    => Word -> (SymWord -> f (SymWord))
    -> Buffer -> f Buffer
  word256At i = lens getter setter where
    getter = EVM.Symbolic.readMemoryWord i
    setter m x = setMemoryWord i x m
  
  -- * Tracing
  
  withTraceLocation
    :: (MonadState VM m) => TraceData -> m Trace
  withTraceLocation x = do
    vm <- get
    let
      Just this =
        currentContract vm
    pure Trace
      { _traceData = x
      , _traceContract = this
      , _traceOpIx = fromMaybe 0 $ (view opIxMap this) Vector.!? (view (state . pc) vm)
      }
  
  pushTrace :: TraceData -> EVM ()
  pushTrace x = do
    trace <- withTraceLocation x
    modifying traces $
      \t -> Zipper.children $ Zipper.insert (Node trace []) t
  
  insertTrace :: TraceData -> EVM ()
  insertTrace x = do
    trace <- withTraceLocation x
    modifying traces $
      \t -> Zipper.nextSpace $ Zipper.insert (Node trace []) t
  
  popTrace :: EVM ()
  popTrace =
    modifying traces $
      \t -> case Zipper.parent t of
              Nothing -> error "internal error (trace root)"
              Just t' -> Zipper.nextSpace t'
  
  zipperRootForest :: Zipper.TreePos Zipper.Empty a -> Forest a
  zipperRootForest z =
    case Zipper.parent z of
      Nothing -> Zipper.toForest z
      Just z' -> zipperRootForest (Zipper.nextSpace z')
  
  traceForest :: VM -> Forest Trace
  traceForest = view (traces . to zipperRootForest)
  
  traceLog :: (MonadState VM m) => Log -> m ()
  traceLog log = do
    trace <- withTraceLocation (EventTrace log)
    modifying traces $
      \t -> Zipper.nextSpace (Zipper.insert (Node trace []) t)
  
  -- * Stack manipulation
  
  push :: Word -> EVM ()
  push = pushSym . w256lit . num
  
  pushSym :: SymWord -> EVM ()
  pushSym x = state . stack %= (x :)
  
  
  stackOp1
    :: (?op :: Word8)
    => ((SymWord) -> Integer)
    -> ((SymWord) -> (SymWord))
    -> EVM ()
  stackOp1 cost f =
    use (state . stack) >>= \case
      (x:xs) ->
        burn (cost x) $ do
          next
          let !y = f x
          state . stack .= y : xs
      _ ->
        underrun
  
  stackOp2
    :: (?op :: Word8)
    => (((SymWord), (SymWord)) -> Integer)
    -> (((SymWord), (SymWord)) -> (SymWord))
    -> EVM ()
  stackOp2 cost f =
    use (state . stack) >>= \case
      (x:y:xs) ->
        burn (cost (x, y)) $ do
          next
          state . stack .= f (x, y) : xs
      _ ->
        underrun
  
  stackOp3
    :: (?op :: Word8)
    => (((SymWord), (SymWord), (SymWord)) -> Integer)
    -> (((SymWord), (SymWord), (SymWord)) -> (SymWord))
    -> EVM ()
  stackOp3 cost f =
    use (state . stack) >>= \case
      (x:y:z:xs) ->
        burn (cost (x, y, z)) $ do
          next
          state . stack .= f (x, y, z) : xs
      _ ->
        underrun
  
  -- * Bytecode data functions
  
  checkJump :: (Integral n) => n -> [SymWord] -> EVM ()
  checkJump x xs = do
    theCode <- use (state . code)
    self <- use (state . codeContract)
    theCodeOps <- use (env . contracts . ix self . codeOps)
    theOpIxMap <- use (env . contracts . ix self . opIxMap)
    if x < num (len theCode) && 0x5b == (fromMaybe (error "tried to jump to symbolic code location") $ unliteral $ EVM.Symbolic.index (num x) theCode)
      then
        if OpJumpdest == snd (theCodeOps RegularVector.! (theOpIxMap Vector.! num x))
        then do
          state . stack .= xs
          state . pc .= num x
        else
          vmError BadJumpDestination
      else vmError BadJumpDestination
  
  opSize :: Word8 -> Int
  opSize x | x >= 0x60 && x <= 0x7f = num x - 0x60 + 2
  opSize _                          = 1
  
  -- Index 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 :: Buffer -> Vector Int
  mkOpIxMap xs = Vector.create $ Vector.new (len xs) >>= \v ->
    -- Loop over the byte string accumulating a vector-mutating action.
    -- This is somewhat obfuscated, but should be fast.
    case xs of
      ConcreteBuffer xs' ->
        let (_, _, _, m) =
              BS.foldl' (go v) (0 :: Word8, 0, 0, return ()) xs'
        in m >> return v
      SymbolicBuffer xs' ->
        let (_, _, _, m) =
              foldl (go' v) (0, 0, 0, return ()) (stripBytecodeMetadataSym xs')
        in m >> return v
  
    where
      -- concrete case
      go v (0, !i, !j, !m) x | x >= 0x60 && x <= 0x7f =
        {- Start of PUSH op. -} (x - 0x60 + 1, i + 1, j,     m >> Vector.write v i j)
      go v (1, !i, !j, !m) _ =
        {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> Vector.write v i j)
      go v (0, !i, !j, !m) _ =
        {- Other op. -}         (0,            i + 1, j + 1, m >> Vector.write v i j)
      go v (n, !i, !j, !m) _ =
        {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j)
  
      -- symbolic case
      go' v (0, !i, !j, !m) x = case unliteral x of
        Just x' -> if x' >= 0x60 && x' <= 0x7f
          -- start of PUSH op --
                   then (x' - 0x60 + 1, i + 1, j,     m >> Vector.write v i j)
          -- other data --
                   else (0,             i + 1, j + 1, m >> Vector.write v i j)
        _ -> error "cannot analyze symbolic code"
  
        {- Start of PUSH op. -} (x - 0x60 + 1, i + 1, j,     m >> Vector.write v i j)
      go' v (1, !i, !j, !m) _ =
        {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> Vector.write v i j)
      go' v (n, !i, !j, !m) _ =
        {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j)
  
  vmOp :: VM -> Maybe Op
  vmOp vm =
    let i  = vm ^. state . pc
        code' = vm ^. state . code
        xs = case code' of
          ConcreteBuffer xs' -> ConcreteBuffer (BS.drop i xs')
          SymbolicBuffer xs' -> SymbolicBuffer (drop i xs')
        op = case xs of
          ConcreteBuffer b -> BS.index b 0
          SymbolicBuffer b -> fromSized $ fromMaybe (error "unexpected symbolic code") (unliteral (b !! 0))
    in if (len code' < i)
       then Nothing
       else Just (readOp op xs)
  
  vmOpIx :: VM -> Maybe Int
  vmOpIx vm =
    do self <- currentContract vm
       (view opIxMap self) Vector.!? (view (state . pc) vm)
  
  opParams :: VM -> Map String (SymWord)
  opParams vm =
    case vmOp vm of
      Just OpCreate ->
        params $ words "value offset size"
      Just OpCall ->
        params $ words "gas to value in-offset in-size out-offset out-size"
      Just OpSstore ->
        params $ words "index value"
      Just OpCodecopy ->
        params $ words "mem-offset code-offset code-size"
      Just OpSha3 ->
        params $ words "offset size"
      Just OpCalldatacopy ->
        params $ words "to from size"
      Just OpExtcodecopy ->
        params $ words "account mem-offset code-offset code-size"
      Just OpReturn ->
        params $ words "offset size"
      Just OpJumpi ->
        params $ words "destination condition"
      _ -> mempty
    where
      params xs =
        if length (vm ^. state . stack) >= length xs
        then Map.fromList (zip xs (vm ^. state . stack))
        else mempty
  
  readOp :: Word8 -> Buffer -> Op
  readOp x _  | x >= 0x80 && x <= 0x8f = OpDup (x - 0x80 + 1)
  readOp x _  | x >= 0x90 && x <= 0x9f = OpSwap (x - 0x90 + 1)
  readOp x _  | x >= 0xa0 && x <= 0xa4 = OpLog (x - 0xa0)
  readOp x xs | x >= 0x60 && x <= 0x7f =
    let n   = x - 0x60 + 1
        xs'' = case xs of
          ConcreteBuffer xs' -> num $ EVM.Concrete.readMemoryWord 0 $ BS.take (num n) xs'
          SymbolicBuffer xs' -> readSWord' 0 $ take (num n) xs'
    in OpPush xs''
  readOp x _ = case x of
    0x00 -> OpStop
    0x01 -> OpAdd
    0x02 -> OpMul
    0x03 -> OpSub
    0x04 -> OpDiv
    0x05 -> OpSdiv
    0x06 -> OpMod
    0x07 -> OpSmod
    0x08 -> OpAddmod
    0x09 -> OpMulmod
    0x0a -> OpExp
    0x0b -> OpSignextend
    0x10 -> OpLt
    0x11 -> OpGt
    0x12 -> OpSlt
    0x13 -> OpSgt
    0x14 -> OpEq
    0x15 -> OpIszero
    0x16 -> OpAnd
    0x17 -> OpOr
    0x18 -> OpXor
    0x19 -> OpNot
    0x1a -> OpByte
    0x1b -> OpShl
    0x1c -> OpShr
    0x1d -> OpSar
    0x20 -> OpSha3
    0x30 -> OpAddress
    0x31 -> OpBalance
    0x32 -> OpOrigin
    0x33 -> OpCaller
    0x34 -> OpCallvalue
    0x35 -> OpCalldataload
    0x36 -> OpCalldatasize
    0x37 -> OpCalldatacopy
    0x38 -> OpCodesize
    0x39 -> OpCodecopy
    0x3a -> OpGasprice
    0x3b -> OpExtcodesize
    0x3c -> OpExtcodecopy
    0x3d -> OpReturndatasize
    0x3e -> OpReturndatacopy
    0x3f -> OpExtcodehash
    0x40 -> OpBlockhash
    0x41 -> OpCoinbase
    0x42 -> OpTimestamp
    0x43 -> OpNumber
    0x44 -> OpDifficulty
    0x45 -> OpGaslimit
    0x46 -> OpChainid
    0x47 -> OpSelfbalance
    0x50 -> OpPop
    0x51 -> OpMload
    0x52 -> OpMstore
    0x53 -> OpMstore8
    0x54 -> OpSload
    0x55 -> OpSstore
    0x56 -> OpJump
    0x57 -> OpJumpi
    0x58 -> OpPc
    0x59 -> OpMsize
    0x5a -> OpGas
    0x5b -> OpJumpdest
    0xf0 -> OpCreate
    0xf1 -> OpCall
    0xf2 -> OpCallcode
    0xf3 -> OpReturn
    0xf4 -> OpDelegatecall
    0xf5 -> OpCreate2
    0xfd -> OpRevert
    0xfa -> OpStaticcall
    0xff -> OpSelfdestruct
    _    -> OpUnknown x
  
  mkCodeOps :: Buffer -> RegularVector.Vector (Int, Op)
  mkCodeOps (ConcreteBuffer bytes) = RegularVector.fromList . toList $ go 0 bytes
    where
      go !i !xs =
        case BS.uncons xs of
          Nothing ->
            mempty
          Just (x, xs') ->
            let j = opSize x
            in (i, readOp x (ConcreteBuffer xs')) Seq.<| go (i + j) (BS.drop j xs)
  mkCodeOps (SymbolicBuffer bytes) = RegularVector.fromList . toList $ go' 0 (stripBytecodeMetadataSym bytes)
    where
      go' !i !xs =
        case uncons xs of
          Nothing ->
            mempty
          Just (x, xs') ->
            let x' = fromSized $ fromMaybe (error "unexpected symbolic code argument") $ unliteral x
                j = opSize x'
            in (i, readOp x' (SymbolicBuffer xs')) Seq.<| go' (i + j) (drop j xs)
  
  -- * Gas cost calculation helpers
  
  -- Gas cost function for CALL, transliterated from the Yellow Paper.
  costOfCall
    :: FeeSchedule Integer
    -> Bool -> Word -> Word -> Word -> Addr
    -> EVM (Integer, Integer)
  costOfCall (FeeSchedule {..}) recipientExists xValue availableGas' xGas' target = do
    acc <- accessAccountForGas target
    let call_base_gas = if acc then g_warm_storage_read else g_cold_account_access
        availableGas = num availableGas'
        xGas = num xGas'
        c_new = if not recipientExists && xValue /= 0
              then num g_newaccount
              else 0
        c_xfer = if xValue /= 0  then num g_callvalue else 0
        c_extra = num 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 + num g_callstipend else c_gascap
    return (c_gascap + c_extra, c_callgas)
  
  -- Gas cost of create, including hash cost if needed
  costOfCreate
    :: FeeSchedule Integer
    -> Word -> Word -> (Integer, Integer)
  costOfCreate (FeeSchedule {..}) availableGas' hashSize =
    (createCost + initGas, initGas)
    where
      availableGas = num availableGas'
      createCost = g_create + hashCost
      hashCost   = g_sha3word * ceilDiv (num hashSize) 32
      initGas    = allButOne64th (availableGas - createCost)
  
  concreteModexpGasFee :: ByteString -> Integer
  concreteModexpGasFee input = max 200 ((multiplicationComplexity * iterCount) `div` 3)
    where (lenb, lene, lenm) = parseModexpLength input
          ez = isZero (96 + lenb) lene input
          e' = w256 $ word $ LS.toStrict $
            lazySlice (96 + lenb) (min 32 lene) input
          nwords :: Integer
          nwords = ceilDiv (num $ max lenb lenm) 8
          multiplicationComplexity = nwords * nwords
          iterCount' :: Integer
          iterCount' | lene <= 32 && ez = 0
                     | lene <= 32 = num (log2 e')
                     | e' == 0 = 8 * (num lene - 32)
                     | otherwise = num (log2 e') + 8 * (num lene - 32)
          iterCount = max iterCount' 1
  
  -- Gas cost of precompiles
  costOfPrecompile :: FeeSchedule Integer -> Addr -> Buffer -> Integer
  costOfPrecompile (FeeSchedule {..}) precompileAddr input =
    case precompileAddr of
      -- ECRECOVER
      0x1 -> 3000
      -- SHA2-256
      0x2 -> num $ (((len input + 31) `div` 32) * 12) + 60
      -- RIPEMD-160
      0x3 -> num $ (((len input + 31) `div` 32) * 120) + 600
      -- IDENTITY
      0x4 -> num $ (((len input + 31) `div` 32) * 3) + 15
      -- MODEXP
      0x5 -> concreteModexpGasFee input'
        where input' = case input of
                 SymbolicBuffer _ -> error "unsupported: symbolic MODEXP gas cost calc"
                 ConcreteBuffer b -> b
      -- ECADD
      0x6 -> g_ecadd
      -- ECMUL
      0x7 -> g_ecmul
      -- ECPAIRING
      0x8 -> num $ ((len input) `div` 192) * (num g_pairing_point) + (num g_pairing_base)
      -- BLAKE2
      0x9 -> let input' = case input of
                           SymbolicBuffer _ -> error "unsupported: symbolic BLAKE2B gas cost calc"
                           ConcreteBuffer b -> b
             in g_fround * (num $ asInteger $ lazySlice 0 4 input')
      _ -> error ("unimplemented precompiled contract " ++ show precompileAddr)
  
  -- Gas cost of memory expansion
  memoryCost :: FeeSchedule Integer -> Integer -> Integer
  memoryCost FeeSchedule{..} byteCount =
    let
      wordCount = ceilDiv byteCount 32
      linearCost = g_memory * wordCount
      quadraticCost = div (wordCount * wordCount) 512
    in
      linearCost + quadraticCost
  
  -- * Arithmetic
  
  ceilDiv :: (Num a, Integral a) => a -> a -> a
  ceilDiv m n = div (m + n - 1) n
  
  allButOne64th :: (Num a, Integral a) => a -> a
  allButOne64th n = n - div n 64
  
  log2 :: FiniteBits b => b -> Int
  log2 x = finiteBitSize x - 1 - countLeadingZeros x
  
  
  -- * Emacs setup
  
  -- Local Variables:
  -- outline-regexp: "-- \\*+\\|data \\|newtype \\|type \\| +-- op: "
  -- outline-heading-alist:
  --   (("-- *" . 1) ("data " . 2) ("newtype " . 2) ("type " . 2))
  -- compile-command: "make"
  -- End:
  