Safe Haskell	Safe-Inferred
Language	GHC2021

EVM

Contents

Data types
Data accessors
Data constructors
Opcode dispatch (exec1)
Opcode helper actions
How to finalize a transaction
Substate manipulation
Cheat codes
General call implementation ("delegateCall")
VM error implementation
Memory helpers
Tracing
Stack manipulation
Bytecode data functions
Gas cost calculation helpers
Arithmetic
Emacs setup

Synopsis

data Error
- = BalanceTooLow W256 W256
- | UnrecognizedOpcode Word8
- | SelfDestruction
- | StackUnderrun
- | BadJumpDestination
- | Revert (Expr Buf)
- | OutOfGas Word64 Word64
- | BadCheatCode (Maybe Word32)
- | StackLimitExceeded
- | IllegalOverflow
- | Query Query
- | Choose Choose
- | StateChangeWhileStatic
- | InvalidMemoryAccess
- | CallDepthLimitReached
- | MaxCodeSizeExceeded W256 W256
- | InvalidFormat
- | PrecompileFailure
- | forall a. UnexpectedSymbolicArg Int String [Expr a]
- | DeadPath
- | NotUnique (Expr EWord)
- | SMTTimeout
- | FFI [AbiValue]
- | NonceOverflow
data VMResult
- = VMFailure Error
- | VMSuccess (Expr Buf)
data VM = VM {
- _result :: Maybe VMResult
- _state :: FrameState
- _frames :: [Frame]
- _env :: Env
- _block :: Block
- _tx :: TxState
- _logs :: [Expr Log]
- _traces :: TreePos Empty Trace
- _cache :: Cache
- _burned :: Word64
- _iterations :: Map CodeLocation Int
- _constraints :: [Prop]
- _keccakEqs :: [Prop]
- _allowFFI :: Bool
}
data Trace = Trace {
- _traceOpIx :: Int
- _traceContract :: Contract
- _traceData :: TraceData
}
data TraceData
- = EventTrace (Expr EWord) (Expr Buf) [Expr EWord]
- | FrameTrace FrameContext
- | QueryTrace Query
- | ErrorTrace Error
- | EntryTrace Text
- | ReturnTrace (Expr Buf) FrameContext
data Query where
- PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query
- PleaseFetchSlot :: Addr -> W256 -> (W256 -> EVM ()) -> Query
- PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query
- PleaseDoFFI :: [String] -> (ByteString -> EVM ()) -> Query
data Choose where
- PleaseChoosePath :: Expr EWord -> (Bool -> EVM ()) -> Choose
type EVM a = State VM a
type CodeLocation = (Addr, Int)
data BranchCondition
- = Case Bool
- | Unknown
- | Inconsistent
data IsUnique a
- = Unique a
- | Multiple
- | InconsistentU
- | TimeoutU
data Cache = Cache {
- _fetchedContracts :: Map Addr Contract
- _fetchedStorage :: Map W256 (Map W256 W256)
- _path :: Map (CodeLocation, Int) Bool
}
data StorageBase
- = Concrete
- | Symbolic
data VMOpts = VMOpts {
- vmoptContract :: Contract
- vmoptCalldata :: (Expr Buf, [Prop])
- vmoptStorageBase :: StorageBase
- vmoptValue :: Expr EWord
- vmoptPriorityFee :: W256
- vmoptAddress :: Addr
- vmoptCaller :: Expr EWord
- vmoptOrigin :: Addr
- vmoptGas :: Word64
- vmoptGaslimit :: Word64
- vmoptNumber :: W256
- vmoptTimestamp :: Expr EWord
- vmoptCoinbase :: Addr
- vmoptPrevRandao :: W256
- vmoptMaxCodeSize :: W256
- vmoptBlockGaslimit :: Word64
- vmoptGasprice :: W256
- vmoptBaseFee :: W256
- vmoptSchedule :: FeeSchedule Word64
- vmoptChainId :: W256
- vmoptCreate :: Bool
- vmoptTxAccessList :: Map Addr [W256]
- vmoptAllowFFI :: Bool
}
data Frame = Frame {
- _frameContext :: FrameContext
- _frameState :: FrameState
}
data FrameContext
- = CreationContext {
  }
- | CallContext {
  - callContextTarget :: Addr
  - callContextContext :: Addr
  - callContextOffset :: W256
  - callContextSize :: W256
  - callContextCodehash :: Expr EWord
  - callContextAbi :: Maybe W256
  - callContextData :: Expr Buf
  - callContextReversion :: (Map Addr Contract, Expr Storage)
  - callContextSubState :: SubState
  }
data FrameState = FrameState {
- _contract :: Addr
- _codeContract :: Addr
- _code :: ContractCode
- _pc :: Int
- _stack :: [Expr EWord]
- _memory :: Expr Buf
- _memorySize :: Word64
- _calldata :: Expr Buf
- _callvalue :: Expr EWord
- _caller :: Expr EWord
- _gas :: Word64
- _returndata :: Expr Buf
- _static :: Bool
}
data TxState = TxState {
- _gasprice :: W256
- _txgaslimit :: Word64
- _txPriorityFee :: W256
- _origin :: Addr
- _toAddr :: Addr
- _value :: Expr EWord
- _substate :: SubState
- _isCreate :: Bool
- _txReversion :: Map Addr Contract
}
data SubState = SubState {
- _selfdestructs :: [Addr]
- _touchedAccounts :: [Addr]
- _accessedAddresses :: Set Addr
- _accessedStorageKeys :: Set (Addr, W256)
- _refunds :: [(Addr, Word64)]
}
data ContractCode
- = InitCode ByteString (Expr Buf)
- | RuntimeCode RuntimeCode
data RuntimeCode
- = ConcreteRuntimeCode ByteString
- | SymbolicRuntimeCode (Vector (Expr Byte))
data Contract = Contract {
- _contractcode :: ContractCode
- _balance :: W256
- _nonce :: W256
- _codehash :: Expr EWord
- _opIxMap :: Vector Int
- _codeOps :: Vector (Int, Op)
- _external :: Bool
}
data StorageModel
- = ConcreteS
- | SymbolicS
- | InitialS
data Env = Env {
- _contracts :: Map Addr Contract
- _chainId :: W256
- _storage :: Expr Storage
- _origStorage :: Map W256 (Map W256 W256)
- _sha3Crack :: Map W256 ByteString
}
data Block = Block {
- _coinbase :: Addr
- _timestamp :: Expr EWord
- _number :: W256
- _prevRandao :: W256
- _gaslimit :: Word64
- _baseFee :: W256
- _maxCodeSize :: W256
- _schedule :: FeeSchedule Word64
}
blankState :: FrameState
static :: Lens' FrameState Bool
stack :: Lens' FrameState [Expr 'EWord]
returndata :: Lens' FrameState (Expr 'Buf)
pc :: Lens' FrameState Int
memorySize :: Lens' FrameState Word64
memory :: Lens' FrameState (Expr 'Buf)
gas :: Lens' FrameState Word64
contract :: Lens' FrameState Addr
codeContract :: Lens' FrameState Addr
code :: Lens' FrameState ContractCode
callvalue :: Lens' FrameState (Expr 'EWord)
caller :: Lens' FrameState (Expr 'EWord)
calldata :: Lens' FrameState (Expr 'Buf)
frameState :: Lens' Frame FrameState
frameContext :: Lens' Frame FrameContext
timestamp :: Lens' Block (Expr 'EWord)
schedule :: Lens' Block (FeeSchedule Word64)
prevRandao :: Lens' Block W256
number :: Lens' Block W256
maxCodeSize :: Lens' Block W256
gaslimit :: Lens' Block Word64
coinbase :: Lens' Block Addr
baseFee :: Lens' Block W256
value :: Lens' TxState (Expr 'EWord)
txgaslimit :: Lens' TxState Word64
txReversion :: Lens' TxState (Map Addr Contract)
txPriorityFee :: Lens' TxState W256
toAddr :: Lens' TxState Addr
substate :: Lens' TxState SubState
origin :: Lens' TxState Addr
isCreate :: Lens' TxState Bool
gasprice :: Lens' TxState W256
touchedAccounts :: Lens' SubState [Addr]
selfdestructs :: Lens' SubState [Addr]
refunds :: Lens' SubState [(Addr, Word64)]
accessedStorageKeys :: Lens' SubState (Set (Addr, W256))
accessedAddresses :: Lens' SubState (Set Addr)
opIxMap :: Lens' Contract (Vector Int)
nonce :: Lens' Contract W256
external :: Lens' Contract Bool
contractcode :: Lens' Contract ContractCode
codehash :: Lens' Contract (Expr 'EWord)
codeOps :: Lens' Contract (Vector (Int, Op))
balance :: Lens' Contract W256
storage :: Lens' Env (Expr 'Storage)
sha3Crack :: Lens' Env (Map W256 ByteString)
origStorage :: Lens' Env (Map W256 (Map W256 W256))
contracts :: Lens' Env (Map Addr Contract)
chainId :: Lens' Env W256
path :: Lens' Cache (Map (CodeLocation, Int) Bool)
fetchedStorage :: Lens' Cache (Map W256 (Map W256 W256))
fetchedContracts :: Lens' Cache (Map Addr Contract)
traceOpIx :: Lens' Trace Int
traceData :: Lens' Trace TraceData
traceContract :: Lens' Trace Contract
tx :: Lens' VM TxState
traces :: Lens' VM (TreePos Empty Trace)
state :: Lens' VM FrameState
result :: Lens' VM (Maybe VMResult)
logs :: Lens' VM [Expr 'Log]
keccakEqs :: Lens' VM [Prop]
iterations :: Lens' VM (Map CodeLocation Int)
frames :: Lens' VM [Frame]
env :: Lens' VM Env
constraints :: Lens' VM [Prop]
cache :: Lens' VM Cache
burned :: Lens' VM Word64
block :: Lens' VM Block
allowFFI :: Lens' VM Bool
bytecode :: Getter Contract (Expr Buf)
unifyCachedStorage :: Map W256 W256 -> Map W256 W256 -> Map W256 W256
unifyCachedContract :: Contract -> Contract -> Contract
currentContract :: VM -> Maybe Contract
makeVm :: VMOpts -> VM
initialContract :: ContractCode -> Contract
next :: (?op :: Word8) => EVM ()
exec1 :: EVM ()
transfer :: Addr -> Addr -> W256 -> EVM ()
callChecks :: (?op :: Word8) => Contract -> Word64 -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> (Word64 -> EVM ()) -> EVM ()
precompiledContract :: (?op :: Word8) => Contract -> Word64 -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> EVM ()
executePrecompile :: (?op :: Word8) => Addr -> Word64 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> EVM ()
truncpadlit :: Int -> ByteString -> ByteString
lazySlice :: W256 -> W256 -> ByteString -> ByteString
parseModexpLength :: ByteString -> (W256, W256, W256)
isZero :: W256 -> W256 -> ByteString -> Bool
asInteger :: ByteString -> Integer
noop :: Monad m => m ()
pushTo :: MonadState s m => ASetter s s [a] [a] -> a -> m ()
pushToSequence :: MonadState s m => ASetter s s (Seq a) (Seq a) -> a -> m ()
getCodeLocation :: VM -> CodeLocation
branch :: CodeLocation -> Expr EWord -> (Bool -> EVM ()) -> EVM ()
fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM ()
accessStorage :: Addr -> Expr EWord -> (Expr EWord -> EVM ()) -> EVM ()
accountExists :: Addr -> VM -> Bool
accountEmpty :: Contract -> Bool
finalize :: EVM ()
loadContract :: Addr -> EVM ()
limitStack :: Int -> EVM () -> EVM ()
notStatic :: EVM () -> EVM ()
burn :: Word64 -> EVM () -> EVM ()
forceConcrete :: Expr EWord -> String -> (W256 -> EVM ()) -> EVM ()
forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM ()) -> EVM ()
forceConcrete3 :: (Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256) -> EVM ()) -> EVM ()
forceConcrete4 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256) -> EVM ()) -> EVM ()
forceConcrete5 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256) -> EVM ()) -> EVM ()
forceConcrete6 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256, W256) -> EVM ()) -> EVM ()
forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM ()) -> EVM ()
refund :: Word64 -> EVM ()
unRefund :: Word64 -> EVM ()
touchAccount :: Addr -> EVM ()
selfdestruct :: Addr -> EVM ()
accessAndBurn :: Addr -> EVM () -> EVM ()
accessAccountForGas :: Addr -> EVM Bool
accessStorageForGas :: Addr -> Expr EWord -> EVM Bool
cheatCode :: Addr
cheat :: (?op :: Word8) => (W256, W256) -> (W256, W256) -> EVM ()
type CheatAction = Expr EWord -> Expr EWord -> Expr Buf -> EVM ()
cheatActions :: Map Word32 CheatAction
ethsign :: PrivateKey -> Digest Keccak_256 -> Signature
delegateCall :: (?op :: Word8) => Contract -> Word64 -> Expr EWord -> Expr EWord -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> (Addr -> EVM ()) -> EVM ()
collision :: Maybe Contract -> Bool
create :: (?op :: Word8) => Addr -> Contract -> Word64 -> W256 -> [Expr EWord] -> Addr -> Expr Buf -> EVM ()
replaceCode :: Addr -> ContractCode -> EVM ()
replaceCodeOfSelf :: ContractCode -> EVM ()
resetState :: EVM ()
vmError :: Error -> EVM ()
underrun :: EVM ()
data FrameResult
- = FrameReturned (Expr Buf)
- | FrameReverted (Expr Buf)
- | FrameErrored Error
finishFrame :: FrameResult -> EVM ()
accessUnboundedMemoryRange :: FeeSchedule Word64 -> Word64 -> Word64 -> EVM () -> EVM ()
accessMemoryRange :: FeeSchedule Word64 -> W256 -> W256 -> EVM () -> EVM ()
accessMemoryWord :: FeeSchedule Word64 -> W256 -> EVM () -> EVM ()
copyBytesToMemory :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM ()
copyCallBytesToMemory :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM ()
readMemory :: Expr EWord -> Expr EWord -> VM -> Expr Buf
withTraceLocation :: MonadState VM m => TraceData -> m Trace
pushTrace :: TraceData -> EVM ()
insertTrace :: TraceData -> EVM ()
popTrace :: EVM ()
zipperRootForest :: TreePos Empty a -> Forest a
traceForest :: VM -> Forest Trace
traceTopLog :: MonadState VM m => [Expr Log] -> m ()
push :: W256 -> EVM ()
pushSym :: Expr EWord -> EVM ()
stackOp1 :: (?op :: Word8) => (Expr EWord -> Word64) -> (Expr EWord -> Expr EWord) -> EVM ()
stackOp2 :: (?op :: Word8) => ((Expr EWord, Expr EWord) -> Word64) -> ((Expr EWord, Expr EWord) -> Expr EWord) -> EVM ()
stackOp3 :: (?op :: Word8) => ((Expr EWord, Expr EWord, Expr EWord) -> Word64) -> ((Expr EWord, Expr EWord, Expr EWord) -> Expr EWord) -> EVM ()
checkJump :: Int -> [Expr EWord] -> EVM ()
opSize :: Word8 -> Int
mkOpIxMap :: ContractCode -> Vector Int
vmOp :: VM -> Maybe Op
vmOpIx :: VM -> Maybe Int
opParams :: VM -> Map String (Expr EWord)
readOp :: Word8 -> [Expr Byte] -> Op
mkCodeOps :: ContractCode -> Vector (Int, Op)
costOfCall :: FeeSchedule Word64 -> Bool -> W256 -> Word64 -> Word64 -> Addr -> EVM (Word64, Word64)
costOfCreate :: FeeSchedule Word64 -> Word64 -> W256 -> (Word64, Word64)
concreteModexpGasFee :: ByteString -> Word64
costOfPrecompile :: FeeSchedule Word64 -> Addr -> Expr Buf -> Word64
memoryCost :: FeeSchedule Word64 -> Word64 -> Word64
ceilDiv :: (Num a, Integral a) => a -> a -> a
allButOne64th :: (Num a, Integral a) => a -> a
log2 :: FiniteBits b => b -> Int
hashcode :: ContractCode -> Expr EWord
opslen :: ContractCode -> Int
codelen :: ContractCode -> Expr EWord
toBuf :: ContractCode -> Expr Buf
codeloc :: EVM CodeLocation

Data types

data Error Source #

EVM failure modes

Instances

Instances details

Show Error Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #

data VMResult Source #

The possible result states of a VM

Constructors

VMFailure Error	An operation failed
VMSuccess (Expr Buf)	Reached STOP, RETURN, or end-of-code

Instances

Instances details

Show VMResult Source #
Instance details Defined in EVM Methods showsPrec :: Int -> VMResult -> ShowS # show :: VMResult -> String # showList :: [VMResult] -> ShowS #

data VM Source #

The state of a stepwise EVM execution

Constructors

VM
Fields _result :: Maybe VMResult _state :: FrameState _frames :: [Frame] _env :: Env _block :: Block _tx :: TxState _logs :: [Expr Log] _traces :: TreePos Empty Trace _cache :: Cache _burned :: Word64 _iterations :: Map CodeLocation Int _constraints :: [Prop] _keccakEqs :: [Prop] _allowFFI :: Bool

Instances

Instances details

Show VM Source #
Instance details Defined in EVM Methods showsPrec :: Int -> VM -> ShowS # show :: VM -> String # showList :: [VM] -> ShowS #

data Trace Source #

Constructors

Trace
Fields _traceOpIx :: Int _traceContract :: Contract _traceData :: TraceData

Instances

Instances details

Show Trace Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Trace -> ShowS # show :: Trace -> String # showList :: [Trace] -> ShowS #

data TraceData Source #

Constructors

EventTrace (Expr EWord) (Expr Buf) [Expr EWord]
FrameTrace FrameContext
QueryTrace Query
ErrorTrace Error
EntryTrace Text
ReturnTrace (Expr Buf) FrameContext

Instances

Instances details

Show TraceData Source #
Instance details Defined in EVM Methods showsPrec :: Int -> TraceData -> ShowS # show :: TraceData -> String # showList :: [TraceData] -> ShowS #

data Query where Source #

Queries halt execution until resolved through RPC calls or SMT queries

Constructors

PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query
PleaseFetchSlot :: Addr -> W256 -> (W256 -> EVM ()) -> Query
PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query
PleaseDoFFI :: [String] -> (ByteString -> EVM ()) -> Query

Instances

Instances details

Show Query Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Query -> ShowS # show :: Query -> String # showList :: [Query] -> ShowS #

data Choose where Source #

Constructors

PleaseChoosePath :: Expr EWord -> (Bool -> EVM ()) -> Choose

Instances

Instances details

Show Choose Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Choose -> ShowS # show :: Choose -> String # showList :: [Choose] -> ShowS #

type EVM a = State VM a Source #

Alias for the type of e.g. exec1.

type CodeLocation = (Addr, Int) Source #

data BranchCondition Source #

The possible return values of a SMT query

Constructors

Case Bool
Unknown
Inconsistent

Instances

Instances details

Show BranchCondition Source #
Instance details Defined in EVM Methods showsPrec :: Int -> BranchCondition -> ShowS # show :: BranchCondition -> String # showList :: [BranchCondition] -> ShowS #

data IsUnique a Source #

The possible return values of a `is unique` SMT query

Constructors

Unique a
Multiple
InconsistentU
TimeoutU

Instances

Instances details

Show a => Show (IsUnique a) Source #
Instance details Defined in EVM Methods showsPrec :: Int -> IsUnique a -> ShowS # show :: IsUnique a -> String # showList :: [IsUnique a] -> ShowS #

data Cache Source #

The cache is data that can be persisted for efficiency: any expensive query that is constant at least within a block.

Constructors

Cache
Fields _fetchedContracts :: Map Addr Contract _fetchedStorage :: Map W256 (Map W256 W256) _path :: Map (CodeLocation, Int) Bool

Instances

Instances details

Monoid Cache Source #
Instance details Defined in EVM Methods mempty :: Cache # mappend :: Cache -> Cache -> Cache # mconcat :: [Cache] -> Cache #
Semigroup Cache Source #
Instance details Defined in EVM Methods (<>) :: Cache -> Cache -> Cache # sconcat :: NonEmpty Cache -> Cache # stimes :: Integral b => b -> Cache -> Cache #
Show Cache Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Cache -> ShowS # show :: Cache -> String # showList :: [Cache] -> ShowS #

data StorageBase Source #

Constructors

Concrete
Symbolic

Instances

Instances details

Show StorageBase Source #
Instance details Defined in EVM Methods showsPrec :: Int -> StorageBase -> ShowS # show :: StorageBase -> String # showList :: [StorageBase] -> ShowS #
Eq StorageBase Source #
Instance details Defined in EVM Methods (==) :: StorageBase -> StorageBase -> Bool # (/=) :: StorageBase -> StorageBase -> Bool #

data VMOpts Source #

A way to specify an initial VM state

Constructors

VMOpts

Fields

vmoptContract :: Contract
vmoptCalldata :: (Expr Buf, [Prop])
vmoptStorageBase :: StorageBase
vmoptValue :: Expr EWord
vmoptPriorityFee :: W256
vmoptAddress :: Addr
vmoptCaller :: Expr EWord
vmoptOrigin :: Addr
vmoptGas :: Word64
vmoptGaslimit :: Word64
vmoptNumber :: W256
vmoptTimestamp :: Expr EWord
vmoptCoinbase :: Addr
vmoptPrevRandao :: W256
vmoptMaxCodeSize :: W256
vmoptBlockGaslimit :: Word64
vmoptGasprice :: W256
vmoptBaseFee :: W256
vmoptSchedule :: FeeSchedule Word64
vmoptChainId :: W256
vmoptCreate :: Bool
vmoptTxAccessList :: Map Addr [W256]
vmoptAllowFFI :: Bool

Instances

Instances details

Show VMOpts Source #
Instance details Defined in EVM Methods showsPrec :: Int -> VMOpts -> ShowS # show :: VMOpts -> String # showList :: [VMOpts] -> ShowS #

data Frame Source #

An entry in the VM's "call/create stack"

Constructors

Frame
Fields _frameContext :: FrameContext _frameState :: FrameState

Instances

Instances details

Show Frame Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Frame -> ShowS # show :: Frame -> String # showList :: [Frame] -> ShowS #

data FrameContext Source #

Call/create info

Constructors

CreationContext
Fields creationContextAddress :: Addr creationContextCodehash :: Expr EWord creationContextReversion :: Map Addr Contract creationContextSubstate :: SubState
CallContext
Fields callContextTarget :: Addr callContextContext :: Addr callContextOffset :: W256 callContextSize :: W256 callContextCodehash :: Expr EWord callContextAbi :: Maybe W256 callContextData :: Expr Buf callContextReversion :: (Map Addr Contract, Expr Storage) callContextSubState :: SubState

Instances

Instances details

Show FrameContext Source #
Instance details Defined in EVM Methods showsPrec :: Int -> FrameContext -> ShowS # show :: FrameContext -> String # showList :: [FrameContext] -> ShowS #

data FrameState Source #

The "registers" of the VM along with memory and data stack

Constructors

FrameState
Fields _contract :: Addr _codeContract :: Addr _code :: ContractCode _pc :: Int _stack :: [Expr EWord] _memory :: Expr Buf _memorySize :: Word64 _calldata :: Expr Buf _callvalue :: Expr EWord _caller :: Expr EWord _gas :: Word64 _returndata :: Expr Buf _static :: Bool

Instances

Instances details

Show FrameState Source #
Instance details Defined in EVM Methods showsPrec :: Int -> FrameState -> ShowS # show :: FrameState -> String # showList :: [FrameState] -> ShowS #

data TxState Source #

The state that spans a whole transaction

Constructors

TxState
Fields _gasprice :: W256 _txgaslimit :: Word64 _txPriorityFee :: W256 _origin :: Addr _toAddr :: Addr _value :: Expr EWord _substate :: SubState _isCreate :: Bool _txReversion :: Map Addr Contract

Instances

Instances details

Show TxState Source #
Instance details Defined in EVM Methods showsPrec :: Int -> TxState -> ShowS # show :: TxState -> String # showList :: [TxState] -> ShowS #

data SubState Source #

The "accrued substate" across a transaction

Constructors

SubState
Fields _selfdestructs :: [Addr] _touchedAccounts :: [Addr] _accessedAddresses :: Set Addr _accessedStorageKeys :: Set (Addr, W256) _refunds :: [(Addr, Word64)]

Instances

Instances details

Show SubState Source #
Instance details Defined in EVM Methods showsPrec :: Int -> SubState -> ShowS # show :: SubState -> String # showList :: [SubState] -> ShowS #

data ContractCode Source #

A contract is either in creation (running its "constructor") or post-creation, and code in these two modes is treated differently by instructions like EXTCODEHASH, so we distinguish these two code types.

The definition follows the structure of code output by solc. We need to use some heuristics here to deal with symbolic data regions that may be present in the bytecode since the fully abstract case is impractical:

initcode has concrete code, followed by an abstract data "section"
runtimecode has a fixed length, but may contain fixed size symbolic regions (due to immutable)

hopefully we do not have to deal with dynamic immutable before we get a real data section...

Constructors

InitCode ByteString (Expr Buf)	Constructor code, during contract creation
RuntimeCode RuntimeCode	Instance code, after contract creation

Instances

Instances details

Show ContractCode Source #
Instance details Defined in EVM Methods showsPrec :: Int -> ContractCode -> ShowS # show :: ContractCode -> String # showList :: [ContractCode] -> ShowS #
Eq ContractCode Source #
Instance details Defined in EVM Methods (==) :: ContractCode -> ContractCode -> Bool # (/=) :: ContractCode -> ContractCode -> Bool #
Ord ContractCode Source #
Instance details Defined in EVM Methods compare :: ContractCode -> ContractCode -> Ordering # (<) :: ContractCode -> ContractCode -> Bool # (<=) :: ContractCode -> ContractCode -> Bool # (>) :: ContractCode -> ContractCode -> Bool # (>=) :: ContractCode -> ContractCode -> Bool # max :: ContractCode -> ContractCode -> ContractCode # min :: ContractCode -> ContractCode -> ContractCode #

data RuntimeCode Source #

We have two variants here to optimize the fully concrete case. ConcreteRuntimeCode just wraps a ByteString SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).

Constructors

ConcreteRuntimeCode ByteString
SymbolicRuntimeCode (Vector (Expr Byte))

Instances

Instances details

Show RuntimeCode Source #
Instance details Defined in EVM Methods showsPrec :: Int -> RuntimeCode -> ShowS # show :: RuntimeCode -> String # showList :: [RuntimeCode] -> ShowS #
Eq RuntimeCode Source #
Instance details Defined in EVM Methods (==) :: RuntimeCode -> RuntimeCode -> Bool # (/=) :: RuntimeCode -> RuntimeCode -> Bool #
Ord RuntimeCode Source #
Instance details Defined in EVM Methods compare :: RuntimeCode -> RuntimeCode -> Ordering # (<) :: RuntimeCode -> RuntimeCode -> Bool # (<=) :: RuntimeCode -> RuntimeCode -> Bool # (>) :: RuntimeCode -> RuntimeCode -> Bool # (>=) :: RuntimeCode -> RuntimeCode -> Bool # max :: RuntimeCode -> RuntimeCode -> RuntimeCode # min :: RuntimeCode -> RuntimeCode -> RuntimeCode #

data Contract Source #

A contract can either have concrete or symbolic storage depending on what type of execution we are doing data Storage = Concrete (Map Word Expr EWord) | Symbolic [(Expr EWord, Expr EWord)] (SArray (WordN 256) (WordN 256)) deriving (Show)

The state of a contract

Constructors

Contract
Fields _contractcode :: ContractCode _balance :: W256 _nonce :: W256 _codehash :: Expr EWord _opIxMap :: Vector Int _codeOps :: Vector (Int, Op) _external :: Bool

Instances

Instances details

Show Contract Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Contract -> ShowS # show :: Contract -> String # showList :: [Contract] -> ShowS #

data StorageModel Source #

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.

Constructors

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.

Instances

Instances details

Read StorageModel Source #
Instance details Defined in EVM Methods readsPrec :: Int -> ReadS StorageModel # readList :: ReadS [StorageModel] # readPrec :: ReadPrec StorageModel # readListPrec :: ReadPrec [StorageModel] #
Show StorageModel Source #
Instance details Defined in EVM Methods showsPrec :: Int -> StorageModel -> ShowS # show :: StorageModel -> String # showList :: [StorageModel] -> ShowS #
ParseField StorageModel Source #
Instance details Defined in EVM Methods parseField :: Maybe Text -> Maybe Text -> Maybe Char -> Maybe String -> Parser StorageModel # parseListOfField :: Maybe Text -> Maybe Text -> Maybe Char -> Maybe String -> Parser [StorageModel] # readField :: ReadM StorageModel # metavar :: proxy StorageModel -> String #

data Env Source #

Various environmental data

Constructors

Env
Fields _contracts :: Map Addr Contract _chainId :: W256 _storage :: Expr Storage _origStorage :: Map W256 (Map W256 W256) _sha3Crack :: Map W256 ByteString

Instances

Instances details

Show Env Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Env -> ShowS # show :: Env -> String # showList :: [Env] -> ShowS #

data Block Source #

Data about the block

Constructors

Block
Fields _coinbase :: Addr _timestamp :: Expr EWord _number :: W256 _prevRandao :: W256 _gaslimit :: Word64 _baseFee :: W256 _maxCodeSize :: W256 _schedule :: FeeSchedule Word64

Instances

Instances details

Show Block Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Block -> ShowS # show :: Block -> String # showList :: [Block] -> ShowS #

blankState :: FrameState Source #

static :: Lens' FrameState Bool Source #

stack :: Lens' FrameState [Expr 'EWord] Source #

returndata :: Lens' FrameState (Expr 'Buf) Source #

pc :: Lens' FrameState Int Source #

memorySize :: Lens' FrameState Word64 Source #

memory :: Lens' FrameState (Expr 'Buf) Source #

gas :: Lens' FrameState Word64 Source #

contract :: Lens' FrameState Addr Source #

codeContract :: Lens' FrameState Addr Source #

code :: Lens' FrameState ContractCode Source #

callvalue :: Lens' FrameState (Expr 'EWord) Source #

caller :: Lens' FrameState (Expr 'EWord) Source #

calldata :: Lens' FrameState (Expr 'Buf) Source #

frameState :: Lens' Frame FrameState Source #

frameContext :: Lens' Frame FrameContext Source #

timestamp :: Lens' Block (Expr 'EWord) Source #

schedule :: Lens' Block (FeeSchedule Word64) Source #

prevRandao :: Lens' Block W256 Source #

number :: Lens' Block W256 Source #

maxCodeSize :: Lens' Block W256 Source #

gaslimit :: Lens' Block Word64 Source #

coinbase :: Lens' Block Addr Source #

baseFee :: Lens' Block W256 Source #

value :: Lens' TxState (Expr 'EWord) Source #

txgaslimit :: Lens' TxState Word64 Source #

txReversion :: Lens' TxState (Map Addr Contract) Source #

txPriorityFee :: Lens' TxState W256 Source #

toAddr :: Lens' TxState Addr Source #

substate :: Lens' TxState SubState Source #

origin :: Lens' TxState Addr Source #

isCreate :: Lens' TxState Bool Source #

gasprice :: Lens' TxState W256 Source #

touchedAccounts :: Lens' SubState [Addr] Source #

selfdestructs :: Lens' SubState [Addr] Source #

refunds :: Lens' SubState [(Addr, Word64)] Source #

accessedStorageKeys :: Lens' SubState (Set (Addr, W256)) Source #

accessedAddresses :: Lens' SubState (Set Addr) Source #

opIxMap :: Lens' Contract (Vector Int) Source #

nonce :: Lens' Contract W256 Source #

external :: Lens' Contract Bool Source #

contractcode :: Lens' Contract ContractCode Source #

codehash :: Lens' Contract (Expr 'EWord) Source #

codeOps :: Lens' Contract (Vector (Int, Op)) Source #

balance :: Lens' Contract W256 Source #

storage :: Lens' Env (Expr 'Storage) Source #

sha3Crack :: Lens' Env (Map W256 ByteString) Source #

origStorage :: Lens' Env (Map W256 (Map W256 W256)) Source #

contracts :: Lens' Env (Map Addr Contract) Source #

chainId :: Lens' Env W256 Source #

path :: Lens' Cache (Map (CodeLocation, Int) Bool) Source #

fetchedStorage :: Lens' Cache (Map W256 (Map W256 W256)) Source #

fetchedContracts :: Lens' Cache (Map Addr Contract) Source #

traceOpIx :: Lens' Trace Int Source #

traceData :: Lens' Trace TraceData Source #

traceContract :: Lens' Trace Contract Source #

tx :: Lens' VM TxState Source #

traces :: Lens' VM (TreePos Empty Trace) Source #

state :: Lens' VM FrameState Source #

result :: Lens' VM (Maybe VMResult) Source #

logs :: Lens' VM [Expr 'Log] Source #

keccakEqs :: Lens' VM [Prop] Source #

iterations :: Lens' VM (Map CodeLocation Int) Source #

frames :: Lens' VM [Frame] Source #

env :: Lens' VM Env Source #

constraints :: Lens' VM [Prop] Source #

cache :: Lens' VM Cache Source #

burned :: Lens' VM Word64 Source #

block :: Lens' VM Block Source #

allowFFI :: Lens' VM Bool Source #

bytecode :: Getter Contract (Expr Buf) Source #

An "external" view of a contract's bytecode, appropriate for e.g. EXTCODEHASH.

unifyCachedStorage :: Map W256 W256 -> Map W256 W256 -> Map W256 W256 Source #

unifyCachedContract :: Contract -> Contract -> Contract Source #

Data accessors

currentContract :: VM -> Maybe Contract Source #

Data constructors

makeVm :: VMOpts -> VM Source #

initialContract :: ContractCode -> Contract Source #

Initialize empty contract with given code

Opcode dispatch (exec1)

next :: (?op :: Word8) => EVM () Source #

Update program counter

exec1 :: EVM () Source #

Executes the EVM one step

transfer :: Addr -> Addr -> W256 -> EVM () Source #

callChecks :: (?op :: Word8) => Contract -> Word64 -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> (Word64 -> EVM ()) -> EVM () Source #

Checks a *CALL for failure; OOG, too many callframes, memory access etc.

precompiledContract :: (?op :: Word8) => Contract -> Word64 -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> EVM () Source #

executePrecompile :: (?op :: Word8) => Addr -> Word64 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> EVM () Source #

truncpadlit :: Int -> ByteString -> ByteString Source #

lazySlice :: W256 -> W256 -> ByteString -> ByteString Source #

parseModexpLength :: ByteString -> (W256, W256, W256) Source #

isZero :: W256 -> W256 -> ByteString -> Bool Source #

asInteger :: ByteString -> Integer Source #

Opcode helper actions

noop :: Monad m => m () Source #

pushTo :: MonadState s m => ASetter s s [a] [a] -> a -> m () Source #

pushToSequence :: MonadState s m => ASetter s s (Seq a) (Seq a) -> a -> m () Source #

getCodeLocation :: VM -> CodeLocation Source #

branch :: CodeLocation -> Expr EWord -> (Bool -> EVM ()) -> EVM () Source #

fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM () Source #

Construct RPC Query and halt execution until resolved

accessStorage Source #

Arguments

:: Addr	Contract address
-> Expr EWord	Storage slot key
-> (Expr EWord -> EVM ())	Continuation
-> EVM ()

accountExists :: Addr -> VM -> Bool Source #

accountEmpty :: Contract -> Bool Source #

How to finalize a transaction

finalize :: EVM () Source #

loadContract :: Addr -> EVM () Source #

Loads the selected contract as the current contract to execute

limitStack :: Int -> EVM () -> EVM () Source #

notStatic :: EVM () -> EVM () Source #

burn :: Word64 -> EVM () -> EVM () Source #

Burn gas, failing if insufficient gas is available

forceConcrete :: Expr EWord -> String -> (W256 -> EVM ()) -> EVM () Source #

forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM ()) -> EVM () Source #

forceConcrete3 :: (Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256) -> EVM ()) -> EVM () Source #

forceConcrete4 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256) -> EVM ()) -> EVM () Source #

forceConcrete5 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256) -> EVM ()) -> EVM () Source #

forceConcrete6 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256, W256) -> EVM ()) -> EVM () Source #

forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM ()) -> EVM () Source #

Substate manipulation

refund :: Word64 -> EVM () Source #

unRefund :: Word64 -> EVM () Source #

touchAccount :: Addr -> EVM () Source #

selfdestruct :: Addr -> EVM () Source #

accessAndBurn :: Addr -> EVM () -> EVM () Source #

accessAccountForGas :: Addr -> EVM Bool Source #

returns a wrapped boolean- if true, this address has been touched before in the txn (warm gas cost as in EIP 2929) otherwise cold

accessStorageForGas :: Addr -> Expr EWord -> EVM Bool Source #

returns a wrapped boolean- if true, this slot has been touched before in the txn (warm gas cost as in EIP 2929) otherwise cold

Cheat codes

cheatCode :: Addr Source #

cheat :: (?op :: Word8) => (W256, W256) -> (W256, W256) -> EVM () Source #

type CheatAction = Expr EWord -> Expr EWord -> Expr Buf -> EVM () Source #

cheatActions :: Map Word32 CheatAction Source #

ethsign :: PrivateKey -> Digest Keccak_256 -> Signature Source #

We don't wanna introduce the machinery needed to sign with a random nonce, so we just use the same nonce every time (420). This is obviusly very insecure, but fine for testing purposes.

General call implementation ("delegateCall")

delegateCall :: (?op :: Word8) => Contract -> Word64 -> Expr EWord -> Expr EWord -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> (Addr -> EVM ()) -> EVM () Source #

collision :: Maybe Contract -> Bool Source #

create :: (?op :: Word8) => Addr -> Contract -> Word64 -> W256 -> [Expr EWord] -> Addr -> Expr Buf -> EVM () Source #

replaceCode :: Addr -> ContractCode -> EVM () Source #

Replace a contract's code, like when CREATE returns from the constructor code.

replaceCodeOfSelf :: ContractCode -> EVM () Source #

resetState :: EVM () Source #

VM error implementation

vmError :: Error -> EVM () Source #

underrun :: EVM () Source #

data FrameResult Source #

A stack frame can be popped in three ways.

Constructors

FrameReturned (Expr Buf)	STOP, RETURN, or no more code
FrameReverted (Expr Buf)	REVERT
FrameErrored Error	Any other error

Instances

Instances details

Show FrameResult Source #
Instance details Defined in EVM Methods showsPrec :: Int -> FrameResult -> ShowS # show :: FrameResult -> String # showList :: [FrameResult] -> ShowS #

finishFrame :: FrameResult -> EVM () Source #

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.

Memory helpers

accessUnboundedMemoryRange :: FeeSchedule Word64 -> Word64 -> Word64 -> EVM () -> EVM () Source #

accessMemoryRange :: FeeSchedule Word64 -> W256 -> W256 -> EVM () -> EVM () Source #

accessMemoryWord :: FeeSchedule Word64 -> W256 -> EVM () -> EVM () Source #

copyBytesToMemory :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM () Source #

copyCallBytesToMemory :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM () Source #

readMemory :: Expr EWord -> Expr EWord -> VM -> Expr Buf Source #

Tracing

withTraceLocation :: MonadState VM m => TraceData -> m Trace Source #

pushTrace :: TraceData -> EVM () Source #

insertTrace :: TraceData -> EVM () Source #

popTrace :: EVM () Source #

zipperRootForest :: TreePos Empty a -> Forest a Source #

traceForest :: VM -> Forest Trace Source #

traceTopLog :: MonadState VM m => [Expr Log] -> m () Source #

Stack manipulation

push :: W256 -> EVM () Source #

pushSym :: Expr EWord -> EVM () Source #

stackOp1 :: (?op :: Word8) => (Expr EWord -> Word64) -> (Expr EWord -> Expr EWord) -> EVM () Source #

stackOp2 :: (?op :: Word8) => ((Expr EWord, Expr EWord) -> Word64) -> ((Expr EWord, Expr EWord) -> Expr EWord) -> EVM () Source #

stackOp3 :: (?op :: Word8) => ((Expr EWord, Expr EWord, Expr EWord) -> Word64) -> ((Expr EWord, Expr EWord, Expr EWord) -> Expr EWord) -> EVM () Source #

Bytecode data functions

checkJump :: Int -> [Expr EWord] -> EVM () Source #

opSize :: Word8 -> Int Source #

mkOpIxMap :: ContractCode -> Vector Int Source #

vmOp :: VM -> Maybe Op Source #

vmOpIx :: VM -> Maybe Int Source #

opParams :: VM -> Map String (Expr EWord) Source #

readOp :: Word8 -> [Expr Byte] -> Op Source #

Reads

mkCodeOps :: ContractCode -> Vector (Int, Op) Source #

Gas cost calculation helpers

costOfCall :: FeeSchedule Word64 -> Bool -> W256 -> Word64 -> Word64 -> Addr -> EVM (Word64, Word64) Source #

costOfCreate :: FeeSchedule Word64 -> Word64 -> W256 -> (Word64, Word64) Source #

concreteModexpGasFee :: ByteString -> Word64 Source #

costOfPrecompile :: FeeSchedule Word64 -> Addr -> Expr Buf -> Word64 Source #

memoryCost :: FeeSchedule Word64 -> Word64 -> Word64 Source #

Arithmetic

ceilDiv :: (Num a, Integral a) => a -> a -> a Source #

allButOne64th :: (Num a, Integral a) => a -> a Source #

log2 :: FiniteBits b => b -> Int Source #

hashcode :: ContractCode -> Expr EWord Source #

opslen :: ContractCode -> Int Source #

The length of the code ignoring any constructor args. This represents the region that can contain executable opcodes

codelen :: ContractCode -> Expr EWord Source #

The length of the code including any constructor args. This can return an abstract value

toBuf :: ContractCode -> Expr Buf Source #

codeloc :: EVM CodeLocation Source #

BalanceTooLow W256 W256
UnrecognizedOpcode Word8
SelfDestruction
StackUnderrun
BadJumpDestination
Revert (Expr Buf)
OutOfGas Word64 Word64
BadCheatCode (Maybe Word32)
StackLimitExceeded
IllegalOverflow
Query Query
Choose Choose
StateChangeWhileStatic
InvalidMemoryAccess
CallDepthLimitReached
MaxCodeSizeExceeded W256 W256
InvalidFormat
PrecompileFailure
forall a. UnexpectedSymbolicArg Int String [Expr a]
DeadPath
NotUnique (Expr EWord)
SMTTimeout
FFI [AbiValue]
NonceOverflow

Data types

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Data accessors

Data constructors

Opcode dispatch (exec1)

Opcode helper actions

How to finalize a transaction

Substate manipulation

Cheat codes

General call implementation ("delegateCall")

VM error implementation

Instances

Memory helpers

Tracing

Stack manipulation

Bytecode data functions

Gas cost calculation helpers

Arithmetic

Emacs setup