| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
EVM.Types
Contents
Synopsis
- data Word512 = Word512 !Word256 !Word256
- data Int512 = Int512 !Int256 !Word256
- truncateToAddr :: W256 -> Addr
- 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 -> Map (Expr EAddr) (Expr EContract) -> 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
- TxValue :: Expr EWord
- Balance :: Expr EAddr -> Expr EWord
- Gas :: Int -> Expr EWord
- CodeSize :: Expr EAddr -> Expr EWord
- CodeHash :: Expr EAddr -> Expr EWord
- LogEntry :: Expr EWord -> Expr Buf -> [Expr EWord] -> Expr Log
- C :: {..} -> Expr EContract
- SymAddr :: Text -> Expr EAddr
- LitAddr :: Addr -> Expr EAddr
- WAddr :: Expr EAddr -> Expr EWord
- ConcreteStore :: Map W256 W256 -> Expr Storage
- AbstractStore :: Expr EAddr -> Maybe W256 -> Expr Storage
- SLoad :: Expr EWord -> Expr Storage -> Expr EWord
- SStore :: 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
- isPBool :: Prop -> Bool
- data EvmError
- = BalanceTooLow (Expr EWord) (Expr EWord)
- | UnrecognizedOpcode Word8
- | SelfDestruction
- | StackUnderrun
- | BadJumpDestination
- | Revert (Expr Buf)
- | OutOfGas Word64 Word64
- | StackLimitExceeded
- | IllegalOverflow
- | StateChangeWhileStatic
- | InvalidMemoryAccess
- | CallDepthLimitReached
- | MaxCodeSizeExceeded W256 W256
- | MaxInitCodeSizeExceeded W256 (Expr EWord)
- | InvalidFormat
- | PrecompileFailure
- | ReturnDataOutOfBounds
- | NonceOverflow
- | BadCheatCode FunctionSelector
- | NonexistentFork Int
- data PartialExec
- data Effect t s where
- data Query t s where
- PleaseFetchContract :: Addr -> BaseState -> (Contract -> EVM t s ()) -> Query t s
- PleaseFetchSlot :: Addr -> W256 -> (W256 -> EVM t s ()) -> Query t s
- PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM Symbolic s ()) -> Query Symbolic s
- PleaseDoFFI :: [String] -> (ByteString -> EVM t s ()) -> Query t s
- data Choose s where
- data BranchCondition
- data VMResult (t :: VMType) s where
- Unfinished :: PartialExec -> VMResult Symbolic s
- VMFailure :: EvmError -> VMResult t s
- VMSuccess :: Expr Buf -> VMResult t s
- HandleEffect :: Effect t s -> VMResult t s
- data VMType
- type family Gas (t :: VMType) = r | r -> t where ...
- data VM (t :: VMType) s = VM {
- result :: Maybe (VMResult t s)
- state :: FrameState t s
- frames :: [Frame t s]
- env :: Env
- block :: Block
- tx :: TxState
- logs :: [Expr Log]
- traces :: TreePos Empty Trace
- cache :: Cache
- burned :: !(Gas t)
- iterations :: Map CodeLocation (Int, [Expr EWord])
- constraints :: [Prop]
- config :: RuntimeConfig
- forks :: Seq ForkState
- currentFork :: Int
- data ForkState = ForkState {}
- type EVM (t :: VMType) s a = StateT (VM t s) (ST s) a
- data BaseState
- data RuntimeConfig = RuntimeConfig {}
- data Frame (t :: VMType) s = Frame {
- context :: FrameContext
- state :: FrameState t s
- data FrameContext
- = CreationContext { }
- | CallContext { }
- data SubState = SubState {
- selfdestructs :: [Expr EAddr]
- touchedAccounts :: [Expr EAddr]
- accessedAddresses :: Set (Expr EAddr)
- accessedStorageKeys :: Set (Expr EAddr, W256)
- refunds :: [(Expr EAddr, Word64)]
- data FrameState (t :: VMType) s = FrameState {}
- data Memory s
- = ConcreteMemory (MutableMemory s)
- | SymbolicMemory !(Expr Buf)
- type MutableMemory s = STVector s Word8
- data TxState = TxState {}
- data Env = Env {}
- data Block = Block {}
- data Contract = Contract {}
- class VMOps (t :: VMType) where
- burn' :: Gas t -> EVM t s () -> EVM t s ()
- burnExp :: Expr EWord -> EVM t s () -> EVM t s ()
- burnSha3 :: Expr EWord -> EVM t s () -> EVM t s ()
- burnCalldatacopy :: Expr EWord -> EVM t s () -> EVM t s ()
- burnCodecopy :: Expr EWord -> EVM t s () -> EVM t s ()
- burnExtcodecopy :: Expr EAddr -> Expr EWord -> EVM t s () -> EVM t s ()
- burnReturndatacopy :: Expr EWord -> EVM t s () -> EVM t s ()
- burnLog :: Expr EWord -> Word8 -> EVM t s () -> EVM t s ()
- initialGas :: Gas t
- ensureGas :: Word64 -> EVM t s () -> EVM t s ()
- gasTryFrom :: Expr EWord -> Either () (Gas t)
- costOfCreate :: FeeSchedule Word64 -> Gas t -> Expr EWord -> Bool -> (Gas t, Gas t)
- costOfCall :: FeeSchedule Word64 -> Bool -> Expr EWord -> Gas t -> Gas t -> Expr EAddr -> (Word64 -> Word64 -> EVM t s ()) -> EVM t s ()
- reclaimRemainingGasAllowance :: VM t s -> EVM t s ()
- payRefunds :: EVM t s ()
- pushGas :: EVM t s ()
- enoughGas :: Word64 -> Gas t -> Bool
- subGas :: Gas t -> Word64 -> Gas t
- toGas :: Word64 -> Gas t
- whenSymbolicElse :: EVM t s a -> EVM t s a -> EVM t s a
- partial :: PartialExec -> EVM t s ()
- branch :: Expr EWord -> (Bool -> EVM t s ()) -> EVM t s ()
- type CodeLocation = (Expr EAddr, Int)
- data Cache = Cache {}
- 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 (t :: VMType) = VMOpts {
- contract :: Contract
- otherContracts :: [(Expr EAddr, Contract)]
- calldata :: (Expr Buf, [Prop])
- baseState :: BaseState
- value :: Expr EWord
- priorityFee :: W256
- address :: Expr EAddr
- caller :: Expr EAddr
- origin :: Expr EAddr
- gas :: Gas t
- gaslimit :: Word64
- number :: W256
- timestamp :: Expr EWord
- coinbase :: Expr EAddr
- prevRandao :: W256
- maxCodeSize :: W256
- blockGaslimit :: Word64
- gasprice :: W256
- baseFee :: W256
- schedule :: FeeSchedule Word64
- chainId :: W256
- create :: Bool
- txAccessList :: Map (Expr EAddr) [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
- maybeLitAddr :: Expr EAddr -> Maybe Addr
- maybeConcreteStore :: Expr Storage -> Maybe (Map W256 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
- paddedShowHex :: (Show a, Integral a) => Int -> a -> String
- untilFixpoint :: Eq a => (a -> a) -> a -> a
Documentation
Instances
Instances
truncateToAddr :: W256 -> Addr Source #
data Expr (a :: EType) where Source #
Expr implements an abstract representation 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
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
data PartialExec Source #
Sometimes we can only partially execute a given program
Instances
| Show PartialExec Source # | |
Defined in EVM.Types Methods showsPrec :: Int -> PartialExec -> ShowS # show :: PartialExec -> String # showList :: [PartialExec] -> ShowS # | |
| Eq PartialExec Source # | |
Defined in EVM.Types | |
| Ord PartialExec Source # | |
Defined in EVM.Types Methods compare :: PartialExec -> PartialExec -> Ordering # (<) :: PartialExec -> PartialExec -> Bool # (<=) :: PartialExec -> PartialExec -> Bool # (>) :: PartialExec -> PartialExec -> Bool # (>=) :: PartialExec -> PartialExec -> Bool # max :: PartialExec -> PartialExec -> PartialExec # min :: PartialExec -> PartialExec -> PartialExec # | |
data Effect t s where 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 -> BaseState -> (Contract -> EVM t s ()) -> Query t s | |
| PleaseFetchSlot :: Addr -> W256 -> (W256 -> EVM t s ()) -> Query t s | |
| PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM Symbolic s ()) -> Query Symbolic s | |
| PleaseDoFFI :: [String] -> (ByteString -> EVM t s ()) -> Query t s |
Execution could proceed down one of two branches
data BranchCondition Source #
The possible return values of a SMT query
Instances
| Show BranchCondition Source # | |
Defined in EVM.Types Methods showsPrec :: Int -> BranchCondition -> ShowS # show :: BranchCondition -> String # showList :: [BranchCondition] -> ShowS # | |
data VMResult (t :: VMType) s where Source #
The possible result states of a VM
Constructors
| Unfinished | |
Fields
| |
| VMFailure | |
| VMSuccess | |
| HandleEffect | |
data VM (t :: VMType) s Source #
The state of a stepwise EVM execution
Constructors
| VM | |
Fields
| |
Instances
Instances
| Generic ForkState Source # | |
| Show ForkState Source # | |
| type Rep ForkState Source # | |
Defined in EVM.Types type Rep ForkState = D1 ('MetaData "ForkState" "EVM.Types" "hevm-0.53.0-inplace" 'False) (C1 ('MetaCons "ForkState" 'PrefixI 'True) ((S1 ('MetaSel ('Just "env") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Env) :*: S1 ('MetaSel ('Just "block") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Block)) :*: (S1 ('MetaSel ('Just "cache") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cache) :*: S1 ('MetaSel ('Just "urlOrAlias") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))) | |
The VM base state (i.e. should new contracts be created with abstract balance / storage?)
Constructors
| EmptyBase | |
| AbstractBase |
data RuntimeConfig Source #
Configuration options that need to be consulted at runtime
Constructors
| RuntimeConfig | |
Instances
| Show RuntimeConfig Source # | |
Defined in EVM.Types Methods showsPrec :: Int -> RuntimeConfig -> ShowS # show :: RuntimeConfig -> String # showList :: [RuntimeConfig] -> ShowS # | |
| (k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "allowFFI" k RuntimeConfig RuntimeConfig a b Source # | |
Defined in EVM.Types Methods labelOptic :: Optic k NoIx RuntimeConfig RuntimeConfig a b # | |
| (k ~ A_Lens, a ~ BaseState, b ~ BaseState) => LabelOptic "baseState" k RuntimeConfig RuntimeConfig a b Source # | |
Defined in EVM.Types Methods labelOptic :: Optic k NoIx RuntimeConfig RuntimeConfig a b # | |
| (k ~ A_Lens, a ~ Maybe (Expr 'EAddr), b ~ Maybe (Expr 'EAddr)) => LabelOptic "overrideCaller" k RuntimeConfig RuntimeConfig a b Source # | |
Defined in EVM.Types Methods labelOptic :: Optic k NoIx RuntimeConfig RuntimeConfig a b # | |
data Frame (t :: VMType) s Source #
An entry in the VM's "call/create stack"
Constructors
| Frame | |
Fields
| |
Instances
| (k ~ A_Lens, a ~ FrameContext, b ~ FrameContext) => LabelOptic "context" k (Frame t s) (Frame t s) a b Source # | |
| (k ~ A_Lens, a ~ FrameState t1 s1, b ~ FrameState t2 s2) => LabelOptic "state" k (Frame t1 s1) (Frame t2 s2) a b Source # | |
| Show (Frame 'Concrete s) Source # | |
| Show (Frame 'Symbolic s) 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 (Expr 'EAddr), b ~ Set (Expr 'EAddr)) => LabelOptic "accessedAddresses" k SubState SubState a b Source # | |
| (k ~ A_Lens, a ~ Set (Expr 'EAddr, W256), b ~ Set (Expr 'EAddr, W256)) => LabelOptic "accessedStorageKeys" k SubState SubState a b Source # | |
| (k ~ A_Lens, a ~ [(Expr 'EAddr, Word64)], b ~ [(Expr 'EAddr, Word64)]) => LabelOptic "refunds" k SubState SubState a b Source # | |
| (k ~ A_Lens, a ~ [Expr 'EAddr], b ~ [Expr 'EAddr]) => LabelOptic "selfdestructs" k SubState SubState a b Source # | |
| (k ~ A_Lens, a ~ [Expr 'EAddr], b ~ [Expr 'EAddr]) => LabelOptic "touchedAccounts" k SubState SubState a b Source # | |
data FrameState (t :: VMType) s Source #
The "registers" of the VM along with memory and data stack
Constructors
| FrameState | |
Instances
Constructors
| ConcreteMemory (MutableMemory s) | |
| SymbolicMemory !(Expr Buf) |
type MutableMemory s = STVector s Word8 Source #
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 ~ Expr 'EAddr, b ~ Expr 'EAddr) => 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 ~ Expr 'EAddr, b ~ Expr 'EAddr) => LabelOptic "toAddr" k TxState TxState a b Source # | |
| (k ~ A_Lens, a ~ Map (Expr 'EAddr) Contract, b ~ Map (Expr 'EAddr) 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 # | |
Various environmental data
Constructors
| Env | |
Instances
Data about the block
Constructors
| Block | |
Instances
Full contract state
Constructors
| Contract | |
Instances
class VMOps (t :: VMType) where Source #
Methods
burn' :: Gas t -> EVM t s () -> EVM t s () Source #
burnExp :: Expr EWord -> EVM t s () -> EVM t s () Source #
burnSha3 :: Expr EWord -> EVM t s () -> EVM t s () Source #
burnCalldatacopy :: Expr EWord -> EVM t s () -> EVM t s () Source #
burnCodecopy :: Expr EWord -> EVM t s () -> EVM t s () Source #
burnExtcodecopy :: Expr EAddr -> Expr EWord -> EVM t s () -> EVM t s () Source #
burnReturndatacopy :: Expr EWord -> EVM t s () -> EVM t s () Source #
burnLog :: Expr EWord -> Word8 -> EVM t s () -> EVM t s () Source #
initialGas :: Gas t Source #
ensureGas :: Word64 -> EVM t s () -> EVM t s () Source #
gasTryFrom :: Expr EWord -> Either () (Gas t) Source #
costOfCreate :: FeeSchedule Word64 -> Gas t -> Expr EWord -> Bool -> (Gas t, Gas t) Source #
costOfCall :: FeeSchedule Word64 -> Bool -> Expr EWord -> Gas t -> Gas t -> Expr EAddr -> (Word64 -> Word64 -> EVM t s ()) -> EVM t s () Source #
reclaimRemainingGasAllowance :: VM t s -> EVM t s () Source #
payRefunds :: EVM t s () Source #
pushGas :: EVM t s () Source #
enoughGas :: Word64 -> Gas t -> Bool Source #
subGas :: Gas t -> Word64 -> Gas t Source #
toGas :: Word64 -> Gas t Source #
whenSymbolicElse :: EVM t s a -> EVM t s a -> EVM t s a Source #
partial :: PartialExec -> EVM t s () Source #
branch :: Expr EWord -> (Bool -> EVM t s ()) -> EVM t s () Source #
Instances
The cache is data that can be persisted for efficiency: any expensive query that is constant at least within a block.
Instances
| Monoid Cache Source # | |
| Semigroup Cache Source # | |
| Generic Cache Source # | |
| Show Cache Source # | |
| (k ~ A_Lens, a ~ Map Addr Contract, b ~ Map Addr Contract) => LabelOptic "fetched" k Cache Cache a b Source # | |
| (k ~ A_Lens, a ~ Map (CodeLocation, Int) Bool, b ~ Map (CodeLocation, Int) Bool) => LabelOptic "path" k Cache Cache a b Source # | |
| type Rep Cache Source # | |
Defined in EVM.Types type Rep Cache = D1 ('MetaData "Cache" "EVM.Types" "hevm-0.53.0-inplace" 'False) (C1 ('MetaCons "Cache" 'PrefixI 'True) (S1 ('MetaSel ('Just "fetched") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Addr Contract)) :*: S1 ('MetaSel ('Just "path") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map (CodeLocation, Int) Bool)))) | |
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
| UnknownCode (Expr EAddr) | Fully abstract code, keyed on an address to give consistent results for e.g. extcodehash |
| InitCode ByteString (Expr Buf) | Constructor code, during contract creation |
| RuntimeCode RuntimeCode | Instance code, after contract creation |
Instances
| Show ContractCode Source # | |
Defined in EVM.Types Methods showsPrec :: Int -> ContractCode -> ShowS # show :: ContractCode -> String # showList :: [ContractCode] -> ShowS # | |
| Eq ContractCode Source # | |
Defined in EVM.Types | |
| Ord ContractCode Source # | |
Defined in EVM.Types Methods compare :: ContractCode -> ContractCode -> Ordering # (<) :: ContractCode -> ContractCode -> Bool # (<=) :: ContractCode -> ContractCode -> Bool # (>) :: ContractCode -> ContractCode -> Bool # (>=) :: ContractCode -> ContractCode -> Bool # max :: ContractCode -> ContractCode -> ContractCode # min :: ContractCode -> ContractCode -> ContractCode # | |
data RuntimeCode Source #
We have two variants here to optimize the fully concrete case. ConcreteRuntimeCode just wraps a ByteString SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).
Constructors
| ConcreteRuntimeCode ByteString | |
| SymbolicRuntimeCode (Vector (Expr Byte)) |
Instances
| Show RuntimeCode Source # | |
Defined in EVM.Types Methods showsPrec :: Int -> RuntimeCode -> ShowS # show :: RuntimeCode -> String # showList :: [RuntimeCode] -> ShowS # | |
| Eq RuntimeCode Source # | |
Defined in EVM.Types | |
| Ord RuntimeCode Source # | |
Defined in EVM.Types Methods compare :: RuntimeCode -> RuntimeCode -> Ordering # (<) :: RuntimeCode -> RuntimeCode -> Bool # (<=) :: RuntimeCode -> RuntimeCode -> Bool # (>) :: RuntimeCode -> RuntimeCode -> Bool # (>=) :: RuntimeCode -> RuntimeCode -> Bool # max :: RuntimeCode -> RuntimeCode -> RuntimeCode # min :: RuntimeCode -> RuntimeCode -> RuntimeCode # | |
Instances
| Generic Trace Source # | |
| Show Trace Source # | |
| Eq Trace Source # | |
| Ord Trace Source # | |
| (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.53.0-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.53.0-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 (Expr 'EAddr) Contract)))) | |
data VMOpts (t :: VMType) Source #
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 | |
newtype FunctionSelector Source #
Constructors
| FunctionSelector | |
Fields | |
Instances
newtype ByteStringS Source #
Constructors
| ByteStringS ByteString |
Instances
| FromJSON ByteStringS Source # | |
Defined in EVM.Types | |
| ToJSON ByteStringS Source # | |
Defined in EVM.Types Methods toJSON :: ByteStringS -> Value # toEncoding :: ByteStringS -> Encoding # toJSONList :: [ByteStringS] -> Value # toEncodingList :: [ByteStringS] -> Encoding # | |
| Generic ByteStringS Source # | |
| Show ByteStringS Source # | |
Defined in EVM.Types Methods showsPrec :: Int -> ByteStringS -> ShowS # show :: ByteStringS -> String # showList :: [ByteStringS] -> ShowS # | |
| Eq ByteStringS Source # | |
Defined in EVM.Types | |
| type Rep ByteStringS Source # | |
Defined in EVM.Types type Rep ByteStringS = D1 ('MetaData "ByteStringS" "EVM.Types" "hevm-0.53.0-inplace" 'True) (C1 ('MetaCons "ByteStringS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ByteString))) | |
Instances
Instances
| FromJSON W64 Source # | |
| ToJSON W64 Source # | |
| Bits W64 Source # | |
Defined in EVM.Types | |
| FiniteBits W64 Source # | |
Defined in EVM.Types Methods finiteBitSize :: W64 -> Int # countLeadingZeros :: W64 -> Int # countTrailingZeros :: W64 -> Int # | |
| Bounded W64 Source # | |
| Enum W64 Source # | |
| Generic W64 Source # | |
| Num W64 Source # | |
| Read W64 Source # | |
| Integral W64 Source # | |
| Real W64 Source # | |
Defined in EVM.Types Methods toRational :: W64 -> Rational # | |
| Show W64 Source # | |
| Eq W64 Source # | |
| Ord W64 Source # | |
| From W64 W256 Source # | |
| TryFrom W256 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 | |
| Generic Nibble Source # | |
| Num Nibble Source # | |
| Integral Nibble Source # | |
| Real Nibble Source # | |
Defined in EVM.Types Methods toRational :: Nibble -> Rational # | |
| 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 #
paddedShowHex :: (Show a, Integral a) => Int -> a -> String Source #
paddedShowHex displays a number in hexadecimal and pads the number
with 0 so that it has a minimum length of w.
untilFixpoint :: Eq a => (a -> a) -> a -> a Source #