-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Ethereum virtual machine evaluator
--   
--   Hevm implements the Ethereum virtual machine semantics. . It can be
--   used as a library, and it also comes with an executable that can run
--   unit test suites, optionally with a visual TTY debugger.
@package hevm
@version 0.50.2

module EVM.Demand

-- | This is an easy way to force full evaluation of a value inside of the
--   IO monad, being essentially just the composition of <tt>evaluate</tt>
--   and <tt>force</tt>.
demand :: (MonadIO m, NFData a) => a -> m ()

module EVM.FeeSchedule
data FeeSchedule n
FeeSchedule :: n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> FeeSchedule n
[g_zero] :: FeeSchedule n -> n
[g_base] :: FeeSchedule n -> n
[g_verylow] :: FeeSchedule n -> n
[g_low] :: FeeSchedule n -> n
[g_mid] :: FeeSchedule n -> n
[g_high] :: FeeSchedule n -> n
[g_extcode] :: FeeSchedule n -> n
[g_balance] :: FeeSchedule n -> n
[g_sload] :: FeeSchedule n -> n
[g_jumpdest] :: FeeSchedule n -> n
[g_sset] :: FeeSchedule n -> n
[g_sreset] :: FeeSchedule n -> n
[r_sclear] :: FeeSchedule n -> n
[g_selfdestruct] :: FeeSchedule n -> n
[g_selfdestruct_newaccount] :: FeeSchedule n -> n
[r_selfdestruct] :: FeeSchedule n -> n
[g_create] :: FeeSchedule n -> n
[g_codedeposit] :: FeeSchedule n -> n
[g_call] :: FeeSchedule n -> n
[g_callvalue] :: FeeSchedule n -> n
[g_callstipend] :: FeeSchedule n -> n
[g_newaccount] :: FeeSchedule n -> n
[g_exp] :: FeeSchedule n -> n
[g_expbyte] :: FeeSchedule n -> n
[g_memory] :: FeeSchedule n -> n
[g_txcreate] :: FeeSchedule n -> n
[g_txdatazero] :: FeeSchedule n -> n
[g_txdatanonzero] :: FeeSchedule n -> n
[g_transaction] :: FeeSchedule n -> n
[g_log] :: FeeSchedule n -> n
[g_logdata] :: FeeSchedule n -> n
[g_logtopic] :: FeeSchedule n -> n
[g_sha3] :: FeeSchedule n -> n
[g_sha3word] :: FeeSchedule n -> n
[g_copy] :: FeeSchedule n -> n
[g_blockhash] :: FeeSchedule n -> n
[g_extcodehash] :: FeeSchedule n -> n
[g_quaddivisor] :: FeeSchedule n -> n
[g_ecadd] :: FeeSchedule n -> n
[g_ecmul] :: FeeSchedule n -> n
[g_pairing_point] :: FeeSchedule n -> n
[g_pairing_base] :: FeeSchedule n -> n
[g_fround] :: FeeSchedule n -> n
[r_block] :: FeeSchedule n -> n
[g_cold_sload] :: FeeSchedule n -> n
[g_cold_account_access] :: FeeSchedule n -> n
[g_warm_storage_read] :: FeeSchedule n -> n
[g_access_list_address] :: FeeSchedule n -> n
[g_access_list_storage_key] :: FeeSchedule n -> n
type EIP n = Num n => FeeSchedule n -> FeeSchedule n
eip150 :: EIP n
eip160 :: EIP n
homestead :: Num n => FeeSchedule n
metropolis :: Num n => FeeSchedule n
eip1108 :: EIP n
eip1884 :: EIP n
eip2028 :: EIP n
eip2200 :: EIP n
istanbul :: Num n => FeeSchedule n
eip2929 :: EIP n
berlin :: Num n => FeeSchedule n
instance GHC.Show.Show n => GHC.Show.Show (EVM.FeeSchedule.FeeSchedule n)

module EVM.Hexdump

-- | <a>prettyHex</a> renders a <a>ByteString</a> as a multi-line
--   <a>String</a> complete with addressing, hex digits, and ASCII
--   representation.
--   
--   Sample output
--   
--   <pre>
--   Length: 100 (0x64) bytes
--   0000:   4b c1 ad 8a  5b 47 d7 57  48 64 e7 cc  5e b5 2f 6e   K...[G.WHd..^./n
--   0010:   c5 b3 a4 73  44 3b 97 53  99 2d 54 e7  1b 2f 91 12   ...sD;.S.-T../..
--   0020:   c8 1a ff c4  3b 2b 72 ea  97 e2 9f e2  93 ad 23 79   ....;+r.......#y
--   0030:   e8 0f 08 54  02 14 fa 09  f0 2d 34 c9  08 6b e1 64   ...T.....-4..k.d
--   0040:   d1 c5 98 7e  d6 a1 98 e2  97 da 46 68  4e 60 11 15   ...~......FhN`..
--   0050:   d8 32 c6 0b  70 f5 2e 76  7f 8d f2 3b  ed de 90 c6   .2..p..v...;....
--   0060:   93 12 9c e1                                          ....
--   </pre>
prettyHex :: Int -> ByteString -> String

-- | <a>simpleHex</a> converts a <a>ByteString</a> to a <a>String</a>
--   showing the octets grouped in 32-bit words.
--   
--   Sample output
--   
--   <pre>
--   4b c1 ad 8a  5b 47 d7 57
--   </pre>
simpleHex :: ByteString -> String

module EVM.Precompiled

-- | Run a given precompiled contract using the C library.
execute :: Int -> ByteString -> Int -> Maybe ByteString

module EVM.TTYCenteredList

-- | Turn a list state value into a widget given an item drawing function.
renderList :: (Ord n, Show n) => (Bool -> e -> Widget n) -> Bool -> List n e -> Widget n
drawListElements :: (Ord n, Show n) => Bool -> List n e -> (Bool -> e -> Widget n) -> Widget n

module EVM.Types
data Word512
Word512 :: {-# UNPACK #-} !Word256 -> {-# UNPACK #-} !Word256 -> Word512
data Int512
Int512 :: {-# UNPACK #-} !Int256 -> {-# UNPACK #-} !Word256 -> Int512
newtype W256
W256 :: Word256 -> W256

-- | 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 -&gt; dstOffset
--   + size in dst with srcOffset -&gt; srcOffset + size from src
--   
--   Note that the shared usage of <a>Buf</a> 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 <i> Storage </i> 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
--   <a>Lit</a>, <a>ConcreteBuf</a>, or <a>ConcreteStore</a>). Failure to
--   adhere to this invariant will result in your concrete term being
--   treated as symbolic, and may produce unexpected errors. In the future
--   we may wish to consider encoding the concreteness of a given term
--   directly in the type of that term, since such type level shenanigans
--   tends to complicate implementation, we skip this for now.
data EType
Buf :: EType
Storage :: EType
Log :: EType
EWord :: EType
Byte :: EType
End :: EType
data Error
Invalid :: Error
IllegalOverflow :: Error
StackLimitExceeded :: Error
InvalidMemoryAccess :: Error
BadJumpDestination :: Error
SelfDestruct :: Error
TmpErr :: String -> Error
data GVar (a :: EType)
[BufVar] :: Int -> GVar Buf
[StoreVar] :: Int -> GVar Storage
data Expr (a :: EType)
[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
[Revert] :: [Prop] -> Expr Buf -> Expr End
[Failure] :: [Prop] -> Error -> Expr End
[Return] :: [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
[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 Prop
[PEq] :: forall a. Typeable a => Expr a -> Expr a -> Prop
[PLT] :: Expr EWord -> Expr EWord -> Prop
[PGT] :: Expr EWord -> Expr EWord -> Prop
[PGEq] :: Expr EWord -> Expr EWord -> Prop
[PLEq] :: Expr EWord -> Expr EWord -> Prop
[PNeg] :: Prop -> Prop
[PAnd] :: Prop -> Prop -> Prop
[POr] :: Prop -> Prop -> Prop
[PBool] :: Bool -> Prop
(.&&) :: Prop -> Prop -> Prop
infixr 3 .&&
(.||) :: Prop -> Prop -> Prop
infixr 2 .||
(.<) :: Expr EWord -> Expr EWord -> Prop
infix 4 .<
(.<=) :: Expr EWord -> Expr EWord -> Prop
infix 4 .<=
(.>) :: Expr EWord -> Expr EWord -> Prop
infix 4 .>
(.>=) :: Expr EWord -> Expr EWord -> Prop
infix 4 .>=
(.==) :: Typeable a => Expr a -> Expr a -> Prop
infix 4 .==
(./=) :: Typeable a => Expr a -> Expr a -> Prop
infix 4 ./=
unlit :: Expr EWord -> Maybe W256
unlitByte :: Expr Byte -> Maybe Word8
newtype ByteStringS
ByteStringS :: ByteString -> ByteStringS
newtype Addr
Addr :: Word160 -> Addr
[addressWord160] :: Addr -> Word160
maybeLitWord :: Expr EWord -> Maybe W256
toChecksumAddress :: String -> String
strip0x :: ByteString -> ByteString
strip0x' :: String -> String
hexByteString :: String -> ByteString -> ByteString
hexText :: Text -> ByteString
readN :: Integral a => String -> a
readNull :: Read a => a -> String -> a
wordField :: Object -> Key -> Parser W256
word64Field :: Object -> Key -> Parser Word64
addrField :: Object -> Key -> Parser Addr
addrFieldMaybe :: Object -> Key -> Parser (Maybe Addr)
dataField :: Object -> Key -> Parser ByteString
toWord512 :: W256 -> Word512
fromWord512 :: Word512 -> W256
num :: (Integral a, Num b) => a -> b
padLeft :: Int -> ByteString -> ByteString
padLeftStr :: Int -> String -> String
padRight :: Int -> ByteString -> ByteString
padRight' :: Int -> String -> String

-- | Right padding / truncating truncpad :: Int -&gt; [SWord 8] -&gt;
--   [SWord 8] truncpad n xs = if m &gt; n then take n xs else mappend xs
--   (replicate (n - m) 0) where m = length xs
padLeft' :: Int -> Vector (Expr Byte) -> Vector (Expr Byte)
word256 :: ByteString -> Word256
word :: ByteString -> W256
byteAt :: (Bits a, Bits b, Integral a, Num b) => a -> Int -> b
fromBE :: Integral a => ByteString -> a
asBE :: Integral a => a -> ByteString
word256Bytes :: W256 -> ByteString
word160Bytes :: Addr -> ByteString
newtype Nibble
Nibble :: Word8 -> Nibble
hi :: Word8 -> Nibble
lo :: Word8 -> Nibble
toByte :: Nibble -> Nibble -> Word8
unpackNibbles :: ByteString -> [Nibble]
packNibbles :: [Nibble] -> ByteString
toWord64 :: W256 -> Maybe Word64
toInt :: W256 -> Maybe Int
keccakBytes :: ByteString -> ByteString
word32 :: [Word8] -> Word32
keccak :: Expr Buf -> Expr EWord
keccak' :: ByteString -> W256
abiKeccak :: ByteString -> Word32
concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
regexMatches :: Text -> Text -> Bool
instance GHC.Generics.Generic EVM.Types.Word512
instance Data.Data.Data EVM.Types.Word512
instance GHC.Generics.Generic EVM.Types.Int512
instance Data.Data.Data EVM.Types.Int512
instance GHC.Enum.Bounded EVM.Types.W256
instance GHC.Classes.Eq EVM.Types.W256
instance GHC.Enum.Enum EVM.Types.W256
instance GHC.Bits.FiniteBits EVM.Types.W256
instance GHC.Bits.Bits EVM.Types.W256
instance GHC.Generics.Generic EVM.Types.W256
instance GHC.Classes.Ord EVM.Types.W256
instance GHC.Real.Real EVM.Types.W256
instance GHC.Real.Integral EVM.Types.W256
instance GHC.Num.Num EVM.Types.W256
instance GHC.Classes.Ord EVM.Types.Error
instance GHC.Classes.Eq EVM.Types.Error
instance GHC.Show.Show EVM.Types.Error
instance GHC.Classes.Eq EVM.Types.ByteStringS
instance GHC.Bits.FiniteBits EVM.Types.Addr
instance GHC.Bits.Bits EVM.Types.Addr
instance GHC.Generics.Generic EVM.Types.Addr
instance GHC.Classes.Eq EVM.Types.Addr
instance GHC.Enum.Enum EVM.Types.Addr
instance GHC.Classes.Ord EVM.Types.Addr
instance GHC.Real.Real EVM.Types.Addr
instance GHC.Real.Integral EVM.Types.Addr
instance GHC.Num.Num EVM.Types.Addr
instance GHC.Generics.Generic EVM.Types.Nibble
instance GHC.Enum.Bounded EVM.Types.Nibble
instance GHC.Classes.Eq EVM.Types.Nibble
instance GHC.Enum.Enum EVM.Types.Nibble
instance GHC.Classes.Ord EVM.Types.Nibble
instance GHC.Real.Real EVM.Types.Nibble
instance GHC.Real.Integral EVM.Types.Nibble
instance GHC.Num.Num EVM.Types.Nibble
instance GHC.Show.Show (EVM.Types.GVar a)
instance GHC.Classes.Eq (EVM.Types.GVar a)
instance GHC.Classes.Ord (EVM.Types.GVar a)
instance GHC.Show.Show (EVM.Types.Expr a)
instance GHC.Classes.Eq (EVM.Types.Expr a)
instance GHC.Classes.Ord (EVM.Types.Expr a)
instance GHC.Show.Show EVM.Types.Prop
instance GHC.Show.Show EVM.Types.Nibble
instance GHC.Read.Read EVM.Types.Addr
instance GHC.Show.Show EVM.Types.Addr
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Types.Addr
instance Data.Aeson.Types.FromJSON.FromJSONKey EVM.Types.Addr
instance Options.Generic.ParseField EVM.Types.Addr
instance Options.Generic.ParseFields EVM.Types.Addr
instance Options.Generic.ParseRecord EVM.Types.Addr
instance GHC.Show.Show EVM.Types.ByteStringS
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Types.ByteStringS
instance GHC.Classes.Eq EVM.Types.Prop
instance GHC.Classes.Ord EVM.Types.Prop
instance GHC.Read.Read EVM.Types.W256
instance GHC.Show.Show EVM.Types.W256
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Types.W256
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Types.W256
instance Data.Aeson.Types.FromJSON.FromJSONKey EVM.Types.W256
instance Options.Generic.ParseField EVM.Types.W256
instance Options.Generic.ParseFields EVM.Types.W256
instance Options.Generic.ParseRecord EVM.Types.W256
instance Data.BinaryWord.BinaryWord EVM.Types.Word512
instance Data.DoubleWord.Base.DoubleWord EVM.Types.Int512
instance GHC.Classes.Eq EVM.Types.Int512
instance GHC.Classes.Ord EVM.Types.Int512
instance GHC.Enum.Bounded EVM.Types.Int512
instance GHC.Enum.Enum EVM.Types.Int512
instance GHC.Num.Num EVM.Types.Int512
instance GHC.Real.Real EVM.Types.Int512
instance GHC.Real.Integral EVM.Types.Int512
instance GHC.Show.Show EVM.Types.Int512
instance GHC.Read.Read EVM.Types.Int512
instance Data.Hashable.Class.Hashable EVM.Types.Int512
instance GHC.Ix.Ix EVM.Types.Int512
instance GHC.Bits.Bits EVM.Types.Int512
instance GHC.Bits.FiniteBits EVM.Types.Int512
instance Data.BinaryWord.BinaryWord EVM.Types.Int512
instance Data.DoubleWord.Base.DoubleWord EVM.Types.Word512
instance GHC.Classes.Eq EVM.Types.Word512
instance GHC.Classes.Ord EVM.Types.Word512
instance GHC.Enum.Bounded EVM.Types.Word512
instance GHC.Enum.Enum EVM.Types.Word512
instance GHC.Num.Num EVM.Types.Word512
instance GHC.Real.Real EVM.Types.Word512
instance GHC.Real.Integral EVM.Types.Word512
instance GHC.Show.Show EVM.Types.Word512
instance GHC.Read.Read EVM.Types.Word512
instance Data.Hashable.Class.Hashable EVM.Types.Word512
instance GHC.Ix.Ix EVM.Types.Word512
instance GHC.Bits.Bits EVM.Types.Word512
instance GHC.Bits.FiniteBits EVM.Types.Word512


module EVM.Traversals
foldProp :: forall b. Monoid b => (forall a. Expr a -> b) -> b -> Prop -> b

-- | Recursively folds a given function over a given expression Recursion
--   schemes do this &amp; a lot more, but defining them over GADT's isn't
--   worth the hassle
foldExpr :: forall b c. Monoid b => (forall a. Expr a -> b) -> b -> Expr c -> b
mapProp :: (forall a. Expr a -> Expr a) -> Prop -> Prop

-- | Recursively applies a given function to every node in a given expr
--   instance Recursion schemes do this &amp; a lot more, but defining them
--   over GADT's isn't worth the hassle
mapExpr :: (forall a. Expr a -> Expr a) -> Expr b -> Expr b
mapExprM :: Monad m => (forall a. Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapPropM :: Monad m => (forall a. Expr a -> m (Expr a)) -> Prop -> m Prop

module EVM.RLP
data RLP
BS :: ByteString -> RLP
List :: [RLP] -> RLP
slice :: Int -> Int -> ByteString -> ByteString
itemInfo :: ByteString -> (Int, Int, Bool, Bool)
rlpdecode :: ByteString -> Maybe RLP
rlplengths :: ByteString -> Int -> Int -> [(Int, Int)]
rlpencode :: RLP -> ByteString
encodeLen :: Int -> ByteString -> ByteString
rlpList :: [RLP] -> ByteString
octets :: W256 -> ByteString
octetsFull :: Int -> W256 -> ByteString
octets160 :: Addr -> ByteString
rlpWord256 :: W256 -> RLP
rlpWordFull :: W256 -> RLP
rlpAddrFull :: Addr -> RLP
rlpWord160 :: Addr -> RLP
instance GHC.Classes.Eq EVM.RLP.RLP
instance GHC.Show.Show EVM.RLP.RLP

module EVM.Patricia
data KV k v a
Put :: k -> v -> a -> KV k v a
Get :: k -> (v -> a) -> KV k v a
newtype DB k v a
DB :: Free (KV k v) a -> DB k v a
insertDB :: k -> v -> DB k v ()
lookupDB :: k -> DB k v v
runDB :: Monad m => (k -> v -> m ()) -> (k -> m v) -> DB k v a -> m a
type Path = [Nibble]
data Ref
Hash :: ByteString -> Ref
Literal :: Node -> Ref
data Node
Empty :: Node
Shortcut :: Path -> Either Ref ByteString -> Node
Full :: Seq Ref -> ByteString -> Node
encodePath :: Path -> Bool -> ByteString
rlpRef :: Ref -> RLP
rlpNode :: Node -> RLP
type NodeDB = DB ByteString Node
putNode :: Node -> NodeDB Ref
getNode :: Ref -> NodeDB Node
lookupPath :: Ref -> Path -> NodeDB ByteString
getVal :: Path -> Node -> NodeDB ByteString
emptyRef :: Ref
emptyRefs :: Seq Ref
addPrefix :: Path -> Node -> NodeDB Node
insertRef :: Ref -> Path -> ByteString -> NodeDB Ref
update :: Node -> Path -> ByteString -> NodeDB Node
delete :: Node -> Path -> NodeDB Node
insert :: Ref -> ByteString -> ByteString -> NodeDB Ref
lookupIn :: Ref -> ByteString -> NodeDB ByteString
type Trie = StateT Ref NodeDB
runTrie :: DB ByteString ByteString a -> Trie a
type MapDB k v a = StateT (Map k v) Maybe a
runMapDB :: Ord k => DB k v a -> MapDB k v a
insertValues :: [(ByteString, ByteString)] -> Maybe Ref
calcRoot :: [(ByteString, ByteString)] -> Maybe ByteString
instance GHC.Base.Functor (EVM.Patricia.KV k v)
instance GHC.Base.Monad (EVM.Patricia.DB k v)
instance GHC.Base.Applicative (EVM.Patricia.DB k v)
instance GHC.Base.Functor (EVM.Patricia.DB k v)
instance GHC.Classes.Eq EVM.Patricia.Ref
instance GHC.Classes.Eq EVM.Patricia.Node
instance GHC.Show.Show EVM.Patricia.Node
instance GHC.Show.Show (EVM.Patricia.NodeDB EVM.Patricia.Node)
instance GHC.Show.Show EVM.Patricia.Ref

module EVM.Op
data Op
OpStop :: Op
OpAdd :: Op
OpMul :: Op
OpSub :: Op
OpDiv :: Op
OpSdiv :: Op
OpMod :: Op
OpSmod :: Op
OpAddmod :: Op
OpMulmod :: Op
OpExp :: Op
OpSignextend :: Op
OpLt :: Op
OpGt :: Op
OpSlt :: Op
OpSgt :: Op
OpEq :: Op
OpIszero :: Op
OpAnd :: Op
OpOr :: Op
OpXor :: Op
OpNot :: Op
OpByte :: Op
OpShl :: Op
OpShr :: Op
OpSar :: Op
OpSha3 :: Op
OpAddress :: Op
OpBalance :: Op
OpOrigin :: Op
OpCaller :: Op
OpCallvalue :: Op
OpCalldataload :: Op
OpCalldatasize :: Op
OpCalldatacopy :: Op
OpCodesize :: Op
OpCodecopy :: Op
OpGasprice :: Op
OpExtcodesize :: Op
OpExtcodecopy :: Op
OpReturndatasize :: Op
OpReturndatacopy :: Op
OpExtcodehash :: Op
OpBlockhash :: Op
OpCoinbase :: Op
OpTimestamp :: Op
OpNumber :: Op
OpPrevRandao :: Op
OpGaslimit :: Op
OpChainid :: Op
OpSelfbalance :: Op
OpPop :: Op
OpMload :: Op
OpMstore :: Op
OpMstore8 :: Op
OpSload :: Op
OpSstore :: Op
OpJump :: Op
OpJumpi :: Op
OpPc :: Op
OpMsize :: Op
OpGas :: Op
OpJumpdest :: Op
OpCreate :: Op
OpCall :: Op
OpStaticcall :: Op
OpCallcode :: Op
OpReturn :: Op
OpDelegatecall :: Op
OpCreate2 :: Op
OpRevert :: Op
OpSelfdestruct :: Op
OpDup :: !Word8 -> Op
OpSwap :: !Word8 -> Op
OpLog :: !Word8 -> Op
OpPush :: Expr EWord -> Op
OpUnknown :: Word8 -> Op
opString :: (Integral a, Show a) => (a, Op) -> String
instance GHC.Classes.Eq EVM.Op.Op
instance GHC.Show.Show EVM.Op.Op


module EVM.Keccak
keccakAssumptions :: [Prop] -> [Expr Buf] -> [Expr Storage] -> [Prop]
instance GHC.Show.Show EVM.Keccak.BuilderState


-- | Helper functions for working with Expr instances. All functions here
--   will return a concrete result if given a concrete input.
module EVM.Expr
op1 :: (Expr EWord -> Expr EWord) -> (W256 -> W256) -> Expr EWord -> Expr EWord
op2 :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord
op3 :: (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord

-- | If a given binary op is commutative, then we always force Lits to the
--   lhs if only one argument is a Lit. This makes writing pattern matches
--   in the simplifier easier.
normArgs :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord
add :: Expr EWord -> Expr EWord -> Expr EWord
sub :: Expr EWord -> Expr EWord -> Expr EWord
mul :: Expr EWord -> Expr EWord -> Expr EWord
div :: Expr EWord -> Expr EWord -> Expr EWord
sdiv :: Expr EWord -> Expr EWord -> Expr EWord
mod :: Expr EWord -> Expr EWord -> Expr EWord
smod :: Expr EWord -> Expr EWord -> Expr EWord
addmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
mulmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
exp :: Expr EWord -> Expr EWord -> Expr EWord
sex :: Expr EWord -> Expr EWord -> Expr EWord
lt :: Expr EWord -> Expr EWord -> Expr EWord
gt :: Expr EWord -> Expr EWord -> Expr EWord
leq :: Expr EWord -> Expr EWord -> Expr EWord
geq :: Expr EWord -> Expr EWord -> Expr EWord
slt :: Expr EWord -> Expr EWord -> Expr EWord
sgt :: Expr EWord -> Expr EWord -> Expr EWord
eq :: Expr EWord -> Expr EWord -> Expr EWord
iszero :: Expr EWord -> Expr EWord
and :: Expr EWord -> Expr EWord -> Expr EWord
or :: Expr EWord -> Expr EWord -> Expr EWord
xor :: Expr EWord -> Expr EWord -> Expr EWord
not :: Expr EWord -> Expr EWord
shl :: Expr EWord -> Expr EWord -> Expr EWord
shr :: Expr EWord -> Expr EWord -> Expr EWord
sar :: Expr EWord -> Expr EWord -> Expr EWord

-- | Extracts the byte at a given index from a Buf.
--   
--   We do our best to return a concrete value wherever possible, but
--   fallback to an abstract expresion if nescessary. Note that a Buf is an
--   infinite structure, so reads outside of the bounds of a ConcreteBuf
--   return 0. This is inline with the semantics of calldata and memory,
--   but not of returndata.
readByte :: Expr EWord -> Expr Buf -> Expr Byte

-- | Reads n bytes starting from idx in buf and returns a left padded word
--   
--   If n is &gt;= 32 this is the same as readWord
readBytes :: Int -> Expr EWord -> Expr Buf -> Expr EWord

-- | Reads the word starting at idx from the given buf
readWord :: Expr EWord -> Expr Buf -> Expr EWord
readWordFromBytes :: Expr EWord -> Expr Buf -> Expr EWord

-- | Copies a slice of src into dst.
--   
--   0 srcOffset srcOffset + size length src
--   ┌--------------┬------------------┬-----------------┐ src: | | ------
--   sl ------ | | └--------------┴------------------┴-----------------┘
--   
--   0 dstOffset dstOffset + size length dst
--   ┌--------┬------------------┬-----------------┐ dst: | hd | | tl |
--   └--------┴------------------┴-----------------┘
maxBytes :: W256
copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf -> Expr Buf
writeByte :: Expr EWord -> Expr Byte -> Expr Buf -> Expr Buf
writeWord :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf

-- | Returns the length of a given buffer
--   
--   If there are any writes to abstract locations, or CopySlices with an
--   abstract size or dstOffset, an abstract expresion will be returned.
bufLength :: Expr Buf -> Expr EWord

-- | If a buffer has a concrete prefix, we return it's length here
concPrefix :: Expr Buf -> Maybe Integer
word256At :: Functor f => Expr EWord -> (Expr EWord -> f (Expr EWord)) -> Expr Buf -> f (Expr Buf)

-- | Returns the first n bytes of buf
take :: W256 -> Expr Buf -> Expr Buf

-- | Returns everything but the first n bytes of buf
drop :: W256 -> Expr Buf -> Expr Buf
slice :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf
toList :: Expr Buf -> Maybe (Vector (Expr Byte))
fromList :: Vector (Expr Byte) -> Expr Buf

-- | Removes any irrelevant writes when reading from a buffer
simplifyReads :: Expr a -> Expr a

-- | Strips writes from the buffer that can be statically determined to be
--   out of range TODO: are the bounds here correct? I think there might be
--   some off by one mistakes...
stripWrites :: W256 -> W256 -> Expr Buf -> Expr Buf

-- | Reads the word at the given slot from the given storage expression.
--   
--   Note that we return a Nothing instead of a 0x0 if we are reading from
--   a store that is backed by a ConcreteStore or an EmptyStore and there
--   have been no explicit writes to the requested slot. This makes
--   implementing rpc storage lookups much easier. If the store is backed
--   by an AbstractStore we always return a symbolic value.
readStorage :: Expr EWord -> Expr EWord -> Expr Storage -> Maybe (Expr EWord)
readStorage' :: Expr EWord -> Expr EWord -> Expr Storage -> Expr EWord

-- | Writes a value to a key in a storage expression.
--   
--   Concrete writes on top of a concrete or empty store will produce a new
--   ConcreteStore, otherwise we add a new write to the storage expression.
writeStorage :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Storage -> Expr Storage

-- | Simple recursive match based AST simplification Note: may not
--   terminate!
simplify :: Expr a -> Expr a
litAddr :: Addr -> Expr EWord
litCode :: ByteString -> [Expr Byte]
to512 :: W256 -> Word512
isLitByte :: Expr Byte -> Bool
isLitWord :: Expr EWord -> Bool

-- | Returns the byte at idx from the given word.
indexWord :: Expr EWord -> Expr EWord -> Expr Byte
padByte :: Expr Byte -> Expr EWord

-- | Converts a list of bytes into a W256. TODO: semantics if the input is
--   too large?
bytesToW256 :: [Word8] -> W256
padBytesLeft :: Int -> [Expr Byte] -> [Expr Byte]
joinBytes :: [Expr Byte] -> Expr EWord
eqByte :: Expr Byte -> Expr Byte -> Expr EWord
min :: Expr EWord -> Expr EWord -> Expr EWord
numBranches :: Expr End -> Int
allLit :: [Expr Byte] -> Bool
instance GHC.Base.Semigroup (EVM.Types.Expr 'EVM.Types.Buf)
instance GHC.Base.Monoid (EVM.Types.Expr 'EVM.Types.Buf)

module EVM.Concrete
wordAt :: Int -> ByteString -> W256
readByteOrZero :: Int -> ByteString -> Word8
byteStringSliceWithDefaultZeroes :: Int -> Int -> ByteString -> ByteString
sliceMemory :: (Integral a, Integral b) => a -> b -> ByteString -> ByteString
writeMemory :: ByteString -> W256 -> W256 -> W256 -> ByteString -> ByteString
(^) :: W256 -> W256 -> W256
createAddress :: Addr -> W256 -> Addr
create2Address :: Addr -> W256 -> ByteString -> Addr


module EVM.CSE
type BufEnv = Map Int (Expr Buf)
type StoreEnv = Map Int (Expr Storage)
eliminateExpr :: Expr a -> (Expr a, BufEnv, StoreEnv)

-- | Common subexpression elimination pass for list of Prop
eliminateProps :: [Prop] -> ([Prop], BufEnv, StoreEnv)
instance GHC.Show.Show EVM.CSE.BuilderState


module EVM.SMT
data CexVars
CexVars :: [Text] -> [Text] -> [Text] -> [Text] -> CexVars
[calldataV] :: CexVars -> [Text]
[buffersV] :: CexVars -> [Text]
[blockContextV] :: CexVars -> [Text]
[txContextV] :: CexVars -> [Text]
data SMTCex
SMTCex :: Map (Expr EWord) W256 -> Map (Expr Buf) ByteString -> Map (Expr EWord) W256 -> Map (Expr EWord) W256 -> SMTCex
[vars] :: SMTCex -> Map (Expr EWord) W256
[buffers] :: SMTCex -> Map (Expr Buf) ByteString
[blockContext] :: SMTCex -> Map (Expr EWord) W256
[txContext] :: SMTCex -> Map (Expr EWord) W256
getVar :: SMTCex -> Text -> W256
data SMT2
SMT2 :: [Builder] -> CexVars -> SMT2
formatSMT2 :: SMT2 -> Text

-- | Reads all intermediate variables from the builder state and produces
--   SMT declaring them as constants
declareIntermediates :: BufEnv -> StoreEnv -> SMT2
assertProps :: [Prop] -> SMT2
prelude :: SMT2
declareBufs :: [Builder] -> SMT2
referencedBufs :: Expr a -> [Builder]
referencedBufs' :: Prop -> [Builder]
referencedVars' :: Prop -> [Builder]
referencedFrameContext' :: Prop -> [Builder]
referencedBlockContext' :: Prop -> [Builder]
declareVars :: [Builder] -> SMT2
referencedVars :: Expr a -> [Builder]
declareFrameContext :: [Builder] -> SMT2
referencedFrameContext :: Expr a -> [Builder]
declareBlockContext :: [Builder] -> SMT2
referencedBlockContext :: Expr a -> [Builder]
exprToSMT :: Expr a -> Builder
sp :: Builder -> Builder -> Builder
zero :: Builder
one :: Builder
propToSMT :: Prop -> Builder

-- | Supported solvers
data Solver
Z3 :: Solver
CVC5 :: Solver
Bitwuzla :: Solver
Custom :: Text -> Solver

-- | A running solver instance
data SolverInstance
SolverInstance :: Solver -> Handle -> Handle -> Handle -> ProcessHandle -> SolverInstance
[_type] :: SolverInstance -> Solver
[_stdin] :: SolverInstance -> Handle
[_stdout] :: SolverInstance -> Handle
[_stderr] :: SolverInstance -> Handle
[_process] :: SolverInstance -> ProcessHandle

-- | A channel representing a group of solvers
newtype SolverGroup
SolverGroup :: Chan Task -> SolverGroup

-- | A script to be executed, a list of models to be extracted in the case
--   of a sat result, and a channel where the result should be written
data Task
Task :: SMT2 -> Chan CheckSatResult -> Task
[script] :: Task -> SMT2
[resultChan] :: Task -> Chan CheckSatResult

-- | The result of a call to (check-sat)
data CheckSatResult
Sat :: SMTCex -> CheckSatResult
Unsat :: CheckSatResult
Unknown :: CheckSatResult
Error :: Text -> CheckSatResult
isSat :: CheckSatResult -> Bool
isErr :: CheckSatResult -> Bool
isUnsat :: CheckSatResult -> Bool
checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult
parseW256 :: SpecConstant -> W256
parseInteger :: SpecConstant -> Integer
parseW8 :: SpecConstant -> Word8
parseErr :: Show a => a -> b
parseVar :: Text -> Expr EWord
parseBlockCtx :: Text -> Expr EWord
parseFrameCtx :: Text -> Expr EWord
getVars :: (Text -> Expr EWord) -> SolverInstance -> [Text] -> IO (Map (Expr EWord) W256)
getBufs :: SolverInstance -> [Text] -> IO (Map (Expr Buf) ByteString)
parseSC :: (Num a, Eq a) => SpecConstant -> a
withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a

-- | Arguments used when spawing a solver instance
solverArgs :: Solver -> Maybe Natural -> [Text]

-- | Spawns a solver instance, and sets the various global config options
--   that we use for our queries
spawnSolver :: Solver -> Maybe Natural -> IO SolverInstance

-- | Cleanly shutdown a running solver instnace
stopSolver :: SolverInstance -> IO ()

-- | Sends a list of commands to the solver. Returns the first error, if
--   there was one.
sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())

-- | Sends a single command to the solver, returns the first available line
--   from the output buffer
sendCommand :: SolverInstance -> Text -> IO Text

-- | Sends a string to the solver and appends a newline, returns the first
--   available line from the output buffer
sendLine :: SolverInstance -> Text -> IO Text

-- | Sends a string to the solver and appends a newline, doesn't return
--   stdout
sendLine' :: SolverInstance -> Text -> IO ()

-- | Returns a string representation of the model for the requested
--   variable
getValue :: SolverInstance -> Text -> IO Text

-- | Reads lines from h until we have a balanced sexpr
readSExpr :: Handle -> IO [Text]

-- | Stores a region of src into dst
copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Builder

-- | Unrolls an exponentiation into a series of multiplications
expandExp :: Expr EWord -> W256 -> Builder

-- | Concatenates a list of bytes into a larger bitvector
concatBytes :: [Expr Byte] -> Builder

-- | Concatenates a list of bytes into a larger bitvector
writeBytes :: ByteString -> Expr Buf -> Builder
encodeConcreteStore :: Map W256 (Map W256 W256) -> Builder
instance GHC.Show.Show EVM.SMT.CexVars
instance GHC.Classes.Eq EVM.SMT.CexVars
instance GHC.Show.Show EVM.SMT.SMTCex
instance GHC.Classes.Eq EVM.SMT.SMTCex
instance GHC.Show.Show EVM.SMT.SMT2
instance GHC.Classes.Eq EVM.SMT.SMT2
instance GHC.Classes.Eq EVM.SMT.CheckSatResult
instance GHC.Show.Show EVM.SMT.CheckSatResult
instance GHC.Show.Show EVM.SMT.Solver
instance GHC.Base.Semigroup EVM.SMT.SMT2
instance GHC.Base.Monoid EVM.SMT.SMT2
instance GHC.Base.Semigroup EVM.SMT.CexVars
instance GHC.Base.Monoid EVM.SMT.CexVars

module EVM.ABI
data AbiValue
AbiUInt :: Int -> Word256 -> AbiValue
AbiInt :: Int -> Int256 -> AbiValue
AbiAddress :: Addr -> AbiValue
AbiBool :: Bool -> AbiValue
AbiBytes :: Int -> ByteString -> AbiValue
AbiBytesDynamic :: ByteString -> AbiValue
AbiString :: ByteString -> AbiValue
AbiArrayDynamic :: AbiType -> Vector AbiValue -> AbiValue
AbiArray :: Int -> AbiType -> Vector AbiValue -> AbiValue
AbiTuple :: Vector AbiValue -> AbiValue
data AbiType
AbiUIntType :: Int -> AbiType
AbiIntType :: Int -> AbiType
AbiAddressType :: AbiType
AbiBoolType :: AbiType
AbiBytesType :: Int -> AbiType
AbiBytesDynamicType :: AbiType
AbiStringType :: AbiType
AbiArrayDynamicType :: AbiType -> AbiType
AbiArrayType :: Int -> AbiType -> AbiType
AbiTupleType :: Vector AbiType -> AbiType
data AbiKind
Dynamic :: AbiKind
Static :: AbiKind
data AbiVals
NoVals :: AbiVals
CAbi :: [AbiValue] -> AbiVals
SAbi :: [Expr EWord] -> AbiVals
abiKind :: AbiType -> AbiKind
data Event
Event :: Text -> Anonymity -> [(Text, AbiType, Indexed)] -> Event
data SolError
SolError :: Text -> [AbiType] -> SolError
data Anonymity
Anonymous :: Anonymity
NotAnonymous :: Anonymity
data Indexed
Indexed :: Indexed
NotIndexed :: Indexed
putAbi :: AbiValue -> Put
getAbi :: AbiType -> Get AbiValue

-- | Decode a sequence type (e.g. tuple / array). Will fail for non
--   sequence types
getAbiSeq :: Int -> [AbiType] -> Get (Vector AbiValue)
genAbiValue :: AbiType -> Gen AbiValue
abiValueType :: AbiValue -> AbiType
abiTypeSolidity :: AbiType -> Text
abiMethod :: Text -> AbiValue -> ByteString
emptyAbi :: AbiValue
encodeAbiValue :: AbiValue -> ByteString
decodeAbiValue :: AbiType -> ByteString -> AbiValue
decodeBuf :: [AbiType] -> Expr Buf -> AbiVals
decodeStaticArgs :: Int -> Int -> Expr Buf -> [Expr EWord]
formatString :: ByteString -> String
parseTypeName :: Vector AbiType -> Text -> Maybe AbiType
makeAbiValue :: AbiType -> String -> AbiValue
parseAbiValue :: AbiType -> ReadP AbiValue
selector :: Text -> ByteString
instance GHC.Generics.Generic EVM.ABI.AbiType
instance GHC.Classes.Ord EVM.ABI.AbiType
instance GHC.Classes.Eq EVM.ABI.AbiType
instance GHC.Read.Read EVM.ABI.AbiType
instance GHC.Generics.Generic EVM.ABI.AbiValue
instance GHC.Classes.Ord EVM.ABI.AbiValue
instance GHC.Classes.Eq EVM.ABI.AbiValue
instance GHC.Read.Read EVM.ABI.AbiValue
instance GHC.Generics.Generic EVM.ABI.AbiKind
instance GHC.Classes.Ord EVM.ABI.AbiKind
instance GHC.Classes.Eq EVM.ABI.AbiKind
instance GHC.Read.Read EVM.ABI.AbiKind
instance GHC.Show.Show EVM.ABI.AbiKind
instance GHC.Generics.Generic EVM.ABI.Anonymity
instance GHC.Classes.Eq EVM.ABI.Anonymity
instance GHC.Classes.Ord EVM.ABI.Anonymity
instance GHC.Show.Show EVM.ABI.Anonymity
instance GHC.Generics.Generic EVM.ABI.Indexed
instance GHC.Classes.Eq EVM.ABI.Indexed
instance GHC.Classes.Ord EVM.ABI.Indexed
instance GHC.Show.Show EVM.ABI.Indexed
instance GHC.Generics.Generic EVM.ABI.Event
instance GHC.Classes.Eq EVM.ABI.Event
instance GHC.Classes.Ord EVM.ABI.Event
instance GHC.Show.Show EVM.ABI.Event
instance GHC.Generics.Generic EVM.ABI.SolError
instance GHC.Classes.Eq EVM.ABI.SolError
instance GHC.Classes.Ord EVM.ABI.SolError
instance GHC.Show.Show EVM.ABI.SolError
instance GHC.Show.Show EVM.ABI.AbiVals
instance GHC.Read.Read EVM.ABI.Boolz
instance GHC.Show.Show EVM.ABI.AbiValue
instance Test.QuickCheck.Arbitrary.Arbitrary EVM.ABI.AbiValue
instance GHC.Show.Show EVM.ABI.AbiType
instance Test.QuickCheck.Arbitrary.Arbitrary EVM.ABI.AbiType

module EVM.Solidity
solidity :: Text -> Text -> IO (Maybe ByteString)
solcRuntime :: Text -> Text -> IO (Maybe ByteString)
solidity' :: Text -> IO (Text, Text)
yul' :: Text -> IO (Text, Text)
yul :: Text -> Text -> IO (Maybe ByteString)
yulRuntime :: Text -> Text -> IO (Maybe ByteString)
data JumpType
JumpInto :: JumpType
JumpFrom :: JumpType
JumpRegular :: JumpType
data SolcContract
SolcContract :: W256 -> W256 -> ByteString -> ByteString -> Text -> [(Text, AbiType)] -> Map Word32 Method -> Map W256 Event -> Map W256 SolError -> Map W256 [Reference] -> Maybe (Map Text StorageItem) -> Seq SrcMap -> Seq SrcMap -> SolcContract
[_runtimeCodehash] :: SolcContract -> W256
[_creationCodehash] :: SolcContract -> W256
[_runtimeCode] :: SolcContract -> ByteString
[_creationCode] :: SolcContract -> ByteString
[_contractName] :: SolcContract -> Text
[_constructorInputs] :: SolcContract -> [(Text, AbiType)]
[_abiMap] :: SolcContract -> Map Word32 Method
[_eventMap] :: SolcContract -> Map W256 Event
[_errorMap] :: SolcContract -> Map W256 SolError
[_immutableReferences] :: SolcContract -> Map W256 [Reference]
[_storageLayout] :: SolcContract -> Maybe (Map Text StorageItem)
[_runtimeSrcmap] :: SolcContract -> Seq SrcMap
[_creationSrcmap] :: SolcContract -> Seq SrcMap
data StorageItem
StorageItem :: SlotType -> Int -> Int -> StorageItem
[_type] :: StorageItem -> SlotType
[_offset] :: StorageItem -> Int
[_slot] :: StorageItem -> Int
data SourceCache
SourceCache :: [(Text, ByteString)] -> [Vector ByteString] -> Map Text Value -> SourceCache
[_sourceFiles] :: SourceCache -> [(Text, ByteString)]
[_sourceLines] :: SourceCache -> [Vector ByteString]
[_sourceAsts] :: SourceCache -> Map Text Value
data SrcMap
SM :: {-# UNPACK #-}Int -> {-# UNPACK #-}Int -> {-# UNPACK #-}Int -> JumpType -> {-# UNPACK #-}Int -> SrcMap
[srcMapOffset] :: SrcMap -> {-# UNPACK #-}Int
[srcMapLength] :: SrcMap -> {-# UNPACK #-}Int
[srcMapFile] :: SrcMap -> {-# UNPACK #-}Int
[srcMapJump] :: SrcMap -> JumpType
[srcMapModifierDepth] :: SrcMap -> {-# UNPACK #-}Int
data CodeType
Creation :: CodeType
Runtime :: CodeType
data Method
Method :: [(Text, AbiType)] -> [(Text, AbiType)] -> Text -> Text -> Mutability -> Method
[_methodOutput] :: Method -> [(Text, AbiType)]
[_methodInputs] :: Method -> [(Text, AbiType)]
[_methodName] :: Method -> Text
[_methodSignature] :: Method -> Text
[_methodMutability] :: Method -> Mutability
data SlotType
StorageMapping :: NonEmpty AbiType -> AbiType -> SlotType
StorageValue :: AbiType -> SlotType
data Reference
Reference :: Int -> Int -> Reference
[_refStart] :: Reference -> Int
[_refLength] :: Reference -> Int
data Mutability

-- | specified to not read blockchain state
Pure :: Mutability

-- | specified to not modify the blockchain state
View :: Mutability

-- | function does not accept Ether - the default
NonPayable :: Mutability

-- | function accepts Ether
Payable :: Mutability
methodName :: Lens' Method Text
methodSignature :: Lens' Method Text
methodInputs :: Lens' Method [(Text, AbiType)]
methodOutput :: Lens' Method [(Text, AbiType)]
methodMutability :: Lens' Method Mutability
abiMap :: Lens' SolcContract (Map Word32 Method)
eventMap :: Lens' SolcContract (Map W256 Event)
errorMap :: Lens' SolcContract (Map W256 SolError)
storageLayout :: Lens' SolcContract (Maybe (Map Text StorageItem))
contractName :: Lens' SolcContract Text
constructorInputs :: Lens' SolcContract [(Text, AbiType)]
creationCode :: Lens' SolcContract ByteString
functionAbi :: Text -> IO Method
makeSrcMaps :: Text -> Maybe (Seq SrcMap)
readSolc :: FilePath -> IO (Maybe (Map Text SolcContract, SourceCache))
readJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])
readStdJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])
readCombinedJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])
runtimeCode :: Lens' SolcContract ByteString
runtimeCodehash :: Lens' SolcContract W256
creationCodehash :: Lens' SolcContract W256
runtimeSrcmap :: Lens' SolcContract (Seq SrcMap)
creationSrcmap :: Lens' SolcContract (Seq SrcMap)
sourceFiles :: Lens' SourceCache [(Text, ByteString)]
sourceLines :: Lens' SourceCache [Vector ByteString]
sourceAsts :: Lens' SourceCache (Map Text Value)
immutableReferences :: Lens' SolcContract (Map W256 [Reference])

-- | When doing CREATE and passing constructor arguments, Solidity loads
--   the argument data via the creation bytecode, since there is no
--   "calldata" for CREATE.
--   
--   This interferes with our ability to look up the current contract by
--   codehash, so we must somehow strip away this extra suffix. Luckily we
--   can detect the end of the actual bytecode by looking for the "metadata
--   hash". (Not 100% correct, but works in practice.)
--   
--   Actually, we strip away the entire BZZR suffix too, because as long as
--   the codehash matches otherwise, we don't care if there is some
--   difference there.
stripBytecodeMetadata :: ByteString -> ByteString
stripBytecodeMetadataSym :: [Expr Byte] -> [Expr Byte]
signature :: AsValue s => s -> Text
solc :: Language -> Text -> IO Text
data Language
Solidity :: Language
Yul :: Language
stdjson :: Language -> Text -> Text
parseMethodInput :: AsValue s => s -> (Text, AbiType)
lineSubrange :: Vector ByteString -> (Int, Int) -> Int -> Maybe (Int, Int)

-- | Every node in the AST has an ID, and other nodes reference those IDs.
--   This function recurses through the tree looking for objects with the
--   "id" key and makes a big map from ID to value.
astIdMap :: Foldable f => f Value -> Map Int Value
astSrcMap :: Map Int Value -> SrcMap -> Maybe Value
containsLinkerHole :: Text -> Bool
makeSourceCache :: [(Text, Maybe ByteString)] -> Map Text Value -> IO SourceCache
instance GHC.Show.Show EVM.Solidity.Language
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Solidity.StandardJSON
instance GHC.Classes.Eq EVM.Solidity.SlotType
instance GHC.Classes.Eq EVM.Solidity.StorageItem
instance GHC.Show.Show EVM.Solidity.StorageItem
instance GHC.Generics.Generic EVM.Solidity.Mutability
instance GHC.Classes.Ord EVM.Solidity.Mutability
instance GHC.Classes.Eq EVM.Solidity.Mutability
instance GHC.Show.Show EVM.Solidity.Mutability
instance GHC.Generics.Generic EVM.Solidity.Method
instance GHC.Classes.Ord EVM.Solidity.Method
instance GHC.Classes.Eq EVM.Solidity.Method
instance GHC.Show.Show EVM.Solidity.Method
instance GHC.Generics.Generic EVM.Solidity.SourceCache
instance GHC.Classes.Eq EVM.Solidity.SourceCache
instance GHC.Show.Show EVM.Solidity.SourceCache
instance GHC.Classes.Eq EVM.Solidity.Reference
instance GHC.Show.Show EVM.Solidity.Reference
instance GHC.Generics.Generic EVM.Solidity.JumpType
instance GHC.Classes.Ord EVM.Solidity.JumpType
instance GHC.Classes.Eq EVM.Solidity.JumpType
instance GHC.Show.Show EVM.Solidity.JumpType
instance GHC.Generics.Generic EVM.Solidity.SrcMap
instance GHC.Classes.Ord EVM.Solidity.SrcMap
instance GHC.Classes.Eq EVM.Solidity.SrcMap
instance GHC.Show.Show EVM.Solidity.SrcMap
instance GHC.Generics.Generic EVM.Solidity.SolcContract
instance GHC.Classes.Eq EVM.Solidity.SolcContract
instance GHC.Show.Show EVM.Solidity.SolcContract
instance GHC.Show.Show EVM.Solidity.SrcMapParseState
instance GHC.Classes.Ord EVM.Solidity.CodeType
instance GHC.Classes.Eq EVM.Solidity.CodeType
instance GHC.Show.Show EVM.Solidity.CodeType
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Solidity.Reference
instance GHC.Base.Semigroup EVM.Solidity.SourceCache
instance GHC.Base.Monoid EVM.Solidity.SourceCache
instance GHC.Show.Show EVM.Solidity.SlotType
instance GHC.Read.Read EVM.Solidity.SlotType

module EVM

-- | EVM failure modes
data Error
BalanceTooLow :: W256 -> W256 -> Error
UnrecognizedOpcode :: Word8 -> Error
SelfDestruction :: Error
StackUnderrun :: Error
BadJumpDestination :: Error
Revert :: Expr Buf -> Error
OutOfGas :: Word64 -> Word64 -> Error
BadCheatCode :: Maybe Word32 -> Error
StackLimitExceeded :: Error
IllegalOverflow :: Error
Query :: Query -> Error
Choose :: Choose -> Error
StateChangeWhileStatic :: Error
InvalidMemoryAccess :: Error
CallDepthLimitReached :: Error
MaxCodeSizeExceeded :: W256 -> W256 -> Error
InvalidFormat :: Error
PrecompileFailure :: Error
UnexpectedSymbolicArg :: Int -> String -> [Expr a] -> Error
DeadPath :: Error
NotUnique :: Expr EWord -> Error
SMTTimeout :: Error
FFI :: [AbiValue] -> Error
NonceOverflow :: Error

-- | The possible result states of a VM
data VMResult

-- | An operation failed
VMFailure :: Error -> VMResult

-- | Reached STOP, RETURN, or end-of-code
VMSuccess :: Expr Buf -> VMResult

-- | The state of a stepwise EVM execution
data VM
VM :: Maybe VMResult -> FrameState -> [Frame] -> Env -> Block -> TxState -> [Expr Log] -> TreePos Empty Trace -> Cache -> Word64 -> Map CodeLocation Int -> [Prop] -> [Prop] -> Bool -> VM
[_result] :: VM -> Maybe VMResult
[_state] :: VM -> FrameState
[_frames] :: VM -> [Frame]
[_env] :: VM -> Env
[_block] :: VM -> Block
[_tx] :: VM -> TxState
[_logs] :: VM -> [Expr Log]
[_traces] :: VM -> TreePos Empty Trace
[_cache] :: VM -> Cache
[_burned] :: VM -> Word64
[_iterations] :: VM -> Map CodeLocation Int
[_constraints] :: VM -> [Prop]
[_keccakEqs] :: VM -> [Prop]
[_allowFFI] :: VM -> Bool
data Trace
Trace :: Int -> Contract -> TraceData -> Trace
[_traceOpIx] :: Trace -> Int
[_traceContract] :: Trace -> Contract
[_traceData] :: Trace -> TraceData
data TraceData
EventTrace :: Expr EWord -> Expr Buf -> [Expr EWord] -> TraceData
FrameTrace :: FrameContext -> TraceData
QueryTrace :: Query -> TraceData
ErrorTrace :: Error -> TraceData
EntryTrace :: Text -> TraceData
ReturnTrace :: Expr Buf -> FrameContext -> TraceData

-- | Queries halt execution until resolved through RPC calls or SMT queries
data Query
[PleaseFetchContract] :: Addr -> (Contract -> EVM ()) -> Query
[PleaseFetchSlot] :: Addr -> W256 -> (W256 -> EVM ()) -> Query
[PleaseAskSMT] :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query
[PleaseDoFFI] :: [String] -> (ByteString -> EVM ()) -> Query
data Choose
[PleaseChoosePath] :: Expr EWord -> (Bool -> EVM ()) -> Choose

-- | Alias for the type of e.g. <tt>exec1</tt>.
type EVM a = State VM a
type CodeLocation = (Addr, Int)

-- | The possible return values of a SMT query
data BranchCondition
Case :: Bool -> BranchCondition
Unknown :: BranchCondition
Inconsistent :: BranchCondition

-- | The possible return values of a `is unique` SMT query
data IsUnique a
Unique :: a -> IsUnique a
Multiple :: IsUnique a
InconsistentU :: IsUnique a
TimeoutU :: IsUnique a

-- | The cache is data that can be persisted for efficiency: any expensive
--   query that is constant at least within a block.
data Cache
Cache :: Map Addr Contract -> Map W256 (Map W256 W256) -> Map (CodeLocation, Int) Bool -> Cache
[_fetchedContracts] :: Cache -> Map Addr Contract
[_fetchedStorage] :: Cache -> Map W256 (Map W256 W256)
[_path] :: Cache -> Map (CodeLocation, Int) Bool
data StorageBase
Concrete :: StorageBase
Symbolic :: StorageBase

-- | A way to specify an initial VM state
data VMOpts
VMOpts :: Contract -> (Expr Buf, [Prop]) -> StorageBase -> Expr EWord -> W256 -> Addr -> Expr EWord -> Addr -> Word64 -> Word64 -> W256 -> Expr EWord -> Addr -> W256 -> W256 -> Word64 -> W256 -> W256 -> FeeSchedule Word64 -> W256 -> Bool -> Map Addr [W256] -> Bool -> VMOpts
[vmoptContract] :: VMOpts -> Contract
[vmoptCalldata] :: VMOpts -> (Expr Buf, [Prop])
[vmoptStorageBase] :: VMOpts -> StorageBase
[vmoptValue] :: VMOpts -> Expr EWord
[vmoptPriorityFee] :: VMOpts -> W256
[vmoptAddress] :: VMOpts -> Addr
[vmoptCaller] :: VMOpts -> Expr EWord
[vmoptOrigin] :: VMOpts -> Addr
[vmoptGas] :: VMOpts -> Word64
[vmoptGaslimit] :: VMOpts -> Word64
[vmoptNumber] :: VMOpts -> W256
[vmoptTimestamp] :: VMOpts -> Expr EWord
[vmoptCoinbase] :: VMOpts -> Addr
[vmoptPrevRandao] :: VMOpts -> W256
[vmoptMaxCodeSize] :: VMOpts -> W256
[vmoptBlockGaslimit] :: VMOpts -> Word64
[vmoptGasprice] :: VMOpts -> W256
[vmoptBaseFee] :: VMOpts -> W256
[vmoptSchedule] :: VMOpts -> FeeSchedule Word64
[vmoptChainId] :: VMOpts -> W256
[vmoptCreate] :: VMOpts -> Bool
[vmoptTxAccessList] :: VMOpts -> Map Addr [W256]
[vmoptAllowFFI] :: VMOpts -> Bool

-- | An entry in the VM's "call/create stack"
data Frame
Frame :: FrameContext -> FrameState -> Frame
[_frameContext] :: Frame -> FrameContext
[_frameState] :: Frame -> FrameState

-- | Call/create info
data FrameContext
CreationContext :: Addr -> Expr EWord -> Map Addr Contract -> SubState -> FrameContext
[creationContextAddress] :: FrameContext -> Addr
[creationContextCodehash] :: FrameContext -> Expr EWord
[creationContextReversion] :: FrameContext -> Map Addr Contract
[creationContextSubstate] :: FrameContext -> SubState
CallContext :: Addr -> Addr -> W256 -> W256 -> Expr EWord -> Maybe W256 -> Expr Buf -> (Map Addr Contract, Expr Storage) -> SubState -> FrameContext
[callContextTarget] :: FrameContext -> Addr
[callContextContext] :: FrameContext -> Addr
[callContextOffset] :: FrameContext -> W256
[callContextSize] :: FrameContext -> W256
[callContextCodehash] :: FrameContext -> Expr EWord
[callContextAbi] :: FrameContext -> Maybe W256
[callContextData] :: FrameContext -> Expr Buf
[callContextReversion] :: FrameContext -> (Map Addr Contract, Expr Storage)
[callContextSubState] :: FrameContext -> SubState

-- | The "registers" of the VM along with memory and data stack
data FrameState
FrameState :: Addr -> Addr -> ContractCode -> Int -> [Expr EWord] -> Expr Buf -> Word64 -> Expr Buf -> Expr EWord -> Expr EWord -> Word64 -> Expr Buf -> Bool -> FrameState
[_contract] :: FrameState -> Addr
[_codeContract] :: FrameState -> Addr
[_code] :: FrameState -> ContractCode
[_pc] :: FrameState -> Int
[_stack] :: FrameState -> [Expr EWord]
[_memory] :: FrameState -> Expr Buf
[_memorySize] :: FrameState -> Word64
[_calldata] :: FrameState -> Expr Buf
[_callvalue] :: FrameState -> Expr EWord
[_caller] :: FrameState -> Expr EWord
[_gas] :: FrameState -> Word64
[_returndata] :: FrameState -> Expr Buf
[_static] :: FrameState -> Bool

-- | The state that spans a whole transaction
data TxState
TxState :: W256 -> Word64 -> W256 -> Addr -> Addr -> Expr EWord -> SubState -> Bool -> Map Addr Contract -> TxState
[_gasprice] :: TxState -> W256
[_txgaslimit] :: TxState -> Word64
[_txPriorityFee] :: TxState -> W256
[_origin] :: TxState -> Addr
[_toAddr] :: TxState -> Addr
[_value] :: TxState -> Expr EWord
[_substate] :: TxState -> SubState
[_isCreate] :: TxState -> Bool
[_txReversion] :: TxState -> Map Addr Contract

-- | The "accrued substate" across a transaction
data SubState
SubState :: [Addr] -> [Addr] -> Set Addr -> Set (Addr, W256) -> [(Addr, Word64)] -> SubState
[_selfdestructs] :: SubState -> [Addr]
[_touchedAccounts] :: SubState -> [Addr]
[_accessedAddresses] :: SubState -> Set Addr
[_accessedStorageKeys] :: SubState -> Set (Addr, W256)
[_refunds] :: SubState -> [(Addr, Word64)]

-- | A contract is either in creation (running its "constructor") or
--   post-creation, and code in these two modes is treated differently by
--   instructions like <tt>EXTCODEHASH</tt>, 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:
--   
--   <ul>
--   <li>initcode has concrete code, followed by an abstract data
--   "section"</li>
--   <li>runtimecode has a fixed length, but may contain fixed size
--   symbolic regions (due to immutable)</li>
--   </ul>
--   
--   hopefully we do not have to deal with dynamic immutable before we get
--   a real data section...
data ContractCode

-- | <a>Constructor</a> code, during contract creation
InitCode :: ByteString -> Expr Buf -> ContractCode

-- | <a>Instance</a> code, after contract creation
RuntimeCode :: RuntimeCode -> ContractCode

-- | We have two variants here to optimize the fully concrete case.
--   ConcreteRuntimeCode just wraps a ByteString SymbolicRuntimeCode is a
--   fixed length vector of potentially symbolic bytes, which lets us
--   handle symbolic pushdata (e.g. from immutable variables in solidity).
data RuntimeCode
ConcreteRuntimeCode :: ByteString -> RuntimeCode
SymbolicRuntimeCode :: Vector (Expr Byte) -> RuntimeCode

-- | A contract can either have concrete or symbolic storage depending on
--   what type of execution we are doing data Storage = Concrete (Map Word
--   Expr EWord) | Symbolic [(Expr EWord, Expr EWord)] (SArray (WordN 256)
--   (WordN 256)) deriving (Show)
--   
--   The state of a contract
data Contract
Contract :: ContractCode -> W256 -> W256 -> Expr EWord -> Vector Int -> Vector (Int, Op) -> Bool -> Contract
[_contractcode] :: Contract -> ContractCode
[_balance] :: Contract -> W256
[_nonce] :: Contract -> W256
[_codehash] :: Contract -> Expr EWord
[_opIxMap] :: Contract -> Vector Int
[_codeOps] :: Contract -> Vector (Int, Op)
[_external] :: Contract -> Bool

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

-- | Uses <a>Concrete</a> Storage. Reading / Writing from abstract
--   locations causes a runtime failure. Can be nicely combined with RPC.
ConcreteS :: StorageModel

-- | Uses <a>Symbolic</a> Storage. Reading / Writing never reaches RPC, but
--   always done using an SMT array with no default value.
SymbolicS :: StorageModel

-- | Uses <a>Symbolic</a> Storage. Reading / Writing never reaches RPC, but
--   always done using an SMT array with 0 as the default value.
InitialS :: StorageModel

-- | Various environmental data
data Env
Env :: Map Addr Contract -> W256 -> Expr Storage -> Map W256 (Map W256 W256) -> Map W256 ByteString -> Env
[_contracts] :: Env -> Map Addr Contract
[_chainId] :: Env -> W256
[_storage] :: Env -> Expr Storage
[_origStorage] :: Env -> Map W256 (Map W256 W256)
[_sha3Crack] :: Env -> Map W256 ByteString

-- | Data about the block
data Block
Block :: Addr -> Expr EWord -> W256 -> W256 -> Word64 -> W256 -> W256 -> FeeSchedule Word64 -> Block
[_coinbase] :: Block -> Addr
[_timestamp] :: Block -> Expr EWord
[_number] :: Block -> W256
[_prevRandao] :: Block -> W256
[_gaslimit] :: Block -> Word64
[_baseFee] :: Block -> W256
[_maxCodeSize] :: Block -> W256
[_schedule] :: Block -> FeeSchedule Word64
blankState :: FrameState
static :: Lens' FrameState Bool
stack :: Lens' FrameState [Expr 'EWord]
returndata :: Lens' FrameState (Expr 'Buf)
pc :: Lens' FrameState Int
memorySize :: Lens' FrameState Word64
memory :: Lens' FrameState (Expr 'Buf)
gas :: Lens' FrameState Word64
contract :: Lens' FrameState Addr
codeContract :: Lens' FrameState Addr
code :: Lens' FrameState ContractCode
callvalue :: Lens' FrameState (Expr 'EWord)
caller :: Lens' FrameState (Expr 'EWord)
calldata :: Lens' FrameState (Expr 'Buf)
frameState :: Lens' Frame FrameState
frameContext :: Lens' Frame FrameContext
timestamp :: Lens' Block (Expr 'EWord)
schedule :: Lens' Block (FeeSchedule Word64)
prevRandao :: Lens' Block W256
number :: Lens' Block W256
maxCodeSize :: Lens' Block W256
gaslimit :: Lens' Block Word64
coinbase :: Lens' Block Addr
baseFee :: Lens' Block W256
value :: Lens' TxState (Expr 'EWord)
txgaslimit :: Lens' TxState Word64
txReversion :: Lens' TxState (Map Addr Contract)
txPriorityFee :: Lens' TxState W256
toAddr :: Lens' TxState Addr
substate :: Lens' TxState SubState
origin :: Lens' TxState Addr
isCreate :: Lens' TxState Bool
gasprice :: Lens' TxState W256
touchedAccounts :: Lens' SubState [Addr]
selfdestructs :: Lens' SubState [Addr]
refunds :: Lens' SubState [(Addr, Word64)]
accessedStorageKeys :: Lens' SubState (Set (Addr, W256))
accessedAddresses :: Lens' SubState (Set Addr)
opIxMap :: Lens' Contract (Vector Int)
nonce :: Lens' Contract W256
external :: Lens' Contract Bool
contractcode :: Lens' Contract ContractCode
codehash :: Lens' Contract (Expr 'EWord)
codeOps :: Lens' Contract (Vector (Int, Op))
balance :: Lens' Contract W256
storage :: Lens' Env (Expr 'Storage)
sha3Crack :: Lens' Env (Map W256 ByteString)
origStorage :: Lens' Env (Map W256 (Map W256 W256))
contracts :: Lens' Env (Map Addr Contract)
chainId :: Lens' Env W256
path :: Lens' Cache (Map (CodeLocation, Int) Bool)
fetchedStorage :: Lens' Cache (Map W256 (Map W256 W256))
fetchedContracts :: Lens' Cache (Map Addr Contract)
traceOpIx :: Lens' Trace Int
traceData :: Lens' Trace TraceData
traceContract :: Lens' Trace Contract
tx :: Lens' VM TxState
traces :: Lens' VM (TreePos Empty Trace)
state :: Lens' VM FrameState
result :: Lens' VM (Maybe VMResult)
logs :: Lens' VM [Expr 'Log]
keccakEqs :: Lens' VM [Prop]
iterations :: Lens' VM (Map CodeLocation Int)
frames :: Lens' VM [Frame]
env :: Lens' VM Env
constraints :: Lens' VM [Prop]
cache :: Lens' VM Cache
burned :: Lens' VM Word64
block :: Lens' VM Block
allowFFI :: Lens' VM Bool

-- | An "external" view of a contract's bytecode, appropriate for e.g.
--   <tt>EXTCODEHASH</tt>.
bytecode :: Getter Contract (Expr Buf)
unifyCachedStorage :: Map W256 W256 -> Map W256 W256 -> Map W256 W256
unifyCachedContract :: Contract -> Contract -> Contract
currentContract :: VM -> Maybe Contract
makeVm :: VMOpts -> VM

-- | Initialize empty contract with given code
initialContract :: ContractCode -> Contract

-- | Update program counter
next :: (?op :: Word8) => EVM ()

-- | Executes the EVM one step
exec1 :: EVM ()
transfer :: Addr -> Addr -> W256 -> EVM ()

-- | Checks a *CALL for failure; OOG, too many callframes, memory access
--   etc.
callChecks :: (?op :: Word8) => Contract -> Word64 -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> (Word64 -> EVM ()) -> EVM ()
precompiledContract :: (?op :: Word8) => Contract -> Word64 -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> EVM ()
executePrecompile :: (?op :: Word8) => Addr -> Word64 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> EVM ()
truncpadlit :: Int -> ByteString -> ByteString
lazySlice :: W256 -> W256 -> ByteString -> ByteString
parseModexpLength :: ByteString -> (W256, W256, W256)
isZero :: W256 -> W256 -> ByteString -> Bool
asInteger :: ByteString -> Integer
noop :: Monad m => m ()
pushTo :: MonadState s m => ASetter s s [a] [a] -> a -> m ()
pushToSequence :: MonadState s m => ASetter s s (Seq a) (Seq a) -> a -> m ()
getCodeLocation :: VM -> CodeLocation
branch :: CodeLocation -> Expr EWord -> (Bool -> EVM ()) -> EVM ()

-- | Construct RPC Query and halt execution until resolved
fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM ()
accessStorage :: Addr -> Expr EWord -> (Expr EWord -> EVM ()) -> EVM ()
accountExists :: Addr -> VM -> Bool
accountEmpty :: Contract -> Bool
finalize :: EVM ()

-- | Loads the selected contract as the current contract to execute
loadContract :: Addr -> EVM ()
limitStack :: Int -> EVM () -> EVM ()
notStatic :: EVM () -> EVM ()

-- | Burn gas, failing if insufficient gas is available
burn :: Word64 -> EVM () -> EVM ()
forceConcrete :: Expr EWord -> String -> (W256 -> EVM ()) -> EVM ()
forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM ()) -> EVM ()
forceConcrete3 :: (Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256) -> EVM ()) -> EVM ()
forceConcrete4 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256) -> EVM ()) -> EVM ()
forceConcrete5 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256) -> EVM ()) -> EVM ()
forceConcrete6 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256, W256) -> EVM ()) -> EVM ()
forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM ()) -> EVM ()
refund :: Word64 -> EVM ()
unRefund :: Word64 -> EVM ()
touchAccount :: Addr -> EVM ()
selfdestruct :: Addr -> EVM ()
accessAndBurn :: Addr -> EVM () -> EVM ()

-- | returns a wrapped boolean- if true, this address has been touched
--   before in the txn (warm gas cost as in EIP 2929) otherwise cold
accessAccountForGas :: Addr -> EVM Bool

-- | returns a wrapped boolean- if true, this slot has been touched before
--   in the txn (warm gas cost as in EIP 2929) otherwise cold
accessStorageForGas :: Addr -> Expr EWord -> EVM Bool
cheatCode :: Addr
cheat :: (?op :: Word8) => (W256, W256) -> (W256, W256) -> EVM ()
type CheatAction = Expr EWord -> Expr EWord -> Expr Buf -> EVM ()
cheatActions :: Map Word32 CheatAction

-- | We don't wanna introduce the machinery needed to sign with a random
--   nonce, so we just use the same nonce every time (420). This is
--   obviusly very insecure, but fine for testing purposes.
ethsign :: PrivateKey -> Digest Keccak_256 -> Signature
delegateCall :: (?op :: Word8) => Contract -> Word64 -> Expr EWord -> Expr EWord -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> (Addr -> EVM ()) -> EVM ()
collision :: Maybe Contract -> Bool
create :: (?op :: Word8) => Addr -> Contract -> Word64 -> W256 -> [Expr EWord] -> Addr -> Expr Buf -> EVM ()

-- | Replace a contract's code, like when CREATE returns from the
--   constructor code.
replaceCode :: Addr -> ContractCode -> EVM ()
replaceCodeOfSelf :: ContractCode -> EVM ()
resetState :: EVM ()
vmError :: Error -> EVM ()
underrun :: EVM ()

-- | A stack frame can be popped in three ways.
data FrameResult

-- | STOP, RETURN, or no more code
FrameReturned :: Expr Buf -> FrameResult

-- | REVERT
FrameReverted :: Expr Buf -> FrameResult

-- | Any other error
FrameErrored :: Error -> FrameResult

-- | This function defines how to pop the current stack frame in either of
--   the ways specified by <a>FrameResult</a>.
--   
--   It also handles the case when the current stack frame is the only one;
--   in this case, we set the final <a>_result</a> of the VM execution.
finishFrame :: FrameResult -> EVM ()
accessUnboundedMemoryRange :: FeeSchedule Word64 -> Word64 -> Word64 -> EVM () -> EVM ()
accessMemoryRange :: FeeSchedule Word64 -> W256 -> W256 -> EVM () -> EVM ()
accessMemoryWord :: FeeSchedule Word64 -> W256 -> EVM () -> EVM ()
copyBytesToMemory :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM ()
copyCallBytesToMemory :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM ()
readMemory :: Expr EWord -> Expr EWord -> VM -> Expr Buf
withTraceLocation :: MonadState VM m => TraceData -> m Trace
pushTrace :: TraceData -> EVM ()
insertTrace :: TraceData -> EVM ()
popTrace :: EVM ()
zipperRootForest :: TreePos Empty a -> Forest a
traceForest :: VM -> Forest Trace
traceTopLog :: MonadState VM m => [Expr Log] -> m ()
push :: W256 -> EVM ()
pushSym :: Expr EWord -> EVM ()
stackOp1 :: (?op :: Word8) => (Expr EWord -> Word64) -> (Expr EWord -> Expr EWord) -> EVM ()
stackOp2 :: (?op :: Word8) => ((Expr EWord, Expr EWord) -> Word64) -> ((Expr EWord, Expr EWord) -> Expr EWord) -> EVM ()
stackOp3 :: (?op :: Word8) => ((Expr EWord, Expr EWord, Expr EWord) -> Word64) -> ((Expr EWord, Expr EWord, Expr EWord) -> Expr EWord) -> EVM ()
checkJump :: Int -> [Expr EWord] -> EVM ()
opSize :: Word8 -> Int
mkOpIxMap :: ContractCode -> Vector Int
vmOp :: VM -> Maybe Op
vmOpIx :: VM -> Maybe Int
opParams :: VM -> Map String (Expr EWord)

-- | Reads
readOp :: Word8 -> [Expr Byte] -> Op
mkCodeOps :: ContractCode -> Vector (Int, Op)
costOfCall :: FeeSchedule Word64 -> Bool -> W256 -> Word64 -> Word64 -> Addr -> EVM (Word64, Word64)
costOfCreate :: FeeSchedule Word64 -> Word64 -> W256 -> (Word64, Word64)
concreteModexpGasFee :: ByteString -> Word64
costOfPrecompile :: FeeSchedule Word64 -> Addr -> Expr Buf -> Word64
memoryCost :: FeeSchedule Word64 -> Word64 -> Word64
ceilDiv :: (Num a, Integral a) => a -> a -> a
allButOne64th :: (Num a, Integral a) => a -> a
log2 :: FiniteBits b => b -> Int
hashcode :: ContractCode -> Expr EWord

-- | The length of the code ignoring any constructor args. This represents
--   the region that can contain executable opcodes
opslen :: ContractCode -> Int

-- | The length of the code including any constructor args. This can return
--   an abstract value
codelen :: ContractCode -> Expr EWord
toBuf :: ContractCode -> Expr Buf
codeloc :: EVM CodeLocation
instance GHC.Show.Show EVM.FrameResult
instance GHC.Base.Semigroup EVM.Cache
instance GHC.Base.Monoid EVM.Cache
instance GHC.Show.Show EVM.BranchCondition
instance GHC.Show.Show a => GHC.Show.Show (EVM.IsUnique a)
instance GHC.Classes.Eq EVM.StorageBase
instance GHC.Show.Show EVM.StorageBase
instance GHC.Show.Show EVM.SubState
instance GHC.Classes.Ord EVM.RuntimeCode
instance GHC.Classes.Eq EVM.RuntimeCode
instance GHC.Show.Show EVM.RuntimeCode
instance GHC.Show.Show EVM.ContractCode
instance GHC.Show.Show EVM.FrameState
instance GHC.Show.Show EVM.TxState
instance GHC.Show.Show EVM.FrameContext
instance GHC.Show.Show EVM.Frame
instance GHC.Show.Show EVM.VMOpts
instance GHC.Show.Show EVM.Cache
instance GHC.Show.Show EVM.StorageModel
instance GHC.Read.Read EVM.StorageModel
instance GHC.Show.Show EVM.Env
instance GHC.Show.Show EVM.Block
instance GHC.Show.Show EVM.TraceData
instance GHC.Show.Show EVM.Trace
instance GHC.Show.Show EVM.VM
instance GHC.Show.Show EVM.Error
instance GHC.Show.Show EVM.VMResult
instance GHC.Classes.Ord EVM.ContractCode
instance GHC.Show.Show EVM.Contract
instance GHC.Show.Show EVM.Query
instance GHC.Show.Show EVM.Choose
instance Options.Generic.ParseField EVM.StorageModel
instance GHC.Classes.Eq EVM.ContractCode

module EVM.Transaction
data AccessListEntry
AccessListEntry :: Addr -> [W256] -> AccessListEntry
[accessAddress] :: AccessListEntry -> Addr
[accessStorageKeys] :: AccessListEntry -> [W256]
data TxType
LegacyTransaction :: TxType
AccessListTransaction :: TxType
EIP1559Transaction :: TxType
data Transaction
Transaction :: ByteString -> Word64 -> Maybe W256 -> W256 -> W256 -> W256 -> Maybe Addr -> W256 -> W256 -> TxType -> [AccessListEntry] -> Maybe W256 -> Maybe W256 -> Transaction
[txData] :: Transaction -> ByteString
[txGasLimit] :: Transaction -> Word64
[txGasPrice] :: Transaction -> Maybe W256
[txNonce] :: Transaction -> W256
[txR] :: Transaction -> W256
[txS] :: Transaction -> W256
[txToAddr] :: Transaction -> Maybe Addr
[txV] :: Transaction -> W256
[txValue] :: Transaction -> W256
[txType] :: Transaction -> TxType
[txAccessList] :: Transaction -> [AccessListEntry]
[txMaxPriorityFeeGas] :: Transaction -> Maybe W256
[txMaxFeePerGas] :: Transaction -> Maybe W256

-- | utility function for getting a more useful representation of
--   accesslistentries duplicates only matter for gas computation
txAccessMap :: Transaction -> Map Addr [W256]
ecrec :: W256 -> W256 -> W256 -> W256 -> Maybe Addr
sender :: Int -> Transaction -> Maybe Addr
signingData :: Int -> Transaction -> ByteString
accessListPrice :: FeeSchedule Word64 -> [AccessListEntry] -> Word64
txGasCost :: FeeSchedule Word64 -> Transaction -> Word64
accountAt :: Addr -> Getter (Map Addr Contract) Contract
touchAccount :: Addr -> Map Addr Contract -> Map Addr Contract
newAccount :: Contract

-- | Increments origin nonce and pays gas deposit
setupTx :: Addr -> Addr -> W256 -> Word64 -> Map Addr Contract -> Map Addr Contract

-- | Given a valid tx loaded into the vm state, subtract gas payment from
--   the origin, increment the nonce and pay receiving address
initTx :: VM -> VM
instance GHC.Show.Show EVM.Transaction.AccessListEntry
instance GHC.Classes.Eq EVM.Transaction.TxType
instance GHC.Show.Show EVM.Transaction.TxType
instance GHC.Show.Show EVM.Transaction.Transaction
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Transaction.Transaction
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Transaction.AccessListEntry

module EVM.Fetch

-- | Abstract representation of an RPC fetch request
data RpcQuery a
[QueryCode] :: Addr -> RpcQuery ByteString
[QueryBlock] :: RpcQuery Block
[QueryBalance] :: Addr -> RpcQuery W256
[QueryNonce] :: Addr -> RpcQuery W256
[QuerySlot] :: Addr -> W256 -> RpcQuery W256
[QueryChainId] :: RpcQuery W256
data BlockNumber
Latest :: BlockNumber
BlockNumber :: W256 -> BlockNumber
type RpcInfo = Maybe (BlockNumber, Text)
rpc :: String -> [Value] -> Value
class ToRPC a
toRPC :: ToRPC a => a -> Value
readText :: Read a => Text -> a
fetchQuery :: Show a => BlockNumber -> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
parseBlock :: (AsValue s, Show s) => s -> Maybe Block
fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value)
fetchContractWithSession :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchSlotWithSession :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe W256)
fetchBlockWithSession :: BlockNumber -> Text -> Session -> IO (Maybe Block)
fetchBlockFrom :: BlockNumber -> Text -> IO (Maybe Block)
fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchSlotFrom :: BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256)
http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher
zero :: Natural -> Maybe Natural -> Fetcher
oracle :: SolverGroup -> RpcInfo -> Fetcher
type Fetcher = Query -> IO (EVM ())

-- | Checks which branches are satisfiable, checking the pathconditions for
--   consistency if the third argument is true. When in debug mode, we do
--   not want to be able to navigate to dead paths, but for normal
--   execution paths with inconsistent pathconditions will be pruned
--   anyway.
checkBranch :: SolverGroup -> Prop -> Prop -> IO BranchCondition
instance GHC.Classes.Eq EVM.Fetch.BlockNumber
instance GHC.Show.Show EVM.Fetch.BlockNumber
instance GHC.Show.Show (EVM.Fetch.RpcQuery a)
instance EVM.Fetch.ToRPC EVM.Types.Addr
instance EVM.Fetch.ToRPC EVM.Types.W256
instance EVM.Fetch.ToRPC GHC.Types.Bool
instance EVM.Fetch.ToRPC EVM.Fetch.BlockNumber

module EVM.Facts
data File
File :: Path -> Data -> File
[filePath] :: File -> Path
[fileData] :: File -> Data
data Fact
BalanceFact :: Addr -> W256 -> Fact
[addr] :: Fact -> Addr
[what] :: Fact -> W256
NonceFact :: Addr -> W256 -> Fact
[addr] :: Fact -> Addr
[what] :: Fact -> W256
StorageFact :: Addr -> W256 -> W256 -> Fact
[addr] :: Fact -> Addr
[what] :: Fact -> W256
[which] :: Fact -> W256
CodeFact :: Addr -> ByteString -> Fact
[addr] :: Fact -> Addr
[blob] :: Fact -> ByteString
newtype Data
Data :: ASCII -> Data
[dataASCII] :: Data -> ASCII
data Path
Path :: [ASCII] -> ASCII -> Path
apply :: VM -> Set Fact -> VM
applyCache :: VM -> Set Fact -> VM
cacheFacts :: Cache -> Set Fact
contractFacts :: Addr -> Contract -> Map W256 (Map W256 W256) -> [Fact]
vmFacts :: VM -> Set Fact
factToFile :: Fact -> File
fileToFact :: File -> Maybe Fact
instance GHC.Show.Show EVM.Facts.Fact
instance GHC.Classes.Eq EVM.Facts.Fact
instance GHC.Show.Show EVM.Facts.Path
instance GHC.Classes.Ord EVM.Facts.Path
instance GHC.Classes.Eq EVM.Facts.Path
instance GHC.Show.Show EVM.Facts.Data
instance GHC.Classes.Ord EVM.Facts.Data
instance GHC.Classes.Eq EVM.Facts.Data
instance GHC.Show.Show EVM.Facts.File
instance GHC.Classes.Ord EVM.Facts.File
instance GHC.Classes.Eq EVM.Facts.File
instance EVM.Facts.AsASCII EVM.Types.Addr
instance EVM.Facts.AsASCII EVM.Types.W256
instance EVM.Facts.AsASCII Data.ByteString.Internal.ByteString
instance GHC.Classes.Ord EVM.Facts.Fact

module EVM.Facts.Git
saveFacts :: RepoAt -> Set Fact -> IO ()
loadFacts :: RepoAt -> IO (Set Fact)
newtype RepoAt
RepoAt :: String -> RepoAt
instance GHC.Show.Show EVM.Facts.Git.RepoAt
instance GHC.Classes.Ord EVM.Facts.Git.RepoAt
instance GHC.Classes.Eq EVM.Facts.Git.RepoAt

module EVM.Exec
ethrunAddress :: Addr
vmForEthrunCreation :: ByteString -> VM
exec :: MonadState VM m => m VMResult
run :: MonadState VM m => m VM
execWhile :: MonadState VM m => (VM -> Bool) -> m Int

module EVM.Stepper

-- | The instruction type of the operational monad
data Action a

-- | Keep executing until an intermediate result is reached
[Exec] :: Action VMResult

-- | Keep executing until an intermediate state is reached
[Run] :: Action VM

-- | Wait for a query to be resolved
[Wait] :: Query -> Action ()

-- | Multiple things can happen
[Ask] :: Choose -> Action ()

-- | Embed a VM state transformation
[EVM] :: EVM a -> Action a

-- | Perform an IO action
[IOAct] :: StateT VM IO a -> Action a

-- | Type alias for an operational monad of <tt>Action</tt>
type Stepper a = Program Action a
exec :: Stepper VMResult

-- | Run the VM until final result, resolving all queries
execFully :: Stepper (Either Error (Expr Buf))
run :: Stepper VM

-- | Run the VM until its final state
runFully :: Stepper VM
wait :: Query -> Stepper ()
ask :: Choose -> Stepper ()
evm :: EVM a -> Stepper a
evmIO :: StateT VM IO a -> Stepper a
entering :: Text -> Stepper a -> Stepper a
enter :: Text -> Stepper ()
interpret :: Fetcher -> Stepper a -> StateT VM IO a

module EVM.Debug
data Mode
Debug :: Mode
Run :: Mode
JsonTrace :: Mode
object :: [(Doc, Doc)] -> Doc
prettyContract :: Contract -> Doc
prettyContracts :: Map Addr Contract -> Doc
srcMapCodePos :: SourceCache -> SrcMap -> Maybe (Text, Int)
srcMapCode :: SourceCache -> SrcMap -> Maybe ByteString
instance GHC.Show.Show EVM.Debug.Mode
instance GHC.Classes.Eq EVM.Debug.Mode

module EVM.Dapp
data DappInfo
DappInfo :: FilePath -> Map Text SolcContract -> Map W256 (CodeType, SolcContract) -> [(Code, SolcContract)] -> SourceCache -> [(Text, [(Test, [AbiType])])] -> Map Word32 Method -> Map W256 Event -> Map W256 SolError -> Map Int Value -> (SrcMap -> Maybe Value) -> DappInfo
[_dappRoot] :: DappInfo -> FilePath
[_dappSolcByName] :: DappInfo -> Map Text SolcContract
[_dappSolcByHash] :: DappInfo -> Map W256 (CodeType, SolcContract)
[_dappSolcByCode] :: DappInfo -> [(Code, SolcContract)]
[_dappSources] :: DappInfo -> SourceCache
[_dappUnitTests] :: DappInfo -> [(Text, [(Test, [AbiType])])]
[_dappAbiMap] :: DappInfo -> Map Word32 Method
[_dappEventMap] :: DappInfo -> Map W256 Event
[_dappErrorMap] :: DappInfo -> Map W256 SolError
[_dappAstIdMap] :: DappInfo -> Map Int Value
[_dappAstSrcMap] :: DappInfo -> SrcMap -> Maybe Value

-- | bytecode modulo immutables, to identify contracts
data Code
Code :: ByteString -> [Reference] -> Code
[raw] :: Code -> ByteString
[immutableLocations] :: Code -> [Reference]
data DappContext
DappContext :: DappInfo -> Map Addr Contract -> DappContext
[_contextInfo] :: DappContext -> DappInfo
[_contextEnv] :: DappContext -> Map Addr Contract
data Test
ConcreteTest :: Text -> Test
SymbolicTest :: Text -> Test
InvariantTest :: Text -> Test
dappUnitTests :: Lens' DappInfo [(Text, [(Test, [AbiType])])]
dappSources :: Lens' DappInfo SourceCache
dappSolcByName :: Lens' DappInfo (Map Text SolcContract)
dappSolcByHash :: Lens' DappInfo (Map W256 (CodeType, SolcContract))
dappSolcByCode :: Lens' DappInfo [(Code, SolcContract)]
dappRoot :: Lens' DappInfo FilePath
dappEventMap :: Lens' DappInfo (Map W256 Event)
dappErrorMap :: Lens' DappInfo (Map W256 SolError)
dappAstSrcMap :: Lens' DappInfo (SrcMap -> Maybe Value)
dappAstIdMap :: Lens' DappInfo (Map Int Value)
dappAbiMap :: Lens' DappInfo (Map Word32 Method)
contextInfo :: Lens' DappContext DappInfo
contextEnv :: Lens' DappContext (Map Addr Contract)
dappInfo :: FilePath -> Map Text SolcContract -> SourceCache -> DappInfo
emptyDapp :: DappInfo
unitTestMarkerAbi :: Word32
findAllUnitTests :: [SolcContract] -> [(Text, [(Test, [AbiType])])]
mkTest :: Text -> Maybe Test
findUnitTests :: Text -> [SolcContract] -> [(Text, [(Test, [AbiType])])]
unitTestMethodsFiltered :: (Text -> Bool) -> SolcContract -> [(Test, [AbiType])]
unitTestMethods :: SolcContract -> [(Test, [AbiType])]
extractSig :: Test -> Text
traceSrcMap :: DappInfo -> Trace -> Maybe SrcMap
srcMap :: DappInfo -> Contract -> Int -> Maybe SrcMap
findSrc :: Contract -> DappInfo -> Maybe SolcContract
lookupCode :: ContractCode -> DappInfo -> Maybe SolcContract
compareCode :: ByteString -> Code -> Bool
showTraceLocation :: DappInfo -> Trace -> Either Text Text
instance GHC.Show.Show EVM.Dapp.Test
instance GHC.Show.Show EVM.Dapp.Code

module EVM.StorageLayout
findContractDefinition :: DappInfo -> SolcContract -> Maybe Value
storageLayout :: DappInfo -> SolcContract -> [Text]
storageVariablesForContract :: Value -> Maybe [Text]
nodeIs :: Text -> Value -> Bool
isStorageVariableDeclaration :: Value -> Bool
slotTypeForDeclaration :: Value -> SlotType
grokDeclarationType :: Value -> SlotType
grokMappingType :: [Value] -> SlotType
grokValueType :: Value -> AbiType

module EVM.Format
formatExpr :: Expr a -> Text
contractNamePart :: Text -> Text
contractPathPart :: Text -> Text
showError :: (?context :: DappContext) => Expr Buf -> Text

-- | Show a <a>Tree</a> using Unicode art
showTree :: Tree String -> String
showTraceTree :: DappInfo -> VM -> Text
showValues :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
prettyvmresult :: (?context :: DappContext) => Expr End -> String
showCall :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
showWordExact :: W256 -> Text
showWordExplanation :: W256 -> DappInfo -> Text
parenthesise :: [Text] -> Text
unindexed :: [(Text, AbiType, Indexed)] -> [AbiType]
showValue :: (?context :: DappContext) => AbiType -> Expr Buf -> Text
textValues :: (?context :: DappContext) => [AbiType] -> Expr Buf -> [Text]
showAbiValue :: (?context :: DappContext) => AbiValue -> Text
prettyIfConcreteWord :: Expr EWord -> Text
formatBytes :: ByteString -> Text
formatBinary :: ByteString -> Text
indent :: Int -> Text -> Text
instance GHC.Show.Show EVM.Format.Signedness

module EVM.SymExec
data ProofResult a b c
Qed :: a -> ProofResult a b c
Cex :: b -> ProofResult a b c
Timeout :: c -> ProofResult a b c
type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End)
type EquivalenceResult = ProofResult ([VM], [VM]) VM ()
isQed :: ProofResult a b c -> Bool
containsA :: Eq a => Eq b => Eq c => ProofResult a b c -> [(d, e, ProofResult a b c)] -> Bool
data VeriOpts
VeriOpts :: Bool -> Bool -> Maybe Integer -> Maybe Integer -> RpcInfo -> VeriOpts
[simp] :: VeriOpts -> Bool
[debug] :: VeriOpts -> Bool
[maxIter] :: VeriOpts -> Maybe Integer
[askSmtIters] :: VeriOpts -> Maybe Integer
[rpcInfo] :: VeriOpts -> RpcInfo
defaultVeriOpts :: VeriOpts
rpcVeriOpts :: (BlockNumber, Text) -> VeriOpts
debugVeriOpts :: VeriOpts
extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
inRange :: Int -> Expr EWord -> Prop
bool :: Expr EWord -> Prop

-- | Abstract calldata argument generation
symAbiArg :: Text -> AbiType -> CalldataFragment
data CalldataFragment
St :: [Prop] -> Expr EWord -> CalldataFragment
Dy :: [Prop] -> Expr EWord -> Expr Buf -> CalldataFragment
Comp :: [CalldataFragment] -> CalldataFragment

-- | Generates calldata matching given type signature, optionally
--   specialized with concrete arguments. Any argument given as
--   "<a>symbolic</a>" or omitted at the tail of the list are kept
--   symbolic.
symCalldata :: Text -> [AbiType] -> [String] -> Expr Buf -> (Expr Buf, [Prop])
cdLen :: [CalldataFragment] -> Expr EWord
writeSelector :: Expr Buf -> Text -> Expr Buf
combineFragments :: [CalldataFragment] -> Expr Buf -> (Expr Buf, [Prop])
abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> Maybe Precondition -> StorageModel -> VM
loadSymVM :: ContractCode -> Expr Storage -> Expr EWord -> Expr EWord -> Expr Buf -> [Prop] -> VM

-- | Interpreter which explores all paths at branching points. returns an
--   Expr representing the possible executions
interpret :: Fetcher -> Maybe Integer -> Maybe Integer -> Stepper (Expr End) -> StateT VM IO (Expr End)
maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool
type Precondition = VM -> Prop
type Postcondition = VM -> Expr End -> Prop
checkAssert :: SolverGroup -> [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> IO (Expr End, [VerifyResult])

-- | Checks if an assertion violation has been encountered
--   
--   hevm recognises the following as an assertion violation:
--   
--   <ol>
--   <li>the invalid opcode (0xfe) (solc &lt; 0.8)</li>
--   <li>a revert with a reason of the form
--   `abi.encodeWithSelector("Panic(uint256)", code)`, where code is one of
--   the following (solc &gt;= 0.8): - 0x00: Used for generic compiler
--   inserted panics. - 0x01: If you call assert with an argument that
--   evaluates to false. - 0x11: If an arithmetic operation results in
--   underflow or overflow outside of an unchecked { ... } block. - 0x12;
--   If you divide or modulo by zero (e.g. 5 / 0 or 23 % 0). - 0x21: If you
--   convert a value that is too big or negative into an enum type. - 0x22:
--   If you access a storage byte array that is incorrectly encoded. -
--   0x31: If you call .pop() on an empty array. - 0x32: If you access an
--   array, bytesN or an array slice at an out-of-bounds or negative index
--   (i.e. x[i] where i &gt;= x.length or i &lt; 0). - 0x41: If you
--   allocate too much memory or create an array that is too large. - 0x51:
--   If you call a zero-initialized variable of internal function
--   type.</li>
--   </ol>
--   
--   see:
--   <a>https://docs.soliditylang.org/en/v0.8.6/control-structures.html?highlight=Panic#panic-via-assert-and-error-via-require</a>
checkAssertions :: [Word256] -> Postcondition

-- | By default hevm checks for all assertions except those which result
--   from arithmetic overflow
defaultPanicCodes :: [Word256]
allPanicCodes :: [Word256]

-- | Produces the revert message for solc &gt;=0.8 assertion violations
panicMsg :: Word256 -> ByteString
verifyContract :: SolverGroup -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> StorageModel -> Maybe Precondition -> Maybe Postcondition -> IO (Expr End, [VerifyResult])
pruneDeadPaths :: [VM] -> [VM]

-- | Stepper that parses the result of Stepper.runFully into an Expr End
runExpr :: Stepper (Expr End)

-- | Converts a given top level expr into a list of final states and the
--   associated path conditions for each state
flattenExpr :: Expr End -> [([Prop], Expr End)]

-- | Strips unreachable branches from a given expr Returns a list of
--   executed SMT queries alongside the reduced expression for debugging
--   purposes Note that the reduced expression loses information relative
--   to the original one if jump conditions are removed. This restriction
--   can be removed once Expr supports attaching knowledge to AST nodes.
--   Although this algorithm currently parallelizes nicely, it does not
--   exploit the incremental nature of the task at hand. Introducing
--   support for incremental queries might let us go even faster here.
--   TODO: handle errors properly
reachable :: SolverGroup -> Expr End -> IO ([SMT2], Expr End)

-- | Evaluate the provided proposition down to its most concrete result
evalProp :: Prop -> Prop

-- | Extract contraints stored in Expr End nodes
extractProps :: Expr End -> [Prop]

-- | Symbolically execute the VM and check all endstates against the
--   postcondition, if available.
verify :: SolverGroup -> VeriOpts -> VM -> Maybe Postcondition -> IO (Expr End, [VerifyResult])

-- | Compares two contract runtimes for trace equivalence by running two
--   VMs and comparing the end states.
equivalenceCheck :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> Maybe (Text, [AbiType]) -> IO [(Maybe SMTCex, Prop, ProofResult () () ())]
both' :: (a -> b) -> (a, a) -> (b, b)
produceModels :: SolverGroup -> Expr End -> IO [(Expr End, CheckSatResult)]
showModel :: Expr Buf -> (Expr End, CheckSatResult) -> IO ()
formatCex :: Expr Buf -> SMTCex -> Text

-- | Takes a buffer and a Cex and replaces all abstract values in the buf
--   with concrete ones from the Cex
subModel :: SMTCex -> Expr a -> Expr a
instance (GHC.Classes.Eq a, GHC.Classes.Eq b, GHC.Classes.Eq c) => GHC.Classes.Eq (EVM.SymExec.ProofResult a b c)
instance (GHC.Show.Show a, GHC.Show.Show b, GHC.Show.Show c) => GHC.Show.Show (EVM.SymExec.ProofResult a b c)
instance GHC.Show.Show EVM.SymExec.VeriOpts
instance GHC.Classes.Eq EVM.SymExec.VeriOpts
instance GHC.Classes.Eq EVM.SymExec.CalldataFragment
instance GHC.Show.Show EVM.SymExec.CalldataFragment

module EVM.UnitTest
data UnitTestOptions
UnitTestOptions :: RpcInfo -> SolverGroup -> Maybe Int -> Maybe Integer -> Maybe Integer -> Bool -> Maybe Int -> Maybe Natural -> Maybe Text -> Maybe Text -> Text -> Int -> Maybe (Text, ByteString) -> (VM -> VM) -> DappInfo -> TestVMParams -> Bool -> UnitTestOptions
[rpcInfo] :: UnitTestOptions -> RpcInfo
[solvers] :: UnitTestOptions -> SolverGroup
[verbose] :: UnitTestOptions -> Maybe Int
[maxIter] :: UnitTestOptions -> Maybe Integer
[askSmtIters] :: UnitTestOptions -> Maybe Integer
[smtDebug] :: UnitTestOptions -> Bool
[maxDepth] :: UnitTestOptions -> Maybe Int
[smtTimeout] :: UnitTestOptions -> Maybe Natural
[solver] :: UnitTestOptions -> Maybe Text
[covMatch] :: UnitTestOptions -> Maybe Text
[match] :: UnitTestOptions -> Text
[fuzzRuns] :: UnitTestOptions -> Int
[replay] :: UnitTestOptions -> Maybe (Text, ByteString)
[vmModifier] :: UnitTestOptions -> VM -> VM
[dapp] :: UnitTestOptions -> DappInfo
[testParams] :: UnitTestOptions -> TestVMParams
[ffiAllowed] :: UnitTestOptions -> Bool
data TestVMParams
TestVMParams :: Addr -> Addr -> Addr -> Word64 -> Word64 -> W256 -> W256 -> W256 -> Addr -> W256 -> W256 -> Word64 -> W256 -> W256 -> W256 -> W256 -> TestVMParams
[testAddress] :: TestVMParams -> Addr
[testCaller] :: TestVMParams -> Addr
[testOrigin] :: TestVMParams -> Addr
[testGasCreate] :: TestVMParams -> Word64
[testGasCall] :: TestVMParams -> Word64
[testBaseFee] :: TestVMParams -> W256
[testPriorityFee] :: TestVMParams -> W256
[testBalanceCreate] :: TestVMParams -> W256
[testCoinbase] :: TestVMParams -> Addr
[testNumber] :: TestVMParams -> W256
[testTimestamp] :: TestVMParams -> W256
[testGaslimit] :: TestVMParams -> Word64
[testGasprice] :: TestVMParams -> W256
[testMaxCodeSize] :: TestVMParams -> W256
[testPrevrandao] :: TestVMParams -> W256
[testChainId] :: TestVMParams -> W256
defaultGasForCreating :: Word64
defaultGasForInvoking :: Word64
defaultBalanceForTestContract :: W256
defaultMaxCodeSize :: W256
type ABIMethod = Text

-- | Generate VeriOpts from UnitTestOptions
makeVeriOpts :: UnitTestOptions -> VeriOpts

-- | Top level CLI endpoint for dapp-test
dappTest :: UnitTestOptions -> String -> Maybe String -> IO Bool

-- | Assuming a constructor is loaded, this stepper will run the
--   constructor to create the test contract, give it an initial balance,
--   and run `setUp()'.
initializeUnitTest :: UnitTestOptions -> SolcContract -> Stepper ()

-- | Assuming a test contract is loaded and initialized, this stepper will
--   run the specified test method and return whether it succeeded.
runUnitTest :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool
execTestStepper :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool
exploreStep :: UnitTestOptions -> ByteString -> Stepper Bool
checkFailures :: UnitTestOptions -> ABIMethod -> Bool -> Stepper Bool

-- | Randomly generates the calldata arguments and runs the test
fuzzTest :: UnitTestOptions -> Text -> [AbiType] -> VM -> Property
tick :: Text -> IO ()

-- | This is like an unresolved source mapping.
data OpLocation
OpLocation :: Contract -> Int -> OpLocation
[srcContract] :: OpLocation -> Contract
[srcOpIx] :: OpLocation -> Int
srcMapForOpLocation :: DappInfo -> OpLocation -> Maybe SrcMap
type CoverageState = (VM, MultiSet OpLocation)
currentOpLocation :: VM -> OpLocation
execWithCoverage :: StateT CoverageState IO VMResult
runWithCoverage :: StateT CoverageState IO VM
interpretWithCoverage :: UnitTestOptions -> Stepper a -> StateT CoverageState IO a
coverageReport :: DappInfo -> MultiSet SrcMap -> Map Text (Vector (Int, ByteString))
coverageForUnitTestContract :: UnitTestOptions -> Map Text SolcContract -> SourceCache -> (Text, [(Test, [AbiType])]) -> IO (MultiSet SrcMap)
runUnitTestContract :: UnitTestOptions -> Map Text SolcContract -> (Text, [(Test, [AbiType])]) -> IO [(Bool, VM)]
runTest :: UnitTestOptions -> VM -> (Test, [AbiType]) -> IO (Text, Either Text Text, VM)
type ExploreTx = (Addr, Addr, ByteString, W256)
decodeCalls :: ByteString -> [ExploreTx]

-- | Runs an invariant test, calls the invariant before execution begins
initialExplorationStepper :: UnitTestOptions -> ABIMethod -> [ExploreTx] -> [Addr] -> Int -> Stepper (Bool, RLP)
explorationStepper :: UnitTestOptions -> ABIMethod -> [ExploreTx] -> [Addr] -> RLP -> Int -> Stepper (Bool, RLP)
getTargetContracts :: UnitTestOptions -> Stepper [Addr]
exploreRun :: UnitTestOptions -> VM -> ABIMethod -> [ExploreTx] -> IO (Text, Either Text Text, VM)
execTest :: UnitTestOptions -> VM -> ABIMethod -> AbiValue -> IO (Bool, VM)

-- | Define the thread spawner for normal test cases
runOne :: UnitTestOptions -> VM -> ABIMethod -> AbiValue -> IO (Text, Either Text Text, VM)

-- | Define the thread spawner for property based tests
fuzzRun :: UnitTestOptions -> VM -> Text -> [AbiType] -> IO (Text, Either Text Text, VM)

-- | Define the thread spawner for symbolic tests
symRun :: UnitTestOptions -> VM -> Text -> [AbiType] -> IO (Text, Either Text Text, VM)
symFailure :: UnitTestOptions -> Text -> Expr Buf -> [AbiType] -> [(Expr End, SMTCex)] -> Text
prettyCalldata :: (?context :: DappContext) => SMTCex -> Expr Buf -> Text -> [AbiType] -> Text
showCalldata :: (?context :: DappContext) => SMTCex -> [AbiType] -> Expr Buf -> Text
showVal :: AbiValue -> Text
execSymTest :: UnitTestOptions -> ABIMethod -> (Expr Buf, [Prop]) -> Stepper (Expr End)
checkSymFailures :: UnitTestOptions -> Stepper VM
indentLines :: Int -> Text -> Text
passOutput :: VM -> UnitTestOptions -> Text -> Text
failOutput :: VM -> UnitTestOptions -> Text -> Text
formatTestLogs :: (?context :: DappContext) => Map W256 Event -> [Expr Log] -> Text
formatTestLog :: (?context :: DappContext) => Map W256 Event -> Expr Log -> Maybe Text
word32Bytes :: Word32 -> ByteString
abiCall :: TestVMParams -> Either (Text, AbiValue) ByteString -> EVM ()
makeTxCall :: TestVMParams -> (Expr Buf, [Prop]) -> EVM ()
initialUnitTestVm :: UnitTestOptions -> SolcContract -> VM
getParametersFromEnvironmentVariables :: Maybe Text -> IO TestVMParams
instance GHC.Show.Show EVM.UnitTest.OpLocation
instance GHC.Classes.Eq EVM.UnitTest.OpLocation
instance GHC.Classes.Ord EVM.UnitTest.OpLocation


module EVM.Dev
checkEquiv :: Typeable a => Expr a -> Expr a -> IO ()
runDappTest :: FilePath -> IO ()
testOpts :: SolverGroup -> FilePath -> FilePath -> IO UnitTestOptions
doTest :: IO ()
analyzeDai :: IO ()
daiExpr :: IO (Expr End)
analyzeVat :: IO ()
analyzeDeposit :: IO ()
reachable' :: Bool -> ByteString -> IO ()
showExpr :: ByteString -> IO ()
summaryStore :: IO ByteString
safeAdd :: IO ByteString
testContract :: IO ByteString
vat :: IO ByteString
initVm :: ByteString -> VM

-- | Builds the Expr for the given evm bytecode object
buildExpr :: SolverGroup -> ByteString -> IO (Expr End)
dai :: IO ByteString

module EVM.TTY
data Name
AbiPane :: Name
StackPane :: Name
BytecodePane :: Name
TracePane :: Name
SolidityPane :: Name
TestPickerPane :: Name
BrowserPane :: Name
Pager :: Name
type UiWidget = Widget Name
data UiVmState
UiVmState :: VM -> Int -> Map Int (VM, Stepper ()) -> Stepper () -> Bool -> UnitTestOptions -> UiVmState
[_uiVm] :: UiVmState -> VM
[_uiStep] :: UiVmState -> Int
[_uiSnapshots] :: UiVmState -> Map Int (VM, Stepper ())
[_uiStepper] :: UiVmState -> Stepper ()
[_uiShowMemory] :: UiVmState -> Bool
[_uiTestOpts] :: UiVmState -> UnitTestOptions
data UiTestPickerState
UiTestPickerState :: List Name (Text, Text) -> DappInfo -> UnitTestOptions -> UiTestPickerState
[_testPickerList] :: UiTestPickerState -> List Name (Text, Text)
[_testPickerDapp] :: UiTestPickerState -> DappInfo
[_testOpts] :: UiTestPickerState -> UnitTestOptions
data UiBrowserState
UiBrowserState :: List Name (Addr, Contract) -> UiVmState -> UiBrowserState
[_browserContractList] :: UiBrowserState -> List Name (Addr, Contract)
[_browserVm] :: UiBrowserState -> UiVmState
data UiState
ViewVm :: UiVmState -> UiState
ViewContracts :: UiBrowserState -> UiState
ViewPicker :: UiTestPickerState -> UiState
ViewHelp :: UiVmState -> UiState
uiVm :: Lens' UiVmState VM
uiTestOpts :: Lens' UiVmState UnitTestOptions
uiStepper :: Lens' UiVmState (Stepper ())
uiStep :: Lens' UiVmState Int
uiSnapshots :: Lens' UiVmState (Map Int (VM, Stepper ()))
uiShowMemory :: Lens' UiVmState Bool
testPickerList :: Lens' UiTestPickerState (List Name (Text, Text))
testPickerDapp :: Lens' UiTestPickerState DappInfo
testOpts :: Lens' UiTestPickerState UnitTestOptions
browserVm :: Lens' UiBrowserState UiVmState
browserContractList :: Lens' UiBrowserState (List Name (Addr, Contract))
_ViewHelp :: Prism' UiState UiVmState
_ViewPicker :: Prism' UiState UiTestPickerState
_ViewContracts :: Prism' UiState UiBrowserState
_ViewVm :: Prism' UiState UiVmState
snapshotInterval :: Int
type Pred a = a -> Bool
data StepMode

-- | Run a specific number of steps
Step :: !Int -> StepMode

-- | Finish when a VM predicate holds
StepUntil :: Pred VM -> StepMode

-- | Each step command in the terminal should finish immediately with one
--   of these outcomes.
data Continuation a

-- | Program finished
Stopped :: a -> Continuation a

-- | Took one step; more steps to go
Continue :: Stepper a -> Continuation a

-- | This turns a <tt>Stepper</tt> into a state action usable from within
--   the TTY loop, yielding a <tt>StepOutcome</tt> depending on the
--   <tt>StepMode</tt>.
interpret :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => StepMode -> Stepper a -> StateT UiVmState IO (Continuation a)
keepExecuting :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => StepMode -> Stepper a -> StateT UiVmState IO (Continuation a)
isUnitTestContract :: Text -> DappInfo -> Bool
mkVty :: IO Vty
runFromVM :: SolverGroup -> RpcInfo -> Maybe Integer -> DappInfo -> VM -> IO VM
initUiVmState :: VM -> UnitTestOptions -> Stepper () -> UiVmState
debuggableTests :: UnitTestOptions -> (Text, [(Test, [AbiType])]) -> [(Text, Text)]
isFuzzTest :: (Test, [AbiType]) -> Bool
main :: UnitTestOptions -> FilePath -> FilePath -> IO ()
takeStep :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => UiVmState -> StepMode -> EventM n UiState ()
backstepUntil :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => (UiVmState -> Pred VM) -> EventM n UiState ()
backstep :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => UiVmState -> IO UiVmState
appEvent :: (?fetcher :: Fetcher, ?maxIter :: Maybe Integer) => BrickEvent Name e -> EventM Name UiState ()
app :: UnitTestOptions -> App UiState () Name
initialUiVmStateForTest :: UnitTestOptions -> (Text, Text) -> UiVmState
myTheme :: [(AttrName, Attr)]
drawUi :: UiState -> [UiWidget]
drawHelpView :: [UiWidget]
drawTestPicker :: UiTestPickerState -> [UiWidget]
drawVmBrowser :: UiBrowserState -> [UiWidget]
drawVm :: UiVmState -> [UiWidget]
drawHelpBar :: UiWidget
stepOneOpcode :: Stepper a -> StateT UiVmState IO ()
isNewTraceAdded :: UiVmState -> Pred VM
isNextSourcePosition :: UiVmState -> Pred VM
isNextSourcePositionWithoutEntering :: UiVmState -> Pred VM
isExecutionHalted :: UiVmState -> Pred VM
currentSrcMap :: DappInfo -> VM -> Maybe SrcMap
drawStackPane :: UiVmState -> UiWidget
message :: VM -> String
drawBytecodePane :: UiVmState -> UiWidget
dim :: Widget n -> Widget n
withHighlight :: Bool -> Widget n -> Widget n
prettyIfConcrete :: Expr Buf -> String
drawTracePane :: UiVmState -> UiWidget
ourWrap :: String -> Widget n
solidityList :: VM -> DappInfo -> List Name (Int, ByteString)
drawSolidityPane :: UiVmState -> UiWidget
ifTallEnough :: Int -> Widget n -> Widget n -> Widget n
opWidget :: (Integral a, Show a) => (a, Op) -> Widget n
selectedAttr :: AttrName
dimAttr :: AttrName
wordAttr :: AttrName
boldAttr :: AttrName
activeAttr :: AttrName
instance GHC.Classes.Ord EVM.TTY.Name
instance GHC.Show.Show EVM.TTY.Name
instance GHC.Classes.Eq EVM.TTY.Name