| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
EVM.Types
Contents
Synopsis
- data Word512 = Word512 !Word256 !Word256
- data Int512 = Int512 !Int256 !Word256
- data EType
- data GVar (a :: EType) where
- data Expr (a :: EType) where
- Lit :: !W256 -> Expr EWord
- Var :: Text -> Expr EWord
- GVar :: GVar a -> Expr a
- LitByte :: !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 = forall a.Typeable a => SomeExpr (Expr a)
- toNum :: Typeable a => Expr a -> Int
- data Prop where
- 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
- (.||) :: Prop -> Prop -> Prop
- (.<) :: Expr EWord -> Expr EWord -> Prop
- (.<=) :: Expr EWord -> Expr EWord -> Prop
- (.>) :: Expr EWord -> Expr EWord -> Prop
- (.>=) :: Expr EWord -> Expr EWord -> Prop
- (.==) :: Typeable a => Expr a -> Expr a -> Prop
- (./=) :: Typeable a => Expr a -> Expr a -> Prop
- pand :: [Prop] -> Prop
- por :: [Prop] -> Prop
- data EvmError
- = BalanceTooLow W256 W256
- | UnrecognizedOpcode Word8
- | SelfDestruction
- | StackUnderrun
- | BadJumpDestination
- | Revert (Expr Buf)
- | OutOfGas Word64 Word64
- | StackLimitExceeded
- | IllegalOverflow
- | StateChangeWhileStatic
- | InvalidMemoryAccess
- | CallDepthLimitReached
- | MaxCodeSizeExceeded W256 W256
- | MaxInitCodeSizeExceeded W256 W256
- | InvalidFormat
- | PrecompileFailure
- | ReturnDataOutOfBounds
- | NonceOverflow
- | BadCheatCode FunctionSelector
- data PartialExec
- data Effect
- data Query where
- PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query
- PleaseFetchSlot :: Addr -> W256 -> (W256 -> EVM ()) -> Query
- PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query
- PleaseDoFFI :: [String] -> (ByteString -> EVM ()) -> Query
- data Choose where
- data BranchCondition
- data VMResult
- data VM = VM {
- result :: Maybe VMResult
- state :: FrameState
- frames :: [Frame]
- env :: Env
- block :: Block
- tx :: TxState
- logs :: [Expr Log]
- traces :: TreePos Empty Trace
- cache :: Cache
- burned :: !Word64
- iterations :: Map CodeLocation (Int, [Expr EWord])
- constraints :: [Prop]
- keccakEqs :: [Prop]
- allowFFI :: Bool
- overrideCaller :: Maybe Addr
- type EVM a = State VM a
- data Frame = Frame {}
- data FrameContext
- = CreationContext { }
- | CallContext { }
- data SubState = SubState {
- selfdestructs :: [Addr]
- touchedAccounts :: [Addr]
- accessedAddresses :: Set Addr
- accessedStorageKeys :: Set (Addr, W256)
- refunds :: [(Addr, Word64)]
- data FrameState = FrameState {}
- data TxState = TxState {}
- data StorageModel
- data Env = Env {}
- data Block = Block {}
- data Contract = Contract {}
- type CodeLocation = (Addr, Int)
- data Cache = Cache {
- fetchedContracts :: Map Addr Contract
- fetchedStorage :: Map W256 (Map W256 W256)
- path :: Map (CodeLocation, Int) Bool
- unifyCachedStorage :: Map W256 W256 -> Map W256 W256 -> Map W256 W256
- unifyCachedContract :: Contract -> Contract -> Contract
- data ContractCode
- data RuntimeCode
- data Trace = Trace {}
- data TraceData
- = EventTrace (Expr EWord) (Expr Buf) [Expr EWord]
- | FrameTrace FrameContext
- | ErrorTrace EvmError
- | EntryTrace Text
- | ReturnTrace (Expr Buf) FrameContext
- data Traces = Traces {}
- data VMOpts = VMOpts {
- contract :: Contract
- calldata :: (Expr Buf, [Prop])
- initialStorage :: Expr Storage
- value :: Expr EWord
- priorityFee :: W256
- address :: Addr
- caller :: Expr EWord
- origin :: Addr
- gas :: Word64
- gaslimit :: Word64
- number :: W256
- timestamp :: Expr EWord
- coinbase :: Addr
- prevRandao :: W256
- maxCodeSize :: W256
- blockGaslimit :: Word64
- gasprice :: W256
- baseFee :: W256
- schedule :: FeeSchedule Word64
- chainId :: W256
- create :: Bool
- txAccessList :: Map Addr [W256]
- allowFFI :: Bool
- type Op = GenericOp (Expr EWord)
- data GenericOp a
- = OpStop
- | OpAdd
- | OpMul
- | OpSub
- | OpDiv
- | OpSdiv
- | OpMod
- | OpSmod
- | OpAddmod
- | OpMulmod
- | OpExp
- | OpSignextend
- | OpLt
- | OpGt
- | OpSlt
- | OpSgt
- | OpEq
- | OpIszero
- | OpAnd
- | OpOr
- | OpXor
- | OpNot
- | OpByte
- | OpShl
- | OpShr
- | OpSar
- | OpSha3
- | OpAddress
- | OpBalance
- | OpOrigin
- | OpCaller
- | OpCallvalue
- | OpCalldataload
- | OpCalldatasize
- | OpCalldatacopy
- | OpCodesize
- | OpCodecopy
- | OpGasprice
- | OpExtcodesize
- | OpExtcodecopy
- | OpReturndatasize
- | OpReturndatacopy
- | OpExtcodehash
- | OpBlockhash
- | OpCoinbase
- | OpTimestamp
- | OpNumber
- | OpPrevRandao
- | OpGaslimit
- | OpChainid
- | OpSelfbalance
- | OpBaseFee
- | OpPop
- | OpMload
- | OpMstore
- | OpMstore8
- | OpSload
- | OpSstore
- | OpJump
- | OpJumpi
- | OpPc
- | OpMsize
- | OpGas
- | OpJumpdest
- | OpCreate
- | OpCall
- | OpStaticcall
- | OpCallcode
- | OpReturn
- | OpDelegatecall
- | OpCreate2
- | OpRevert
- | OpSelfdestruct
- | OpDup !Word8
- | OpSwap !Word8
- | OpLog !Word8
- | OpPush0
- | OpPush a
- | OpUnknown Word8
- newtype FunctionSelector = FunctionSelector {}
- newtype ByteStringS = ByteStringS ByteString
- newtype W256 = W256 Word256
- wordField :: Object -> Key -> Parser W256
- newtype W64 = W64 Word64
- word64Field :: Object -> Key -> Parser Word64
- newtype Addr = Addr {}
- toChecksumAddress :: String -> String
- addrField :: Object -> Key -> Parser Addr
- addrFieldMaybe :: Object -> Key -> Parser (Maybe Addr)
- newtype Nibble = Nibble Word8
- 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
Documentation
Instances
Instances
data GVar (a :: EType) where Source #
Instances
| Show (GVar a) Source # | |
| Eq (GVar a) Source # | |
| Ord (GVar a) Source # | |
data Expr (a :: EType) where Source #
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.
Constructors
Instances
| Monoid (Expr 'Buf) Source # | |
| Semigroup (Expr 'Buf) Source # | |
| Show (Expr a) Source # | |
| Eq (Expr a) Source # | |
| Ord (Expr a) Source # | |
| TraversableTerm (Expr a) Source # | |
Instances
| Show SomeExpr Source # | |
| Eq SomeExpr Source # | |
| Ord SomeExpr Source # | |
Defined in EVM.Types | |
Constructors
| 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 |
Core EVM Error Types
Constructors
Instances
| Show EvmError Source # | |
| Eq EvmError Source # | |
| Ord EvmError Source # | |
Defined in EVM.Types | |
data PartialExec Source #
Sometimes we can only partially execute a given program
Constructors
| UnexpectedSymbolicArg | |
| MaxIterationsReached | |
Instances
| Show PartialExec Source # | |
| Eq PartialExec Source # | |
Defined in EVM.Types Methods (==) :: PartialExec -> PartialExec -> Bool Source # (/=) :: PartialExec -> PartialExec -> Bool Source # | |
| Ord PartialExec Source # | |
Defined in EVM.Types Methods compare :: PartialExec -> PartialExec -> Ordering Source # (<) :: PartialExec -> PartialExec -> Bool Source # (<=) :: PartialExec -> PartialExec -> Bool Source # (>) :: PartialExec -> PartialExec -> Bool Source # (>=) :: PartialExec -> PartialExec -> Bool Source # max :: PartialExec -> PartialExec -> PartialExec Source # min :: PartialExec -> PartialExec -> PartialExec Source # | |
Effect types used by the vm implementation for side effects & control flow
Queries halt execution until resolved through RPC calls or SMT queries
Constructors
| PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query | |
| PleaseFetchSlot :: Addr -> W256 -> (W256 -> EVM ()) -> Query | |
| PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query | |
| PleaseDoFFI :: [String] -> (ByteString -> EVM ()) -> Query |
Execution could proceed down one of two branches
data BranchCondition Source #
The possible return values of a SMT query
The possible result states of a VM
Constructors
| VMFailure EvmError | An operation failed |
| VMSuccess (Expr Buf) | Reached STOP, RETURN, or end-of-code |
| HandleEffect Effect | An effect must be handled for execution to continue |
| Unfinished PartialExec | Execution could not continue further |
The state of a stepwise EVM execution
Constructors
| VM | |
Fields
| |
Instances
An entry in the VM's "call/create stack"
Constructors
| Frame | |
Fields
| |
Instances
| Show Frame Source # | |
| (k ~ A_Lens, a ~ FrameContext, b ~ FrameContext) => LabelOptic "context" k Frame Frame a b Source # | |
| (k ~ A_Lens, a ~ FrameState, b ~ FrameState) => LabelOptic "state" k Frame Frame a b Source # | |
data FrameContext Source #
Call/create info
Constructors
| CreationContext | |
| CallContext | |
Instances
The "accrued substate" across a transaction
Constructors
| SubState | |
Fields
| |
Instances
| Show SubState Source # | |
| Eq SubState Source # | |
| Ord SubState Source # | |
Defined in EVM.Types | |
| (k ~ A_Lens, a ~ Set Addr, b ~ Set Addr) => LabelOptic "accessedAddresses" k SubState SubState a b Source # | |
| (k ~ A_Lens, a ~ Set (Addr, W256), b ~ Set (Addr, W256)) => LabelOptic "accessedStorageKeys" k SubState SubState a b Source # | |
| (k ~ A_Lens, a ~ [(Addr, Word64)], b ~ [(Addr, Word64)]) => LabelOptic "refunds" k SubState SubState a b Source # | |
| (k ~ A_Lens, a ~ [Addr], b ~ [Addr]) => LabelOptic "selfdestructs" k SubState SubState a b Source # | |
| (k ~ A_Lens, a ~ [Addr], b ~ [Addr]) => LabelOptic "touchedAccounts" k SubState SubState a b Source # | |
data FrameState Source #
The "registers" of the VM along with memory and data stack
Constructors
| FrameState | |
Instances
The state that spans a whole transaction
Constructors
| TxState | |
Instances
| Show TxState Source # | |
| (k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "gaslimit" k TxState TxState a b Source # | |
| (k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "gasprice" k TxState TxState a b Source # | |
| (k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "isCreate" k TxState TxState a b Source # | |
| (k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "origin" k TxState TxState a b Source # | |
| (k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "priorityFee" k TxState TxState a b Source # | |
| (k ~ A_Lens, a ~ SubState, b ~ SubState) => LabelOptic "substate" k TxState TxState a b Source # | |
| (k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "toAddr" k TxState TxState a b Source # | |
| (k ~ A_Lens, a ~ Map Addr Contract, b ~ Map Addr Contract) => LabelOptic "txReversion" k TxState TxState a b Source # | |
| (k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "value" k TxState TxState a b Source # | |
data StorageModel Source #
When doing symbolic execution, we have three different ways to model the storage of contracts. This determines not only the initial contract storage model but also how RPC or state fetched contracts will be modeled.
Constructors
| ConcreteS | Uses |
| SymbolicS | Uses |
| InitialS | Uses |
Instances
| Read StorageModel Source # | |
| Show StorageModel Source # | |
| ParseField StorageModel Source # | |
Defined in EVM.Types Methods parseField :: Maybe Text -> Maybe Text -> Maybe Char -> Maybe String -> Parser StorageModel Source # parseListOfField :: Maybe Text -> Maybe Text -> Maybe Char -> Maybe String -> Parser [StorageModel] Source # readField :: ReadM StorageModel Source # metavar :: proxy StorageModel -> String Source # | |
Various environmental data
Constructors
| Env | |
Instances
Data about the block
Constructors
| Block | |
Instances
The state of a contract
Constructors
| Contract | |
Instances
| Show Contract Source # | |
| Eq Contract Source # | |
| Ord Contract Source # | |
Defined in EVM.Types | |
| (k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "balance" k Contract Contract a b Source # | |
| (k ~ A_Lens, a ~ Vector (Int, Op), b ~ Vector (Int, Op)) => LabelOptic "codeOps" k Contract Contract a b Source # | |
| (k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "codehash" k Contract Contract a b Source # | |
| (k ~ A_Lens, a ~ ContractCode, b ~ ContractCode) => LabelOptic "contractcode" k Contract Contract a b Source # | |
| (k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "external" k Contract Contract a b Source # | |
| (k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "nonce" k Contract Contract a b Source # | |
| (k ~ A_Lens, a ~ Vector Int, b ~ Vector Int) => LabelOptic "opIxMap" k Contract Contract a b Source # | |
type CodeLocation = (Addr, Int) Source #
A unique id for a given pc
The cache is data that can be persisted for efficiency: any expensive query that is constant at least within a block.
Constructors
| Cache | |
Fields
| |
Instances
data ContractCode Source #
A contract is either in creation (running its "constructor") or
post-creation, and code in these two modes is treated differently
by instructions like EXTCODEHASH, so we distinguish these two
code types.
The definition follows the structure of code output by solc. We need to use some heuristics here to deal with symbolic data regions that may be present in the bytecode since the fully abstract case is impractical:
- initcode has concrete code, followed by an abstract data "section"
- runtimecode has a fixed length, but may contain fixed size symbolic regions (due to immutable)
hopefully we do not have to deal with dynamic immutable before we get a real data section...
Constructors
| InitCode ByteString (Expr Buf) | Constructor code, during contract creation |
| RuntimeCode RuntimeCode | Instance code, after contract creation |
Instances
| Show ContractCode Source # | |
| Eq ContractCode Source # | |
Defined in EVM.Types Methods (==) :: ContractCode -> ContractCode -> Bool Source # (/=) :: ContractCode -> ContractCode -> Bool Source # | |
| Ord ContractCode Source # | |
Defined in EVM.Types Methods compare :: ContractCode -> ContractCode -> Ordering Source # (<) :: ContractCode -> ContractCode -> Bool Source # (<=) :: ContractCode -> ContractCode -> Bool Source # (>) :: ContractCode -> ContractCode -> Bool Source # (>=) :: ContractCode -> ContractCode -> Bool Source # max :: ContractCode -> ContractCode -> ContractCode Source # min :: ContractCode -> ContractCode -> ContractCode Source # | |
data RuntimeCode Source #
We have two variants here to optimize the fully concrete case. ConcreteRuntimeCode just wraps a ByteString SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).
Constructors
| ConcreteRuntimeCode ByteString | |
| SymbolicRuntimeCode (Vector (Expr Byte)) |
Instances
| Show RuntimeCode Source # | |
| Eq RuntimeCode Source # | |
Defined in EVM.Types Methods (==) :: RuntimeCode -> RuntimeCode -> Bool Source # (/=) :: RuntimeCode -> RuntimeCode -> Bool Source # | |
| Ord RuntimeCode Source # | |
Defined in EVM.Types Methods compare :: RuntimeCode -> RuntimeCode -> Ordering Source # (<) :: RuntimeCode -> RuntimeCode -> Bool Source # (<=) :: RuntimeCode -> RuntimeCode -> Bool Source # (>) :: RuntimeCode -> RuntimeCode -> Bool Source # (>=) :: RuntimeCode -> RuntimeCode -> Bool Source # max :: RuntimeCode -> RuntimeCode -> RuntimeCode Source # min :: RuntimeCode -> RuntimeCode -> RuntimeCode Source # | |
Instances
| Generic Trace Source # | |
| Show Trace Source # | |
| Eq Trace Source # | |
| Ord Trace Source # | |
Defined in EVM.Types | |
| (k ~ A_Lens, a ~ Contract, b ~ Contract) => LabelOptic "contract" k Trace Trace a b Source # | |
| (k ~ A_Lens, a ~ Int, b ~ Int) => LabelOptic "opIx" k Trace Trace a b Source # | |
| (k ~ A_Lens, a ~ TraceData, b ~ TraceData) => LabelOptic "tracedata" k Trace Trace a b Source # | |
| type Rep Trace Source # | |
Defined in EVM.Types type Rep Trace = D1 ('MetaData "Trace" "EVM.Types" "hevm-0.51.2-inplace" 'False) (C1 ('MetaCons "Trace" 'PrefixI 'True) (S1 ('MetaSel ('Just "opIx") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: (S1 ('MetaSel ('Just "contract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Contract) :*: S1 ('MetaSel ('Just "tracedata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TraceData)))) | |
Constructors
| EventTrace (Expr EWord) (Expr Buf) [Expr EWord] | |
| FrameTrace FrameContext | |
| ErrorTrace EvmError | |
| EntryTrace Text | |
| ReturnTrace (Expr Buf) FrameContext |
Instances
Wrapper type containing vm traces and the context needed to pretty print them properly
Instances
| Monoid Traces Source # | |
| Semigroup Traces Source # | |
| Generic Traces Source # | |
| Show Traces Source # | |
| Eq Traces Source # | |
| Ord Traces Source # | |
| type Rep Traces Source # | |
Defined in EVM.Types type Rep Traces = D1 ('MetaData "Traces" "EVM.Types" "hevm-0.51.2-inplace" 'False) (C1 ('MetaCons "Traces" 'PrefixI 'True) (S1 ('MetaSel ('Just "traces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Forest Trace)) :*: S1 ('MetaSel ('Just "contracts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Addr Contract)))) | |
A specification for an initial VM state
Constructors
| VMOpts | |
Fields
| |
Instances
Constructors
Instances
| Functor GenericOp Source # | |
| Show a => Show (GenericOp a) Source # | |
| Eq a => Eq (GenericOp a) Source # | |
| Ord a => Ord (GenericOp a) Source # | |
Defined in EVM.Types Methods compare :: GenericOp a -> GenericOp a -> Ordering Source # (<) :: GenericOp a -> GenericOp a -> Bool Source # (<=) :: GenericOp a -> GenericOp a -> Bool Source # (>) :: GenericOp a -> GenericOp a -> Bool Source # (>=) :: GenericOp a -> GenericOp a -> Bool Source # | |
newtype FunctionSelector Source #
Constructors
| FunctionSelector | |
Fields | |
Instances
newtype ByteStringS Source #
Constructors
| ByteStringS ByteString |
Instances
Instances
Instances
| FromJSON W64 Source # | |
| ToJSON W64 Source # | |
| Bits W64 Source # | |
Defined in EVM.Types Methods (.&.) :: W64 -> W64 -> W64 Source # (.|.) :: W64 -> W64 -> W64 Source # xor :: W64 -> W64 -> W64 Source # complement :: W64 -> W64 Source # shift :: W64 -> Int -> W64 Source # rotate :: W64 -> Int -> W64 Source # setBit :: W64 -> Int -> W64 Source # clearBit :: W64 -> Int -> W64 Source # complementBit :: W64 -> Int -> W64 Source # testBit :: W64 -> Int -> Bool Source # bitSizeMaybe :: W64 -> Maybe Int Source # bitSize :: W64 -> Int Source # isSigned :: W64 -> Bool Source # shiftL :: W64 -> Int -> W64 Source # unsafeShiftL :: W64 -> Int -> W64 Source # shiftR :: W64 -> Int -> W64 Source # unsafeShiftR :: W64 -> Int -> W64 Source # rotateL :: W64 -> Int -> W64 Source # | |
| FiniteBits W64 Source # | |
| Bounded W64 Source # | |
| Enum W64 Source # | |
Defined in EVM.Types | |
| Generic W64 Source # | |
| Num W64 Source # | |
| Read W64 Source # | |
| Integral W64 Source # | |
| Real W64 Source # | |
| Show W64 Source # | |
| Eq W64 Source # | |
| Ord W64 Source # | |
| type Rep W64 Source # | |
Constructors
| Addr | |
Fields | |
Instances
toChecksumAddress :: String -> String Source #
A four bit value
Instances
| Bounded Nibble Source # | |
| Enum Nibble Source # | |
Defined in EVM.Types Methods succ :: Nibble -> Nibble Source # pred :: Nibble -> Nibble Source # toEnum :: Int -> Nibble Source # fromEnum :: Nibble -> Int Source # enumFrom :: Nibble -> [Nibble] Source # enumFromThen :: Nibble -> Nibble -> [Nibble] Source # enumFromTo :: Nibble -> Nibble -> [Nibble] Source # enumFromThenTo :: Nibble -> Nibble -> Nibble -> [Nibble] Source # | |
| Generic Nibble Source # | |
| Num Nibble Source # | |
| Integral Nibble Source # | |
Defined in EVM.Types | |
| Real Nibble Source # | |
| Show Nibble Source # | |
| Eq Nibble Source # | |
| Ord Nibble Source # | |
| From Nibble Int Source # | |
| type Rep Nibble Source # | |
fromWord512 :: Word512 -> W256 Source #
word256 :: ByteString -> Word256 Source #
word :: ByteString -> W256 Source #
fromBE :: Integral a => ByteString -> a Source #
asBE :: Integral a => a -> ByteString Source #
word256Bytes :: W256 -> ByteString Source #
word160Bytes :: Addr -> ByteString Source #
unpackNibbles :: ByteString -> [Nibble] Source #
packNibbles :: [Nibble] -> ByteString Source #
bssToBs :: ByteStringS -> ByteString Source #
keccakBytes :: ByteString -> ByteString Source #
keccak' :: ByteString -> W256 Source #
internalError :: HasCallStack => [Char] -> a Source #
concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] Source #
padLeft :: Int -> ByteString -> ByteString Source #
padRight :: Int -> ByteString -> ByteString Source #
formatString :: ByteString -> String Source #