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

Synopsis

data Error
- = BalanceTooLow W256 W256
- | UnrecognizedOpcode Word8
- | SelfDestruction
- | StackUnderrun
- | BadJumpDestination
- | Revert (Expr Buf)
- | OutOfGas Word64 Word64
- | BadCheatCode FunctionSelector
- | 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]
- | ReturnDataOutOfBounds
- | 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
- overrideCaller :: Maybe Addr
}
data Trace = Trace {
- opIx :: Int
- contract :: 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 VMOpts = VMOpts {
- contract :: Contract
- calldata :: (Expr Buf, [Prop])
- initialStorage :: Expr Storage
- value :: Expr EWord
- priorityFee :: W256
- address :: Addr
- caller :: Expr EWord
- origin :: Addr
- gas :: Word64
- gaslimit :: Word64
- number :: W256
- timestamp :: Expr EWord
- coinbase :: Addr
- prevRandao :: W256
- maxCodeSize :: W256
- blockGaslimit :: Word64
- gasprice :: W256
- baseFee :: W256
- schedule :: FeeSchedule Word64
- chainId :: W256
- create :: Bool
- txAccessList :: Map Addr [W256]
- allowFFI :: Bool
}
data Frame = Frame {
- context :: FrameContext
- state :: FrameState
}
data FrameContext
- = CreationContext {
  - address :: Addr
  - codehash :: Expr EWord
  - createreversion :: Map Addr Contract
  - substate :: SubState
  }
- | CallContext {
  - target :: Addr
  - context :: Addr
  - offset :: W256
  - size :: W256
  - codehash :: Expr EWord
  - abi :: Maybe W256
  - calldata :: Expr Buf
  - callreversion :: (Map Addr Contract, Expr Storage)
  - subState :: 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
- gaslimit :: Word64
- priorityFee :: 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 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
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 => Lens s s [a] [a] -> a -> m ()
pushToSequence :: MonadState s m => Setter 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 FunctionSelector CheatAction
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 :: Word64 -> Word64 -> EVM () -> EVM ()
accessMemoryRange :: W256 -> W256 -> EVM () -> EVM ()
accessMemoryWord :: 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 :: TraceData -> EVM Trace
pushTrace :: TraceData -> EVM ()
insertTrace :: TraceData -> EVM ()
popTrace :: EVM ()
zipperRootForest :: TreePos Empty a -> Forest a
traceForest :: VM -> Forest Trace
traceTopLog :: [Expr Log] -> EVM ()
push :: W256 -> EVM ()
pushSym :: Expr EWord -> EVM ()
stackOp1 :: (?op :: Word8) => Word64 -> (Expr EWord -> Expr EWord) -> EVM ()
stackOp2 :: (?op :: Word8) => Word64 -> ((Expr EWord, Expr EWord) -> Expr EWord) -> EVM ()
stackOp3 :: (?op :: Word8) => Word64 -> ((Expr EWord, Expr EWord, Expr EWord) -> Expr EWord) -> EVM ()
use' :: (VM -> a) -> EVM a
checkJump :: Int -> [Expr EWord] -> EVM ()
opSize :: Word8 -> Int
mkOpIxMap :: ContractCode -> Vector Int
vmOp :: VM -> Maybe Op
vmOpIx :: VM -> Maybe Int
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
hashcode :: ContractCode -> Expr EWord
opslen :: ContractCode -> Int
codelen :: ContractCode -> Expr EWord
toBuf :: ContractCode -> Expr Buf
codeloc :: EVM CodeLocation
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 (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 overrideCaller :: Maybe Addr

Instances

Instances details

Generic VM Source #
Instance details Defined in EVM Associated Types type Rep VM :: Type -> Type # Methods from :: VM -> Rep VM x # to :: Rep VM x -> VM #
Show VM Source #
Instance details Defined in EVM Methods showsPrec :: Int -> VM -> ShowS # show :: VM -> String # showList :: [VM] -> ShowS #
(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "allowFFI" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ Block, b ~ Block) => LabelOptic "block" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "burned" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ Cache, b ~ Cache) => LabelOptic "cache" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ [Prop], b ~ [Prop]) => LabelOptic "constraints" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ Env, b ~ Env) => LabelOptic "env" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ [Frame], b ~ [Frame]) => LabelOptic "frames" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ Map CodeLocation Int, b ~ Map CodeLocation Int) => LabelOptic "iterations" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ [Prop], b ~ [Prop]) => LabelOptic "keccakEqs" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ [Expr 'Log], b ~ [Expr 'Log]) => LabelOptic "logs" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ Maybe Addr, b ~ Maybe Addr) => LabelOptic "overrideCaller" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ Maybe VMResult, b ~ Maybe VMResult) => LabelOptic "result" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ FrameState, b ~ FrameState) => LabelOptic "state" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ TreePos Empty Trace, b ~ TreePos Empty Trace) => LabelOptic "traces" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
(k ~ A_Lens, a ~ TxState, b ~ TxState) => LabelOptic "tx" k VM VM a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VM VM a b #
type Rep VM Source #
Instance details Defined in EVM type Rep VM = D1 ('MetaData "VM" "EVM" "hevm-0.50.5-inplace" 'False) (C1 ('MetaCons "VM" 'PrefixI 'True) (((S1 ('MetaSel ('Just "result") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe VMResult)) :: (S1 ('MetaSel ('Just "state") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FrameState) :: S1 ('MetaSel ('Just "frames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Frame]))) :: ((S1 ('MetaSel ('Just "env") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Env) :: S1 ('MetaSel ('Just "block") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Block)) :: (S1 ('MetaSel ('Just "tx") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TxState) :: S1 ('MetaSel ('Just "logs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr 'Log])))) :: (((S1 ('MetaSel ('Just "traces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TreePos Empty Trace)) :: S1 ('MetaSel ('Just "cache") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cache)) :: (S1 ('MetaSel ('Just "burned") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :: S1 ('MetaSel ('Just "iterations") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map CodeLocation Int)))) :: ((S1 ('MetaSel ('Just "constraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]) :: S1 ('MetaSel ('Just "keccakEqs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop])) :: (S1 ('MetaSel ('Just "allowFFI") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "overrideCaller") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Addr)))))))

data Trace Source #

Constructors

Trace
Fields opIx :: Int contract :: Contract tracedata :: TraceData

Instances

Instances details

Generic Trace Source #
Instance details Defined in EVM Associated Types type Rep Trace :: Type -> Type # Methods from :: Trace -> Rep Trace x # to :: Rep Trace x -> Trace #
Show Trace Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Trace -> ShowS # show :: Trace -> String # showList :: [Trace] -> ShowS #
(k ~ A_Lens, a ~ Contract, b ~ Contract) => LabelOptic "contract" k Trace Trace a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Trace Trace a b #
(k ~ A_Lens, a ~ Int, b ~ Int) => LabelOptic "opIx" k Trace Trace a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Trace Trace a b #
(k ~ A_Lens, a ~ TraceData, b ~ TraceData) => LabelOptic "tracedata" k Trace Trace a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Trace Trace a b #
type Rep Trace Source #
Instance details Defined in EVM type Rep Trace = D1 ('MetaData "Trace" "EVM" "hevm-0.50.5-inplace" 'False) (C1 ('MetaCons "Trace" 'PrefixI 'True) (S1 ('MetaSel ('Just "opIx") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: (S1 ('MetaSel ('Just "contract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Contract) :: S1 ('MetaSel ('Just "tracedata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TraceData))))

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

Generic TraceData Source #
Instance details Defined in EVM Associated Types type Rep TraceData :: Type -> Type # Methods from :: TraceData -> Rep TraceData x # to :: Rep TraceData x -> TraceData #
Show TraceData Source #
Instance details Defined in EVM Methods showsPrec :: Int -> TraceData -> ShowS # show :: TraceData -> String # showList :: [TraceData] -> ShowS #
type Rep TraceData Source #
Instance details Defined in EVM type Rep TraceData = D1 ('MetaData "TraceData" "EVM" "hevm-0.50.5-inplace" 'False) ((C1 ('MetaCons "EventTrace" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'EWord)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'Buf)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr 'EWord]))) :+: (C1 ('MetaCons "FrameTrace" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FrameContext)) :+: C1 ('MetaCons "QueryTrace" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Query)))) :+: (C1 ('MetaCons "ErrorTrace" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Error)) :+: (C1 ('MetaCons "EntryTrace" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "ReturnTrace" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'Buf)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FrameContext)))))

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 #
Generic Cache Source #
Instance details Defined in EVM Associated Types type Rep Cache :: Type -> Type # Methods from :: Cache -> Rep Cache x # to :: Rep Cache x -> Cache #
Show Cache Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Cache -> ShowS # show :: Cache -> String # showList :: [Cache] -> ShowS #
(k ~ A_Lens, a ~ Map Addr Contract, b ~ Map Addr Contract) => LabelOptic "fetchedContracts" k Cache Cache a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Cache Cache a b #
(k ~ A_Lens, a ~ Map W256 (Map W256 W256), b ~ Map W256 (Map W256 W256)) => LabelOptic "fetchedStorage" k Cache Cache a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Cache Cache a b #
(k ~ A_Lens, a ~ Map (CodeLocation, Int) Bool, b ~ Map (CodeLocation, Int) Bool) => LabelOptic "path" k Cache Cache a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Cache Cache a b #
type Rep Cache Source #
Instance details Defined in EVM type Rep Cache = D1 ('MetaData "Cache" "EVM" "hevm-0.50.5-inplace" 'False) (C1 ('MetaCons "Cache" 'PrefixI 'True) (S1 ('MetaSel ('Just "fetchedContracts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Addr Contract)) :: (S1 ('MetaSel ('Just "fetchedStorage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map W256 (Map W256 W256))) :: S1 ('MetaSel ('Just "path") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map (CodeLocation, Int) Bool)))))

data VMOpts Source #

A way to specify an initial VM state

Constructors

VMOpts

Fields

Instances

Instances details

Show VMOpts Source #
Instance details Defined in EVM Methods showsPrec :: Int -> VMOpts -> ShowS # show :: VMOpts -> String # showList :: [VMOpts] -> ShowS #
(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "address" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "allowFFI" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "baseFee" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "blockGaslimit" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ (Expr 'Buf, [Prop]), b ~ (Expr 'Buf, [Prop])) => LabelOptic "calldata" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "caller" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "chainId" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "coinbase" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Contract, b ~ Contract) => LabelOptic "contract" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "create" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "gas" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "gaslimit" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "gasprice" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Expr 'Storage, b ~ Expr 'Storage) => LabelOptic "initialStorage" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "maxCodeSize" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "number" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "origin" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "prevRandao" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "priorityFee" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ FeeSchedule Word64, b ~ FeeSchedule Word64) => LabelOptic "schedule" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "timestamp" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Map Addr [W256], b ~ Map Addr [W256]) => LabelOptic "txAccessList" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #
(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "value" k VMOpts VMOpts a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx VMOpts VMOpts a b #

data Frame Source #

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

Constructors

Frame
Fields context :: FrameContext state :: FrameState

Instances

Instances details

Show Frame Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Frame -> ShowS # show :: Frame -> String # showList :: [Frame] -> ShowS #
(k ~ A_Lens, a ~ FrameContext, b ~ FrameContext) => LabelOptic "context" k Frame Frame a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Frame Frame a b #
(k ~ A_Lens, a ~ FrameState, b ~ FrameState) => LabelOptic "state" k Frame Frame a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Frame Frame a b #

data FrameContext Source #

Call/create info

Constructors

CreationContext
Fields address :: Addr codehash :: Expr EWord createreversion :: Map Addr Contract substate :: SubState
CallContext
Fields target :: Addr context :: Addr offset :: W256 size :: W256 codehash :: Expr EWord abi :: Maybe W256 calldata :: Expr Buf callreversion :: (Map Addr Contract, Expr Storage) subState :: SubState

Instances

Instances details

Generic FrameContext Source #
Instance details Defined in EVM Associated Types type Rep FrameContext :: Type -> Type # Methods from :: FrameContext -> Rep FrameContext x # to :: Rep FrameContext x -> FrameContext #
Show FrameContext Source #
Instance details Defined in EVM Methods showsPrec :: Int -> FrameContext -> ShowS # show :: FrameContext -> String # showList :: [FrameContext] -> ShowS #
(k ~ An_AffineTraversal, a ~ Maybe W256, b ~ Maybe W256) => LabelOptic "abi" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
(k ~ An_AffineTraversal, a ~ Addr, b ~ Addr) => LabelOptic "address" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
(k ~ An_AffineTraversal, a ~ Expr 'Buf, b ~ Expr 'Buf) => LabelOptic "calldata" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
(k ~ An_AffineTraversal, a ~ (Map Addr Contract, Expr 'Storage), b ~ (Map Addr Contract, Expr 'Storage)) => LabelOptic "callreversion" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "codehash" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
(k ~ An_AffineTraversal, a ~ Addr, b ~ Addr) => LabelOptic "context" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
(k ~ An_AffineTraversal, a ~ Map Addr Contract, b ~ Map Addr Contract) => LabelOptic "createreversion" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
(k ~ An_AffineTraversal, a ~ W256, b ~ W256) => LabelOptic "offset" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
(k ~ An_AffineTraversal, a ~ W256, b ~ W256) => LabelOptic "size" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
(k ~ An_AffineTraversal, a ~ SubState, b ~ SubState) => LabelOptic "subState" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
(k ~ An_AffineTraversal, a ~ SubState, b ~ SubState) => LabelOptic "substate" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
(k ~ An_AffineTraversal, a ~ Addr, b ~ Addr) => LabelOptic "target" k FrameContext FrameContext a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameContext FrameContext a b #
type Rep FrameContext Source #
Instance details Defined in EVM type Rep FrameContext = D1 ('MetaData "FrameContext" "EVM" "hevm-0.50.5-inplace" 'False) (C1 ('MetaCons "CreationContext" 'PrefixI 'True) ((S1 ('MetaSel ('Just "address") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Addr) :: S1 ('MetaSel ('Just "codehash") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'EWord))) :: (S1 ('MetaSel ('Just "createreversion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Addr Contract)) :: S1 ('MetaSel ('Just "substate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SubState))) :+: C1 ('MetaCons "CallContext" 'PrefixI 'True) (((S1 ('MetaSel ('Just "target") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Addr) :: S1 ('MetaSel ('Just "context") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Addr)) :: (S1 ('MetaSel ('Just "offset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 W256) :: S1 ('MetaSel ('Just "size") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 W256))) :: ((S1 ('MetaSel ('Just "codehash") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'EWord)) :: S1 ('MetaSel ('Just "abi") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe W256))) :: (S1 ('MetaSel ('Just "calldata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'Buf)) :: (S1 ('MetaSel ('Just "callreversion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Addr Contract, Expr 'Storage)) :*: S1 ('MetaSel ('Just "subState") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SubState))))))

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

Generic FrameState Source #
Instance details Defined in EVM Associated Types type Rep FrameState :: Type -> Type # Methods from :: FrameState -> Rep FrameState x # to :: Rep FrameState x -> FrameState #
Show FrameState Source #
Instance details Defined in EVM Methods showsPrec :: Int -> FrameState -> ShowS # show :: FrameState -> String # showList :: [FrameState] -> ShowS #
(k ~ A_Lens, a ~ Expr 'Buf, b ~ Expr 'Buf) => LabelOptic "calldata" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "caller" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "callvalue" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ ContractCode, b ~ ContractCode) => LabelOptic "code" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "codeContract" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "contract" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "gas" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ Expr 'Buf, b ~ Expr 'Buf) => LabelOptic "memory" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "memorySize" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ Int, b ~ Int) => LabelOptic "pc" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ Expr 'Buf, b ~ Expr 'Buf) => LabelOptic "returndata" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ [Expr 'EWord], b ~ [Expr 'EWord]) => LabelOptic "stack" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "static" k FrameState FrameState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx FrameState FrameState a b #
type Rep FrameState Source #
Instance details Defined in EVM type Rep FrameState = D1 ('MetaData "FrameState" "EVM" "hevm-0.50.5-inplace" 'False) (C1 ('MetaCons "FrameState" 'PrefixI 'True) (((S1 ('MetaSel ('Just "contract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Addr) :: (S1 ('MetaSel ('Just "codeContract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Addr) :: S1 ('MetaSel ('Just "code") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ContractCode))) :: (S1 ('MetaSel ('Just "pc") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :: (S1 ('MetaSel ('Just "stack") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr 'EWord]) :: S1 ('MetaSel ('Just "memory") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'Buf))))) :: ((S1 ('MetaSel ('Just "memorySize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64) :: (S1 ('MetaSel ('Just "calldata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'Buf)) :: S1 ('MetaSel ('Just "callvalue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'EWord)))) :: ((S1 ('MetaSel ('Just "caller") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'EWord)) :: S1 ('MetaSel ('Just "gas") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64)) :: (S1 ('MetaSel ('Just "returndata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'Buf)) :: S1 ('MetaSel ('Just "static") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))))

data TxState Source #

The state that spans a whole transaction

Constructors

TxState
Fields gasprice :: W256 gaslimit :: Word64 priorityFee :: 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 #
(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "gaslimit" k TxState TxState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx TxState TxState a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "gasprice" k TxState TxState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx TxState TxState a b #
(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "isCreate" k TxState TxState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx TxState TxState a b #
(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "origin" k TxState TxState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx TxState TxState a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "priorityFee" k TxState TxState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx TxState TxState a b #
(k ~ A_Lens, a ~ SubState, b ~ SubState) => LabelOptic "substate" k TxState TxState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx TxState TxState a b #
(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "toAddr" k TxState TxState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx TxState TxState a b #
(k ~ A_Lens, a ~ Map Addr Contract, b ~ Map Addr Contract) => LabelOptic "txReversion" k TxState TxState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx TxState TxState a b #
(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "value" k TxState TxState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx TxState TxState a b #

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 #
(k ~ A_Lens, a ~ Set Addr, b ~ Set Addr) => LabelOptic "accessedAddresses" k SubState SubState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx SubState SubState a b #
(k ~ A_Lens, a ~ Set (Addr, W256), b ~ Set (Addr, W256)) => LabelOptic "accessedStorageKeys" k SubState SubState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx SubState SubState a b #
(k ~ A_Lens, a ~ [(Addr, Word64)], b ~ [(Addr, Word64)]) => LabelOptic "refunds" k SubState SubState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx SubState SubState a b #
(k ~ A_Lens, a ~ [Addr], b ~ [Addr]) => LabelOptic "selfdestructs" k SubState SubState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx SubState SubState a b #
(k ~ A_Lens, a ~ [Addr], b ~ [Addr]) => LabelOptic "touchedAccounts" k SubState SubState a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx SubState SubState a b #

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 #

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 #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "balance" k Contract Contract a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Contract Contract a b #
(k ~ A_Lens, a ~ Vector (Int, Op), b ~ Vector (Int, Op)) => LabelOptic "codeOps" k Contract Contract a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Contract Contract a b #
(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "codehash" k Contract Contract a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Contract Contract a b #
(k ~ A_Lens, a ~ ContractCode, b ~ ContractCode) => LabelOptic "contractcode" k Contract Contract a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Contract Contract a b #
(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "external" k Contract Contract a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Contract Contract a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "nonce" k Contract Contract a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Contract Contract a b #
(k ~ A_Lens, a ~ Vector Int, b ~ Vector Int) => LabelOptic "opIxMap" k Contract Contract a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Contract Contract a b #

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

Generic Env Source #
Instance details Defined in EVM Associated Types type Rep Env :: Type -> Type # Methods from :: Env -> Rep Env x # to :: Rep Env x -> Env #
Show Env Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Env -> ShowS # show :: Env -> String # showList :: [Env] -> ShowS #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "chainId" k Env Env a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Env Env a b #
(k ~ A_Lens, a ~ Map Addr Contract, b ~ Map Addr Contract) => LabelOptic "contracts" k Env Env a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Env Env a b #
(k ~ A_Lens, a ~ Map W256 (Map W256 W256), b ~ Map W256 (Map W256 W256)) => LabelOptic "origStorage" k Env Env a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Env Env a b #
(k ~ A_Lens, a ~ Map W256 ByteString, b ~ Map W256 ByteString) => LabelOptic "sha3Crack" k Env Env a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Env Env a b #
(k ~ A_Lens, a ~ Expr 'Storage, b ~ Expr 'Storage) => LabelOptic "storage" k Env Env a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Env Env a b #
type Rep Env Source #
Instance details Defined in EVM type Rep Env = D1 ('MetaData "Env" "EVM" "hevm-0.50.5-inplace" 'False) (C1 ('MetaCons "Env" 'PrefixI 'True) ((S1 ('MetaSel ('Just "contracts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Addr Contract)) :: S1 ('MetaSel ('Just "chainId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 W256)) :: (S1 ('MetaSel ('Just "storage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'Storage)) :: (S1 ('MetaSel ('Just "origStorage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map W256 (Map W256 W256))) :: S1 ('MetaSel ('Just "sha3Crack") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map W256 ByteString))))))

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

Generic Block Source #
Instance details Defined in EVM Associated Types type Rep Block :: Type -> Type # Methods from :: Block -> Rep Block x # to :: Rep Block x -> Block #
Show Block Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Block -> ShowS # show :: Block -> String # showList :: [Block] -> ShowS #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "baseFee" k Block Block a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Block Block a b #
(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "coinbase" k Block Block a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Block Block a b #
(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "gaslimit" k Block Block a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Block Block a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "maxCodeSize" k Block Block a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Block Block a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "number" k Block Block a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Block Block a b #
(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "prevRandao" k Block Block a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Block Block a b #
(k ~ A_Lens, a ~ FeeSchedule Word64, b ~ FeeSchedule Word64) => LabelOptic "schedule" k Block Block a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Block Block a b #
(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "timestamp" k Block Block a b Source #
Instance details Defined in EVM Methods labelOptic :: Optic k NoIx Block Block a b #
type Rep Block Source #
Instance details Defined in EVM type Rep Block = D1 ('MetaData "Block" "EVM" "hevm-0.50.5-inplace" 'False) (C1 ('MetaCons "Block" 'PrefixI 'True) (((S1 ('MetaSel ('Just "coinbase") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Addr) :: S1 ('MetaSel ('Just "timestamp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'EWord))) :: (S1 ('MetaSel ('Just "number") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 W256) :: S1 ('MetaSel ('Just "prevRandao") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 W256))) :: ((S1 ('MetaSel ('Just "gaslimit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64) :: S1 ('MetaSel ('Just "baseFee") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 W256)) :: (S1 ('MetaSel ('Just "maxCodeSize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 W256) :*: S1 ('MetaSel ('Just "schedule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FeeSchedule Word64))))))

blankState :: FrameState 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 => Lens s s [a] [a] -> a -> m () Source #

pushToSequence :: MonadState s m => Setter 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 :: Addr -> Expr EWord -> (Expr EWord -> EVM ()) -> EVM () Source #

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 FunctionSelector CheatAction Source #

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 :: Word64 -> Word64 -> EVM () -> EVM () Source #

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

accessMemoryWord :: 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 :: TraceData -> EVM 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 :: [Expr Log] -> EVM () Source #

Stack manipulation

push :: W256 -> EVM () Source #

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

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

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

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

Bytecode data functions

use' :: (VM -> a) -> EVM a Source #

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 #

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 #

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 #

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 W256 W256
UnrecognizedOpcode Word8
SelfDestruction
StackUnderrun
BadJumpDestination
Revert (Expr Buf)
OutOfGas Word64 Word64
BadCheatCode FunctionSelector
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]
ReturnDataOutOfBounds
NonceOverflow