-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Ethereum virtual machine evaluator
--
-- Hevm implements the Ethereum virtual machine semantics. . It can be
-- used as a library, and it also comes with an executable that can run
-- unit test suites, optionally with a visual TTY debugger.
@package hevm
@version 0.51.2
module EVM.FeeSchedule
data FeeSchedule n
FeeSchedule :: n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> FeeSchedule n
[$sel:g_zero:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_base:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_verylow:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_low:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_mid:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_high:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_extcode:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_balance:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_sload:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_jumpdest:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_sset:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_sreset:FeeSchedule] :: FeeSchedule n -> n
[$sel:r_sclear:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_selfdestruct:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_selfdestruct_newaccount:FeeSchedule] :: FeeSchedule n -> n
[$sel:r_selfdestruct:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_create:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_codedeposit:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_call:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_callvalue:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_callstipend:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_newaccount:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_exp:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_expbyte:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_memory:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_txcreate:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_txdatazero:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_txdatanonzero:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_transaction:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_log:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_logdata:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_logtopic:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_sha3:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_sha3word:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_initcodeword:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_copy:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_blockhash:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_extcodehash:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_quaddivisor:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_ecadd:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_ecmul:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_pairing_point:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_pairing_base:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_fround:FeeSchedule] :: FeeSchedule n -> n
[$sel:r_block:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_cold_sload:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_cold_account_access:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_warm_storage_read:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_access_list_address:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_access_list_storage_key:FeeSchedule] :: FeeSchedule n -> n
type EIP n = Num n => FeeSchedule n -> FeeSchedule n
eip150 :: EIP n
eip160 :: EIP n
homestead :: Num n => FeeSchedule n
metropolis :: Num n => FeeSchedule n
eip1108 :: EIP n
eip1884 :: EIP n
eip2028 :: EIP n
eip2200 :: EIP n
istanbul :: Num n => FeeSchedule n
eip2929 :: EIP n
berlin :: Num n => FeeSchedule n
instance GHC.Show.Show n => GHC.Show.Show (EVM.FeeSchedule.FeeSchedule n)
module EVM.Hexdump
-- | prettyHex renders a ByteString as a multi-line
-- String complete with addressing, hex digits, and ASCII
-- representation.
--
-- Sample output
--
--
-- Length: 100 (0x64) bytes
-- 0000: 4b c1 ad 8a 5b 47 d7 57 48 64 e7 cc 5e b5 2f 6e K...[G.WHd..^./n
-- 0010: c5 b3 a4 73 44 3b 97 53 99 2d 54 e7 1b 2f 91 12 ...sD;.S.-T../..
-- 0020: c8 1a ff c4 3b 2b 72 ea 97 e2 9f e2 93 ad 23 79 ....;+r.......#y
-- 0030: e8 0f 08 54 02 14 fa 09 f0 2d 34 c9 08 6b e1 64 ...T.....-4..k.d
-- 0040: d1 c5 98 7e d6 a1 98 e2 97 da 46 68 4e 60 11 15 ...~......FhN`..
-- 0050: d8 32 c6 0b 70 f5 2e 76 7f 8d f2 3b ed de 90 c6 .2..p..v...;....
-- 0060: 93 12 9c e1 ....
--
prettyHex :: Int -> ByteString -> String
-- | simpleHex converts a ByteString to a String
-- showing the octets grouped in 32-bit words.
--
-- Sample output
--
--
-- 4b c1 ad 8a 5b 47 d7 57
--
simpleHex :: ByteString -> String
-- | paddedShowHex displays a number in hexidecimal and pads the
-- number with 0 so that it has a minimum length of w.
paddedShowHex :: (Show a, Integral a) => Int -> a -> String
module EVM.Precompiled
-- | Run a given precompiled contract using the C library.
execute :: Int -> ByteString -> Int -> Maybe ByteString
module EVM.TTYCenteredList
-- | Turn a list state value into a widget given an item drawing function.
renderList :: (Ord n, Show n) => (Bool -> e -> Widget n) -> Bool -> List n e -> Widget n
drawListElements :: (Ord n, Show n) => Bool -> List n e -> (Bool -> e -> Widget n) -> Widget n
module EVM.Types
data Word512
Word512 :: {-# UNPACK #-} !Word256 -> {-# UNPACK #-} !Word256 -> Word512
data Int512
Int512 :: {-# UNPACK #-} !Int256 -> {-# UNPACK #-} !Word256 -> Int512
data EType
Buf :: EType
Storage :: EType
Log :: EType
EWord :: EType
Byte :: EType
End :: EType
data GVar (a :: EType)
[BufVar] :: Int -> GVar Buf
[StoreVar] :: Int -> GVar Storage
-- | Expr implements an abstract respresentation of an EVM program
--
-- This type can give insight into the provenance of a term which is
-- useful, both for the aesthetic purpose of printing terms in a richer
-- way, but also to allow optimizations on the AST instead of letting the
-- SMT solver do all the heavy lifting.
--
-- Memory, calldata, and returndata are all represented as a Buf.
-- Semantically speaking a Buf is a byte array with of size 2^256.
--
-- Bufs have two base constructors: - AbstractBuf: all elements are fully
-- abstract values - ConcreteBuf bs: all elements past (length bs) are
-- zero
--
-- Bufs can be read from with: - ReadByte idx buf: read the byte at idx
-- from buf - ReadWord idx buf: read the byte at idx from buf
--
-- Bufs can be written to with: - WriteByte idx val buf: write val to idx
-- in buf - WriteWord idx val buf: write val to idx in buf - CopySlice
-- srcOffset dstOffset size src dst: overwrite dstOffset -> dstOffset
-- + size in dst with srcOffset -> srcOffset + size from src
--
-- Note that the shared usage of Buf does allow for the
-- construction of some badly typed Expr instances (e.g. an MSTORE on top
-- of the contents of calldata instead of some previous instance of
-- memory), we accept this for the sake of simplifying pattern matches
-- against a Buf expression.
--
-- Storage expressions are similar, but instead of writing regions of
-- bytes, we write a word to a particular key in a given addresses
-- storage. Note that as with a Buf, writes can be sequenced on top of
-- concrete, empty and fully abstract starting states.
--
-- One important principle is that of local context: e.g. each term
-- representing a write to a Buf Storage Logs will always
-- contain a copy of the state that is being added to, this ensures that
-- all context relevant to a given operation is contained within the term
-- that represents that operation.
--
-- When dealing with Expr instances we assume that concrete expressions
-- have been reduced to their smallest possible representation (i.e. a
-- Lit, ConcreteBuf, or ConcreteStore). Failure to
-- adhere to this invariant will result in your concrete term being
-- treated as symbolic, and may produce unexpected errors. In the future
-- we may wish to consider encoding the concreteness of a given term
-- directly in the type of that term, since such type level shenanigans
-- tends to complicate implementation, we skip this for now.
data Expr (a :: EType)
[Lit] :: {-# UNPACK #-} !W256 -> Expr EWord
[Var] :: Text -> Expr EWord
[GVar] :: GVar a -> Expr a
[LitByte] :: {-# UNPACK #-} !Word8 -> Expr Byte
[IndexWord] :: Expr EWord -> Expr EWord -> Expr Byte
[EqByte] :: Expr Byte -> Expr Byte -> Expr EWord
[JoinBytes] :: Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr EWord
[Partial] :: [Prop] -> Traces -> PartialExec -> Expr End
[Failure] :: [Prop] -> Traces -> EvmError -> Expr End
[Success] :: [Prop] -> Traces -> Expr Buf -> Expr Storage -> Expr End
[ITE] :: Expr EWord -> Expr End -> Expr End -> Expr End
[Add] :: Expr EWord -> Expr EWord -> Expr EWord
[Sub] :: Expr EWord -> Expr EWord -> Expr EWord
[Mul] :: Expr EWord -> Expr EWord -> Expr EWord
[Div] :: Expr EWord -> Expr EWord -> Expr EWord
[SDiv] :: Expr EWord -> Expr EWord -> Expr EWord
[Mod] :: Expr EWord -> Expr EWord -> Expr EWord
[SMod] :: Expr EWord -> Expr EWord -> Expr EWord
[AddMod] :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
[MulMod] :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
[Exp] :: Expr EWord -> Expr EWord -> Expr EWord
[SEx] :: Expr EWord -> Expr EWord -> Expr EWord
[Min] :: Expr EWord -> Expr EWord -> Expr EWord
[Max] :: Expr EWord -> Expr EWord -> Expr EWord
[LT] :: Expr EWord -> Expr EWord -> Expr EWord
[GT] :: Expr EWord -> Expr EWord -> Expr EWord
[LEq] :: Expr EWord -> Expr EWord -> Expr EWord
[GEq] :: Expr EWord -> Expr EWord -> Expr EWord
[SLT] :: Expr EWord -> Expr EWord -> Expr EWord
[SGT] :: Expr EWord -> Expr EWord -> Expr EWord
[Eq] :: Expr EWord -> Expr EWord -> Expr EWord
[IsZero] :: Expr EWord -> Expr EWord
[And] :: Expr EWord -> Expr EWord -> Expr EWord
[Or] :: Expr EWord -> Expr EWord -> Expr EWord
[Xor] :: Expr EWord -> Expr EWord -> Expr EWord
[Not] :: Expr EWord -> Expr EWord
[SHL] :: Expr EWord -> Expr EWord -> Expr EWord
[SHR] :: Expr EWord -> Expr EWord -> Expr EWord
[SAR] :: Expr EWord -> Expr EWord -> Expr EWord
[Keccak] :: Expr Buf -> Expr EWord
[SHA256] :: Expr Buf -> Expr EWord
[Origin] :: Expr EWord
[BlockHash] :: Expr EWord -> Expr EWord
[Coinbase] :: Expr EWord
[Timestamp] :: Expr EWord
[BlockNumber] :: Expr EWord
[PrevRandao] :: Expr EWord
[GasLimit] :: Expr EWord
[ChainId] :: Expr EWord
[BaseFee] :: Expr EWord
[CallValue] :: Int -> Expr EWord
[Caller] :: Int -> Expr EWord
[Address] :: Int -> Expr EWord
[Balance] :: Int -> Int -> Expr EWord -> Expr EWord
[SelfBalance] :: Int -> Int -> Expr EWord
[Gas] :: Int -> Int -> Expr EWord
[CodeSize] :: Expr EWord -> Expr EWord
[ExtCodeHash] :: Expr EWord -> Expr EWord
[LogEntry] :: Expr EWord -> Expr Buf -> [Expr EWord] -> Expr Log
[Create] :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> [Expr Log] -> Expr Storage -> Expr EWord
[Create2] :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> [Expr Log] -> Expr Storage -> Expr EWord
[Call] :: Expr EWord -> Maybe (Expr EWord) -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr Log] -> Expr Storage -> Expr EWord
[CallCode] :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr Log] -> Expr Storage -> Expr EWord
[DelegeateCall] :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr Log] -> Expr Storage -> Expr EWord
[EmptyStore] :: Expr Storage
[ConcreteStore] :: Map W256 (Map W256 W256) -> Expr Storage
[AbstractStore] :: Expr Storage
[SLoad] :: Expr EWord -> Expr EWord -> Expr Storage -> Expr EWord
[SStore] :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Storage -> Expr Storage
[ConcreteBuf] :: ByteString -> Expr Buf
[AbstractBuf] :: Text -> Expr Buf
[ReadWord] :: Expr EWord -> Expr Buf -> Expr EWord
[ReadByte] :: Expr EWord -> Expr Buf -> Expr Byte
[WriteWord] :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf
[WriteByte] :: Expr EWord -> Expr Byte -> Expr Buf -> Expr Buf
[CopySlice] :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf -> Expr Buf
[BufLength] :: Expr Buf -> Expr EWord
data SomeExpr
SomeExpr :: Expr a -> SomeExpr
toNum :: Typeable a => Expr a -> Int
data Prop
[PEq] :: forall a. Typeable a => Expr a -> Expr a -> Prop
[PLT] :: Expr EWord -> Expr EWord -> Prop
[PGT] :: Expr EWord -> Expr EWord -> Prop
[PGEq] :: Expr EWord -> Expr EWord -> Prop
[PLEq] :: Expr EWord -> Expr EWord -> Prop
[PNeg] :: Prop -> Prop
[PAnd] :: Prop -> Prop -> Prop
[POr] :: Prop -> Prop -> Prop
[PImpl] :: Prop -> Prop -> Prop
[PBool] :: Bool -> Prop
(.&&) :: Prop -> Prop -> Prop
infixr 3 .&&
(.||) :: Prop -> Prop -> Prop
infixr 2 .||
(.<) :: Expr EWord -> Expr EWord -> Prop
infix 4 .<
(.<=) :: Expr EWord -> Expr EWord -> Prop
infix 4 .<=
(.>) :: Expr EWord -> Expr EWord -> Prop
infix 4 .>
(.>=) :: Expr EWord -> Expr EWord -> Prop
infix 4 .>=
(.==) :: Typeable a => Expr a -> Expr a -> Prop
infix 4 .==
(./=) :: Typeable a => Expr a -> Expr a -> Prop
infix 4 ./=
pand :: [Prop] -> Prop
por :: [Prop] -> Prop
-- | Core EVM Error Types
data EvmError
BalanceTooLow :: W256 -> W256 -> EvmError
UnrecognizedOpcode :: Word8 -> EvmError
SelfDestruction :: EvmError
StackUnderrun :: EvmError
BadJumpDestination :: EvmError
Revert :: Expr Buf -> EvmError
OutOfGas :: Word64 -> Word64 -> EvmError
StackLimitExceeded :: EvmError
IllegalOverflow :: EvmError
StateChangeWhileStatic :: EvmError
InvalidMemoryAccess :: EvmError
CallDepthLimitReached :: EvmError
MaxCodeSizeExceeded :: W256 -> W256 -> EvmError
MaxInitCodeSizeExceeded :: W256 -> W256 -> EvmError
InvalidFormat :: EvmError
PrecompileFailure :: EvmError
ReturnDataOutOfBounds :: EvmError
NonceOverflow :: EvmError
BadCheatCode :: FunctionSelector -> EvmError
-- | Sometimes we can only partially execute a given program
data PartialExec
UnexpectedSymbolicArg :: Int -> String -> [SomeExpr] -> PartialExec
[$sel:pc:UnexpectedSymbolicArg] :: PartialExec -> Int
[$sel:msg:UnexpectedSymbolicArg] :: PartialExec -> String
[$sel:args:UnexpectedSymbolicArg] :: PartialExec -> [SomeExpr]
MaxIterationsReached :: Int -> Addr -> PartialExec
[$sel:pc:UnexpectedSymbolicArg] :: PartialExec -> Int
[$sel:addr:UnexpectedSymbolicArg] :: PartialExec -> Addr
-- | Effect types used by the vm implementation for side effects &
-- control flow
data Effect
Query :: Query -> Effect
Choose :: Choose -> Effect
-- | Queries halt execution until resolved through RPC calls or SMT queries
data Query
[PleaseFetchContract] :: Addr -> (Contract -> EVM ()) -> Query
[PleaseFetchSlot] :: Addr -> W256 -> (W256 -> EVM ()) -> Query
[PleaseAskSMT] :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query
[PleaseDoFFI] :: [String] -> (ByteString -> EVM ()) -> Query
-- | Execution could proceed down one of two branches
data Choose
[PleaseChoosePath] :: Expr EWord -> (Bool -> EVM ()) -> Choose
-- | The possible return values of a SMT query
data BranchCondition
Case :: Bool -> BranchCondition
Unknown :: BranchCondition
-- | The possible result states of a VM
data VMResult
-- | An operation failed
VMFailure :: EvmError -> VMResult
-- | Reached STOP, RETURN, or end-of-code
VMSuccess :: Expr Buf -> VMResult
-- | An effect must be handled for execution to continue
HandleEffect :: Effect -> VMResult
-- | Execution could not continue further
Unfinished :: PartialExec -> VMResult
-- | The state of a stepwise EVM execution
data VM
VM :: Maybe VMResult -> FrameState -> [Frame] -> Env -> Block -> TxState -> [Expr Log] -> TreePos Empty Trace -> Cache -> {-# UNPACK #-} !Word64 -> Map CodeLocation (Int, [Expr EWord]) -> [Prop] -> [Prop] -> Bool -> Maybe Addr -> VM
[$sel:result:VM] :: VM -> Maybe VMResult
[$sel:state:VM] :: VM -> FrameState
[$sel:frames:VM] :: VM -> [Frame]
[$sel:env:VM] :: VM -> Env
[$sel:block:VM] :: VM -> Block
[$sel:tx:VM] :: VM -> TxState
[$sel:logs:VM] :: VM -> [Expr Log]
[$sel:traces:VM] :: VM -> TreePos Empty Trace
[$sel:cache:VM] :: VM -> Cache
[$sel:burned:VM] :: VM -> {-# UNPACK #-} !Word64
-- | how many times we've visited a loc, and what the contents of the stack
-- were when we were there last
[$sel:iterations:VM] :: VM -> Map CodeLocation (Int, [Expr EWord])
[$sel:constraints:VM] :: VM -> [Prop]
[$sel:keccakEqs:VM] :: VM -> [Prop]
[$sel:allowFFI:VM] :: VM -> Bool
[$sel:overrideCaller:VM] :: VM -> Maybe Addr
-- | Alias for the type of e.g. exec1.
type EVM a = State VM a
-- | An entry in the VM's "call/create stack"
data Frame
Frame :: FrameContext -> FrameState -> Frame
[$sel:context:Frame] :: Frame -> FrameContext
[$sel:state:Frame] :: Frame -> FrameState
-- | Call/create info
data FrameContext
CreationContext :: Addr -> Expr EWord -> Map Addr Contract -> SubState -> FrameContext
[$sel:address:CreationContext] :: FrameContext -> Addr
[$sel:codehash:CreationContext] :: FrameContext -> Expr EWord
[$sel:createreversion:CreationContext] :: FrameContext -> Map Addr Contract
[$sel:substate:CreationContext] :: FrameContext -> SubState
CallContext :: Addr -> Addr -> W256 -> W256 -> Expr EWord -> Maybe W256 -> Expr Buf -> (Map Addr Contract, Expr Storage) -> SubState -> FrameContext
[$sel:target:CreationContext] :: FrameContext -> Addr
[$sel:context:CreationContext] :: FrameContext -> Addr
[$sel:offset:CreationContext] :: FrameContext -> W256
[$sel:size:CreationContext] :: FrameContext -> W256
[$sel:codehash:CreationContext] :: FrameContext -> Expr EWord
[$sel:abi:CreationContext] :: FrameContext -> Maybe W256
[$sel:calldata:CreationContext] :: FrameContext -> Expr Buf
[$sel:callreversion:CreationContext] :: FrameContext -> (Map Addr Contract, Expr Storage)
[$sel:subState:CreationContext] :: FrameContext -> SubState
-- | The "accrued substate" across a transaction
data SubState
SubState :: [Addr] -> [Addr] -> Set Addr -> Set (Addr, W256) -> [(Addr, Word64)] -> SubState
[$sel:selfdestructs:SubState] :: SubState -> [Addr]
[$sel:touchedAccounts:SubState] :: SubState -> [Addr]
[$sel:accessedAddresses:SubState] :: SubState -> Set Addr
[$sel:accessedStorageKeys:SubState] :: SubState -> Set (Addr, W256)
[$sel:refunds:SubState] :: SubState -> [(Addr, Word64)]
-- | The "registers" of the VM along with memory and data stack
data FrameState
FrameState :: Addr -> Addr -> ContractCode -> {-# UNPACK #-} !Int -> [Expr EWord] -> Expr Buf -> Word64 -> Expr Buf -> Expr EWord -> Expr EWord -> {-# UNPACK #-} !Word64 -> Expr Buf -> Bool -> FrameState
[$sel:contract:FrameState] :: FrameState -> Addr
[$sel:codeContract:FrameState] :: FrameState -> Addr
[$sel:code:FrameState] :: FrameState -> ContractCode
[$sel:pc:FrameState] :: FrameState -> {-# UNPACK #-} !Int
[$sel:stack:FrameState] :: FrameState -> [Expr EWord]
[$sel:memory:FrameState] :: FrameState -> Expr Buf
[$sel:memorySize:FrameState] :: FrameState -> Word64
[$sel:calldata:FrameState] :: FrameState -> Expr Buf
[$sel:callvalue:FrameState] :: FrameState -> Expr EWord
[$sel:caller:FrameState] :: FrameState -> Expr EWord
[$sel:gas:FrameState] :: FrameState -> {-# UNPACK #-} !Word64
[$sel:returndata:FrameState] :: FrameState -> Expr Buf
[$sel:static:FrameState] :: FrameState -> Bool
-- | The state that spans a whole transaction
data TxState
TxState :: W256 -> Word64 -> W256 -> Addr -> Addr -> Expr EWord -> SubState -> Bool -> Map Addr Contract -> TxState
[$sel:gasprice:TxState] :: TxState -> W256
[$sel:gaslimit:TxState] :: TxState -> Word64
[$sel:priorityFee:TxState] :: TxState -> W256
[$sel:origin:TxState] :: TxState -> Addr
[$sel:toAddr:TxState] :: TxState -> Addr
[$sel:value:TxState] :: TxState -> Expr EWord
[$sel:substate:TxState] :: TxState -> SubState
[$sel:isCreate:TxState] :: TxState -> Bool
[$sel:txReversion:TxState] :: TxState -> Map Addr Contract
-- | When doing symbolic execution, we have three different ways to model
-- the storage of contracts. This determines not only the initial
-- contract storage model but also how RPC or state fetched contracts
-- will be modeled.
data StorageModel
-- | Uses Concrete Storage. Reading / Writing from abstract
-- locations causes a runtime failure. Can be nicely combined with RPC.
ConcreteS :: StorageModel
-- | Uses Symbolic Storage. Reading / Writing never reaches RPC,
-- but always done using an SMT array with no default value.
SymbolicS :: StorageModel
-- | Uses Symbolic Storage. Reading / Writing never reaches RPC,
-- but always done using an SMT array with 0 as the default value.
InitialS :: StorageModel
-- | Various environmental data
data Env
Env :: Map Addr Contract -> W256 -> Expr Storage -> Map W256 (Map W256 W256) -> Map W256 ByteString -> Env
[$sel:contracts:Env] :: Env -> Map Addr Contract
[$sel:chainId:Env] :: Env -> W256
[$sel:storage:Env] :: Env -> Expr Storage
[$sel:origStorage:Env] :: Env -> Map W256 (Map W256 W256)
[$sel:sha3Crack:Env] :: Env -> Map W256 ByteString
-- | Data about the block
data Block
Block :: Addr -> Expr EWord -> W256 -> W256 -> Word64 -> W256 -> W256 -> FeeSchedule Word64 -> Block
[$sel:coinbase:Block] :: Block -> Addr
[$sel:timestamp:Block] :: Block -> Expr EWord
[$sel:number:Block] :: Block -> W256
[$sel:prevRandao:Block] :: Block -> W256
[$sel:gaslimit:Block] :: Block -> Word64
[$sel:baseFee:Block] :: Block -> W256
[$sel:maxCodeSize:Block] :: Block -> W256
[$sel:schedule:Block] :: Block -> FeeSchedule Word64
-- | The state of a contract
data Contract
Contract :: ContractCode -> W256 -> W256 -> Expr EWord -> Vector Int -> Vector (Int, Op) -> Bool -> Contract
[$sel:contractcode:Contract] :: Contract -> ContractCode
[$sel:balance:Contract] :: Contract -> W256
[$sel:nonce:Contract] :: Contract -> W256
[$sel:codehash:Contract] :: Contract -> Expr EWord
[$sel:opIxMap:Contract] :: Contract -> Vector Int
[$sel:codeOps:Contract] :: Contract -> Vector (Int, Op)
[$sel:external:Contract] :: Contract -> Bool
-- | A unique id for a given pc
type CodeLocation = (Addr, Int)
-- | The cache is data that can be persisted for efficiency: any expensive
-- query that is constant at least within a block.
data Cache
Cache :: Map Addr Contract -> Map W256 (Map W256 W256) -> Map (CodeLocation, Int) Bool -> Cache
[$sel:fetchedContracts:Cache] :: Cache -> Map Addr Contract
[$sel:fetchedStorage:Cache] :: Cache -> Map W256 (Map W256 W256)
[$sel:path:Cache] :: Cache -> Map (CodeLocation, Int) Bool
unifyCachedStorage :: Map W256 W256 -> Map W256 W256 -> Map W256 W256
unifyCachedContract :: Contract -> Contract -> Contract
-- | 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...
data ContractCode
-- | Constructor code, during contract creation
InitCode :: ByteString -> Expr Buf -> ContractCode
-- | Instance code, after contract creation
RuntimeCode :: RuntimeCode -> ContractCode
-- | 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).
data RuntimeCode
ConcreteRuntimeCode :: ByteString -> RuntimeCode
SymbolicRuntimeCode :: Vector (Expr Byte) -> RuntimeCode
data Trace
Trace :: Int -> Contract -> TraceData -> Trace
[$sel:opIx:Trace] :: Trace -> Int
[$sel:contract:Trace] :: Trace -> Contract
[$sel:tracedata:Trace] :: Trace -> TraceData
data TraceData
EventTrace :: Expr EWord -> Expr Buf -> [Expr EWord] -> TraceData
FrameTrace :: FrameContext -> TraceData
ErrorTrace :: EvmError -> TraceData
EntryTrace :: Text -> TraceData
ReturnTrace :: Expr Buf -> FrameContext -> TraceData
-- | Wrapper type containing vm traces and the context needed to pretty
-- print them properly
data Traces
Traces :: Forest Trace -> Map Addr Contract -> Traces
[$sel:traces:Traces] :: Traces -> Forest Trace
[$sel:contracts:Traces] :: Traces -> Map Addr Contract
-- | A specification for an initial VM state
data VMOpts
VMOpts :: Contract -> (Expr Buf, [Prop]) -> Expr Storage -> Expr EWord -> W256 -> Addr -> Expr EWord -> Addr -> Word64 -> Word64 -> W256 -> Expr EWord -> Addr -> W256 -> W256 -> Word64 -> W256 -> W256 -> FeeSchedule Word64 -> W256 -> Bool -> Map Addr [W256] -> Bool -> VMOpts
[$sel:contract:VMOpts] :: VMOpts -> Contract
[$sel:calldata:VMOpts] :: VMOpts -> (Expr Buf, [Prop])
[$sel:initialStorage:VMOpts] :: VMOpts -> Expr Storage
[$sel:value:VMOpts] :: VMOpts -> Expr EWord
[$sel:priorityFee:VMOpts] :: VMOpts -> W256
[$sel:address:VMOpts] :: VMOpts -> Addr
[$sel:caller:VMOpts] :: VMOpts -> Expr EWord
[$sel:origin:VMOpts] :: VMOpts -> Addr
[$sel:gas:VMOpts] :: VMOpts -> Word64
[$sel:gaslimit:VMOpts] :: VMOpts -> Word64
[$sel:number:VMOpts] :: VMOpts -> W256
[$sel:timestamp:VMOpts] :: VMOpts -> Expr EWord
[$sel:coinbase:VMOpts] :: VMOpts -> Addr
[$sel:prevRandao:VMOpts] :: VMOpts -> W256
[$sel:maxCodeSize:VMOpts] :: VMOpts -> W256
[$sel:blockGaslimit:VMOpts] :: VMOpts -> Word64
[$sel:gasprice:VMOpts] :: VMOpts -> W256
[$sel:baseFee:VMOpts] :: VMOpts -> W256
[$sel:schedule:VMOpts] :: VMOpts -> FeeSchedule Word64
[$sel:chainId:VMOpts] :: VMOpts -> W256
[$sel:create:VMOpts] :: VMOpts -> Bool
[$sel:txAccessList:VMOpts] :: VMOpts -> Map Addr [W256]
[$sel:allowFFI:VMOpts] :: VMOpts -> Bool
type Op = GenericOp (Expr EWord)
data GenericOp a
OpStop :: GenericOp a
OpAdd :: GenericOp a
OpMul :: GenericOp a
OpSub :: GenericOp a
OpDiv :: GenericOp a
OpSdiv :: GenericOp a
OpMod :: GenericOp a
OpSmod :: GenericOp a
OpAddmod :: GenericOp a
OpMulmod :: GenericOp a
OpExp :: GenericOp a
OpSignextend :: GenericOp a
OpLt :: GenericOp a
OpGt :: GenericOp a
OpSlt :: GenericOp a
OpSgt :: GenericOp a
OpEq :: GenericOp a
OpIszero :: GenericOp a
OpAnd :: GenericOp a
OpOr :: GenericOp a
OpXor :: GenericOp a
OpNot :: GenericOp a
OpByte :: GenericOp a
OpShl :: GenericOp a
OpShr :: GenericOp a
OpSar :: GenericOp a
OpSha3 :: GenericOp a
OpAddress :: GenericOp a
OpBalance :: GenericOp a
OpOrigin :: GenericOp a
OpCaller :: GenericOp a
OpCallvalue :: GenericOp a
OpCalldataload :: GenericOp a
OpCalldatasize :: GenericOp a
OpCalldatacopy :: GenericOp a
OpCodesize :: GenericOp a
OpCodecopy :: GenericOp a
OpGasprice :: GenericOp a
OpExtcodesize :: GenericOp a
OpExtcodecopy :: GenericOp a
OpReturndatasize :: GenericOp a
OpReturndatacopy :: GenericOp a
OpExtcodehash :: GenericOp a
OpBlockhash :: GenericOp a
OpCoinbase :: GenericOp a
OpTimestamp :: GenericOp a
OpNumber :: GenericOp a
OpPrevRandao :: GenericOp a
OpGaslimit :: GenericOp a
OpChainid :: GenericOp a
OpSelfbalance :: GenericOp a
OpBaseFee :: GenericOp a
OpPop :: GenericOp a
OpMload :: GenericOp a
OpMstore :: GenericOp a
OpMstore8 :: GenericOp a
OpSload :: GenericOp a
OpSstore :: GenericOp a
OpJump :: GenericOp a
OpJumpi :: GenericOp a
OpPc :: GenericOp a
OpMsize :: GenericOp a
OpGas :: GenericOp a
OpJumpdest :: GenericOp a
OpCreate :: GenericOp a
OpCall :: GenericOp a
OpStaticcall :: GenericOp a
OpCallcode :: GenericOp a
OpReturn :: GenericOp a
OpDelegatecall :: GenericOp a
OpCreate2 :: GenericOp a
OpRevert :: GenericOp a
OpSelfdestruct :: GenericOp a
OpDup :: !Word8 -> GenericOp a
OpSwap :: !Word8 -> GenericOp a
OpLog :: !Word8 -> GenericOp a
OpPush0 :: GenericOp a
OpPush :: a -> GenericOp a
OpUnknown :: Word8 -> GenericOp a
-- |
-- https://docs.soliditylang.org/en/v0.8.19/abi-spec.html#function-selector
newtype FunctionSelector
FunctionSelector :: Word32 -> FunctionSelector
[$sel:unFunctionSelector:FunctionSelector] :: FunctionSelector -> Word32
newtype ByteStringS
ByteStringS :: ByteString -> ByteStringS
newtype W256
W256 :: Word256 -> W256
wordField :: Object -> Key -> Parser W256
newtype W64
W64 :: Word64 -> W64
word64Field :: Object -> Key -> Parser Word64
newtype Addr
Addr :: Word160 -> Addr
[$sel:addressWord160:Addr] :: Addr -> Word160
toChecksumAddress :: String -> String
addrField :: Object -> Key -> Parser Addr
addrFieldMaybe :: Object -> Key -> Parser (Maybe Addr)
-- | A four bit value
newtype Nibble
Nibble :: Word8 -> Nibble
toWord512 :: W256 -> Word512
fromWord512 :: Word512 -> W256
maybeLitByte :: Expr Byte -> Maybe Word8
maybeLitWord :: Expr EWord -> Maybe W256
word256 :: ByteString -> Word256
word :: ByteString -> W256
fromBE :: Integral a => ByteString -> a
asBE :: Integral a => a -> ByteString
word256Bytes :: W256 -> ByteString
word160Bytes :: Addr -> ByteString
hi :: Word8 -> Nibble
lo :: Word8 -> Nibble
toByte :: Nibble -> Nibble -> Word8
unpackNibbles :: ByteString -> [Nibble]
packNibbles :: [Nibble] -> ByteString
toWord64 :: W256 -> Maybe Word64
toInt :: W256 -> Maybe Int
bssToBs :: ByteStringS -> ByteString
keccakBytes :: ByteString -> ByteString
word32 :: [Word8] -> Word32
keccak :: Expr Buf -> Expr EWord
keccak' :: ByteString -> W256
abiKeccak :: ByteString -> FunctionSelector
internalError :: HasCallStack => [Char] -> a
concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
regexMatches :: Text -> Text -> Bool
readNull :: Read a => a -> String -> a
padLeft :: Int -> ByteString -> ByteString
padLeft' :: Int -> Vector (Expr Byte) -> Vector (Expr Byte)
padRight :: Int -> ByteString -> ByteString
padRight' :: Int -> String -> String
formatString :: ByteString -> String
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "baseFee" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Addr, b GHC.Types.~ EVM.Types.Addr) => Optics.Label.LabelOptic "coinbase" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "gaslimit" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "maxCodeSize" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "number" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "prevRandao" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.FeeSchedule.FeeSchedule GHC.Word.Word64, b GHC.Types.~ EVM.FeeSchedule.FeeSchedule GHC.Word.Word64) => Optics.Label.LabelOptic "schedule" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "timestamp" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "chainId" k EVM.Types.Env EVM.Types.Env a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract, b GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract) => Optics.Label.LabelOptic "contracts" k EVM.Types.Env EVM.Types.Env a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map EVM.Types.W256 (Data.Map.Internal.Map EVM.Types.W256 EVM.Types.W256), b GHC.Types.~ Data.Map.Internal.Map EVM.Types.W256 (Data.Map.Internal.Map EVM.Types.W256 EVM.Types.W256)) => Optics.Label.LabelOptic "origStorage" k EVM.Types.Env EVM.Types.Env a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map EVM.Types.W256 Data.ByteString.Internal.Type.ByteString, b GHC.Types.~ Data.Map.Internal.Map EVM.Types.W256 Data.ByteString.Internal.Type.ByteString) => Optics.Label.LabelOptic "sha3Crack" k EVM.Types.Env EVM.Types.Env a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Storage, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Storage) => Optics.Label.LabelOptic "storage" k EVM.Types.Env EVM.Types.Env a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "balance" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Vector.Vector (GHC.Types.Int, EVM.Types.Op), b GHC.Types.~ Data.Vector.Vector (GHC.Types.Int, EVM.Types.Op)) => Optics.Label.LabelOptic "codeOps" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "codehash" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.ContractCode, b GHC.Types.~ EVM.Types.ContractCode) => Optics.Label.LabelOptic "contractcode" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "external" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "nonce" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Vector.Storable.Vector GHC.Types.Int, b GHC.Types.~ Data.Vector.Storable.Vector GHC.Types.Int) => Optics.Label.LabelOptic "opIxMap" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ GHC.Maybe.Maybe EVM.Types.W256, b GHC.Types.~ GHC.Maybe.Maybe EVM.Types.W256) => Optics.Label.LabelOptic "abi" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.Addr, b GHC.Types.~ EVM.Types.Addr) => Optics.Label.LabelOptic "address" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf) => Optics.Label.LabelOptic "calldata" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ (Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract, EVM.Types.Expr 'EVM.Types.Storage), b GHC.Types.~ (Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract, EVM.Types.Expr 'EVM.Types.Storage)) => Optics.Label.LabelOptic "callreversion" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "codehash" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.Addr, b GHC.Types.~ EVM.Types.Addr) => Optics.Label.LabelOptic "context" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract, b GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract) => Optics.Label.LabelOptic "createreversion" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "offset" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "size" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.SubState, b GHC.Types.~ EVM.Types.SubState) => Optics.Label.LabelOptic "subState" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.SubState, b GHC.Types.~ EVM.Types.SubState) => Optics.Label.LabelOptic "substate" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.Addr, b GHC.Types.~ EVM.Types.Addr) => Optics.Label.LabelOptic "target" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.FrameContext, b GHC.Types.~ EVM.Types.FrameContext) => Optics.Label.LabelOptic "context" k EVM.Types.Frame EVM.Types.Frame a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.FrameState, b GHC.Types.~ EVM.Types.FrameState) => Optics.Label.LabelOptic "state" k EVM.Types.Frame EVM.Types.Frame a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Addr, b GHC.Types.~ EVM.Types.Addr) => Optics.Label.LabelOptic "address" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "allowFFI" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "baseFee" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "blockGaslimit" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ (EVM.Types.Expr 'EVM.Types.Buf, [EVM.Types.Prop]), b GHC.Types.~ (EVM.Types.Expr 'EVM.Types.Buf, [EVM.Types.Prop])) => Optics.Label.LabelOptic "calldata" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "caller" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "chainId" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Addr, b GHC.Types.~ EVM.Types.Addr) => Optics.Label.LabelOptic "coinbase" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Contract, b GHC.Types.~ EVM.Types.Contract) => Optics.Label.LabelOptic "contract" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "create" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "gas" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "gaslimit" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "gasprice" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Storage, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Storage) => Optics.Label.LabelOptic "initialStorage" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "maxCodeSize" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "number" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Addr, b GHC.Types.~ EVM.Types.Addr) => Optics.Label.LabelOptic "origin" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "prevRandao" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "priorityFee" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.FeeSchedule.FeeSchedule GHC.Word.Word64, b GHC.Types.~ EVM.FeeSchedule.FeeSchedule GHC.Word.Word64) => Optics.Label.LabelOptic "schedule" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "timestamp" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr [EVM.Types.W256], b GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr [EVM.Types.W256]) => Optics.Label.LabelOptic "txAccessList" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "value" k EVM.Types.VMOpts EVM.Types.VMOpts a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Contract, b GHC.Types.~ EVM.Types.Contract) => Optics.Label.LabelOptic "contract" k EVM.Types.Trace EVM.Types.Trace a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Int, b GHC.Types.~ GHC.Types.Int) => Optics.Label.LabelOptic "opIx" k EVM.Types.Trace EVM.Types.Trace a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.TraceData, b GHC.Types.~ EVM.Types.TraceData) => Optics.Label.LabelOptic "tracedata" k EVM.Types.Trace EVM.Types.Trace a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract, b GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract) => Optics.Label.LabelOptic "fetchedContracts" k EVM.Types.Cache EVM.Types.Cache a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map EVM.Types.W256 (Data.Map.Internal.Map EVM.Types.W256 EVM.Types.W256), b GHC.Types.~ Data.Map.Internal.Map EVM.Types.W256 (Data.Map.Internal.Map EVM.Types.W256 EVM.Types.W256)) => Optics.Label.LabelOptic "fetchedStorage" k EVM.Types.Cache EVM.Types.Cache a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map (EVM.Types.CodeLocation, GHC.Types.Int) GHC.Types.Bool, b GHC.Types.~ Data.Map.Internal.Map (EVM.Types.CodeLocation, GHC.Types.Int) GHC.Types.Bool) => Optics.Label.LabelOptic "path" k EVM.Types.Cache EVM.Types.Cache a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Set.Internal.Set EVM.Types.Addr, b GHC.Types.~ Data.Set.Internal.Set EVM.Types.Addr) => Optics.Label.LabelOptic "accessedAddresses" k EVM.Types.SubState EVM.Types.SubState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Set.Internal.Set (EVM.Types.Addr, EVM.Types.W256), b GHC.Types.~ Data.Set.Internal.Set (EVM.Types.Addr, EVM.Types.W256)) => Optics.Label.LabelOptic "accessedStorageKeys" k EVM.Types.SubState EVM.Types.SubState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [(EVM.Types.Addr, GHC.Word.Word64)], b GHC.Types.~ [(EVM.Types.Addr, GHC.Word.Word64)]) => Optics.Label.LabelOptic "refunds" k EVM.Types.SubState EVM.Types.SubState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Addr], b GHC.Types.~ [EVM.Types.Addr]) => Optics.Label.LabelOptic "selfdestructs" k EVM.Types.SubState EVM.Types.SubState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Addr], b GHC.Types.~ [EVM.Types.Addr]) => Optics.Label.LabelOptic "touchedAccounts" k EVM.Types.SubState EVM.Types.SubState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "gaslimit" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "gasprice" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "isCreate" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Addr, b GHC.Types.~ EVM.Types.Addr) => Optics.Label.LabelOptic "origin" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "priorityFee" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.SubState, b GHC.Types.~ EVM.Types.SubState) => Optics.Label.LabelOptic "substate" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Addr, b GHC.Types.~ EVM.Types.Addr) => Optics.Label.LabelOptic "toAddr" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract, b GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract) => Optics.Label.LabelOptic "txReversion" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "value" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf) => Optics.Label.LabelOptic "calldata" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "caller" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "callvalue" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.ContractCode, b GHC.Types.~ EVM.Types.ContractCode) => Optics.Label.LabelOptic "code" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Addr, b GHC.Types.~ EVM.Types.Addr) => Optics.Label.LabelOptic "codeContract" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Addr, b GHC.Types.~ EVM.Types.Addr) => Optics.Label.LabelOptic "contract" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "gas" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf) => Optics.Label.LabelOptic "memory" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "memorySize" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Int, b GHC.Types.~ GHC.Types.Int) => Optics.Label.LabelOptic "pc" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf) => Optics.Label.LabelOptic "returndata" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Expr 'EVM.Types.EWord], b GHC.Types.~ [EVM.Types.Expr 'EVM.Types.EWord]) => Optics.Label.LabelOptic "stack" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "static" k EVM.Types.FrameState EVM.Types.FrameState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "allowFFI" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Block, b GHC.Types.~ EVM.Types.Block) => Optics.Label.LabelOptic "block" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "burned" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Cache, b GHC.Types.~ EVM.Types.Cache) => Optics.Label.LabelOptic "cache" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Prop], b GHC.Types.~ [EVM.Types.Prop]) => Optics.Label.LabelOptic "constraints" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Env, b GHC.Types.~ EVM.Types.Env) => Optics.Label.LabelOptic "env" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Frame], b GHC.Types.~ [EVM.Types.Frame]) => Optics.Label.LabelOptic "frames" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map EVM.Types.CodeLocation (GHC.Types.Int, [EVM.Types.Expr 'EVM.Types.EWord]), b GHC.Types.~ Data.Map.Internal.Map EVM.Types.CodeLocation (GHC.Types.Int, [EVM.Types.Expr 'EVM.Types.EWord])) => Optics.Label.LabelOptic "iterations" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Prop], b GHC.Types.~ [EVM.Types.Prop]) => Optics.Label.LabelOptic "keccakEqs" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Expr 'EVM.Types.Log], b GHC.Types.~ [EVM.Types.Expr 'EVM.Types.Log]) => Optics.Label.LabelOptic "logs" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Maybe.Maybe EVM.Types.Addr, b GHC.Types.~ GHC.Maybe.Maybe EVM.Types.Addr) => Optics.Label.LabelOptic "overrideCaller" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Maybe.Maybe EVM.Types.VMResult, b GHC.Types.~ GHC.Maybe.Maybe EVM.Types.VMResult) => Optics.Label.LabelOptic "result" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.FrameState, b GHC.Types.~ EVM.Types.FrameState) => Optics.Label.LabelOptic "state" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Tree.Zipper.TreePos Data.Tree.Zipper.Empty EVM.Types.Trace, b GHC.Types.~ Data.Tree.Zipper.TreePos Data.Tree.Zipper.Empty EVM.Types.Trace) => Optics.Label.LabelOptic "traces" k EVM.Types.VM EVM.Types.VM a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.TxState, b GHC.Types.~ EVM.Types.TxState) => Optics.Label.LabelOptic "tx" k EVM.Types.VM EVM.Types.VM a b
instance GHC.Generics.Generic EVM.Types.Word512
instance Data.Data.Data EVM.Types.Word512
instance GHC.Generics.Generic EVM.Types.Int512
instance Data.Data.Data EVM.Types.Int512
instance GHC.Show.Show EVM.Types.BranchCondition
instance GHC.Show.Show EVM.Types.StorageModel
instance GHC.Read.Read EVM.Types.StorageModel
instance GHC.Base.Functor EVM.Types.GenericOp
instance GHC.Classes.Ord a => GHC.Classes.Ord (EVM.Types.GenericOp a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (EVM.Types.GenericOp a)
instance GHC.Show.Show a => GHC.Show.Show (EVM.Types.GenericOp a)
instance GHC.Real.Integral EVM.Types.FunctionSelector
instance GHC.Enum.Enum EVM.Types.FunctionSelector
instance GHC.Real.Real EVM.Types.FunctionSelector
instance GHC.Classes.Ord EVM.Types.FunctionSelector
instance GHC.Classes.Eq EVM.Types.FunctionSelector
instance GHC.Num.Num EVM.Types.FunctionSelector
instance GHC.Bits.Bits EVM.Types.FunctionSelector
instance GHC.Generics.Generic EVM.Types.ByteStringS
instance GHC.Classes.Eq EVM.Types.ByteStringS
instance GHC.Enum.Bounded EVM.Types.W256
instance GHC.Classes.Eq EVM.Types.W256
instance GHC.Enum.Enum EVM.Types.W256
instance GHC.Bits.FiniteBits EVM.Types.W256
instance GHC.Generics.Generic EVM.Types.W256
instance GHC.Bits.Bits EVM.Types.W256
instance GHC.Classes.Ord EVM.Types.W256
instance GHC.Real.Real EVM.Types.W256
instance GHC.Real.Integral EVM.Types.W256
instance GHC.Num.Num EVM.Types.W256
instance GHC.Enum.Bounded EVM.Types.W64
instance GHC.Classes.Eq EVM.Types.W64
instance GHC.Enum.Enum EVM.Types.W64
instance GHC.Bits.FiniteBits EVM.Types.W64
instance GHC.Bits.Bits EVM.Types.W64
instance GHC.Generics.Generic EVM.Types.W64
instance GHC.Classes.Ord EVM.Types.W64
instance GHC.Real.Real EVM.Types.W64
instance GHC.Real.Integral EVM.Types.W64
instance GHC.Num.Num EVM.Types.W64
instance GHC.Bits.FiniteBits EVM.Types.Addr
instance GHC.Bits.Bits EVM.Types.Addr
instance GHC.Generics.Generic EVM.Types.Addr
instance GHC.Classes.Eq EVM.Types.Addr
instance GHC.Enum.Enum EVM.Types.Addr
instance GHC.Classes.Ord EVM.Types.Addr
instance GHC.Real.Real EVM.Types.Addr
instance GHC.Real.Integral EVM.Types.Addr
instance GHC.Num.Num EVM.Types.Addr
instance GHC.Show.Show EVM.Types.SubState
instance GHC.Classes.Ord EVM.Types.SubState
instance GHC.Classes.Eq EVM.Types.SubState
instance GHC.Classes.Ord EVM.Types.EvmError
instance GHC.Classes.Eq EVM.Types.EvmError
instance GHC.Show.Show EVM.Types.EvmError
instance GHC.Classes.Ord EVM.Types.RuntimeCode
instance GHC.Classes.Eq EVM.Types.RuntimeCode
instance GHC.Show.Show EVM.Types.RuntimeCode
instance GHC.Classes.Ord EVM.Types.ContractCode
instance GHC.Show.Show EVM.Types.ContractCode
instance GHC.Show.Show EVM.Types.Contract
instance GHC.Classes.Ord EVM.Types.Contract
instance GHC.Classes.Eq EVM.Types.Contract
instance GHC.Generics.Generic EVM.Types.FrameContext
instance GHC.Show.Show EVM.Types.FrameContext
instance GHC.Classes.Ord EVM.Types.FrameContext
instance GHC.Classes.Eq EVM.Types.FrameContext
instance GHC.Generics.Generic EVM.Types.TraceData
instance GHC.Show.Show EVM.Types.TraceData
instance GHC.Classes.Ord EVM.Types.TraceData
instance GHC.Classes.Eq EVM.Types.TraceData
instance GHC.Generics.Generic EVM.Types.Trace
instance GHC.Show.Show EVM.Types.Trace
instance GHC.Classes.Ord EVM.Types.Trace
instance GHC.Classes.Eq EVM.Types.Trace
instance GHC.Generics.Generic EVM.Types.Traces
instance GHC.Show.Show EVM.Types.Traces
instance GHC.Classes.Ord EVM.Types.Traces
instance GHC.Classes.Eq EVM.Types.Traces
instance GHC.Classes.Ord EVM.Types.PartialExec
instance GHC.Classes.Eq EVM.Types.PartialExec
instance GHC.Show.Show EVM.Types.PartialExec
instance GHC.Generics.Generic EVM.Types.Cache
instance GHC.Show.Show EVM.Types.Cache
instance GHC.Generics.Generic EVM.Types.Block
instance GHC.Show.Show EVM.Types.Block
instance GHC.Generics.Generic EVM.Types.Env
instance GHC.Show.Show EVM.Types.Env
instance GHC.Show.Show EVM.Types.TxState
instance GHC.Generics.Generic EVM.Types.FrameState
instance GHC.Show.Show EVM.Types.FrameState
instance GHC.Show.Show EVM.Types.Frame
instance GHC.Show.Show EVM.Types.VMOpts
instance GHC.Generics.Generic EVM.Types.VM
instance GHC.Show.Show EVM.Types.VM
instance GHC.Generics.Generic EVM.Types.Nibble
instance GHC.Enum.Bounded EVM.Types.Nibble
instance GHC.Classes.Eq EVM.Types.Nibble
instance GHC.Enum.Enum EVM.Types.Nibble
instance GHC.Classes.Ord EVM.Types.Nibble
instance GHC.Real.Real EVM.Types.Nibble
instance GHC.Real.Integral EVM.Types.Nibble
instance GHC.Num.Num EVM.Types.Nibble
instance GHC.Show.Show (EVM.Types.GVar a)
instance GHC.Classes.Eq (EVM.Types.GVar a)
instance GHC.Classes.Ord (EVM.Types.GVar a)
instance GHC.Show.Show (EVM.Types.Expr a)
instance GHC.Classes.Eq (EVM.Types.Expr a)
instance GHC.Classes.Ord (EVM.Types.Expr a)
instance GHC.Show.Show EVM.Types.SomeExpr
instance GHC.Show.Show EVM.Types.Prop
instance GHC.Show.Show EVM.Types.Effect
instance GHC.Show.Show EVM.Types.VMResult
instance Witch.From.From EVM.Types.Nibble GHC.Types.Int
instance GHC.Show.Show EVM.Types.Nibble
instance GHC.Show.Show EVM.Types.Query
instance GHC.Show.Show EVM.Types.Choose
instance GHC.Base.Semigroup EVM.Types.Cache
instance GHC.Base.Monoid EVM.Types.Cache
instance GHC.Classes.Eq EVM.Types.SomeExpr
instance GHC.Classes.Ord EVM.Types.SomeExpr
instance GHC.Classes.Eq EVM.Types.Prop
instance GHC.Classes.Ord EVM.Types.Prop
instance GHC.Classes.Eq EVM.Types.ContractCode
instance GHC.Base.Semigroup EVM.Types.Traces
instance GHC.Base.Monoid EVM.Types.Traces
instance Witch.From.From EVM.Types.Addr GHC.Num.Integer.Integer
instance Witch.From.From EVM.Types.Addr EVM.Types.W256
instance Witch.TryFrom.TryFrom EVM.Types.W256 EVM.Types.Addr
instance GHC.Read.Read EVM.Types.Addr
instance GHC.Show.Show EVM.Types.Addr
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Types.Addr
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Types.Addr
instance Data.Aeson.Types.ToJSON.ToJSONKey EVM.Types.Addr
instance Data.Aeson.Types.FromJSON.FromJSONKey EVM.Types.Addr
instance Options.Generic.ParseField EVM.Types.Addr
instance Options.Generic.ParseFields EVM.Types.Addr
instance Options.Generic.ParseRecord EVM.Types.Addr
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Types.W64
instance GHC.Read.Read EVM.Types.W64
instance GHC.Show.Show EVM.Types.W64
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Types.W64
instance Witch.From.From EVM.Types.W256 GHC.Num.Integer.Integer
instance Witch.From.From GHC.Word.Word8 EVM.Types.W256
instance Witch.From.From GHC.Word.Word32 EVM.Types.W256
instance Witch.From.From GHC.Word.Word64 EVM.Types.W256
instance Witch.From.From Data.DoubleWord.Word256 EVM.Types.W256
instance Witch.TryFrom.TryFrom GHC.Types.Int EVM.Types.W256
instance Witch.TryFrom.TryFrom Data.DoubleWord.Int256 EVM.Types.W256
instance Witch.TryFrom.TryFrom GHC.Num.Integer.Integer EVM.Types.W256
instance Witch.TryFrom.TryFrom EVM.Types.W256 EVM.Types.FunctionSelector
instance Witch.TryFrom.TryFrom EVM.Types.W256 GHC.Types.Int
instance Witch.TryFrom.TryFrom EVM.Types.W256 GHC.Int.Int64
instance Witch.TryFrom.TryFrom EVM.Types.W256 Data.DoubleWord.Int256
instance Witch.TryFrom.TryFrom EVM.Types.W256 GHC.Word.Word8
instance Witch.TryFrom.TryFrom EVM.Types.W256 GHC.Word.Word32
instance Witch.TryFrom.TryFrom EVM.Types.W256 GHC.Word.Word64
instance Witch.TryFrom.TryFrom EVM.Types.Word512 EVM.Types.W256
instance GHC.Read.Read EVM.Types.W256
instance GHC.Show.Show EVM.Types.W256
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Types.W256
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Types.W256
instance Data.Aeson.Types.FromJSON.FromJSONKey EVM.Types.W256
instance Options.Generic.ParseField EVM.Types.W256
instance Options.Generic.ParseFields EVM.Types.W256
instance Options.Generic.ParseRecord EVM.Types.W256
instance GHC.Show.Show EVM.Types.ByteStringS
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Types.ByteStringS
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Types.ByteStringS
instance GHC.Show.Show EVM.Types.FunctionSelector
instance Options.Generic.ParseField EVM.Types.StorageModel
instance Data.BinaryWord.BinaryWord EVM.Types.Word512
instance Data.DoubleWord.Base.DoubleWord EVM.Types.Int512
instance GHC.Classes.Eq EVM.Types.Int512
instance GHC.Classes.Ord EVM.Types.Int512
instance GHC.Enum.Bounded EVM.Types.Int512
instance GHC.Enum.Enum EVM.Types.Int512
instance GHC.Num.Num EVM.Types.Int512
instance GHC.Real.Real EVM.Types.Int512
instance GHC.Real.Integral EVM.Types.Int512
instance GHC.Show.Show EVM.Types.Int512
instance GHC.Read.Read EVM.Types.Int512
instance Data.Hashable.Class.Hashable EVM.Types.Int512
instance GHC.Ix.Ix EVM.Types.Int512
instance GHC.Bits.Bits EVM.Types.Int512
instance GHC.Bits.FiniteBits EVM.Types.Int512
instance Data.BinaryWord.BinaryWord EVM.Types.Int512
instance Data.DoubleWord.Base.DoubleWord EVM.Types.Word512
instance GHC.Classes.Eq EVM.Types.Word512
instance GHC.Classes.Ord EVM.Types.Word512
instance GHC.Enum.Bounded EVM.Types.Word512
instance GHC.Enum.Enum EVM.Types.Word512
instance GHC.Num.Num EVM.Types.Word512
instance GHC.Real.Real EVM.Types.Word512
instance GHC.Real.Integral EVM.Types.Word512
instance GHC.Show.Show EVM.Types.Word512
instance GHC.Read.Read EVM.Types.Word512
instance Data.Hashable.Class.Hashable EVM.Types.Word512
instance GHC.Ix.Ix EVM.Types.Word512
instance GHC.Bits.Bits EVM.Types.Word512
instance GHC.Bits.FiniteBits EVM.Types.Word512
instance Witch.From.From Data.DoubleWord.Int256 GHC.Num.Integer.Integer
instance Witch.From.From GHC.Word.Word8 Data.DoubleWord.Word256
instance Witch.From.From GHC.Word.Word32 Data.DoubleWord.Word256
instance Witch.From.From Data.DoubleWord.Word256 GHC.Num.Integer.Integer
instance Witch.TryFrom.TryFrom GHC.Types.Int Data.DoubleWord.Word256
instance Witch.TryFrom.TryFrom Data.DoubleWord.Word160 GHC.Word.Word8
instance Witch.TryFrom.TryFrom Data.DoubleWord.Word256 GHC.Types.Int
instance Witch.TryFrom.TryFrom Data.DoubleWord.Word256 Data.DoubleWord.Int256
instance Witch.TryFrom.TryFrom Data.DoubleWord.Word256 GHC.Word.Word8
instance Witch.TryFrom.TryFrom Data.DoubleWord.Word256 GHC.Word.Word32
module EVM.Traversals
foldProp :: forall b. Monoid b => (forall a. Expr a -> b) -> b -> Prop -> b
foldTrace :: forall b. Monoid b => (forall a. Expr a -> b) -> b -> Trace -> b
foldTraces :: forall b. Monoid b => (forall a. Expr a -> b) -> b -> Traces -> b
-- | Recursively folds a given function over a given expression Recursion
-- schemes do this & a lot more, but defining them over GADT's isn't
-- worth the hassle
foldExpr :: forall b c. Monoid b => (forall a. Expr a -> b) -> b -> Expr c -> b
mapProp :: (forall a. Expr a -> Expr a) -> Prop -> Prop
mapTrace :: (forall a. Expr a -> Expr a) -> Trace -> Trace
-- | Recursively applies a given function to every node in a given expr
-- instance Recursion schemes do this & a lot more, but defining them
-- over GADT's isn't worth the hassle
mapExpr :: (forall a. Expr a -> Expr a) -> Expr b -> Expr b
mapExprM :: Monad m => (forall a. Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapPropM :: Monad m => (forall a. Expr a -> m (Expr a)) -> Prop -> m Prop
mapTracesM :: forall m. Monad m => (forall a. Expr a -> m (Expr a)) -> Traces -> m Traces
mapTraceM :: forall m. Monad m => (forall a. Expr a -> m (Expr a)) -> Trace -> m Trace
-- | Generic operations over AST terms
class TraversableTerm a
mapTerm :: TraversableTerm a => (forall b. Expr b -> Expr b) -> a -> a
foldTerm :: forall c. (TraversableTerm a, Monoid c) => (forall b. Expr b -> c) -> c -> a -> c
instance EVM.Traversals.TraversableTerm (EVM.Types.Expr a)
instance EVM.Traversals.TraversableTerm EVM.Types.Prop
module EVM.RLP
data RLP
BS :: ByteString -> RLP
List :: [RLP] -> RLP
slice :: Int -> Int -> ByteString -> ByteString
itemInfo :: ByteString -> (Int, Int, Bool, Bool)
rlpdecode :: ByteString -> Maybe RLP
rlplengths :: ByteString -> Int -> Int -> [(Int, Int)]
rlpencode :: RLP -> ByteString
encodeLen :: Int -> ByteString -> ByteString
rlpList :: [RLP] -> ByteString
octets :: W256 -> ByteString
octetsFull :: Int -> W256 -> ByteString
octets160 :: Addr -> ByteString
rlpWord256 :: W256 -> RLP
rlpWordFull :: W256 -> RLP
rlpAddrFull :: Addr -> RLP
rlpWord160 :: Addr -> RLP
instance GHC.Classes.Eq EVM.RLP.RLP
instance GHC.Show.Show EVM.RLP.RLP
module EVM.Patricia
data KV k v a
Put :: k -> v -> a -> KV k v a
Get :: k -> (v -> a) -> KV k v a
newtype DB k v a
DB :: Free (KV k v) a -> DB k v a
insertDB :: k -> v -> DB k v ()
lookupDB :: k -> DB k v v
runDB :: Monad m => (k -> v -> m ()) -> (k -> m v) -> DB k v a -> m a
type Path = [Nibble]
data Ref
Hash :: ByteString -> Ref
Literal :: Node -> Ref
data Node
Empty :: Node
Shortcut :: Path -> Either Ref ByteString -> Node
Full :: Seq Ref -> ByteString -> Node
encodePath :: Path -> Bool -> ByteString
rlpRef :: Ref -> RLP
rlpNode :: Node -> RLP
type NodeDB = DB ByteString Node
putNode :: Node -> NodeDB Ref
getNode :: Ref -> NodeDB Node
lookupPath :: Ref -> Path -> NodeDB ByteString
getVal :: Path -> Node -> NodeDB ByteString
emptyRef :: Ref
emptyRefs :: Seq Ref
addPrefix :: Path -> Node -> NodeDB Node
insertRef :: Ref -> Path -> ByteString -> NodeDB Ref
update :: Node -> Path -> ByteString -> NodeDB Node
delete :: Node -> Path -> NodeDB Node
insert :: Ref -> ByteString -> ByteString -> NodeDB Ref
lookupIn :: Ref -> ByteString -> NodeDB ByteString
type Trie = StateT Ref NodeDB
runTrie :: DB ByteString ByteString a -> Trie a
type MapDB k v a = StateT (Map k v) Maybe a
runMapDB :: Ord k => DB k v a -> MapDB k v a
insertValues :: [(ByteString, ByteString)] -> Maybe Ref
calcRoot :: [(ByteString, ByteString)] -> Maybe ByteString
instance GHC.Base.Functor (EVM.Patricia.KV k v)
instance GHC.Base.Monad (EVM.Patricia.DB k v)
instance GHC.Base.Applicative (EVM.Patricia.DB k v)
instance GHC.Base.Functor (EVM.Patricia.DB k v)
instance GHC.Classes.Eq EVM.Patricia.Ref
instance GHC.Classes.Eq EVM.Patricia.Node
instance GHC.Show.Show EVM.Patricia.Node
instance GHC.Show.Show (EVM.Patricia.NodeDB EVM.Patricia.Node)
instance GHC.Show.Show EVM.Patricia.Ref
module EVM.Keccak
keccakAssumptions :: [Prop] -> [Expr Buf] -> [Expr Storage] -> [Prop]
instance GHC.Show.Show EVM.Keccak.BuilderState
-- | Helper functions for working with Expr instances. All functions here
-- will return a concrete result if given a concrete input.
module EVM.Expr
op1 :: (Expr EWord -> Expr EWord) -> (W256 -> W256) -> Expr EWord -> Expr EWord
op2 :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord
op3 :: (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
-- | If a given binary op is commutative, then we always force Lits to the
-- lhs if only one argument is a Lit. This makes writing pattern matches
-- in the simplifier easier.
normArgs :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord
add :: Expr EWord -> Expr EWord -> Expr EWord
sub :: Expr EWord -> Expr EWord -> Expr EWord
mul :: Expr EWord -> Expr EWord -> Expr EWord
div :: Expr EWord -> Expr EWord -> Expr EWord
sdiv :: Expr EWord -> Expr EWord -> Expr EWord
mod :: Expr EWord -> Expr EWord -> Expr EWord
smod :: Expr EWord -> Expr EWord -> Expr EWord
addmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
mulmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
exp :: Expr EWord -> Expr EWord -> Expr EWord
sex :: Expr EWord -> Expr EWord -> Expr EWord
lt :: Expr EWord -> Expr EWord -> Expr EWord
gt :: Expr EWord -> Expr EWord -> Expr EWord
leq :: Expr EWord -> Expr EWord -> Expr EWord
geq :: Expr EWord -> Expr EWord -> Expr EWord
slt :: Expr EWord -> Expr EWord -> Expr EWord
sgt :: Expr EWord -> Expr EWord -> Expr EWord
eq :: Expr EWord -> Expr EWord -> Expr EWord
iszero :: Expr EWord -> Expr EWord
and :: Expr EWord -> Expr EWord -> Expr EWord
or :: Expr EWord -> Expr EWord -> Expr EWord
xor :: Expr EWord -> Expr EWord -> Expr EWord
not :: Expr EWord -> Expr EWord
shl :: Expr EWord -> Expr EWord -> Expr EWord
shr :: Expr EWord -> Expr EWord -> Expr EWord
sar :: Expr EWord -> Expr EWord -> Expr EWord
-- | Extracts the byte at a given index from a Buf.
--
-- We do our best to return a concrete value wherever possible, but
-- fallback to an abstract expresion if nescessary. Note that a Buf is an
-- infinite structure, so reads outside of the bounds of a ConcreteBuf
-- return 0. This is inline with the semantics of calldata and memory,
-- but not of returndata.
readByte :: Expr EWord -> Expr Buf -> Expr Byte
-- | Reads n bytes starting from idx in buf and returns a left padded word
--
-- If n is >= 32 this is the same as readWord
readBytes :: Int -> Expr EWord -> Expr Buf -> Expr EWord
-- | Reads the word starting at idx from the given buf
readWord :: Expr EWord -> Expr Buf -> Expr EWord
readWordFromBytes :: Expr EWord -> Expr Buf -> Expr EWord
-- | Copies a slice of src into dst.
--
-- 0 srcOffset srcOffset + size length src
-- ┌--------------┬------------------┬-----------------┐ src: | | ------
-- sl ------ | | └--------------┴------------------┴-----------------┘
--
-- 0 dstOffset dstOffset + size length dst
-- ┌--------┬------------------┬-----------------┐ dst: | hd | | tl |
-- └--------┴------------------┴-----------------┘
maxBytes :: W256
copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf -> Expr Buf
writeByte :: Expr EWord -> Expr Byte -> Expr Buf -> Expr Buf
writeWord :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf
-- | Returns the length of a given buffer
--
-- If there are any writes to abstract locations, or CopySlices with an
-- abstract size or dstOffset, an abstract expresion will be returned.
bufLength :: Expr Buf -> Expr EWord
bufLengthEnv :: Map Int (Expr Buf) -> Bool -> Expr Buf -> Expr EWord
-- | If a buffer has a concrete prefix, we return it's length here
concPrefix :: Expr Buf -> Maybe Integer
-- | Return the minimum possible length of a buffer. In the case of an
-- abstract buffer, it is the largest write that is made on a concrete
-- location. Parameterized by an environment for buffer variables.
minLength :: Map Int (Expr Buf) -> Expr Buf -> Maybe Integer
word256At :: Expr EWord -> Lens (Expr Buf) (Expr Buf) (Expr EWord) (Expr EWord)
-- | Returns the first n bytes of buf
take :: W256 -> Expr Buf -> Expr Buf
-- | Returns everything but the first n bytes of buf
drop :: W256 -> Expr Buf -> Expr Buf
slice :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf
toList :: Expr Buf -> Maybe (Vector (Expr Byte))
fromList :: Vector (Expr Byte) -> Expr Buf
-- | Removes any irrelevant writes when reading from a buffer
simplifyReads :: Expr a -> Expr a
-- | Strips writes from the buffer that can be statically determined to be
-- out of range TODO: are the bounds here correct? I think there might be
-- some off by one mistakes...
stripWrites :: W256 -> W256 -> Expr Buf -> Expr Buf
-- | Reads the word at the given slot from the given storage expression.
--
-- Note that we return a Nothing instead of a 0x0 if we are reading from
-- a store that is backed by a ConcreteStore or an EmptyStore and there
-- have been no explicit writes to the requested slot. This makes
-- implementing rpc storage lookups much easier. If the store is backed
-- by an AbstractStore we always return a symbolic value.
readStorage :: Expr EWord -> Expr EWord -> Expr Storage -> Maybe (Expr EWord)
readStorage' :: Expr EWord -> Expr EWord -> Expr Storage -> Expr EWord
-- | Writes a value to a key in a storage expression.
--
-- Concrete writes on top of a concrete or empty store will produce a new
-- ConcreteStore, otherwise we add a new write to the storage expression.
writeStorage :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Storage -> Expr Storage
-- | Simple recursive match based AST simplification Note: may not
-- terminate!
simplify :: Expr a -> Expr a
litAddr :: Addr -> Expr EWord
exprToAddr :: Expr EWord -> Maybe Addr
litCode :: ByteString -> [Expr Byte]
to512 :: W256 -> Word512
isLitByte :: Expr Byte -> Bool
isLitWord :: Expr EWord -> Bool
-- | Returns the byte at idx from the given word.
indexWord :: Expr EWord -> Expr EWord -> Expr Byte
padByte :: Expr Byte -> Expr EWord
-- | Converts a list of bytes into a W256. TODO: semantics if the input is
-- too large?
bytesToW256 :: [Word8] -> W256
padBytesLeft :: Int -> [Expr Byte] -> [Expr Byte]
joinBytes :: [Expr Byte] -> Expr EWord
eqByte :: Expr Byte -> Expr Byte -> Expr EWord
min :: Expr EWord -> Expr EWord -> Expr EWord
max :: Expr EWord -> Expr EWord -> Expr EWord
numBranches :: Expr End -> Int
allLit :: [Expr Byte] -> Bool
-- | True if the given expression contains any node that satisfies the
-- input predicate
containsNode :: (forall a. Expr a -> Bool) -> Expr b -> Bool
inRange :: Int -> Expr EWord -> Prop
instance GHC.Base.Semigroup (EVM.Types.Expr 'EVM.Types.Buf)
instance GHC.Base.Monoid (EVM.Types.Expr 'EVM.Types.Buf)
module EVM.Op
type Op = GenericOp (Expr EWord)
data GenericOp a
OpStop :: GenericOp a
OpAdd :: GenericOp a
OpMul :: GenericOp a
OpSub :: GenericOp a
OpDiv :: GenericOp a
OpSdiv :: GenericOp a
OpMod :: GenericOp a
OpSmod :: GenericOp a
OpAddmod :: GenericOp a
OpMulmod :: GenericOp a
OpExp :: GenericOp a
OpSignextend :: GenericOp a
OpLt :: GenericOp a
OpGt :: GenericOp a
OpSlt :: GenericOp a
OpSgt :: GenericOp a
OpEq :: GenericOp a
OpIszero :: GenericOp a
OpAnd :: GenericOp a
OpOr :: GenericOp a
OpXor :: GenericOp a
OpNot :: GenericOp a
OpByte :: GenericOp a
OpShl :: GenericOp a
OpShr :: GenericOp a
OpSar :: GenericOp a
OpSha3 :: GenericOp a
OpAddress :: GenericOp a
OpBalance :: GenericOp a
OpOrigin :: GenericOp a
OpCaller :: GenericOp a
OpCallvalue :: GenericOp a
OpCalldataload :: GenericOp a
OpCalldatasize :: GenericOp a
OpCalldatacopy :: GenericOp a
OpCodesize :: GenericOp a
OpCodecopy :: GenericOp a
OpGasprice :: GenericOp a
OpExtcodesize :: GenericOp a
OpExtcodecopy :: GenericOp a
OpReturndatasize :: GenericOp a
OpReturndatacopy :: GenericOp a
OpExtcodehash :: GenericOp a
OpBlockhash :: GenericOp a
OpCoinbase :: GenericOp a
OpTimestamp :: GenericOp a
OpNumber :: GenericOp a
OpPrevRandao :: GenericOp a
OpGaslimit :: GenericOp a
OpChainid :: GenericOp a
OpSelfbalance :: GenericOp a
OpBaseFee :: GenericOp a
OpPop :: GenericOp a
OpMload :: GenericOp a
OpMstore :: GenericOp a
OpMstore8 :: GenericOp a
OpSload :: GenericOp a
OpSstore :: GenericOp a
OpJump :: GenericOp a
OpJumpi :: GenericOp a
OpPc :: GenericOp a
OpMsize :: GenericOp a
OpGas :: GenericOp a
OpJumpdest :: GenericOp a
OpCreate :: GenericOp a
OpCall :: GenericOp a
OpStaticcall :: GenericOp a
OpCallcode :: GenericOp a
OpReturn :: GenericOp a
OpDelegatecall :: GenericOp a
OpCreate2 :: GenericOp a
OpRevert :: GenericOp a
OpSelfdestruct :: GenericOp a
OpDup :: !Word8 -> GenericOp a
OpSwap :: !Word8 -> GenericOp a
OpLog :: !Word8 -> GenericOp a
OpPush0 :: GenericOp a
OpPush :: a -> GenericOp a
OpUnknown :: Word8 -> GenericOp a
opString :: (Integral a, Show a) => (a, Op) -> String
intToOpName :: Int -> String
getOp :: Word8 -> GenericOp Word8
readOp :: Word8 -> [Expr Byte] -> Op
module EVM.Concrete
wordAt :: Int -> ByteString -> W256
readByteOrZero :: Int -> ByteString -> Word8
byteStringSliceWithDefaultZeroes :: Int -> Int -> ByteString -> ByteString
sliceMemory :: W256 -> W256 -> ByteString -> ByteString
writeMemory :: ByteString -> W256 -> W256 -> W256 -> ByteString -> ByteString
(^) :: W256 -> W256 -> W256
createAddress :: Addr -> W256 -> Addr
create2Address :: Addr -> W256 -> ByteString -> Addr
module EVM.CSE
type BufEnv = Map Int (Expr Buf)
type StoreEnv = Map Int (Expr Storage)
eliminateExpr :: Expr a -> (Expr a, BufEnv, StoreEnv)
-- | Common subexpression elimination pass for list of Prop
eliminateProps :: [Prop] -> ([Prop], BufEnv, StoreEnv)
instance GHC.Show.Show EVM.CSE.BuilderState
module EVM.SMT
data CexVars
CexVars :: [Text] -> Map Text (Expr EWord) -> [(Expr EWord, Expr EWord)] -> [Text] -> [Text] -> CexVars
[$sel:calldata:CexVars] :: CexVars -> [Text]
[$sel:buffers:CexVars] :: CexVars -> Map Text (Expr EWord)
[$sel:storeReads:CexVars] :: CexVars -> [(Expr EWord, Expr EWord)]
[$sel:blockContext:CexVars] :: CexVars -> [Text]
[$sel:txContext:CexVars] :: CexVars -> [Text]
-- | A model for a buffer, either in it's compressed form (for storing
-- parsed models from a solver), or as a bytestring (for presentation to
-- users)
data BufModel
Comp :: CompressedBuf -> BufModel
Flat :: ByteString -> BufModel
-- | This representation lets us store buffers of arbitrary length without
-- exhausting the available memory, it closely matches the format used by
-- smt-lib when returning models for arrays
data CompressedBuf
Base :: Word8 -> W256 -> CompressedBuf
[$sel:byte:Base] :: CompressedBuf -> Word8
[$sel:length:Base] :: CompressedBuf -> W256
Write :: Word8 -> W256 -> CompressedBuf -> CompressedBuf
[$sel:byte:Base] :: CompressedBuf -> Word8
[$sel:idx:Base] :: CompressedBuf -> W256
[$sel:next:Base] :: CompressedBuf -> CompressedBuf
-- | a final post shrinking cex, buffers here are all represented as
-- concrete bytestrings
data SMTCex
SMTCex :: Map (Expr EWord) W256 -> Map (Expr Buf) BufModel -> Map W256 (Map W256 W256) -> Map (Expr EWord) W256 -> Map (Expr EWord) W256 -> SMTCex
[$sel:vars:SMTCex] :: SMTCex -> Map (Expr EWord) W256
[$sel:buffers:SMTCex] :: SMTCex -> Map (Expr Buf) BufModel
[$sel:store:SMTCex] :: SMTCex -> Map W256 (Map W256 W256)
[$sel:blockContext:SMTCex] :: SMTCex -> Map (Expr EWord) W256
[$sel:txContext:SMTCex] :: SMTCex -> Map (Expr EWord) W256
flattenBufs :: SMTCex -> Maybe SMTCex
-- | Attemps to collapse a compressed buffer representation down to a
-- flattened one
collapse :: BufModel -> Maybe BufModel
getVar :: SMTCex -> Text -> W256
data SMT2
SMT2 :: [Builder] -> CexVars -> SMT2
formatSMT2 :: SMT2 -> Text
-- | Reads all intermediate variables from the builder state and produces
-- SMT declaring them as constants
declareIntermediates :: BufEnv -> StoreEnv -> SMT2
assertProps :: [Prop] -> SMT2
referencedBufsGo :: Expr a -> [Builder]
referencedBufs :: Expr a -> [Builder]
referencedBufs' :: Prop -> [Builder]
referencedVarsGo :: Expr a -> [Builder]
referencedVars :: Expr a -> [Builder]
referencedVars' :: Prop -> [Builder]
referencedFrameContextGo :: Expr a -> [(Builder, [Prop])]
referencedFrameContext :: Expr a -> [(Builder, [Prop])]
referencedFrameContext' :: Prop -> [(Builder, [Prop])]
referencedBlockContextGo :: Expr a -> [(Builder, [Prop])]
referencedBlockContext :: Expr a -> [(Builder, [Prop])]
referencedBlockContext' :: Prop -> [(Builder, [Prop])]
-- | This function overapproximates the reads from the abstract storage.
-- Potentially, it can return locations that do not read a slot directly
-- from the abstract store but from subsequent writes on the store (e.g,
-- SLoad addr idx (SStore addr idx val AbstractStore)). However, we
-- expect that most of such reads will have been simplified away.
findStorageReads :: Prop -> [(Expr EWord, Expr EWord)]
findBufferAccess :: TraversableTerm a => [a] -> [(Expr EWord, Expr EWord, Expr Buf)]
-- | Asserts that buffer reads beyond the size of the buffer are equal to
-- zero. Looks for buffer reads in the a list of given predicates and the
-- buffer and storage environments.
assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop]
-- | Finds the maximum read index for each abstract buffer in the input
-- props
discoverMaxReads :: [Prop] -> BufEnv -> StoreEnv -> Map Text (Expr EWord)
-- | Returns an SMT2 object with all buffers referenced from the input
-- props declared, and with the appropriate cex extraction metadata
-- attached
declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2
declareVars :: [Builder] -> SMT2
declareFrameContext :: [(Builder, [Prop])] -> SMT2
declareBlockContext :: [(Builder, [Prop])] -> SMT2
prelude :: SMT2
exprToSMT :: Expr a -> Builder
sp :: Builder -> Builder -> Builder
zero :: Builder
one :: Builder
propToSMT :: Prop -> Builder
-- | Stores a region of src into dst
copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Builder
-- | Unrolls an exponentiation into a series of multiplications
expandExp :: Expr EWord -> W256 -> Builder
-- | Concatenates a list of bytes into a larger bitvector
concatBytes :: [Expr Byte] -> Builder
-- | Concatenates a list of bytes into a larger bitvector
writeBytes :: ByteString -> Expr Buf -> Builder
encodeConcreteStore :: Map W256 (Map W256 W256) -> Builder
parseW256 :: SpecConstant -> W256
parseInteger :: SpecConstant -> Integer
parseW8 :: SpecConstant -> Word8
parseSC :: (Num a, Eq a) => SpecConstant -> a
parseErr :: Show a => a -> b
parseVar :: Text -> Expr EWord
parseBlockCtx :: Text -> Expr EWord
parseFrameCtx :: Text -> Expr EWord
getVars :: (Text -> Expr EWord) -> (Text -> IO Text) -> [Text] -> IO (Map (Expr EWord) W256)
-- | Queries the solver for models for each of the expressions representing
-- the max read index for a given buffer
queryMaxReads :: (Text -> IO Text) -> Map Text (Expr EWord) -> IO (Map Text W256)
-- | Gets the initial model for each buffer, these will often be much too
-- large for our purposes
getBufs :: (Text -> IO Text) -> [Text] -> IO (Map (Expr Buf) BufModel)
getStore :: (Text -> IO Text) -> [(Expr EWord, Expr EWord)] -> IO (Map W256 (Map W256 W256))
queryValue :: (Text -> IO Text) -> Expr EWord -> IO W256
-- | Interpret an N-dimensional array as a value of type a. Parameterized
-- by an interpretation function for array values.
interpretNDArray :: (Map Symbol Term -> Term -> a) -> Map Symbol Term -> Term -> W256 -> a
-- | Interpret an 1-dimensional array as a function
interpret1DArray :: Map Symbol Term -> Term -> W256 -> W256
-- | Interpret an 2-dimensional array as a function
interpret2DArray :: Map Symbol Term -> Term -> W256 -> W256 -> W256
instance GHC.Show.Show EVM.SMT.CexVars
instance GHC.Classes.Eq EVM.SMT.CexVars
instance GHC.Show.Show EVM.SMT.CompressedBuf
instance GHC.Classes.Eq EVM.SMT.CompressedBuf
instance GHC.Show.Show EVM.SMT.BufModel
instance GHC.Classes.Eq EVM.SMT.BufModel
instance GHC.Show.Show EVM.SMT.SMTCex
instance GHC.Classes.Eq EVM.SMT.SMTCex
instance GHC.Show.Show EVM.SMT.SMT2
instance GHC.Classes.Eq EVM.SMT.SMT2
instance GHC.Base.Semigroup EVM.SMT.SMT2
instance GHC.Base.Monoid EVM.SMT.SMT2
instance GHC.Base.Semigroup EVM.SMT.CexVars
instance GHC.Base.Monoid EVM.SMT.CexVars
module EVM.Solvers
-- | Supported solvers
data Solver
Z3 :: Solver
CVC5 :: Solver
Bitwuzla :: Solver
Custom :: Text -> Solver
-- | A running solver instance
data SolverInstance
SolverInstance :: Solver -> Handle -> Handle -> Handle -> ProcessHandle -> SolverInstance
[$sel:solvertype:SolverInstance] :: SolverInstance -> Solver
[$sel:stdin:SolverInstance] :: SolverInstance -> Handle
[$sel:stdout:SolverInstance] :: SolverInstance -> Handle
[$sel:stderr:SolverInstance] :: SolverInstance -> Handle
[$sel:process:SolverInstance] :: SolverInstance -> ProcessHandle
-- | A channel representing a group of solvers
newtype SolverGroup
SolverGroup :: Chan Task -> SolverGroup
-- | A script to be executed, a list of models to be extracted in the case
-- of a sat result, and a channel where the result should be written
data Task
Task :: SMT2 -> Chan CheckSatResult -> Task
[$sel:script:Task] :: Task -> SMT2
[$sel:resultChan:Task] :: Task -> Chan CheckSatResult
-- | The result of a call to (check-sat)
data CheckSatResult
Sat :: SMTCex -> CheckSatResult
Unsat :: CheckSatResult
Unknown :: CheckSatResult
Error :: Text -> CheckSatResult
isSat :: CheckSatResult -> Bool
isErr :: CheckSatResult -> Bool
isUnsat :: CheckSatResult -> Bool
checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult
withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
getModel :: SolverInstance -> CexVars -> IO SMTCex
mkTimeout :: Maybe Natural -> Text
-- | Arguments used when spawing a solver instance
solverArgs :: Solver -> Maybe Natural -> [Text]
-- | Spawns a solver instance, and sets the various global config options
-- that we use for our queries
spawnSolver :: Solver -> Maybe Natural -> IO SolverInstance
-- | Cleanly shutdown a running solver instnace
stopSolver :: SolverInstance -> IO ()
-- | Sends a list of commands to the solver. Returns the first error, if
-- there was one.
sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
-- | Sends a single command to the solver, returns the first available line
-- from the output buffer
sendCommand :: SolverInstance -> Text -> IO Text
-- | Sends a string to the solver and appends a newline, returns the first
-- available line from the output buffer
sendLine :: SolverInstance -> Text -> IO Text
-- | Sends a string to the solver and appends a newline, doesn't return
-- stdout
sendLine' :: SolverInstance -> Text -> IO ()
-- | Returns a string representation of the model for the requested
-- variable
getValue :: SolverInstance -> Text -> IO Text
-- | Reads lines from h until we have a balanced sexpr
readSExpr :: Handle -> IO [Text]
splitSExpr :: [Text] -> Text
data Par
LPar :: Par
RPar :: Par
getSExpr :: Text -> (Text, Text)
instance GHC.Classes.Eq EVM.Solvers.CheckSatResult
instance GHC.Show.Show EVM.Solvers.CheckSatResult
instance GHC.Show.Show EVM.Solvers.Solver
module EVM.Assembler
assemble :: [Op] -> Vector (Expr Byte)
module EVM.ABI
data AbiValue
AbiUInt :: Int -> Word256 -> AbiValue
AbiInt :: Int -> Int256 -> AbiValue
AbiAddress :: Addr -> AbiValue
AbiBool :: Bool -> AbiValue
AbiBytes :: Int -> ByteString -> AbiValue
AbiBytesDynamic :: ByteString -> AbiValue
AbiString :: ByteString -> AbiValue
AbiArrayDynamic :: AbiType -> Vector AbiValue -> AbiValue
AbiArray :: Int -> AbiType -> Vector AbiValue -> AbiValue
AbiTuple :: Vector AbiValue -> AbiValue
AbiFunction :: ByteString -> AbiValue
data AbiType
AbiUIntType :: Int -> AbiType
AbiIntType :: Int -> AbiType
AbiAddressType :: AbiType
AbiBoolType :: AbiType
AbiBytesType :: Int -> AbiType
AbiBytesDynamicType :: AbiType
AbiStringType :: AbiType
AbiArrayDynamicType :: AbiType -> AbiType
AbiArrayType :: Int -> AbiType -> AbiType
AbiTupleType :: Vector AbiType -> AbiType
AbiFunctionType :: AbiType
data AbiKind
Dynamic :: AbiKind
Static :: AbiKind
data AbiVals
NoVals :: AbiVals
CAbi :: [AbiValue] -> AbiVals
SAbi :: [Expr EWord] -> AbiVals
abiKind :: AbiType -> AbiKind
data Event
Event :: Text -> Anonymity -> [(Text, AbiType, Indexed)] -> Event
data SolError
SolError :: Text -> [AbiType] -> SolError
data Anonymity
Anonymous :: Anonymity
NotAnonymous :: Anonymity
data Indexed
Indexed :: Indexed
NotIndexed :: Indexed
putAbi :: AbiValue -> Put
getAbi :: AbiType -> Get AbiValue
-- | Decode a sequence type (e.g. tuple / array). Will fail for non
-- sequence types
getAbiSeq :: Int -> [AbiType] -> Get (Vector AbiValue)
genAbiValue :: AbiType -> Gen AbiValue
abiValueType :: AbiValue -> AbiType
abiTypeSolidity :: AbiType -> Text
abiMethod :: Text -> AbiValue -> ByteString
emptyAbi :: AbiValue
encodeAbiValue :: AbiValue -> ByteString
decodeAbiValue :: AbiType -> ByteString -> AbiValue
decodeBuf :: [AbiType] -> Expr Buf -> AbiVals
decodeStaticArgs :: Int -> Int -> Expr Buf -> [Expr EWord]
formatString :: ByteString -> String
parseTypeName :: Vector AbiType -> Text -> Maybe AbiType
makeAbiValue :: AbiType -> String -> AbiValue
parseAbiValue :: AbiType -> ReadP AbiValue
selector :: Text -> ByteString
instance Data.Data.Data EVM.ABI.AbiType
instance GHC.Generics.Generic EVM.ABI.AbiType
instance GHC.Classes.Ord EVM.ABI.AbiType
instance GHC.Classes.Eq EVM.ABI.AbiType
instance GHC.Read.Read EVM.ABI.AbiType
instance GHC.Generics.Generic EVM.ABI.AbiValue
instance GHC.Classes.Ord EVM.ABI.AbiValue
instance GHC.Classes.Eq EVM.ABI.AbiValue
instance GHC.Read.Read EVM.ABI.AbiValue
instance GHC.Generics.Generic EVM.ABI.AbiKind
instance GHC.Classes.Ord EVM.ABI.AbiKind
instance GHC.Classes.Eq EVM.ABI.AbiKind
instance GHC.Read.Read EVM.ABI.AbiKind
instance GHC.Show.Show EVM.ABI.AbiKind
instance GHC.Generics.Generic EVM.ABI.Anonymity
instance GHC.Classes.Eq EVM.ABI.Anonymity
instance GHC.Classes.Ord EVM.ABI.Anonymity
instance GHC.Show.Show EVM.ABI.Anonymity
instance GHC.Generics.Generic EVM.ABI.Indexed
instance GHC.Classes.Eq EVM.ABI.Indexed
instance GHC.Classes.Ord EVM.ABI.Indexed
instance GHC.Show.Show EVM.ABI.Indexed
instance GHC.Generics.Generic EVM.ABI.Event
instance GHC.Classes.Eq EVM.ABI.Event
instance GHC.Classes.Ord EVM.ABI.Event
instance GHC.Show.Show EVM.ABI.Event
instance GHC.Generics.Generic EVM.ABI.SolError
instance GHC.Classes.Eq EVM.ABI.SolError
instance GHC.Classes.Ord EVM.ABI.SolError
instance GHC.Show.Show EVM.ABI.SolError
instance GHC.Show.Show EVM.ABI.AbiVals
instance GHC.Read.Read EVM.ABI.Boolz
instance GHC.Show.Show EVM.ABI.AbiValue
instance Test.QuickCheck.Arbitrary.Arbitrary EVM.ABI.AbiValue
instance GHC.Show.Show EVM.ABI.AbiType
instance Test.QuickCheck.Arbitrary.Arbitrary EVM.ABI.AbiType
module EVM.Solidity
solidity :: Text -> Text -> IO (Maybe ByteString)
solcRuntime :: Text -> Text -> IO (Maybe ByteString)
solidity' :: Text -> IO (Text, Text)
yul' :: Text -> IO (Text, Text)
yul :: Text -> Text -> IO (Maybe ByteString)
yulRuntime :: Text -> Text -> IO (Maybe ByteString)
data JumpType
JumpInto :: JumpType
JumpFrom :: JumpType
JumpRegular :: JumpType
data SolcContract
SolcContract :: W256 -> W256 -> ByteString -> ByteString -> Text -> [(Text, AbiType)] -> Map FunctionSelector Method -> Map W256 Event -> Map W256 SolError -> Map W256 [Reference] -> Maybe (Map Text StorageItem) -> Seq SrcMap -> Seq SrcMap -> SolcContract
[$sel:runtimeCodehash:SolcContract] :: SolcContract -> W256
[$sel:creationCodehash:SolcContract] :: SolcContract -> W256
[$sel:runtimeCode:SolcContract] :: SolcContract -> ByteString
[$sel:creationCode:SolcContract] :: SolcContract -> ByteString
[$sel:contractName:SolcContract] :: SolcContract -> Text
[$sel:constructorInputs:SolcContract] :: SolcContract -> [(Text, AbiType)]
[$sel:abiMap:SolcContract] :: SolcContract -> Map FunctionSelector Method
[$sel:eventMap:SolcContract] :: SolcContract -> Map W256 Event
[$sel:errorMap:SolcContract] :: SolcContract -> Map W256 SolError
[$sel:immutableReferences:SolcContract] :: SolcContract -> Map W256 [Reference]
[$sel:storageLayout:SolcContract] :: SolcContract -> Maybe (Map Text StorageItem)
[$sel:runtimeSrcmap:SolcContract] :: SolcContract -> Seq SrcMap
[$sel:creationSrcmap:SolcContract] :: SolcContract -> Seq SrcMap
-- | A mapping from contract identifiers (filepath:name) to a SolcContract
-- object
newtype Contracts
Contracts :: Map Text SolcContract -> Contracts
-- | The various project types understood by hevm
data ProjectType
DappTools :: ProjectType
CombinedJSON :: ProjectType
Foundry :: ProjectType
data BuildOutput
BuildOutput :: Contracts -> SourceCache -> BuildOutput
[$sel:contracts:BuildOutput] :: BuildOutput -> Contracts
[$sel:sources:BuildOutput] :: BuildOutput -> SourceCache
data StorageItem
StorageItem :: SlotType -> Int -> Int -> StorageItem
[$sel:slotType:StorageItem] :: StorageItem -> SlotType
[$sel:offset:StorageItem] :: StorageItem -> Int
[$sel:slot:StorageItem] :: StorageItem -> Int
data SourceCache
SourceCache :: Map Int (FilePath, ByteString) -> Map Int (Vector ByteString) -> Map Text Value -> SourceCache
[$sel:files:SourceCache] :: SourceCache -> Map Int (FilePath, ByteString)
[$sel:lines:SourceCache] :: SourceCache -> Map Int (Vector ByteString)
[$sel:asts:SourceCache] :: SourceCache -> Map Text Value
data SrcMap
SM :: {-# UNPACK #-} !Int -> {-# UNPACK #-} !Int -> {-# UNPACK #-} !Int -> JumpType -> {-# UNPACK #-} !Int -> SrcMap
[$sel:offset:SM] :: SrcMap -> {-# UNPACK #-} !Int
[$sel:length:SM] :: SrcMap -> {-# UNPACK #-} !Int
[$sel:file:SM] :: SrcMap -> {-# UNPACK #-} !Int
[$sel:jump:SM] :: SrcMap -> JumpType
[$sel:modifierDepth:SM] :: SrcMap -> {-# UNPACK #-} !Int
data CodeType
Creation :: CodeType
Runtime :: CodeType
data Method
Method :: [(Text, AbiType)] -> [(Text, AbiType)] -> Text -> Text -> Mutability -> Method
[$sel:output:Method] :: Method -> [(Text, AbiType)]
[$sel:inputs:Method] :: Method -> [(Text, AbiType)]
[$sel:name:Method] :: Method -> Text
[$sel:methodSignature:Method] :: Method -> Text
[$sel:mutability:Method] :: Method -> Mutability
data SlotType
StorageMapping :: NonEmpty AbiType -> AbiType -> SlotType
StorageValue :: AbiType -> SlotType
data Reference
Reference :: Int -> Int -> Reference
[$sel:start:Reference] :: Reference -> Int
[$sel:length:Reference] :: Reference -> Int
data Mutability
-- | specified to not read blockchain state
Pure :: Mutability
-- | specified to not modify the blockchain state
View :: Mutability
-- | function does not accept Ether - the default
NonPayable :: Mutability
-- | function accepts Ether
Payable :: Mutability
-- | Reads all solc ouput json files found under the provided filepath and
-- returns them merged into a BuildOutput
readBuildOutput :: FilePath -> ProjectType -> IO (Either String BuildOutput)
functionAbi :: Text -> IO Method
makeSrcMaps :: Text -> Maybe (Seq SrcMap)
readSolc :: ProjectType -> FilePath -> FilePath -> IO (Either String BuildOutput)
readJSON :: ProjectType -> Text -> Text -> Maybe (Contracts, Asts, Sources)
-- | Parses the standard json output from solc
readStdJSON :: Text -> Maybe (Contracts, Asts, Sources)
-- | When doing CREATE and passing constructor arguments, Solidity loads
-- the argument data via the creation bytecode, since there is no
-- "calldata" for CREATE.
--
-- This interferes with our ability to look up the current contract by
-- codehash, so we must somehow strip away this extra suffix. Luckily we
-- can detect the end of the actual bytecode by looking for the "metadata
-- hash". (Not 100% correct, but works in practice.)
--
-- Actually, we strip away the entire BZZR suffix too, because as long as
-- the codehash matches otherwise, we don't care if there is some
-- difference there.
stripBytecodeMetadata :: ByteString -> ByteString
stripBytecodeMetadataSym :: [Expr Byte] -> [Expr Byte]
signature :: AsValue s => s -> Text
solc :: Language -> Text -> IO Text
data Language
Solidity :: Language
Yul :: Language
stdjson :: Language -> Text -> Text
parseMethodInput :: AsValue s => s -> (Text, AbiType)
lineSubrange :: Vector ByteString -> (Int, Int) -> Int -> Maybe (Int, Int)
-- | Every node in the AST has an ID, and other nodes reference those IDs.
-- This function recurses through the tree looking for objects with the
-- "id" key and makes a big map from ID to value.
astIdMap :: Foldable f => f Value -> Map Int Value
astSrcMap :: Map Int Value -> SrcMap -> Maybe Value
containsLinkerHole :: Text -> Bool
makeSourceCache :: FilePath -> Sources -> Asts -> IO SourceCache
instance GHC.Classes.Eq EVM.Solidity.SlotType
instance GHC.Classes.Eq EVM.Solidity.StorageItem
instance GHC.Show.Show EVM.Solidity.StorageItem
instance GHC.Generics.Generic EVM.Solidity.Mutability
instance GHC.Classes.Ord EVM.Solidity.Mutability
instance GHC.Classes.Eq EVM.Solidity.Mutability
instance GHC.Show.Show EVM.Solidity.Mutability
instance GHC.Generics.Generic EVM.Solidity.Method
instance GHC.Classes.Ord EVM.Solidity.Method
instance GHC.Classes.Eq EVM.Solidity.Method
instance GHC.Show.Show EVM.Solidity.Method
instance GHC.Base.Monoid EVM.Solidity.Asts
instance GHC.Base.Semigroup EVM.Solidity.Asts
instance GHC.Classes.Eq EVM.Solidity.Asts
instance GHC.Show.Show EVM.Solidity.Asts
instance GHC.Classes.Ord EVM.Solidity.SrcFile
instance GHC.Classes.Eq EVM.Solidity.SrcFile
instance GHC.Show.Show EVM.Solidity.SrcFile
instance GHC.Base.Monoid EVM.Solidity.Sources
instance GHC.Base.Semigroup EVM.Solidity.Sources
instance GHC.Classes.Eq EVM.Solidity.Sources
instance GHC.Show.Show EVM.Solidity.Sources
instance Options.Generic.ParseField EVM.Solidity.ProjectType
instance GHC.Read.Read EVM.Solidity.ProjectType
instance GHC.Show.Show EVM.Solidity.ProjectType
instance GHC.Classes.Eq EVM.Solidity.ProjectType
instance GHC.Generics.Generic EVM.Solidity.SourceCache
instance GHC.Classes.Eq EVM.Solidity.SourceCache
instance GHC.Show.Show EVM.Solidity.SourceCache
instance GHC.Classes.Eq EVM.Solidity.Reference
instance GHC.Show.Show EVM.Solidity.Reference
instance GHC.Generics.Generic EVM.Solidity.JumpType
instance GHC.Classes.Ord EVM.Solidity.JumpType
instance GHC.Classes.Eq EVM.Solidity.JumpType
instance GHC.Show.Show EVM.Solidity.JumpType
instance GHC.Generics.Generic EVM.Solidity.SrcMap
instance GHC.Classes.Ord EVM.Solidity.SrcMap
instance GHC.Classes.Eq EVM.Solidity.SrcMap
instance GHC.Show.Show EVM.Solidity.SrcMap
instance GHC.Generics.Generic EVM.Solidity.SolcContract
instance GHC.Classes.Eq EVM.Solidity.SolcContract
instance GHC.Show.Show EVM.Solidity.SolcContract
instance GHC.Base.Monoid EVM.Solidity.Contracts
instance GHC.Base.Semigroup EVM.Solidity.Contracts
instance GHC.Classes.Eq EVM.Solidity.Contracts
instance GHC.Show.Show EVM.Solidity.Contracts
instance GHC.Classes.Eq EVM.Solidity.BuildOutput
instance GHC.Show.Show EVM.Solidity.BuildOutput
instance GHC.Show.Show EVM.Solidity.SrcMapParseState
instance GHC.Classes.Ord EVM.Solidity.CodeType
instance GHC.Classes.Eq EVM.Solidity.CodeType
instance GHC.Show.Show EVM.Solidity.CodeType
instance GHC.Show.Show EVM.Solidity.Language
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Solidity.StandardJSON
instance GHC.Base.Semigroup EVM.Solidity.BuildOutput
instance GHC.Base.Monoid EVM.Solidity.BuildOutput
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Solidity.Reference
instance GHC.Base.Semigroup EVM.Solidity.SourceCache
instance GHC.Base.Monoid EVM.Solidity.SourceCache
instance GHC.Show.Show EVM.Solidity.SlotType
instance GHC.Read.Read EVM.Solidity.SlotType
module EVM.Sign
deriveAddr :: Integer -> Maybe Addr
sign :: W256 -> Integer -> (Word8, W256, W256)
-- | We don't want to introduce the machinery needed to sign with a random
-- nonce, so we just use the same nonce every time (420). This is
-- obviously very insecure, but fine for testing purposes.
ethsign :: PrivateKey -> Digest Keccak_256 -> Signature
ecrec :: W256 -> W256 -> W256 -> W256 -> Maybe Addr
module EVM
blankState :: FrameState
-- | An "external" view of a contract's bytecode, appropriate for e.g.
-- EXTCODEHASH.
bytecode :: Getter Contract (Expr Buf)
currentContract :: VM -> Maybe Contract
makeVm :: VMOpts -> VM
-- | Initialize empty contract with given code
initialContract :: ContractCode -> Contract
-- | Update program counter
next :: (?op :: Word8) => EVM ()
-- | Executes the EVM one step
exec1 :: EVM ()
transfer :: Addr -> Addr -> W256 -> EVM ()
-- | Checks a *CALL for failure; OOG, too many callframes, memory access
-- etc.
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
query :: Query -> EVM ()
choose :: Choose -> EVM ()
branch :: CodeLocation -> Expr EWord -> (Bool -> EVM ()) -> EVM ()
-- | Construct RPC Query and halt execution until resolved
fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM ()
accessStorage :: Addr -> Expr EWord -> (Expr EWord -> EVM ()) -> EVM ()
accountExists :: Addr -> VM -> Bool
accountEmpty :: Contract -> Bool
finalize :: EVM ()
-- | Loads the selected contract as the current contract to execute
loadContract :: Addr -> EVM ()
limitStack :: Int -> EVM () -> EVM ()
notStatic :: EVM () -> EVM ()
-- | Burn gas, failing if insufficient gas is available
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 ()
-- | returns a wrapped boolean- if true, this address has been touched
-- before in the txn (warm gas cost as in EIP 2929) otherwise cold
accessAccountForGas :: Addr -> EVM Bool
-- | returns a wrapped boolean- if true, this slot has been touched before
-- in the txn (warm gas cost as in EIP 2929) otherwise cold
accessStorageForGas :: Addr -> 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 -> W256 -> Word64 -> W256 -> [Expr EWord] -> Addr -> Expr Buf -> EVM ()
-- | Replace a contract's code, like when CREATE returns from the
-- constructor code.
replaceCode :: Addr -> ContractCode -> EVM ()
replaceCodeOfSelf :: ContractCode -> EVM ()
resetState :: EVM ()
vmError :: EvmError -> EVM ()
partial :: PartialExec -> EVM ()
wrap :: Typeable a => [Expr a] -> [SomeExpr]
underrun :: EVM ()
-- | A stack frame can be popped in three ways.
data FrameResult
-- | STOP, RETURN, or no more code
FrameReturned :: Expr Buf -> FrameResult
-- | REVERT
FrameReverted :: Expr Buf -> FrameResult
-- | Any other error
FrameErrored :: EvmError -> FrameResult
-- | This function defines how to pop the current stack frame in either of
-- the ways specified by FrameResult.
--
-- It also handles the case when the current stack frame is the only one;
-- in this case, we set the final _result of the VM execution.
finishFrame :: FrameResult -> EVM ()
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
traceForest' :: Expr End -> Forest Trace
traceContext :: Expr End -> Map Addr Contract
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 ()
isValidJumpDest :: VM -> Int -> Bool
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 -> Bool -> (Word64, Word64)
concreteModexpGasFee :: ByteString -> Word64
costOfPrecompile :: FeeSchedule Word64 -> Addr -> Expr Buf -> Word64
memoryCost :: FeeSchedule Word64 -> Word64 -> Word64
hashcode :: ContractCode -> Expr EWord
-- | The length of the code ignoring any constructor args. This represents
-- the region that can contain executable opcodes
opslen :: ContractCode -> Int
-- | The length of the code including any constructor args. This can return
-- an abstract value
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
instance GHC.Show.Show EVM.FrameResult
module EVM.Facts
data File
File :: Path -> Data -> File
[$sel:filePath:File] :: File -> Path
[$sel:fileData:File] :: File -> Data
data Fact
BalanceFact :: Addr -> W256 -> Fact
[$sel:addr:BalanceFact] :: Fact -> Addr
[$sel:what:BalanceFact] :: Fact -> W256
NonceFact :: Addr -> W256 -> Fact
[$sel:addr:BalanceFact] :: Fact -> Addr
[$sel:what:BalanceFact] :: Fact -> W256
StorageFact :: Addr -> W256 -> W256 -> Fact
[$sel:addr:BalanceFact] :: Fact -> Addr
[$sel:what:BalanceFact] :: Fact -> W256
[$sel:which:BalanceFact] :: Fact -> W256
CodeFact :: Addr -> ByteString -> Fact
[$sel:addr:BalanceFact] :: Fact -> Addr
[$sel:blob:BalanceFact] :: Fact -> ByteString
newtype Data
Data :: ASCII -> Data
[$sel:dataASCII:Data] :: Data -> ASCII
data Path
Path :: [ASCII] -> ASCII -> Path
apply :: VM -> Set Fact -> VM
applyCache :: VM -> Set Fact -> VM
cacheFacts :: Cache -> Set Fact
contractFacts :: Addr -> Contract -> Map W256 (Map W256 W256) -> [Fact]
vmFacts :: VM -> Set Fact
factToFile :: Fact -> File
fileToFact :: File -> Maybe Fact
instance GHC.Show.Show EVM.Facts.Fact
instance GHC.Classes.Eq EVM.Facts.Fact
instance GHC.Show.Show EVM.Facts.Path
instance GHC.Classes.Ord EVM.Facts.Path
instance GHC.Classes.Eq EVM.Facts.Path
instance GHC.Show.Show EVM.Facts.Data
instance GHC.Classes.Ord EVM.Facts.Data
instance GHC.Classes.Eq EVM.Facts.Data
instance GHC.Show.Show EVM.Facts.File
instance GHC.Classes.Ord EVM.Facts.File
instance GHC.Classes.Eq EVM.Facts.File
instance EVM.Facts.AsASCII EVM.Types.Addr
instance EVM.Facts.AsASCII EVM.Types.W256
instance EVM.Facts.AsASCII Data.ByteString.Internal.Type.ByteString
instance GHC.Classes.Ord EVM.Facts.Fact
module EVM.Facts.Git
saveFacts :: RepoAt -> Set Fact -> IO ()
loadFacts :: RepoAt -> IO (Set Fact)
newtype RepoAt
RepoAt :: String -> RepoAt
instance GHC.Show.Show EVM.Facts.Git.RepoAt
instance GHC.Classes.Ord EVM.Facts.Git.RepoAt
instance GHC.Classes.Eq EVM.Facts.Git.RepoAt
module EVM.Exec
ethrunAddress :: Addr
vmForEthrunCreation :: ByteString -> VM
exec :: State VM VMResult
run :: State VM VM
execWhile :: (VM -> Bool) -> State VM Int
module EVM.Debug
data Mode
Debug :: Mode
Run :: Mode
JsonTrace :: Mode
object :: [(Doc, Doc)] -> Doc
prettyContract :: Contract -> Doc
prettyContracts :: Map Addr Contract -> Doc
srcMapCodePos :: SourceCache -> SrcMap -> Maybe (FilePath, Int)
srcMapCode :: SourceCache -> SrcMap -> Maybe ByteString
instance GHC.Show.Show EVM.Debug.Mode
instance GHC.Classes.Eq EVM.Debug.Mode
module EVM.Dapp
data DappInfo
DappInfo :: FilePath -> Map Text SolcContract -> Map W256 (CodeType, SolcContract) -> [(Code, SolcContract)] -> SourceCache -> [(Text, [(Test, [AbiType])])] -> Map FunctionSelector Method -> Map W256 Event -> Map W256 SolError -> Map Int Value -> (SrcMap -> Maybe Value) -> DappInfo
[$sel:root:DappInfo] :: DappInfo -> FilePath
[$sel:solcByName:DappInfo] :: DappInfo -> Map Text SolcContract
[$sel:solcByHash:DappInfo] :: DappInfo -> Map W256 (CodeType, SolcContract)
[$sel:solcByCode:DappInfo] :: DappInfo -> [(Code, SolcContract)]
[$sel:sources:DappInfo] :: DappInfo -> SourceCache
[$sel:unitTests:DappInfo] :: DappInfo -> [(Text, [(Test, [AbiType])])]
[$sel:abiMap:DappInfo] :: DappInfo -> Map FunctionSelector Method
[$sel:eventMap:DappInfo] :: DappInfo -> Map W256 Event
[$sel:errorMap:DappInfo] :: DappInfo -> Map W256 SolError
[$sel:astIdMap:DappInfo] :: DappInfo -> Map Int Value
[$sel:astSrcMap:DappInfo] :: DappInfo -> SrcMap -> Maybe Value
-- | bytecode modulo immutables, to identify contracts
data Code
Code :: ByteString -> [Reference] -> Code
[$sel:raw:Code] :: Code -> ByteString
[$sel:immutableLocations:Code] :: Code -> [Reference]
data DappContext
DappContext :: DappInfo -> Map Addr Contract -> DappContext
[$sel:info:DappContext] :: DappContext -> DappInfo
[$sel:env:DappContext] :: DappContext -> Map Addr Contract
data Test
ConcreteTest :: Text -> Test
SymbolicTest :: Text -> Test
InvariantTest :: Text -> Test
dappInfo :: FilePath -> BuildOutput -> DappInfo
emptyDapp :: DappInfo
unitTestMarkerAbi :: FunctionSelector
findAllUnitTests :: [SolcContract] -> [(Text, [(Test, [AbiType])])]
mkTest :: Text -> Maybe Test
findUnitTests :: Text -> [SolcContract] -> [(Text, [(Test, [AbiType])])]
unitTestMethodsFiltered :: (Text -> Bool) -> SolcContract -> [(Test, [AbiType])]
unitTestMethods :: SolcContract -> [(Test, [AbiType])]
extractSig :: Test -> Text
traceSrcMap :: DappInfo -> Trace -> Maybe SrcMap
srcMap :: DappInfo -> Contract -> Int -> Maybe SrcMap
findSrc :: Contract -> DappInfo -> Maybe SolcContract
lookupCode :: ContractCode -> DappInfo -> Maybe SolcContract
compareCode :: ByteString -> Code -> Bool
showTraceLocation :: DappInfo -> Trace -> Either Text Text
instance GHC.Show.Show EVM.Dapp.Code
instance GHC.Show.Show EVM.Dapp.Test
module EVM.StorageLayout
findContractDefinition :: DappInfo -> SolcContract -> Maybe Value
storageLayout :: DappInfo -> SolcContract -> [Text]
storageVariablesForContract :: Value -> Maybe [Text]
nodeIs :: Text -> Value -> Bool
isStorageVariableDeclaration :: Value -> Bool
slotTypeForDeclaration :: Value -> SlotType
grokDeclarationType :: Value -> SlotType
grokMappingType :: [Value] -> SlotType
grokValueType :: Value -> AbiType
module EVM.Format
formatExpr :: Expr a -> Text
formatSomeExpr :: SomeExpr -> Text
formatPartial :: PartialExec -> Text
contractNamePart :: Text -> Text
contractPathPart :: Text -> Text
showError :: (?context :: DappContext) => Expr Buf -> Text
-- | Show a Tree using Unicode art
showTree :: Tree String -> String
showTraceTree :: DappInfo -> VM -> Text
showTraceTree' :: DappInfo -> Expr End -> Text
showValues :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
prettyvmresult :: Expr End -> String
showCall :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
showWordExact :: W256 -> Text
showWordExplanation :: W256 -> DappInfo -> Text
parenthesise :: [Text] -> Text
unindexed :: [(Text, AbiType, Indexed)] -> [AbiType]
showValue :: (?context :: DappContext) => AbiType -> Expr Buf -> Text
textValues :: (?context :: DappContext) => [AbiType] -> Expr Buf -> [Text]
showAbiValue :: (?context :: DappContext) => AbiValue -> Text
prettyIfConcreteWord :: Expr EWord -> Text
formatBytes :: ByteString -> Text
formatBinary :: ByteString -> Text
indent :: Int -> Text -> Text
strip0x :: ByteString -> ByteString
strip0x' :: String -> String
hexByteString :: String -> ByteString -> ByteString
hexText :: Text -> ByteString
bsToHex :: ByteString -> String
instance GHC.Show.Show EVM.Format.Signedness
module EVM.Transaction
data AccessListEntry
AccessListEntry :: Addr -> [W256] -> AccessListEntry
[$sel:address:AccessListEntry] :: AccessListEntry -> Addr
[$sel:storageKeys:AccessListEntry] :: AccessListEntry -> [W256]
data TxType
LegacyTransaction :: TxType
AccessListTransaction :: TxType
EIP1559Transaction :: TxType
data Transaction
Transaction :: ByteString -> Word64 -> Maybe W256 -> W256 -> W256 -> W256 -> Maybe Addr -> W256 -> W256 -> TxType -> [AccessListEntry] -> Maybe W256 -> Maybe W256 -> W256 -> Transaction
[$sel:txdata:Transaction] :: Transaction -> ByteString
[$sel:gasLimit:Transaction] :: Transaction -> Word64
[$sel:gasPrice:Transaction] :: Transaction -> Maybe W256
[$sel:nonce:Transaction] :: Transaction -> W256
[$sel:r:Transaction] :: Transaction -> W256
[$sel:s:Transaction] :: Transaction -> W256
[$sel:toAddr:Transaction] :: Transaction -> Maybe Addr
[$sel:v:Transaction] :: Transaction -> W256
[$sel:value:Transaction] :: Transaction -> W256
[$sel:txtype:Transaction] :: Transaction -> TxType
[$sel:accessList:Transaction] :: Transaction -> [AccessListEntry]
[$sel:maxPriorityFeeGas:Transaction] :: Transaction -> Maybe W256
[$sel:maxFeePerGas:Transaction] :: Transaction -> Maybe W256
[$sel:chainId:Transaction] :: Transaction -> W256
emptyTransaction :: Transaction
-- | utility function for getting a more useful representation of
-- accesslistentries duplicates only matter for gas computation
txAccessMap :: Transaction -> Map Addr [W256]
sender :: Transaction -> Maybe Addr
sign :: Integer -> Transaction -> Transaction
signingData :: Transaction -> ByteString
accessListPrice :: FeeSchedule Word64 -> [AccessListEntry] -> Word64
txGasCost :: FeeSchedule Word64 -> Transaction -> Word64
accountAt :: Addr -> Getter (Map Addr Contract) Contract
touchAccount :: Addr -> Map Addr Contract -> Map Addr Contract
newAccount :: Contract
-- | Increments origin nonce and pays gas deposit
setupTx :: Addr -> Addr -> W256 -> Word64 -> Map Addr Contract -> Map Addr Contract
-- | Given a valid tx loaded into the vm state, subtract gas payment from
-- the origin, increment the nonce and pay receiving address
initTx :: VM -> VM
instance GHC.Generics.Generic EVM.Transaction.AccessListEntry
instance GHC.Show.Show EVM.Transaction.AccessListEntry
instance GHC.Generics.Generic EVM.Transaction.TxType
instance GHC.Classes.Eq EVM.Transaction.TxType
instance GHC.Show.Show EVM.Transaction.TxType
instance GHC.Generics.Generic EVM.Transaction.Transaction
instance GHC.Show.Show EVM.Transaction.Transaction
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Transaction.Transaction
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Transaction.Transaction
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Transaction.TxType
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Transaction.AccessListEntry
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Transaction.AccessListEntry
module EVM.Fetch
-- | Abstract representation of an RPC fetch request
data RpcQuery a
[QueryCode] :: Addr -> RpcQuery ByteString
[QueryBlock] :: RpcQuery Block
[QueryBalance] :: Addr -> RpcQuery W256
[QueryNonce] :: Addr -> RpcQuery W256
[QuerySlot] :: Addr -> W256 -> RpcQuery W256
[QueryChainId] :: RpcQuery W256
data BlockNumber
Latest :: BlockNumber
BlockNumber :: W256 -> BlockNumber
type RpcInfo = Maybe (BlockNumber, Text)
rpc :: String -> [Value] -> Value
class ToRPC a
toRPC :: ToRPC a => a -> Value
readText :: Read a => Text -> a
fetchQuery :: Show a => BlockNumber -> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
parseBlock :: (AsValue s, Show s) => s -> Maybe Block
fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value)
fetchContractWithSession :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchSlotWithSession :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe W256)
fetchBlockWithSession :: BlockNumber -> Text -> Session -> IO (Maybe Block)
fetchBlockFrom :: BlockNumber -> Text -> IO (Maybe Block)
fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchSlotFrom :: BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256)
fetchChainIdFrom :: Text -> IO (Maybe W256)
http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher
zero :: Natural -> Maybe Natural -> Fetcher
oracle :: SolverGroup -> RpcInfo -> Fetcher
type Fetcher = Query -> IO (EVM ())
-- | Checks which branches are satisfiable, checking the pathconditions for
-- consistency if the third argument is true. When in debug mode, we do
-- not want to be able to navigate to dead paths, but for normal
-- execution paths with inconsistent pathconditions will be pruned
-- anyway.
checkBranch :: SolverGroup -> Prop -> Prop -> IO BranchCondition
instance GHC.Classes.Eq EVM.Fetch.BlockNumber
instance GHC.Show.Show EVM.Fetch.BlockNumber
instance GHC.Show.Show (EVM.Fetch.RpcQuery a)
instance EVM.Fetch.ToRPC EVM.Types.Addr
instance EVM.Fetch.ToRPC EVM.Types.W256
instance EVM.Fetch.ToRPC GHC.Types.Bool
instance EVM.Fetch.ToRPC EVM.Fetch.BlockNumber
module EVM.Stepper
-- | The instruction type of the operational monad
data Action a
-- | Keep executing until an intermediate result is reached
[Exec] :: Action VMResult
-- | Keep executing until an intermediate state is reached
[Run] :: Action VM
-- | Wait for a query to be resolved
[Wait] :: Query -> Action ()
-- | Multiple things can happen
[Ask] :: Choose -> Action ()
-- | Embed a VM state transformation
[EVM] :: EVM a -> Action a
-- | Perform an IO action
[IOAct] :: StateT VM IO a -> Action a
-- | Type alias for an operational monad of Action
type Stepper a = Program Action a
exec :: Stepper VMResult
-- | Run the VM until final result, resolving all queries
execFully :: Stepper (Either EvmError (Expr Buf))
run :: Stepper VM
-- | Run the VM until its final state
runFully :: Stepper VM
wait :: Query -> Stepper ()
ask :: Choose -> Stepper ()
evm :: EVM a -> Stepper a
evmIO :: StateT VM IO a -> Stepper a
entering :: Text -> Stepper a -> Stepper a
enter :: Text -> Stepper ()
interpret :: Fetcher -> VM -> Stepper a -> IO a
module EVM.SymExec
-- | A method name, and the (ordered) types of it's arguments
data Sig
Sig :: Text -> [AbiType] -> Sig
data LoopHeuristic
Naive :: LoopHeuristic
StackBased :: LoopHeuristic
data ProofResult a b c
Qed :: a -> ProofResult a b c
Cex :: b -> ProofResult a b c
Timeout :: c -> ProofResult a b c
type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End)
type EquivResult = ProofResult () (SMTCex) ()
isTimeout :: ProofResult a b c -> Bool
isCex :: ProofResult a b c -> Bool
isQed :: ProofResult a b c -> Bool
data VeriOpts
VeriOpts :: Bool -> Bool -> Maybe Integer -> Integer -> LoopHeuristic -> RpcInfo -> VeriOpts
[$sel:simp:VeriOpts] :: VeriOpts -> Bool
[$sel:debug:VeriOpts] :: VeriOpts -> Bool
[$sel:maxIter:VeriOpts] :: VeriOpts -> Maybe Integer
[$sel:askSmtIters:VeriOpts] :: VeriOpts -> Integer
[$sel:loopHeuristic:VeriOpts] :: VeriOpts -> LoopHeuristic
[$sel:rpcInfo:VeriOpts] :: VeriOpts -> RpcInfo
defaultVeriOpts :: VeriOpts
rpcVeriOpts :: (BlockNumber, Text) -> VeriOpts
debugVeriOpts :: VeriOpts
extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
bool :: Expr EWord -> Prop
-- | Abstract calldata argument generation
symAbiArg :: Text -> AbiType -> CalldataFragment
data CalldataFragment
St :: [Prop] -> Expr EWord -> CalldataFragment
Dy :: [Prop] -> Expr EWord -> Expr Buf -> CalldataFragment
Comp :: [CalldataFragment] -> CalldataFragment
-- | Generates calldata matching given type signature, optionally
-- specialized with concrete arguments. Any argument given as
-- "symbolic" or omitted at the tail of the list are kept
-- symbolic.
symCalldata :: Text -> [AbiType] -> [String] -> Expr Buf -> (Expr Buf, [Prop])
cdLen :: [CalldataFragment] -> Expr EWord
writeSelector :: Expr Buf -> Text -> Expr Buf
combineFragments :: [CalldataFragment] -> Expr Buf -> (Expr Buf, [Prop])
abstractVM :: (Expr Buf, [Prop]) -> ByteString -> Maybe Precondition -> Expr Storage -> VM
loadSymVM :: ContractCode -> Expr Storage -> Expr EWord -> Expr EWord -> (Expr Buf, [Prop]) -> VM
-- | Interpreter which explores all paths at branching points. Returns an
-- 'Expr End' representing the possible executions.
interpret :: Fetcher -> Maybe Integer -> Integer -> LoopHeuristic -> VM -> Stepper (Expr End) -> IO (Expr End)
maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool
askSmtItersReached :: VM -> Integer -> Bool
-- | Loop head detection heuristic
--
-- The main thing we wish to differentiate between, are actual loop
-- heads, and branch points inside of internal functions that are called
-- multiple times.
--
-- One way to do this is to observe that for internal functions, the
-- compiler must always store a stack item representing the location that
-- it must jump back to. If we compare the stack at the time of the
-- previous visit, and the time of the current visit, and notice that
-- this location has changed, then we can guess that the location is a
-- jump point within an internal function instead of a loop (where such
-- locations should be constant between iterations).
--
-- This heuristic is not perfect, and can certainly be tricked, but
-- should generally be good enough for most compiler generated and non
-- pathological user generated loops.
isLoopHead :: LoopHeuristic -> VM -> Maybe Bool
type Precondition = VM -> Prop
type Postcondition = VM -> Expr End -> Prop
checkAssert :: SolverGroup -> [Word256] -> ByteString -> Maybe Sig -> [String] -> VeriOpts -> IO (Expr End, [VerifyResult])
-- | Checks if an assertion violation has been encountered
--
-- hevm recognises the following as an assertion violation:
--
--
-- - the invalid opcode (0xfe) (solc < 0.8)
-- - a revert with a reason of the form
-- `abi.encodeWithSelector("Panic(uint256)", code)`, where code is one of
-- the following (solc >= 0.8): - 0x00: Used for generic compiler
-- inserted panics. - 0x01: If you call assert with an argument that
-- evaluates to false. - 0x11: If an arithmetic operation results in
-- underflow or overflow outside of an unchecked { ... } block. - 0x12;
-- If you divide or modulo by zero (e.g. 5 / 0 or 23 % 0). - 0x21: If you
-- convert a value that is too big or negative into an enum type. - 0x22:
-- If you access a storage byte array that is incorrectly encoded. -
-- 0x31: If you call .pop() on an empty array. - 0x32: If you access an
-- array, bytesN or an array slice at an out-of-bounds or negative index
-- (i.e. x[i] where i >= x.length or i < 0). - 0x41: If you
-- allocate too much memory or create an array that is too large. - 0x51:
-- If you call a zero-initialized variable of internal function
-- type.
--
--
-- see:
-- https://docs.soliditylang.org/en/v0.8.6/control-structures.html?highlight=Panic#panic-via-assert-and-error-via-require
checkAssertions :: [Word256] -> Postcondition
-- | By default hevm only checks for user-defined assertions
defaultPanicCodes :: [Word256]
allPanicCodes :: [Word256]
-- | Produces the revert message for solc >=0.8 assertion violations
panicMsg :: Word256 -> ByteString
-- | Builds a buffer representing calldata from the provided method
-- description and concrete arguments
mkCalldata :: Maybe Sig -> [String] -> (Expr Buf, [Prop])
verifyContract :: SolverGroup -> ByteString -> Maybe Sig -> [String] -> VeriOpts -> Expr Storage -> Maybe Precondition -> Maybe Postcondition -> IO (Expr End, [VerifyResult])
-- | Stepper that parses the result of Stepper.runFully into an Expr End
runExpr :: Stepper (Expr End)
-- | Converts a given top level expr into a list of final states and the
-- associated path conditions for each state.
flattenExpr :: Expr End -> [Expr End]
-- | Strips unreachable branches from a given expr Returns a list of
-- executed SMT queries alongside the reduced expression for debugging
-- purposes Note that the reduced expression loses information relative
-- to the original one if jump conditions are removed. This restriction
-- can be removed once Expr supports attaching knowledge to AST nodes.
-- Although this algorithm currently parallelizes nicely, it does not
-- exploit the incremental nature of the task at hand. Introducing
-- support for incremental queries might let us go even faster here.
-- TODO: handle errors properly
reachable :: SolverGroup -> Expr End -> IO ([SMT2], Expr End)
-- | Evaluate the provided proposition down to its most concrete result
evalProp :: Prop -> Prop
-- | Extract contraints stored in Expr End nodes
extractProps :: Expr End -> [Prop]
isPartial :: Expr a -> Bool
getPartials :: [Expr End] -> [PartialExec]
-- | Symbolically execute the VM and check all endstates against the
-- postcondition, if available.
verify :: SolverGroup -> VeriOpts -> VM -> Maybe Postcondition -> IO (Expr End, [VerifyResult])
type UnsatCache = TVar [Set Prop]
-- | Compares two contract runtimes for trace equivalence by running two
-- VMs and comparing the end states.
--
-- We do this by asking the solver to find a common input for each pair
-- of endstates that satisfies the path conditions for both sides and
-- produces a differing output. If we can find such an input, then we
-- have a clear equivalence break, and since we run this check for every
-- pair of end states, the check is exhaustive.
equivalenceCheck :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> (Expr Buf, [Prop]) -> IO [EquivResult]
equivalenceCheck' :: SolverGroup -> [Expr End] -> [Expr End] -> VeriOpts -> IO [EquivResult]
both' :: (a -> b) -> (a, a) -> (b, b)
produceModels :: SolverGroup -> Expr End -> IO [(Expr End, CheckSatResult)]
showModel :: Expr Buf -> (Expr End, CheckSatResult) -> IO ()
formatCex :: Expr Buf -> SMTCex -> Text
-- | Takes a buffer and a Cex and replaces all abstract values in the buf
-- with concrete ones from the Cex.
subModel :: SMTCex -> Expr a -> Expr a
instance GHC.Generics.Generic EVM.SymExec.LoopHeuristic
instance Options.Generic.ParseRecord EVM.SymExec.LoopHeuristic
instance Options.Generic.ParseFields EVM.SymExec.LoopHeuristic
instance Options.Generic.ParseField EVM.SymExec.LoopHeuristic
instance GHC.Read.Read EVM.SymExec.LoopHeuristic
instance GHC.Show.Show EVM.SymExec.LoopHeuristic
instance GHC.Classes.Eq EVM.SymExec.LoopHeuristic
instance (GHC.Classes.Eq a, GHC.Classes.Eq b, GHC.Classes.Eq c) => GHC.Classes.Eq (EVM.SymExec.ProofResult a b c)
instance (GHC.Show.Show a, GHC.Show.Show b, GHC.Show.Show c) => GHC.Show.Show (EVM.SymExec.ProofResult a b c)
instance GHC.Show.Show EVM.SymExec.VeriOpts
instance GHC.Classes.Eq EVM.SymExec.VeriOpts
instance GHC.Classes.Eq EVM.SymExec.CalldataFragment
instance GHC.Show.Show EVM.SymExec.CalldataFragment
module EVM.UnitTest
data UnitTestOptions
UnitTestOptions :: RpcInfo -> SolverGroup -> Maybe Int -> Maybe Integer -> Integer -> Bool -> Maybe Int -> Maybe Natural -> Maybe Text -> Maybe Text -> Text -> Int -> Maybe (Text, ByteString) -> (VM -> VM) -> DappInfo -> TestVMParams -> Bool -> UnitTestOptions
[$sel:rpcInfo:UnitTestOptions] :: UnitTestOptions -> RpcInfo
[$sel:solvers:UnitTestOptions] :: UnitTestOptions -> SolverGroup
[$sel:verbose:UnitTestOptions] :: UnitTestOptions -> Maybe Int
[$sel:maxIter:UnitTestOptions] :: UnitTestOptions -> Maybe Integer
[$sel:askSmtIters:UnitTestOptions] :: UnitTestOptions -> Integer
[$sel:smtDebug:UnitTestOptions] :: UnitTestOptions -> Bool
[$sel:maxDepth:UnitTestOptions] :: UnitTestOptions -> Maybe Int
[$sel:smtTimeout:UnitTestOptions] :: UnitTestOptions -> Maybe Natural
[$sel:solver:UnitTestOptions] :: UnitTestOptions -> Maybe Text
[$sel:covMatch:UnitTestOptions] :: UnitTestOptions -> Maybe Text
[$sel:match:UnitTestOptions] :: UnitTestOptions -> Text
[$sel:fuzzRuns:UnitTestOptions] :: UnitTestOptions -> Int
[$sel:replay:UnitTestOptions] :: UnitTestOptions -> Maybe (Text, ByteString)
[$sel:vmModifier:UnitTestOptions] :: UnitTestOptions -> VM -> VM
[$sel:dapp:UnitTestOptions] :: UnitTestOptions -> DappInfo
[$sel:testParams:UnitTestOptions] :: UnitTestOptions -> TestVMParams
[$sel:ffiAllowed:UnitTestOptions] :: UnitTestOptions -> Bool
data TestVMParams
TestVMParams :: Addr -> Addr -> Addr -> Word64 -> Word64 -> W256 -> W256 -> W256 -> Addr -> W256 -> W256 -> Word64 -> W256 -> W256 -> W256 -> W256 -> TestVMParams
[$sel:address:TestVMParams] :: TestVMParams -> Addr
[$sel:caller:TestVMParams] :: TestVMParams -> Addr
[$sel:origin:TestVMParams] :: TestVMParams -> Addr
[$sel:gasCreate:TestVMParams] :: TestVMParams -> Word64
[$sel:gasCall:TestVMParams] :: TestVMParams -> Word64
[$sel:baseFee:TestVMParams] :: TestVMParams -> W256
[$sel:priorityFee:TestVMParams] :: TestVMParams -> W256
[$sel:balanceCreate:TestVMParams] :: TestVMParams -> W256
[$sel:coinbase:TestVMParams] :: TestVMParams -> Addr
[$sel:number:TestVMParams] :: TestVMParams -> W256
[$sel:timestamp:TestVMParams] :: TestVMParams -> W256
[$sel:gaslimit:TestVMParams] :: TestVMParams -> Word64
[$sel:gasprice:TestVMParams] :: TestVMParams -> W256
[$sel:maxCodeSize:TestVMParams] :: TestVMParams -> W256
[$sel:prevrandao:TestVMParams] :: TestVMParams -> W256
[$sel:chainId:TestVMParams] :: TestVMParams -> W256
defaultGasForCreating :: Word64
defaultGasForInvoking :: Word64
defaultBalanceForTestContract :: W256
defaultMaxCodeSize :: W256
type ABIMethod = Text
-- | Generate VeriOpts from UnitTestOptions
makeVeriOpts :: UnitTestOptions -> VeriOpts
-- | Top level CLI endpoint for hevm test
unitTest :: UnitTestOptions -> Contracts -> Maybe String -> IO Bool
-- | Assuming a constructor is loaded, this stepper will run the
-- constructor to create the test contract, give it an initial balance,
-- and run `setUp()'.
initializeUnitTest :: UnitTestOptions -> SolcContract -> Stepper ()
-- | Assuming a test contract is loaded and initialized, this stepper will
-- run the specified test method and return whether it succeeded.
runUnitTest :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool
execTestStepper :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool
exploreStep :: UnitTestOptions -> ByteString -> Stepper Bool
checkFailures :: UnitTestOptions -> ABIMethod -> Bool -> Stepper Bool
-- | Randomly generates the calldata arguments and runs the test
fuzzTest :: UnitTestOptions -> Text -> [AbiType] -> VM -> Property
tick :: Text -> IO ()
-- | This is like an unresolved source mapping.
data OpLocation
OpLocation :: Contract -> Int -> OpLocation
[$sel:srcContract:OpLocation] :: OpLocation -> Contract
[$sel:srcOpIx:OpLocation] :: OpLocation -> Int
srcMapForOpLocation :: DappInfo -> OpLocation -> Maybe SrcMap
type CoverageState = (VM, MultiSet OpLocation)
currentOpLocation :: VM -> OpLocation
execWithCoverage :: StateT CoverageState IO VMResult
runWithCoverage :: StateT CoverageState IO VM
interpretWithCoverage :: UnitTestOptions -> Stepper a -> StateT CoverageState IO a
coverageReport :: DappInfo -> MultiSet SrcMap -> Map FilePath (Vector (Int, ByteString))
coverageForUnitTestContract :: UnitTestOptions -> Map Text SolcContract -> SourceCache -> (Text, [(Test, [AbiType])]) -> IO (MultiSet SrcMap)
runUnitTestContract :: UnitTestOptions -> Map Text SolcContract -> (Text, [(Test, [AbiType])]) -> IO [(Bool, VM)]
runTest :: UnitTestOptions -> VM -> (Test, [AbiType]) -> IO (Text, Either Text Text, VM)
type ExploreTx = (Addr, Addr, ByteString, W256)
decodeCalls :: ByteString -> [ExploreTx]
-- | Runs an invariant test, calls the invariant before execution begins
initialExplorationStepper :: UnitTestOptions -> ABIMethod -> [ExploreTx] -> [Addr] -> Int -> Stepper (Bool, RLP)
explorationStepper :: UnitTestOptions -> ABIMethod -> [ExploreTx] -> [Addr] -> RLP -> Int -> Stepper (Bool, RLP)
getTargetContracts :: UnitTestOptions -> Stepper [Addr]
exploreRun :: UnitTestOptions -> VM -> ABIMethod -> [ExploreTx] -> IO (Text, Either Text Text, VM)
execTest :: UnitTestOptions -> VM -> ABIMethod -> AbiValue -> IO (Bool, VM)
-- | Define the thread spawner for normal test cases
runOne :: UnitTestOptions -> VM -> ABIMethod -> AbiValue -> IO (Text, Either Text Text, VM)
-- | Define the thread spawner for property based tests
fuzzRun :: UnitTestOptions -> VM -> Text -> [AbiType] -> IO (Text, Either Text Text, VM)
-- | Define the thread spawner for symbolic tests
symRun :: UnitTestOptions -> VM -> Text -> [AbiType] -> IO (Text, Either Text Text, VM)
symFailure :: UnitTestOptions -> Text -> Expr Buf -> [AbiType] -> [(Expr End, SMTCex)] -> Text
prettyCalldata :: (?context :: DappContext) => SMTCex -> Expr Buf -> Text -> [AbiType] -> Text
showCalldata :: (?context :: DappContext) => SMTCex -> [AbiType] -> Expr Buf -> Text
showVal :: AbiValue -> Text
execSymTest :: UnitTestOptions -> ABIMethod -> (Expr Buf, [Prop]) -> Stepper (Expr End)
checkSymFailures :: UnitTestOptions -> Stepper VM
indentLines :: Int -> Text -> Text
passOutput :: VM -> UnitTestOptions -> Text -> Text
failOutput :: VM -> UnitTestOptions -> Text -> Text
formatTestLogs :: (?context :: DappContext) => Map W256 Event -> [Expr Log] -> Text
formatTestLog :: (?context :: DappContext) => Map W256 Event -> Expr Log -> Maybe Text
abiCall :: TestVMParams -> Either (Text, AbiValue) ByteString -> EVM ()
makeTxCall :: TestVMParams -> (Expr Buf, [Prop]) -> EVM ()
initialUnitTestVm :: UnitTestOptions -> SolcContract -> VM
getParametersFromEnvironmentVariables :: Maybe Text -> IO TestVMParams
instance GHC.Show.Show EVM.UnitTest.OpLocation
instance GHC.Classes.Eq EVM.UnitTest.OpLocation
instance GHC.Classes.Ord EVM.UnitTest.OpLocation
module EVM.Dev
checkEquiv :: Typeable a => Expr a -> Expr a -> IO ()
runDappTest :: FilePath -> IO ()
testOpts :: SolverGroup -> FilePath -> FilePath -> IO UnitTestOptions
doTest :: IO ()
analyzeDai :: IO ()
daiExpr :: IO (Expr End)
analyzeVat :: IO ()
analyzeDeposit :: IO ()
reachable' :: Bool -> ByteString -> IO ()
showExpr :: ByteString -> IO ()
summaryStore :: IO ByteString
safeAdd :: IO ByteString
testContract :: IO ByteString
vat :: IO ByteString
initVm :: ByteString -> VM
-- | Builds the Expr for the given evm bytecode object
buildExpr :: SolverGroup -> ByteString -> IO (Expr End)
dai :: IO ByteString
module EVM.TTY
data Name
AbiPane :: Name
StackPane :: Name
BytecodePane :: Name
TracePane :: Name
SolidityPane :: Name
TestPickerPane :: Name
BrowserPane :: Name
Pager :: Name
type UiWidget = Widget Name
data UiVmState
UiVmState :: VM -> Int -> Map Int (VM, Stepper ()) -> Stepper () -> Bool -> UnitTestOptions -> UiVmState
[$sel:vm:UiVmState] :: UiVmState -> VM
[$sel:step:UiVmState] :: UiVmState -> Int
[$sel:snapshots:UiVmState] :: UiVmState -> Map Int (VM, Stepper ())
[$sel:stepper:UiVmState] :: UiVmState -> Stepper ()
[$sel:showMemory:UiVmState] :: UiVmState -> Bool
[$sel:testOpts:UiVmState] :: UiVmState -> UnitTestOptions
data UiTestPickerState
UiTestPickerState :: List Name (Text, Text) -> DappInfo -> UnitTestOptions -> UiTestPickerState
[$sel:tests:UiTestPickerState] :: UiTestPickerState -> List Name (Text, Text)
[$sel:dapp:UiTestPickerState] :: UiTestPickerState -> DappInfo
[$sel:opts:UiTestPickerState] :: UiTestPickerState -> UnitTestOptions
data UiBrowserState
UiBrowserState :: List Name (Addr, Contract) -> UiVmState -> UiBrowserState
[$sel:contracts:UiBrowserState] :: UiBrowserState -> List Name (Addr, Contract)
[$sel:vm:UiBrowserState] :: UiBrowserState -> UiVmState
data UiState
ViewVm :: UiVmState -> UiState
ViewContracts :: UiBrowserState -> UiState
ViewPicker :: UiTestPickerState -> UiState
ViewHelp :: UiVmState -> UiState
_ViewHelp :: Prism' UiState UiVmState
_ViewPicker :: Prism' UiState UiTestPickerState
_ViewContracts :: Prism' UiState UiBrowserState
_ViewVm :: Prism' UiState UiVmState
snapshotInterval :: Int
type Pred a = a -> Bool
data StepMode
-- | Run a specific number of steps
Step :: !Int -> StepMode
-- | Finish when a VM predicate holds
StepUntil :: Pred VM -> StepMode
-- | Each step command in the terminal should finish immediately with one
-- of these outcomes.
data Continuation a
-- | Program finished
Stopped :: a -> Continuation a
-- | Took one step; more steps to go
Continue :: Stepper a -> Continuation a
-- | This turns a Stepper into a state action usable from within
-- the TTY loop, yielding a StepOutcome depending on the
-- StepMode.
interpret :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => StepMode -> Stepper a -> StateT UiVmState IO (Continuation a)
keepExecuting :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => StepMode -> Stepper a -> StateT UiVmState IO (Continuation a)
isUnitTestContract :: Text -> DappInfo -> Bool
mkVty :: IO Vty
runFromVM :: SolverGroup -> RpcInfo -> Maybe Integer -> DappInfo -> VM -> IO VM
initUiVmState :: VM -> UnitTestOptions -> Stepper () -> UiVmState
debuggableTests :: UnitTestOptions -> (Text, [(Test, [AbiType])]) -> [(Text, Text)]
isFuzzTest :: (Test, [AbiType]) -> Bool
main :: UnitTestOptions -> FilePath -> Maybe BuildOutput -> IO ()
takeStep :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => UiVmState -> StepMode -> EventM n UiState ()
backstepUntil :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => (UiVmState -> Pred VM) -> EventM n UiState ()
backstep :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => UiVmState -> IO UiVmState
appEvent :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => BrickEvent Name e -> EventM Name UiState ()
app :: UnitTestOptions -> App UiState () Name
initialUiVmStateForTest :: UnitTestOptions -> (Text, Text) -> UiVmState
myTheme :: [(AttrName, Attr)]
drawUi :: UiState -> [UiWidget]
drawHelpView :: [UiWidget]
drawTestPicker :: UiTestPickerState -> [UiWidget]
drawVmBrowser :: UiBrowserState -> [UiWidget]
drawVm :: UiVmState -> [UiWidget]
drawHelpBar :: UiWidget
stepOneOpcode :: Stepper a -> StateT UiVmState IO ()
isNewTraceAdded :: UiVmState -> Pred VM
isNextSourcePosition :: UiVmState -> Pred VM
isNextSourcePositionWithoutEntering :: UiVmState -> Pred VM
isExecutionHalted :: UiVmState -> Pred VM
currentSrcMap :: DappInfo -> VM -> Maybe SrcMap
drawStackPane :: UiVmState -> UiWidget
message :: VM -> String
drawBytecodePane :: UiVmState -> UiWidget
dim :: Widget n -> Widget n
withHighlight :: Bool -> Widget n -> Widget n
prettyIfConcrete :: Expr Buf -> String
drawTracePane :: UiVmState -> UiWidget
ourWrap :: String -> Widget n
solidityList :: VM -> DappInfo -> List Name (Int, ByteString)
drawSolidityPane :: UiVmState -> UiWidget
ifTallEnough :: Int -> Widget n -> Widget n -> Widget n
opWidget :: (Integral a, Show a) => (a, Op) -> Widget n
selectedAttr :: AttrName
dimAttr :: AttrName
wordAttr :: AttrName
boldAttr :: AttrName
activeAttr :: AttrName
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Brick.Widgets.List.List EVM.TTY.Name (EVM.Types.Addr, EVM.Types.Contract), b GHC.Types.~ Brick.Widgets.List.List EVM.TTY.Name (EVM.Types.Addr, EVM.Types.Contract)) => Optics.Label.LabelOptic "contracts" k EVM.TTY.UiBrowserState EVM.TTY.UiBrowserState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.TTY.UiVmState, b GHC.Types.~ EVM.TTY.UiVmState) => Optics.Label.LabelOptic "vm" k EVM.TTY.UiBrowserState EVM.TTY.UiBrowserState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Dapp.DappInfo, b GHC.Types.~ EVM.Dapp.DappInfo) => Optics.Label.LabelOptic "dapp" k EVM.TTY.UiTestPickerState EVM.TTY.UiTestPickerState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.UnitTest.UnitTestOptions, b GHC.Types.~ EVM.UnitTest.UnitTestOptions) => Optics.Label.LabelOptic "opts" k EVM.TTY.UiTestPickerState EVM.TTY.UiTestPickerState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Brick.Widgets.List.List EVM.TTY.Name (Data.Text.Internal.Text, Data.Text.Internal.Text), b GHC.Types.~ Brick.Widgets.List.List EVM.TTY.Name (Data.Text.Internal.Text, Data.Text.Internal.Text)) => Optics.Label.LabelOptic "tests" k EVM.TTY.UiTestPickerState EVM.TTY.UiTestPickerState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "showMemory" k EVM.TTY.UiVmState EVM.TTY.UiVmState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map GHC.Types.Int (EVM.Types.VM, EVM.Stepper.Stepper ()), b GHC.Types.~ Data.Map.Internal.Map GHC.Types.Int (EVM.Types.VM, EVM.Stepper.Stepper ())) => Optics.Label.LabelOptic "snapshots" k EVM.TTY.UiVmState EVM.TTY.UiVmState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Int, b GHC.Types.~ GHC.Types.Int) => Optics.Label.LabelOptic "step" k EVM.TTY.UiVmState EVM.TTY.UiVmState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Stepper.Stepper (), b GHC.Types.~ EVM.Stepper.Stepper ()) => Optics.Label.LabelOptic "stepper" k EVM.TTY.UiVmState EVM.TTY.UiVmState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.UnitTest.UnitTestOptions, b GHC.Types.~ EVM.UnitTest.UnitTestOptions) => Optics.Label.LabelOptic "testOpts" k EVM.TTY.UiVmState EVM.TTY.UiVmState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.VM, b GHC.Types.~ EVM.Types.VM) => Optics.Label.LabelOptic "vm" k EVM.TTY.UiVmState EVM.TTY.UiVmState a b
instance GHC.Classes.Ord EVM.TTY.Name
instance GHC.Show.Show EVM.TTY.Name
instance GHC.Classes.Eq EVM.TTY.Name