Safe Haskell	None
Language	Haskell2010

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 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
data VMResult
- = VMFailure Error
- | VMSuccess Buffer
data VM = VM {
- _result :: Maybe VMResult
- _state :: FrameState
- _frames :: [Frame]
- _env :: Env
- _block :: Block
- _tx :: TxState
- _logs :: Seq Log
- _traces :: TreePos Empty Trace
- _cache :: Cache
- _burned :: Word
- _constraints :: [(SBool, Whiff)]
- _iterations :: Map CodeLocation Int
- _allowFFI :: Bool
}
data Trace = Trace {
- _traceOpIx :: Int
- _traceContract :: Contract
- _traceData :: TraceData
}
data TraceData
- = EventTrace Log
- | FrameTrace FrameContext
- | QueryTrace Query
- | ErrorTrace Error
- | EntryTrace Text
- | ReturnTrace Buffer FrameContext
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
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 {
- _fetched :: Map Addr Contract
- _path :: Map (CodeLocation, Int) Bool
}
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
}
data Log = Log Addr Buffer [SymWord]
data Frame = Frame {
- _frameContext :: FrameContext
- _frameState :: FrameState
}
data FrameContext
- = CreationContext {
  }
- | CallContext {
  - callContextTarget :: Addr
  - callContextContext :: Addr
  - callContextOffset :: Word
  - callContextSize :: Word
  - callContextCodehash :: W256
  - callContextAbi :: Maybe Word
  - callContextData :: Buffer
  - callContextReversion :: Map Addr Contract
  - callContextSubState :: SubState
  }
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
}
data TxState = TxState {
- _gasprice :: Word
- _txgaslimit :: Word
- _txPriorityFee :: Word
- _origin :: Addr
- _toAddr :: Addr
- _value :: SymWord
- _substate :: SubState
- _isCreate :: Bool
- _txReversion :: Map Addr Contract
}
data SubState = SubState {
- _selfdestructs :: [Addr]
- _touchedAccounts :: [Addr]
- _accessedAddresses :: Set Addr
- _accessedStorageKeys :: Set (Addr, W256)
- _refunds :: [(Addr, Integer)]
}
data ContractCode
- = InitCode Buffer
- | RuntimeCode Buffer
data Storage
- = Concrete (Map Word SymWord)
- | Symbolic [(SymWord, SymWord)] (SArray (WordN 256) (WordN 256))
data Contract = Contract {
- _contractcode :: ContractCode
- _storage :: Storage
- _balance :: Word
- _nonce :: Word
- _codehash :: W256
- _opIxMap :: Vector Int
- _codeOps :: Vector (Int, Op)
- _external :: Bool
- _origStorage :: Map Word Word
}
data StorageModel
- = ConcreteS
- | SymbolicS
- | InitialS
data Env = Env {
- _contracts :: Map Addr Contract
- _chainId :: Word
- _storageModel :: StorageModel
- _sha3Crack :: Map Word ByteString
- _keccakUsed :: [([SWord 8], SWord 256)]
}
data Block = Block {
- _coinbase :: Addr
- _timestamp :: SymWord
- _number :: Word
- _difficulty :: Word
- _gaslimit :: Word
- _baseFee :: Word
- _maxCodeSize :: Word
- _schedule :: FeeSchedule Integer
}
blankState :: FrameState
static :: Lens' FrameState Bool
stack :: Lens' FrameState [SymWord]
returndata :: Lens' FrameState Buffer
pc :: Lens' FrameState Int
memorySize :: Lens' FrameState Int
memory :: Lens' FrameState Buffer
gas :: Lens' FrameState Word
contract :: Lens' FrameState Addr
codeContract :: Lens' FrameState Addr
code :: Lens' FrameState Buffer
callvalue :: Lens' FrameState SymWord
caller :: Lens' FrameState SAddr
calldata :: Lens' FrameState (Buffer, SymWord)
frameState :: Lens' Frame FrameState
frameContext :: Lens' Frame FrameContext
timestamp :: Lens' Block SymWord
schedule :: Lens' Block (FeeSchedule Integer)
number :: Lens' Block Word
maxCodeSize :: Lens' Block Word
gaslimit :: Lens' Block Word
difficulty :: Lens' Block Word
coinbase :: Lens' Block Addr
baseFee :: Lens' Block Word
value :: Lens' TxState SymWord
txgaslimit :: Lens' TxState Word
txReversion :: Lens' TxState (Map Addr Contract)
txPriorityFee :: Lens' TxState Word
toAddr :: Lens' TxState Addr
substate :: Lens' TxState SubState
origin :: Lens' TxState Addr
isCreate :: Lens' TxState Bool
gasprice :: Lens' TxState Word
touchedAccounts :: Lens' SubState [Addr]
selfdestructs :: Lens' SubState [Addr]
refunds :: Lens' SubState [(Addr, Integer)]
accessedStorageKeys :: Lens' SubState (Set (Addr, W256))
accessedAddresses :: Lens' SubState (Set Addr)
storage :: Lens' Contract Storage
origStorage :: Lens' Contract (Map Word Word)
opIxMap :: Lens' Contract (Vector Int)
nonce :: Lens' Contract Word
external :: Lens' Contract Bool
contractcode :: Lens' Contract ContractCode
codehash :: Lens' Contract W256
codeOps :: Lens' Contract (Vector (Int, Op))
balance :: Lens' Contract Word
storageModel :: Lens' Env StorageModel
sha3Crack :: Lens' Env (Map Word ByteString)
keccakUsed :: Lens' Env [([SWord 8], SWord 256)]
contracts :: Lens' Env (Map Addr Contract)
chainId :: Lens' Env Word
path :: Lens' Cache (Map (CodeLocation, Int) Bool)
fetched :: 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 (Seq Log)
iterations :: Lens' VM (Map CodeLocation Int)
frames :: Lens' VM [Frame]
env :: Lens' VM Env
constraints :: Lens' VM [(SBool, Whiff)]
cache :: Lens' VM Cache
burned :: Lens' VM Word
block :: Lens' VM Block
allowFFI :: Lens' VM Bool
bytecode :: Getter Contract Buffer
unifyCachedContract :: Contract -> Contract -> Contract
currentContract :: VM -> Maybe Contract
makeVm :: VMOpts -> VM
initialContract :: ContractCode -> Contract
contractWithStore :: ContractCode -> Storage -> Contract
next :: (?op :: Word8) => EVM ()
exec1 :: EVM ()
transfer :: Addr -> Addr -> Word -> EVM ()
callChecks :: (?op :: Word8) => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> (Integer -> EVM ()) -> EVM ()
precompiledContract :: (?op :: Word8) => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> EVM ()
executePrecompile :: (?op :: Word8) => Addr -> Integer -> Word -> Word -> Word -> Word -> [SymWord] -> EVM ()
truncpadlit :: Int -> ByteString -> ByteString
lazySlice :: Word -> Word -> ByteString -> ByteString
parseModexpLength :: ByteString -> (Word, Word, Word)
isZero :: Word -> Word -> 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
makeUnique :: SymWord -> (Word -> EVM ()) -> EVM ()
askSMT :: CodeLocation -> (SBool, Whiff) -> (Bool -> EVM ()) -> EVM ()
fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM ()
readStorage :: Storage -> SymWord -> Maybe SymWord
writeStorage :: SymWord -> SymWord -> Storage -> Storage
accessStorage :: Addr -> SymWord -> (SymWord -> EVM ()) -> EVM ()
accountExists :: Addr -> VM -> Bool
accountEmpty :: Contract -> Bool
finalize :: EVM ()
loadContract :: Addr -> EVM ()
limitStack :: Int -> EVM () -> EVM ()
notStatic :: EVM () -> EVM ()
burn :: Integer -> EVM () -> EVM ()
forceConcreteAddr :: SAddr -> (Addr -> EVM ()) -> EVM ()
forceConcrete :: SymWord -> (Word -> EVM ()) -> EVM ()
forceConcrete2 :: (SymWord, SymWord) -> ((Word, Word) -> EVM ()) -> EVM ()
forceConcrete3 :: (SymWord, SymWord, SymWord) -> ((Word, Word, Word) -> EVM ()) -> EVM ()
forceConcrete4 :: (SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word) -> EVM ()) -> EVM ()
forceConcrete5 :: (SymWord, SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word, Word) -> EVM ()) -> EVM ()
forceConcrete6 :: (SymWord, SymWord, SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word, Word, Word) -> EVM ()) -> EVM ()
forceConcreteBuffer :: Buffer -> (ByteString -> EVM ()) -> EVM ()
refund :: Integer -> EVM ()
unRefund :: Integer -> EVM ()
touchAccount :: Addr -> EVM ()
selfdestruct :: Addr -> EVM ()
accessAndBurn :: Addr -> EVM () -> EVM ()
accessAccountForGas :: Addr -> EVM Bool
accessStorageForGas :: Addr -> SymWord -> EVM Bool
cheatCode :: Addr
cheat :: (?op :: Word8) => (Word, Word) -> (Word, Word) -> EVM ()
type CheatAction = Word -> Word -> Buffer -> EVM ()
cheatActions :: Map Word32 CheatAction
ethsign :: PrivateKey -> Digest Keccak_256 -> Signature
delegateCall :: (?op :: Word8) => Contract -> Word -> SAddr -> SAddr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> (Addr -> EVM ()) -> EVM ()
collision :: Maybe Contract -> Bool
create :: (?op :: Word8) => Addr -> Contract -> Word -> Word -> [SymWord] -> Addr -> Buffer -> EVM ()
replaceCode :: Addr -> ContractCode -> EVM ()
replaceCodeOfSelf :: ContractCode -> EVM ()
resetState :: EVM ()
vmError :: Error -> EVM ()
underrun :: EVM ()
data FrameResult
- = FrameReturned Buffer
- | FrameReverted Buffer
- | FrameErrored Error
finishFrame :: FrameResult -> EVM ()
accessUnboundedMemoryRange :: FeeSchedule Integer -> Word -> Word -> EVM () -> EVM ()
accessMemoryRange :: FeeSchedule Integer -> Word -> Word -> EVM () -> EVM ()
accessMemoryWord :: FeeSchedule Integer -> Word -> EVM () -> EVM ()
copyBytesToMemory :: Buffer -> Word -> Word -> Word -> EVM ()
copyCallBytesToMemory :: Buffer -> Word -> Word -> Word -> EVM ()
readMemory :: Word -> Word -> VM -> Buffer
word256At :: Functor f => Word -> (SymWord -> f SymWord) -> Buffer -> f Buffer
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
traceLog :: MonadState VM m => Log -> m ()
push :: Word -> EVM ()
pushSym :: SymWord -> EVM ()
stackOp1 :: (?op :: Word8) => (SymWord -> Integer) -> (SymWord -> SymWord) -> EVM ()
stackOp2 :: (?op :: Word8) => ((SymWord, SymWord) -> Integer) -> ((SymWord, SymWord) -> SymWord) -> EVM ()
stackOp3 :: (?op :: Word8) => ((SymWord, SymWord, SymWord) -> Integer) -> ((SymWord, SymWord, SymWord) -> SymWord) -> EVM ()
checkJump :: Integral n => n -> [SymWord] -> EVM ()
opSize :: Word8 -> Int
mkOpIxMap :: Buffer -> Vector Int
vmOp :: VM -> Maybe Op
vmOpIx :: VM -> Maybe Int
opParams :: VM -> Map String SymWord
readOp :: Word8 -> Buffer -> Op
mkCodeOps :: Buffer -> Vector (Int, Op)
costOfCall :: FeeSchedule Integer -> Bool -> Word -> Word -> Word -> Addr -> EVM (Integer, Integer)
costOfCreate :: FeeSchedule Integer -> Word -> Word -> (Integer, Integer)
concreteModexpGasFee :: ByteString -> Integer
costOfPrecompile :: FeeSchedule Integer -> Addr -> Buffer -> Integer
memoryCost :: FeeSchedule Integer -> Integer -> Integer
ceilDiv :: (Num a, Integral a) => a -> a -> a
allButOne64th :: (Num a, Integral a) => a -> a
log2 :: FiniteBits b => b -> Int

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 Buffer	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 #
SDisplay VMResult Source #
Instance details Defined in EVM.Emacs Methods sexp :: VMResult -> SExpr Text Source #

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 :: Seq Log _traces :: TreePos Empty Trace _cache :: Cache _burned :: Word _constraints :: [(SBool, Whiff)] _iterations :: Map CodeLocation Int _allowFFI :: Bool

Instances

Instances details

Show VM Source #
Instance details Defined in EVM Methods showsPrec :: Int -> VM -> ShowS # show :: VM -> String # showList :: [VM] -> ShowS #
SDisplay VM Source #
Instance details Defined in EVM.Emacs Methods sexp :: VM -> SExpr Text Source #

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 Log
FrameTrace FrameContext
QueryTrace Query
ErrorTrace Error
EntryTrace Text
ReturnTrace Buffer 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 -> 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

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 :: Whiff -> (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 _fetched :: Map Addr Contract _path :: Map (CodeLocation, Int) Bool

Instances

Instances details

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

data VMOpts Source #

A way to specify an initial VM state

Constructors

VMOpts

Fields

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

Instances

Instances details

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

data Log Source #

A log entry

Constructors

Log Addr Buffer [SymWord]

Instances

Instances details

Show Log Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Log -> ShowS # show :: Log -> String # showList :: [Log] -> 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 #
SDisplay Frame Source #
Instance details Defined in EVM.Emacs Methods sexp :: Frame -> SExpr Text Source #

data FrameContext Source #

Call/create info

Constructors

CreationContext
Fields creationContextAddress :: Addr creationContextCodehash :: W256 creationContextReversion :: Map Addr Contract creationContextSubstate :: SubState
CallContext
Fields callContextTarget :: Addr callContextContext :: Addr callContextOffset :: Word callContextSize :: Word callContextCodehash :: W256 callContextAbi :: Maybe Word callContextData :: Buffer callContextReversion :: Map Addr Contract callContextSubState :: SubState

Instances

Instances details

Show FrameContext Source #
Instance details Defined in EVM Methods showsPrec :: Int -> FrameContext -> ShowS # show :: FrameContext -> String # showList :: [FrameContext] -> ShowS #
SDisplay FrameContext Source #
Instance details Defined in EVM.Emacs Methods sexp :: FrameContext -> SExpr Text Source #

data FrameState Source #

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

Constructors

FrameState
Fields _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

Instances

Instances details

Show FrameState Source #
Instance details Defined in EVM Methods showsPrec :: Int -> FrameState -> ShowS # show :: FrameState -> String # showList :: [FrameState] -> ShowS #
SDisplay FrameState Source #
Instance details Defined in EVM.Emacs Methods sexp :: FrameState -> SExpr Text Source #

data TxState Source #

The state that spans a whole transaction

Constructors

TxState
Fields _gasprice :: Word _txgaslimit :: Word _txPriorityFee :: Word _origin :: Addr _toAddr :: Addr _value :: SymWord _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, Integer)]

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.

Constructors

InitCode Buffer	Constructor code, during contract creation
RuntimeCode Buffer	Instance code, after contract creation

Instances

Instances details

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 #
Show ContractCode Source #
Instance details Defined in EVM Methods showsPrec :: Int -> ContractCode -> ShowS # show :: ContractCode -> String # showList :: [ContractCode] -> ShowS #

data Storage Source #

A contract can either have concrete or symbolic storage depending on what type of execution we are doing

Constructors

Concrete (Map Word SymWord)
Symbolic [(SymWord, SymWord)] (SArray (WordN 256) (WordN 256))

Instances

Instances details

Eq Storage Source #
Instance details Defined in EVM Methods (==) :: Storage -> Storage -> Bool # (/=) :: Storage -> Storage -> Bool #
Show Storage Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Storage -> ShowS # show :: Storage -> String # showList :: [Storage] -> ShowS #
SDisplay Storage Source #
Instance details Defined in EVM.Emacs Methods sexp :: Storage -> SExpr Text Source #

data Contract Source #

The state of a contract

Constructors

Contract
Fields _contractcode :: ContractCode _storage :: Storage _balance :: Word _nonce :: Word _codehash :: W256 _opIxMap :: Vector Int _codeOps :: Vector (Int, Op) _external :: Bool _origStorage :: Map Word Word

Instances

Instances details

Show Contract Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Contract -> ShowS # show :: Contract -> String # showList :: [Contract] -> ShowS #
FromJSON Contract Source #
Instance details Defined in EVM.VMTest Methods parseJSON :: Value -> Parser Contract # parseJSONList :: Value -> Parser [Contract] #
SDisplay Contract Source #
Instance details Defined in EVM.Emacs Methods sexp :: Contract -> SExpr Text Source #

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 :: Word _storageModel :: StorageModel _sha3Crack :: Map Word ByteString _keccakUsed :: [([SWord 8], SWord 256)]

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 :: SymWord _number :: Word _difficulty :: Word _gaslimit :: Word _baseFee :: Word _maxCodeSize :: Word _schedule :: FeeSchedule Integer

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 [SymWord] Source #

returndata :: Lens' FrameState Buffer Source #

pc :: Lens' FrameState Int Source #

memorySize :: Lens' FrameState Int Source #

memory :: Lens' FrameState Buffer Source #

gas :: Lens' FrameState Word Source #

contract :: Lens' FrameState Addr Source #

codeContract :: Lens' FrameState Addr Source #

code :: Lens' FrameState Buffer Source #

callvalue :: Lens' FrameState SymWord Source #

caller :: Lens' FrameState SAddr Source #

calldata :: Lens' FrameState (Buffer, SymWord) Source #

frameState :: Lens' Frame FrameState Source #

frameContext :: Lens' Frame FrameContext Source #

timestamp :: Lens' Block SymWord Source #

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

number :: Lens' Block Word Source #

maxCodeSize :: Lens' Block Word Source #

gaslimit :: Lens' Block Word Source #

difficulty :: Lens' Block Word Source #

coinbase :: Lens' Block Addr Source #

baseFee :: Lens' Block Word Source #

value :: Lens' TxState SymWord Source #

txgaslimit :: Lens' TxState Word Source #

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

txPriorityFee :: Lens' TxState Word Source #

toAddr :: Lens' TxState Addr Source #

substate :: Lens' TxState SubState Source #

origin :: Lens' TxState Addr Source #

isCreate :: Lens' TxState Bool Source #

gasprice :: Lens' TxState Word Source #

touchedAccounts :: Lens' SubState [Addr] Source #

selfdestructs :: Lens' SubState [Addr] Source #

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

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

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

storage :: Lens' Contract Storage Source #

origStorage :: Lens' Contract (Map Word Word) Source #

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

nonce :: Lens' Contract Word Source #

external :: Lens' Contract Bool Source #

contractcode :: Lens' Contract ContractCode Source #

codehash :: Lens' Contract W256 Source #

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

balance :: Lens' Contract Word Source #

storageModel :: Lens' Env StorageModel Source #

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

keccakUsed :: Lens' Env [([SWord 8], SWord 256)] Source #

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

chainId :: Lens' Env Word Source #

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

fetched :: 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 (Seq Log) Source #

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

frames :: Lens' VM [Frame] Source #

env :: Lens' VM Env Source #

constraints :: Lens' VM [(SBool, Whiff)] Source #

cache :: Lens' VM Cache Source #

burned :: Lens' VM Word Source #

block :: Lens' VM Block Source #

allowFFI :: Lens' VM Bool Source #

bytecode :: Getter Contract Buffer Source #

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

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

contractWithStore :: ContractCode -> Storage -> Contract Source #

Opcode dispatch (exec1)

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

Update program counter

exec1 :: EVM () Source #

Executes the EVM one step

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

callChecks :: (?op :: Word8) => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> (Integer -> EVM ()) -> EVM () Source #

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

precompiledContract :: (?op :: Word8) => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> EVM () Source #

executePrecompile :: (?op :: Word8) => Addr -> Integer -> Word -> Word -> Word -> Word -> [SymWord] -> EVM () Source #

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

lazySlice :: Word -> Word -> ByteString -> ByteString Source #

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

isZero :: Word -> Word -> 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 #

makeUnique :: SymWord -> (Word -> EVM ()) -> EVM () Source #

Ask the SMT solver to provide a concrete model for val iff a unique model exists

askSMT :: CodeLocation -> (SBool, Whiff) -> (Bool -> EVM ()) -> EVM () Source #

Construct SMT Query and halt execution until resolved

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

Construct RPC Query and halt execution until resolved

readStorage :: Storage -> SymWord -> Maybe SymWord Source #

writeStorage :: SymWord -> SymWord -> Storage -> Storage Source #

accessStorage Source #

Arguments

:: Addr	Contract address
-> SymWord	Storage slot key
-> (SymWord -> 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 :: Integer -> EVM () -> EVM () Source #

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

forceConcreteAddr :: SAddr -> (Addr -> EVM ()) -> EVM () Source #

forceConcrete :: SymWord -> (Word -> EVM ()) -> EVM () Source #

forceConcrete2 :: (SymWord, SymWord) -> ((Word, Word) -> EVM ()) -> EVM () Source #

forceConcrete3 :: (SymWord, SymWord, SymWord) -> ((Word, Word, Word) -> EVM ()) -> EVM () Source #

forceConcrete4 :: (SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word) -> EVM ()) -> EVM () Source #

forceConcrete5 :: (SymWord, SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word, Word) -> EVM ()) -> EVM () Source #

forceConcrete6 :: (SymWord, SymWord, SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word, Word, Word) -> EVM ()) -> EVM () Source #

forceConcreteBuffer :: Buffer -> (ByteString -> EVM ()) -> EVM () Source #

Substate manipulation

refund :: Integer -> EVM () Source #

unRefund :: Integer -> 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 -> SymWord -> 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) => (Word, Word) -> (Word, Word) -> EVM () Source #

type CheatAction = Word -> Word -> Buffer -> EVM () Source #

cheatActions :: Map Word32 CheatAction Source #

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

Hack deterministic signing, totally insecure...

General call implementation ("delegateCall")

delegateCall :: (?op :: Word8) => Contract -> Word -> SAddr -> SAddr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> (Addr -> EVM ()) -> EVM () Source #

collision :: Maybe Contract -> Bool Source #

create :: (?op :: Word8) => Addr -> Contract -> Word -> Word -> [SymWord] -> Addr -> Buffer -> 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 Buffer	STOP, RETURN, or no more code
FrameReverted Buffer	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 Integer -> Word -> Word -> EVM () -> EVM () Source #

accessMemoryRange :: FeeSchedule Integer -> Word -> Word -> EVM () -> EVM () Source #

accessMemoryWord :: FeeSchedule Integer -> Word -> EVM () -> EVM () Source #

copyBytesToMemory :: Buffer -> Word -> Word -> Word -> EVM () Source #

copyCallBytesToMemory :: Buffer -> Word -> Word -> Word -> EVM () Source #

readMemory :: Word -> Word -> VM -> Buffer Source #

word256At :: Functor f => Word -> (SymWord -> f SymWord) -> Buffer -> f Buffer 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 #

traceLog :: MonadState VM m => Log -> m () Source #

Stack manipulation

push :: Word -> EVM () Source #

pushSym :: SymWord -> EVM () Source #

stackOp1 :: (?op :: Word8) => (SymWord -> Integer) -> (SymWord -> SymWord) -> EVM () Source #

stackOp2 :: (?op :: Word8) => ((SymWord, SymWord) -> Integer) -> ((SymWord, SymWord) -> SymWord) -> EVM () Source #

stackOp3 :: (?op :: Word8) => ((SymWord, SymWord, SymWord) -> Integer) -> ((SymWord, SymWord, SymWord) -> SymWord) -> EVM () Source #

Bytecode data functions

checkJump :: Integral n => n -> [SymWord] -> EVM () Source #

opSize :: Word8 -> Int Source #

mkOpIxMap :: Buffer -> Vector Int Source #

vmOp :: VM -> Maybe Op Source #

vmOpIx :: VM -> Maybe Int Source #

opParams :: VM -> Map String SymWord Source #

readOp :: Word8 -> Buffer -> Op Source #

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

Gas cost calculation helpers

costOfCall :: FeeSchedule Integer -> Bool -> Word -> Word -> Word -> Addr -> EVM (Integer, Integer) Source #

costOfCreate :: FeeSchedule Integer -> Word -> Word -> (Integer, Integer) Source #

concreteModexpGasFee :: ByteString -> Integer Source #

costOfPrecompile :: FeeSchedule Integer -> Addr -> Buffer -> Integer Source #

memoryCost :: FeeSchedule Integer -> Integer -> Integer 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 #

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

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