hevm-0.51.1: Ethereum virtual machine evaluator
Safe HaskellSafe-Inferred
LanguageGHC2021

EVM.Types

Synopsis

Documentation

data Word512 Source #

Constructors

Word512 !Word256 !Word256 

Instances

Instances details
Data Word512 Source # 
Instance details

Defined in EVM.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Word512 -> c Word512 #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Word512 #

toConstr :: Word512 -> Constr #

dataTypeOf :: Word512 -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Word512) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Word512) #

gmapT :: (forall b. Data b => b -> b) -> Word512 -> Word512 #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Word512 -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Word512 -> r #

gmapQ :: (forall d. Data d => d -> u) -> Word512 -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Word512 -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Word512 -> m Word512 #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Word512 -> m Word512 #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Word512 -> m Word512 #

Bits Word512 Source # 
Instance details

Defined in EVM.Types

FiniteBits Word512 Source # 
Instance details

Defined in EVM.Types

Bounded Word512 Source # 
Instance details

Defined in EVM.Types

Enum Word512 Source # 
Instance details

Defined in EVM.Types

Generic Word512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Word512 :: Type -> Type #

Methods

from :: Word512 -> Rep Word512 x #

to :: Rep Word512 x -> Word512 #

Ix Word512 Source # 
Instance details

Defined in EVM.Types

Num Word512 Source # 
Instance details

Defined in EVM.Types

Read Word512 Source # 
Instance details

Defined in EVM.Types

Integral Word512 Source # 
Instance details

Defined in EVM.Types

Real Word512 Source # 
Instance details

Defined in EVM.Types

Show Word512 Source # 
Instance details

Defined in EVM.Types

BinaryWord Word512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type UnsignedWord Word512 #

type SignedWord Word512 #

DoubleWord Word512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type LoWord Word512 #

type HiWord Word512 #

Eq Word512 Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: Word512 -> Word512 -> Bool #

(/=) :: Word512 -> Word512 -> Bool #

Ord Word512 Source # 
Instance details

Defined in EVM.Types

Hashable Word512 Source # 
Instance details

Defined in EVM.Types

Methods

hashWithSalt :: Int -> Word512 -> Int #

hash :: Word512 -> Int #

type Rep Word512 Source # 
Instance details

Defined in EVM.Types

type SignedWord Word512 Source # 
Instance details

Defined in EVM.Types

type UnsignedWord Word512 Source # 
Instance details

Defined in EVM.Types

type HiWord Word512 Source # 
Instance details

Defined in EVM.Types

type LoWord Word512 Source # 
Instance details

Defined in EVM.Types

data Int512 Source #

Constructors

Int512 !Int256 !Word256 

Instances

Instances details
Data Int512 Source # 
Instance details

Defined in EVM.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Int512 -> c Int512 #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Int512 #

toConstr :: Int512 -> Constr #

dataTypeOf :: Int512 -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Int512) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Int512) #

gmapT :: (forall b. Data b => b -> b) -> Int512 -> Int512 #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Int512 -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Int512 -> r #

gmapQ :: (forall d. Data d => d -> u) -> Int512 -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Int512 -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Int512 -> m Int512 #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Int512 -> m Int512 #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Int512 -> m Int512 #

Bits Int512 Source # 
Instance details

Defined in EVM.Types

FiniteBits Int512 Source # 
Instance details

Defined in EVM.Types

Bounded Int512 Source # 
Instance details

Defined in EVM.Types

Enum Int512 Source # 
Instance details

Defined in EVM.Types

Generic Int512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Int512 :: Type -> Type #

Methods

from :: Int512 -> Rep Int512 x #

to :: Rep Int512 x -> Int512 #

Ix Int512 Source # 
Instance details

Defined in EVM.Types

Num Int512 Source # 
Instance details

Defined in EVM.Types

Read Int512 Source # 
Instance details

Defined in EVM.Types

Integral Int512 Source # 
Instance details

Defined in EVM.Types

Real Int512 Source # 
Instance details

Defined in EVM.Types

Show Int512 Source # 
Instance details

Defined in EVM.Types

BinaryWord Int512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type UnsignedWord Int512 #

type SignedWord Int512 #

DoubleWord Int512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type LoWord Int512 #

type HiWord Int512 #

Eq Int512 Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: Int512 -> Int512 -> Bool #

(/=) :: Int512 -> Int512 -> Bool #

Ord Int512 Source # 
Instance details

Defined in EVM.Types

Hashable Int512 Source # 
Instance details

Defined in EVM.Types

Methods

hashWithSalt :: Int -> Int512 -> Int #

hash :: Int512 -> Int #

type Rep Int512 Source # 
Instance details

Defined in EVM.Types

type SignedWord Int512 Source # 
Instance details

Defined in EVM.Types

type UnsignedWord Int512 Source # 
Instance details

Defined in EVM.Types

type HiWord Int512 Source # 
Instance details

Defined in EVM.Types

type LoWord Int512 Source # 
Instance details

Defined in EVM.Types

data EType Source #

Constructors

Buf 
Storage 
Log 
EWord 
Byte 
End 

data GVar (a :: EType) where Source #

Constructors

BufVar :: Int -> GVar Buf 
StoreVar :: Int -> GVar Storage 

Instances

Instances details
Show (GVar a) Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> GVar a -> ShowS #

show :: GVar a -> String #

showList :: [GVar a] -> ShowS #

Eq (GVar a) Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: GVar a -> GVar a -> Bool #

(/=) :: GVar a -> GVar a -> Bool #

Ord (GVar a) Source # 
Instance details

Defined in EVM.Types

Methods

compare :: GVar a -> GVar a -> Ordering #

(<) :: GVar a -> GVar a -> Bool #

(<=) :: GVar a -> GVar a -> Bool #

(>) :: GVar a -> GVar a -> Bool #

(>=) :: GVar a -> GVar a -> Bool #

max :: GVar a -> GVar a -> GVar a #

min :: GVar a -> GVar a -> GVar a #

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

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] -> PartialExec -> Expr End 
Failure :: [Prop] -> EvmError -> Expr End 
Success :: [Prop] -> 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 

Instances

Instances details
Monoid (Expr 'Buf) Source # 
Instance details

Defined in EVM.Expr

Methods

mempty :: Expr 'Buf #

mappend :: Expr 'Buf -> Expr 'Buf -> Expr 'Buf #

mconcat :: [Expr 'Buf] -> Expr 'Buf #

Semigroup (Expr 'Buf) Source # 
Instance details

Defined in EVM.Expr

Methods

(<>) :: Expr 'Buf -> Expr 'Buf -> Expr 'Buf #

sconcat :: NonEmpty (Expr 'Buf) -> Expr 'Buf #

stimes :: Integral b => b -> Expr 'Buf -> Expr 'Buf #

Show (Expr a) Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Expr a -> ShowS #

show :: Expr a -> String #

showList :: [Expr a] -> ShowS #

Eq (Expr a) Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: Expr a -> Expr a -> Bool #

(/=) :: Expr a -> Expr a -> Bool #

Ord (Expr a) Source # 
Instance details

Defined in EVM.Types

Methods

compare :: Expr a -> Expr a -> Ordering #

(<) :: Expr a -> Expr a -> Bool #

(<=) :: Expr a -> Expr a -> Bool #

(>) :: Expr a -> Expr a -> Bool #

(>=) :: Expr a -> Expr a -> Bool #

max :: Expr a -> Expr a -> Expr a #

min :: Expr a -> Expr a -> Expr a #

TraversableTerm (Expr a) Source # 
Instance details

Defined in EVM.Traversals

Methods

mapTerm :: (forall (b :: EType). Expr b -> Expr b) -> Expr a -> Expr a Source #

foldTerm :: Monoid c => (forall (b :: EType). Expr b -> c) -> c -> Expr a -> c Source #

data SomeExpr Source #

Constructors

forall a.Typeable a => SomeExpr (Expr a) 

Instances

Instances details
Show SomeExpr Source # 
Instance details

Defined in EVM.Types

Eq SomeExpr Source # 
Instance details

Defined in EVM.Types

Ord SomeExpr Source # 
Instance details

Defined in EVM.Types

toNum :: Typeable a => Expr a -> Int Source #

data Prop where Source #

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 

Instances

Instances details
Show Prop Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Prop -> ShowS #

show :: Prop -> String #

showList :: [Prop] -> ShowS #

Eq Prop Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: Prop -> Prop -> Bool #

(/=) :: Prop -> Prop -> Bool #

Ord Prop Source # 
Instance details

Defined in EVM.Types

Methods

compare :: Prop -> Prop -> Ordering #

(<) :: Prop -> Prop -> Bool #

(<=) :: Prop -> Prop -> Bool #

(>) :: Prop -> Prop -> Bool #

(>=) :: Prop -> Prop -> Bool #

max :: Prop -> Prop -> Prop #

min :: Prop -> Prop -> Prop #

TraversableTerm Prop Source # 
Instance details

Defined in EVM.Traversals

Methods

mapTerm :: (forall (b :: EType). Expr b -> Expr b) -> Prop -> Prop Source #

foldTerm :: Monoid c => (forall (b :: EType). Expr b -> c) -> c -> Prop -> c Source #

(.&&) :: Prop -> Prop -> Prop infixr 3 Source #

(.||) :: Prop -> Prop -> Prop infixr 2 Source #

(.<) :: Expr EWord -> Expr EWord -> Prop infix 4 Source #

(.<=) :: Expr EWord -> Expr EWord -> Prop infix 4 Source #

(.>) :: Expr EWord -> Expr EWord -> Prop infix 4 Source #

(.>=) :: Expr EWord -> Expr EWord -> Prop infix 4 Source #

(.==) :: Typeable a => Expr a -> Expr a -> Prop infix 4 Source #

(./=) :: Typeable a => Expr a -> Expr a -> Prop infix 4 Source #

por :: [Prop] -> Prop Source #

data PartialExec Source #

Sometimes we can only partially execute a given program

Constructors

UnexpectedSymbolicArg 

Fields

MaxIterationsReached 

Fields

data Effect Source #

Effect types used by the vm implementation for side effects & control flow

Constructors

Query Query 
Choose Choose 

Instances

Instances details
Show Effect Source # 
Instance details

Defined in EVM.Types

data Query where Source #

Queries halt execution until resolved through RPC calls or SMT queries

Constructors

PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query 
PleaseFetchSlot :: Addr -> W256 -> (W256 -> EVM ()) -> Query 
PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query 
PleaseDoFFI :: [String] -> (ByteString -> EVM ()) -> Query 

Instances

Instances details
Show Query Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Query -> ShowS #

show :: Query -> String #

showList :: [Query] -> ShowS #

data Choose where Source #

Execution could proceed down one of two branches

Constructors

PleaseChoosePath :: Expr EWord -> (Bool -> EVM ()) -> Choose 

Instances

Instances details
Show Choose Source # 
Instance details

Defined in EVM.Types

data BranchCondition Source #

The possible return values of a SMT query

Constructors

Case Bool 
Unknown 

Instances

Instances details
Show BranchCondition Source # 
Instance details

Defined in EVM.Types

data VMResult Source #

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

Instances

Instances details
Show VMResult Source # 
Instance details

Defined in EVM.Types

data VM Source #

The state of a stepwise EVM execution

Constructors

VM 

Fields

Instances

Instances details
Generic VM Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep VM :: Type -> Type #

Methods

from :: VM -> Rep VM x #

to :: Rep VM x -> VM #

Show VM Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> VM -> ShowS #

show :: VM -> String #

showList :: [VM] -> ShowS #

(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "allowFFI" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ Block, b ~ Block) => LabelOptic "block" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "burned" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ Cache, b ~ Cache) => LabelOptic "cache" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ [Prop], b ~ [Prop]) => LabelOptic "constraints" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ Env, b ~ Env) => LabelOptic "env" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ [Frame], b ~ [Frame]) => LabelOptic "frames" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ Map CodeLocation (Int, [Expr 'EWord]), b ~ Map CodeLocation (Int, [Expr 'EWord])) => LabelOptic "iterations" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ [Prop], b ~ [Prop]) => LabelOptic "keccakEqs" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ [Expr 'Log], b ~ [Expr 'Log]) => LabelOptic "logs" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ Maybe Addr, b ~ Maybe Addr) => LabelOptic "overrideCaller" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ Maybe VMResult, b ~ Maybe VMResult) => LabelOptic "result" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ FrameState, b ~ FrameState) => LabelOptic "state" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ TreePos Empty Trace, b ~ TreePos Empty Trace) => LabelOptic "traces" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

(k ~ A_Lens, a ~ TxState, b ~ TxState) => LabelOptic "tx" k VM VM a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx VM VM a b #

type Rep VM Source # 
Instance details

Defined in EVM.Types

type Rep VM = D1 ('MetaData "VM" "EVM.Types" "hevm-0.51.1-inplace" 'False) (C1 ('MetaCons "VM" 'PrefixI 'True) (((S1 ('MetaSel ('Just "result") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe VMResult)) :*: (S1 ('MetaSel ('Just "state") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FrameState) :*: S1 ('MetaSel ('Just "frames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Frame]))) :*: ((S1 ('MetaSel ('Just "env") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Env) :*: S1 ('MetaSel ('Just "block") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Block)) :*: (S1 ('MetaSel ('Just "tx") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TxState) :*: S1 ('MetaSel ('Just "logs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr 'Log])))) :*: (((S1 ('MetaSel ('Just "traces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TreePos Empty Trace)) :*: S1 ('MetaSel ('Just "cache") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cache)) :*: (S1 ('MetaSel ('Just "burned") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Just "iterations") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map CodeLocation (Int, [Expr 'EWord]))))) :*: ((S1 ('MetaSel ('Just "constraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]) :*: S1 ('MetaSel ('Just "keccakEqs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop])) :*: (S1 ('MetaSel ('Just "allowFFI") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "overrideCaller") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Addr)))))))

type EVM a = State VM a Source #

Alias for the type of e.g. exec1.

data Frame Source #

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

Constructors

Frame 

Instances

Instances details
Show Frame Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Frame -> ShowS #

show :: Frame -> String #

showList :: [Frame] -> ShowS #

(k ~ A_Lens, a ~ FrameContext, b ~ FrameContext) => LabelOptic "context" k Frame Frame a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Frame Frame a b #

(k ~ A_Lens, a ~ FrameState, b ~ FrameState) => LabelOptic "state" k Frame Frame a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Frame Frame a b #

data FrameContext Source #

Call/create info

Instances

Instances details
Generic FrameContext Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep FrameContext :: Type -> Type #

Show FrameContext Source # 
Instance details

Defined in EVM.Types

(k ~ An_AffineTraversal, a ~ Maybe W256, b ~ Maybe W256) => LabelOptic "abi" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

(k ~ An_AffineTraversal, a ~ Addr, b ~ Addr) => LabelOptic "address" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

(k ~ An_AffineTraversal, a ~ Expr 'Buf, b ~ Expr 'Buf) => LabelOptic "calldata" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

(k ~ An_AffineTraversal, a ~ (Map Addr Contract, Expr 'Storage), b ~ (Map Addr Contract, Expr 'Storage)) => LabelOptic "callreversion" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "codehash" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

(k ~ An_AffineTraversal, a ~ Addr, b ~ Addr) => LabelOptic "context" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

(k ~ An_AffineTraversal, a ~ Map Addr Contract, b ~ Map Addr Contract) => LabelOptic "createreversion" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

(k ~ An_AffineTraversal, a ~ W256, b ~ W256) => LabelOptic "offset" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

(k ~ An_AffineTraversal, a ~ W256, b ~ W256) => LabelOptic "size" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

(k ~ An_AffineTraversal, a ~ SubState, b ~ SubState) => LabelOptic "subState" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

(k ~ An_AffineTraversal, a ~ SubState, b ~ SubState) => LabelOptic "substate" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

(k ~ An_AffineTraversal, a ~ Addr, b ~ Addr) => LabelOptic "target" k FrameContext FrameContext a b Source # 
Instance details

Defined in EVM.Types

type Rep FrameContext Source # 
Instance details

Defined in EVM.Types

type Rep FrameContext = D1 ('MetaData "FrameContext" "EVM.Types" "hevm-0.51.1-inplace" 'False) (C1 ('MetaCons "CreationContext" 'PrefixI 'True) ((S1 ('MetaSel ('Just "address") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Addr) :*: S1 ('MetaSel ('Just "codehash") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'EWord))) :*: (S1 ('MetaSel ('Just "createreversion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Addr Contract)) :*: S1 ('MetaSel ('Just "substate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SubState))) :+: C1 ('MetaCons "CallContext" 'PrefixI 'True) (((S1 ('MetaSel ('Just "target") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Addr) :*: S1 ('MetaSel ('Just "context") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Addr)) :*: (S1 ('MetaSel ('Just "offset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 W256) :*: S1 ('MetaSel ('Just "size") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 W256))) :*: ((S1 ('MetaSel ('Just "codehash") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'EWord)) :*: S1 ('MetaSel ('Just "abi") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe W256))) :*: (S1 ('MetaSel ('Just "calldata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'Buf)) :*: (S1 ('MetaSel ('Just "callreversion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Addr Contract, Expr 'Storage)) :*: S1 ('MetaSel ('Just "subState") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SubState))))))

data SubState Source #

The "accrued substate" across a transaction

Instances

Instances details
Show SubState Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Set Addr, b ~ Set Addr) => LabelOptic "accessedAddresses" k SubState SubState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Set (Addr, W256), b ~ Set (Addr, W256)) => LabelOptic "accessedStorageKeys" k SubState SubState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ [(Addr, Word64)], b ~ [(Addr, Word64)]) => LabelOptic "refunds" k SubState SubState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ [Addr], b ~ [Addr]) => LabelOptic "selfdestructs" k SubState SubState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ [Addr], b ~ [Addr]) => LabelOptic "touchedAccounts" k SubState SubState a b Source # 
Instance details

Defined in EVM.Types

data FrameState Source #

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

Instances

Instances details
Generic FrameState Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep FrameState :: Type -> Type #

Show FrameState Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'Buf, b ~ Expr 'Buf) => LabelOptic "calldata" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "caller" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "callvalue" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ ContractCode, b ~ ContractCode) => LabelOptic "code" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "codeContract" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "contract" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "gas" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'Buf, b ~ Expr 'Buf) => LabelOptic "memory" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "memorySize" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Int, b ~ Int) => LabelOptic "pc" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'Buf, b ~ Expr 'Buf) => LabelOptic "returndata" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ [Expr 'EWord], b ~ [Expr 'EWord]) => LabelOptic "stack" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "static" k FrameState FrameState a b Source # 
Instance details

Defined in EVM.Types

type Rep FrameState Source # 
Instance details

Defined in EVM.Types

type Rep FrameState = D1 ('MetaData "FrameState" "EVM.Types" "hevm-0.51.1-inplace" 'False) (C1 ('MetaCons "FrameState" 'PrefixI 'True) (((S1 ('MetaSel ('Just "contract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Addr) :*: (S1 ('MetaSel ('Just "codeContract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Addr) :*: S1 ('MetaSel ('Just "code") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ContractCode))) :*: (S1 ('MetaSel ('Just "pc") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: (S1 ('MetaSel ('Just "stack") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr 'EWord]) :*: S1 ('MetaSel ('Just "memory") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'Buf))))) :*: ((S1 ('MetaSel ('Just "memorySize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64) :*: (S1 ('MetaSel ('Just "calldata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'Buf)) :*: S1 ('MetaSel ('Just "callvalue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'EWord)))) :*: ((S1 ('MetaSel ('Just "caller") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'EWord)) :*: S1 ('MetaSel ('Just "gas") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64)) :*: (S1 ('MetaSel ('Just "returndata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr 'Buf)) :*: S1 ('MetaSel ('Just "static") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))))

data TxState Source #

The state that spans a whole transaction

Instances

Instances details
Show TxState Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "gaslimit" k TxState TxState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "gasprice" k TxState TxState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "isCreate" k TxState TxState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "origin" k TxState TxState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "priorityFee" k TxState TxState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ SubState, b ~ SubState) => LabelOptic "substate" k TxState TxState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "toAddr" k TxState TxState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Map Addr Contract, b ~ Map Addr Contract) => LabelOptic "txReversion" k TxState TxState a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "value" k TxState TxState a b Source # 
Instance details

Defined in EVM.Types

data StorageModel Source #

When doing symbolic execution, we have three different ways to model the storage of contracts. This determines not only the initial contract storage model but also how RPC or state fetched contracts will be modeled.

Constructors

ConcreteS

Uses Concrete Storage. Reading / Writing from abstract locations causes a runtime failure. Can be nicely combined with RPC.

SymbolicS

Uses Symbolic Storage. Reading / Writing never reaches RPC, but always done using an SMT array with no default value.

InitialS

Uses Symbolic Storage. Reading / Writing never reaches RPC, but always done using an SMT array with 0 as the default value.

data Env Source #

Various environmental data

Instances

Instances details
Generic Env Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Env :: Type -> Type #

Methods

from :: Env -> Rep Env x #

to :: Rep Env x -> Env #

Show Env Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Env -> ShowS #

show :: Env -> String #

showList :: [Env] -> ShowS #

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "chainId" k Env Env a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Env Env a b #

(k ~ A_Lens, a ~ Map Addr Contract, b ~ Map Addr Contract) => LabelOptic "contracts" k Env Env a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Env Env a b #

(k ~ A_Lens, a ~ Map W256 (Map W256 W256), b ~ Map W256 (Map W256 W256)) => LabelOptic "origStorage" k Env Env a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Env Env a b #

(k ~ A_Lens, a ~ Map W256 ByteString, b ~ Map W256 ByteString) => LabelOptic "sha3Crack" k Env Env a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Env Env a b #

(k ~ A_Lens, a ~ Expr 'Storage, b ~ Expr 'Storage) => LabelOptic "storage" k Env Env a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Env Env a b #

type Rep Env Source # 
Instance details

Defined in EVM.Types

data Block Source #

Data about the block

Instances

Instances details
Generic Block Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Block :: Type -> Type #

Methods

from :: Block -> Rep Block x #

to :: Rep Block x -> Block #

Show Block Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Block -> ShowS #

show :: Block -> String #

showList :: [Block] -> ShowS #

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "baseFee" k Block Block a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Block Block a b #

(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "coinbase" k Block Block a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Block Block a b #

(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "gaslimit" k Block Block a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Block Block a b #

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "maxCodeSize" k Block Block a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Block Block a b #

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "number" k Block Block a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Block Block a b #

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "prevRandao" k Block Block a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Block Block a b #

(k ~ A_Lens, a ~ FeeSchedule Word64, b ~ FeeSchedule Word64) => LabelOptic "schedule" k Block Block a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Block Block a b #

(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "timestamp" k Block Block a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Block Block a b #

type Rep Block Source # 
Instance details

Defined in EVM.Types

data Contract Source #

The state of a contract

Instances

Instances details
Show Contract Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "balance" k Contract Contract a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Vector (Int, Op), b ~ Vector (Int, Op)) => LabelOptic "codeOps" k Contract Contract a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "codehash" k Contract Contract a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ ContractCode, b ~ ContractCode) => LabelOptic "contractcode" k Contract Contract a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "external" k Contract Contract a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "nonce" k Contract Contract a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Vector Int, b ~ Vector Int) => LabelOptic "opIxMap" k Contract Contract a b Source # 
Instance details

Defined in EVM.Types

type CodeLocation = (Addr, Int) Source #

A unique id for a given pc

data Cache Source #

The cache is data that can be persisted for efficiency: any expensive query that is constant at least within a block.

Instances

Instances details
Monoid Cache Source # 
Instance details

Defined in EVM.Types

Methods

mempty :: Cache #

mappend :: Cache -> Cache -> Cache #

mconcat :: [Cache] -> Cache #

Semigroup Cache Source # 
Instance details

Defined in EVM.Types

Methods

(<>) :: Cache -> Cache -> Cache #

sconcat :: NonEmpty Cache -> Cache #

stimes :: Integral b => b -> Cache -> Cache #

Generic Cache Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Cache :: Type -> Type #

Methods

from :: Cache -> Rep Cache x #

to :: Rep Cache x -> Cache #

Show Cache Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Cache -> ShowS #

show :: Cache -> String #

showList :: [Cache] -> ShowS #

(k ~ A_Lens, a ~ Map Addr Contract, b ~ Map Addr Contract) => LabelOptic "fetchedContracts" k Cache Cache a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Cache Cache a b #

(k ~ A_Lens, a ~ Map W256 (Map W256 W256), b ~ Map W256 (Map W256 W256)) => LabelOptic "fetchedStorage" k Cache Cache a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Cache Cache a b #

(k ~ A_Lens, a ~ Map (CodeLocation, Int) Bool, b ~ Map (CodeLocation, Int) Bool) => LabelOptic "path" k Cache Cache a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Cache Cache a b #

type Rep Cache Source # 
Instance details

Defined in EVM.Types

type Rep Cache = D1 ('MetaData "Cache" "EVM.Types" "hevm-0.51.1-inplace" 'False) (C1 ('MetaCons "Cache" 'PrefixI 'True) (S1 ('MetaSel ('Just "fetchedContracts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Addr Contract)) :*: (S1 ('MetaSel ('Just "fetchedStorage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map W256 (Map W256 W256))) :*: S1 ('MetaSel ('Just "path") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map (CodeLocation, Int) Bool)))))

data 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

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).

data Trace Source #

Constructors

Trace 

Instances

Instances details
Generic Trace Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Trace :: Type -> Type #

Methods

from :: Trace -> Rep Trace x #

to :: Rep Trace x -> Trace #

Show Trace Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Trace -> ShowS #

show :: Trace -> String #

showList :: [Trace] -> ShowS #

(k ~ A_Lens, a ~ Contract, b ~ Contract) => LabelOptic "contract" k Trace Trace a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Trace Trace a b #

(k ~ A_Lens, a ~ Int, b ~ Int) => LabelOptic "opIx" k Trace Trace a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Trace Trace a b #

(k ~ A_Lens, a ~ TraceData, b ~ TraceData) => LabelOptic "tracedata" k Trace Trace a b Source # 
Instance details

Defined in EVM.Types

Methods

labelOptic :: Optic k NoIx Trace Trace a b #

type Rep Trace Source # 
Instance details

Defined in EVM.Types

data TraceData Source #

Instances

Instances details
Generic TraceData Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep TraceData :: Type -> Type #

Show TraceData Source # 
Instance details

Defined in EVM.Types

type Rep TraceData Source # 
Instance details

Defined in EVM.Types

data VMOpts Source #

A specification for an initial VM state

Instances

Instances details
Show VMOpts Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "address" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "allowFFI" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "baseFee" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "blockGaslimit" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ (Expr 'Buf, [Prop]), b ~ (Expr 'Buf, [Prop])) => LabelOptic "calldata" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "caller" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "chainId" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "coinbase" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Contract, b ~ Contract) => LabelOptic "contract" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Bool, b ~ Bool) => LabelOptic "create" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "gas" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Word64, b ~ Word64) => LabelOptic "gaslimit" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "gasprice" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'Storage, b ~ Expr 'Storage) => LabelOptic "initialStorage" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "maxCodeSize" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "number" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Addr, b ~ Addr) => LabelOptic "origin" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "prevRandao" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ W256, b ~ W256) => LabelOptic "priorityFee" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ FeeSchedule Word64, b ~ FeeSchedule Word64) => LabelOptic "schedule" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "timestamp" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Map Addr [W256], b ~ Map Addr [W256]) => LabelOptic "txAccessList" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

(k ~ A_Lens, a ~ Expr 'EWord, b ~ Expr 'EWord) => LabelOptic "value" k VMOpts VMOpts a b Source # 
Instance details

Defined in EVM.Types

newtype FunctionSelector Source #

Instances

Instances details
Enum FunctionSelector Source # 
Instance details

Defined in EVM.Types

Num FunctionSelector Source # 
Instance details

Defined in EVM.Types

Integral FunctionSelector Source # 
Instance details

Defined in EVM.Types

Real FunctionSelector Source # 
Instance details

Defined in EVM.Types

Show FunctionSelector Source # 
Instance details

Defined in EVM.Types

Eq FunctionSelector Source # 
Instance details

Defined in EVM.Types

Ord FunctionSelector Source # 
Instance details

Defined in EVM.Types

newtype ByteStringS Source #

Constructors

ByteStringS ByteString 

Instances

Instances details
FromJSON ByteStringS Source # 
Instance details

Defined in EVM.Types

ToJSON ByteStringS Source # 
Instance details

Defined in EVM.Types

Generic ByteStringS Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep ByteStringS :: Type -> Type #

Show ByteStringS Source # 
Instance details

Defined in EVM.Types

Eq ByteStringS Source # 
Instance details

Defined in EVM.Types

type Rep ByteStringS Source # 
Instance details

Defined in EVM.Types

type Rep ByteStringS = D1 ('MetaData "ByteStringS" "EVM.Types" "hevm-0.51.1-inplace" 'True) (C1 ('MetaCons "ByteStringS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ByteString)))

newtype W256 Source #

Constructors

W256 Word256 

Instances

Instances details
FromJSON W256 Source # 
Instance details

Defined in EVM.Types

FromJSONKey W256 Source # 
Instance details

Defined in EVM.Types

ToJSON W256 Source # 
Instance details

Defined in EVM.Types

Bits W256 Source # 
Instance details

Defined in EVM.Types

FiniteBits W256 Source # 
Instance details

Defined in EVM.Types

Bounded W256 Source # 
Instance details

Defined in EVM.Types

Enum W256 Source # 
Instance details

Defined in EVM.Types

Methods

succ :: W256 -> W256 #

pred :: W256 -> W256 #

toEnum :: Int -> W256 #

fromEnum :: W256 -> Int #

enumFrom :: W256 -> [W256] #

enumFromThen :: W256 -> W256 -> [W256] #

enumFromTo :: W256 -> W256 -> [W256] #

enumFromThenTo :: W256 -> W256 -> W256 -> [W256] #

Generic W256 Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep W256 :: Type -> Type #

Methods

from :: W256 -> Rep W256 x #

to :: Rep W256 x -> W256 #

Num W256 Source # 
Instance details

Defined in EVM.Types

Methods

(+) :: W256 -> W256 -> W256 #

(-) :: W256 -> W256 -> W256 #

(*) :: W256 -> W256 -> W256 #

negate :: W256 -> W256 #

abs :: W256 -> W256 #

signum :: W256 -> W256 #

fromInteger :: Integer -> W256 #

Read W256 Source # 
Instance details

Defined in EVM.Types

Integral W256 Source # 
Instance details

Defined in EVM.Types

Methods

quot :: W256 -> W256 -> W256 #

rem :: W256 -> W256 -> W256 #

div :: W256 -> W256 -> W256 #

mod :: W256 -> W256 -> W256 #

quotRem :: W256 -> W256 -> (W256, W256) #

divMod :: W256 -> W256 -> (W256, W256) #

toInteger :: W256 -> Integer #

Real W256 Source # 
Instance details

Defined in EVM.Types

Methods

toRational :: W256 -> Rational #

Show W256 Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> W256 -> ShowS #

show :: W256 -> String #

showList :: [W256] -> ShowS #

Eq W256 Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: W256 -> W256 -> Bool #

(/=) :: W256 -> W256 -> Bool #

Ord W256 Source # 
Instance details

Defined in EVM.Types

Methods

compare :: W256 -> W256 -> Ordering #

(<) :: W256 -> W256 -> Bool #

(<=) :: W256 -> W256 -> Bool #

(>) :: W256 -> W256 -> Bool #

(>=) :: W256 -> W256 -> Bool #

max :: W256 -> W256 -> W256 #

min :: W256 -> W256 -> W256 #

ToRPC W256 Source # 
Instance details

Defined in EVM.Fetch

Methods

toRPC :: W256 -> Value Source #

ParseField W256 Source # 
Instance details

Defined in EVM.Types

ParseFields W256 Source # 
Instance details

Defined in EVM.Types

ParseRecord W256 Source # 
Instance details

Defined in EVM.Types

type Rep W256 Source # 
Instance details

Defined in EVM.Types

type Rep W256 = D1 ('MetaData "W256" "EVM.Types" "hevm-0.51.1-inplace" 'True) (C1 ('MetaCons "W256" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word256)))

newtype W64 Source #

Constructors

W64 Word64 

Instances

Instances details
FromJSON W64 Source # 
Instance details

Defined in EVM.Types

ToJSON W64 Source # 
Instance details

Defined in EVM.Types

Bits W64 Source # 
Instance details

Defined in EVM.Types

Methods

(.&.) :: W64 -> W64 -> W64 #

(.|.) :: W64 -> W64 -> W64 #

xor :: W64 -> W64 -> W64 #

complement :: W64 -> W64 #

shift :: W64 -> Int -> W64 #

rotate :: W64 -> Int -> W64 #

zeroBits :: W64 #

bit :: Int -> W64 #

setBit :: W64 -> Int -> W64 #

clearBit :: W64 -> Int -> W64 #

complementBit :: W64 -> Int -> W64 #

testBit :: W64 -> Int -> Bool #

bitSizeMaybe :: W64 -> Maybe Int #

bitSize :: W64 -> Int #

isSigned :: W64 -> Bool #

shiftL :: W64 -> Int -> W64 #

unsafeShiftL :: W64 -> Int -> W64 #

shiftR :: W64 -> Int -> W64 #

unsafeShiftR :: W64 -> Int -> W64 #

rotateL :: W64 -> Int -> W64 #

rotateR :: W64 -> Int -> W64 #

popCount :: W64 -> Int #

FiniteBits W64 Source # 
Instance details

Defined in EVM.Types

Bounded W64 Source # 
Instance details

Defined in EVM.Types

Methods

minBound :: W64 #

maxBound :: W64 #

Enum W64 Source # 
Instance details

Defined in EVM.Types

Methods

succ :: W64 -> W64 #

pred :: W64 -> W64 #

toEnum :: Int -> W64 #

fromEnum :: W64 -> Int #

enumFrom :: W64 -> [W64] #

enumFromThen :: W64 -> W64 -> [W64] #

enumFromTo :: W64 -> W64 -> [W64] #

enumFromThenTo :: W64 -> W64 -> W64 -> [W64] #

Generic W64 Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep W64 :: Type -> Type #

Methods

from :: W64 -> Rep W64 x #

to :: Rep W64 x -> W64 #

Num W64 Source # 
Instance details

Defined in EVM.Types

Methods

(+) :: W64 -> W64 -> W64 #

(-) :: W64 -> W64 -> W64 #

(*) :: W64 -> W64 -> W64 #

negate :: W64 -> W64 #

abs :: W64 -> W64 #

signum :: W64 -> W64 #

fromInteger :: Integer -> W64 #

Read W64 Source # 
Instance details

Defined in EVM.Types

Integral W64 Source # 
Instance details

Defined in EVM.Types

Methods

quot :: W64 -> W64 -> W64 #

rem :: W64 -> W64 -> W64 #

div :: W64 -> W64 -> W64 #

mod :: W64 -> W64 -> W64 #

quotRem :: W64 -> W64 -> (W64, W64) #

divMod :: W64 -> W64 -> (W64, W64) #

toInteger :: W64 -> Integer #

Real W64 Source # 
Instance details

Defined in EVM.Types

Methods

toRational :: W64 -> Rational #

Show W64 Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> W64 -> ShowS #

show :: W64 -> String #

showList :: [W64] -> ShowS #

Eq W64 Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: W64 -> W64 -> Bool #

(/=) :: W64 -> W64 -> Bool #

Ord W64 Source # 
Instance details

Defined in EVM.Types

Methods

compare :: W64 -> W64 -> Ordering #

(<) :: W64 -> W64 -> Bool #

(<=) :: W64 -> W64 -> Bool #

(>) :: W64 -> W64 -> Bool #

(>=) :: W64 -> W64 -> Bool #

max :: W64 -> W64 -> W64 #

min :: W64 -> W64 -> W64 #

type Rep W64 Source # 
Instance details

Defined in EVM.Types

type Rep W64 = D1 ('MetaData "W64" "EVM.Types" "hevm-0.51.1-inplace" 'True) (C1 ('MetaCons "W64" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64)))

newtype Addr Source #

Constructors

Addr 

Instances

Instances details
FromJSON Addr Source # 
Instance details

Defined in EVM.Types

FromJSONKey Addr Source # 
Instance details

Defined in EVM.Types

ToJSON Addr Source # 
Instance details

Defined in EVM.Types

ToJSONKey Addr Source # 
Instance details

Defined in EVM.Types

Bits Addr Source # 
Instance details

Defined in EVM.Types

FiniteBits Addr Source # 
Instance details

Defined in EVM.Types

Enum Addr Source # 
Instance details

Defined in EVM.Types

Methods

succ :: Addr -> Addr #

pred :: Addr -> Addr #

toEnum :: Int -> Addr #

fromEnum :: Addr -> Int #

enumFrom :: Addr -> [Addr] #

enumFromThen :: Addr -> Addr -> [Addr] #

enumFromTo :: Addr -> Addr -> [Addr] #

enumFromThenTo :: Addr -> Addr -> Addr -> [Addr] #

Generic Addr Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Addr :: Type -> Type #

Methods

from :: Addr -> Rep Addr x #

to :: Rep Addr x -> Addr #

Num Addr Source # 
Instance details

Defined in EVM.Types

Methods

(+) :: Addr -> Addr -> Addr #

(-) :: Addr -> Addr -> Addr #

(*) :: Addr -> Addr -> Addr #

negate :: Addr -> Addr #

abs :: Addr -> Addr #

signum :: Addr -> Addr #

fromInteger :: Integer -> Addr #

Read Addr Source # 
Instance details

Defined in EVM.Types

Integral Addr Source # 
Instance details

Defined in EVM.Types

Methods

quot :: Addr -> Addr -> Addr #

rem :: Addr -> Addr -> Addr #

div :: Addr -> Addr -> Addr #

mod :: Addr -> Addr -> Addr #

quotRem :: Addr -> Addr -> (Addr, Addr) #

divMod :: Addr -> Addr -> (Addr, Addr) #

toInteger :: Addr -> Integer #

Real Addr Source # 
Instance details

Defined in EVM.Types

Methods

toRational :: Addr -> Rational #

Show Addr Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Addr -> ShowS #

show :: Addr -> String #

showList :: [Addr] -> ShowS #

Eq Addr Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: Addr -> Addr -> Bool #

(/=) :: Addr -> Addr -> Bool #

Ord Addr Source # 
Instance details

Defined in EVM.Types

Methods

compare :: Addr -> Addr -> Ordering #

(<) :: Addr -> Addr -> Bool #

(<=) :: Addr -> Addr -> Bool #

(>) :: Addr -> Addr -> Bool #

(>=) :: Addr -> Addr -> Bool #

max :: Addr -> Addr -> Addr #

min :: Addr -> Addr -> Addr #

ToRPC Addr Source # 
Instance details

Defined in EVM.Fetch

Methods

toRPC :: Addr -> Value Source #

ParseField Addr Source # 
Instance details

Defined in EVM.Types

ParseFields Addr Source # 
Instance details

Defined in EVM.Types

ParseRecord Addr Source # 
Instance details

Defined in EVM.Types

type Rep Addr Source # 
Instance details

Defined in EVM.Types

type Rep Addr = D1 ('MetaData "Addr" "EVM.Types" "hevm-0.51.1-inplace" 'True) (C1 ('MetaCons "Addr" 'PrefixI 'True) (S1 ('MetaSel ('Just "addressWord160") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word160)))

newtype Nibble Source #

A four bit value

Constructors

Nibble Word8 

Instances

Instances details
Bounded Nibble Source # 
Instance details

Defined in EVM.Types

Enum Nibble Source # 
Instance details

Defined in EVM.Types

Generic Nibble Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Nibble :: Type -> Type #

Methods

from :: Nibble -> Rep Nibble x #

to :: Rep Nibble x -> Nibble #

Num Nibble Source # 
Instance details

Defined in EVM.Types

Integral Nibble Source # 
Instance details

Defined in EVM.Types

Real Nibble Source # 
Instance details

Defined in EVM.Types

Show Nibble Source # 
Instance details

Defined in EVM.Types

Eq Nibble Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: Nibble -> Nibble -> Bool #

(/=) :: Nibble -> Nibble -> Bool #

Ord Nibble Source # 
Instance details

Defined in EVM.Types

type Rep Nibble Source # 
Instance details

Defined in EVM.Types

type Rep Nibble = D1 ('MetaData "Nibble" "EVM.Types" "hevm-0.51.1-inplace" 'True) (C1 ('MetaCons "Nibble" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word8)))

num :: (Integral a, Num b) => a -> b Source #

This just overflows silently, and is generally a terrible footgun, should be removed

concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] Source #

readNull :: Read a => a -> String -> a Source #