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


-- | Symbolic EVM Evaluator
--   
--   Symbolic EVM Evaluator
@package hevm
@version 0.53.0

module EVM.FeeSchedule
data FeeSchedule n
FeeSchedule :: n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> n -> FeeSchedule n
[$sel:g_zero:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_base:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_verylow:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_low:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_mid:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_high:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_extcode:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_balance:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_sload:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_jumpdest:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_sset:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_sreset:FeeSchedule] :: FeeSchedule n -> n
[$sel:r_sclear:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_selfdestruct:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_selfdestruct_newaccount:FeeSchedule] :: FeeSchedule n -> n
[$sel:r_selfdestruct:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_create:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_codedeposit:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_call:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_callvalue:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_callstipend:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_newaccount:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_exp:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_expbyte:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_memory:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_txcreate:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_txdatazero:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_txdatanonzero:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_transaction:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_log:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_logdata:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_logtopic:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_sha3:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_sha3word:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_initcodeword:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_copy:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_blockhash:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_extcodehash:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_quaddivisor:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_ecadd:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_ecmul:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_pairing_point:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_pairing_base:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_fround:FeeSchedule] :: FeeSchedule n -> n
[$sel:r_block:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_cold_sload:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_cold_account_access:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_warm_storage_read:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_access_list_address:FeeSchedule] :: FeeSchedule n -> n
[$sel:g_access_list_storage_key:FeeSchedule] :: FeeSchedule n -> n
feeSchedule :: Num n => FeeSchedule n
instance GHC.Show.Show n => GHC.Show.Show (EVM.FeeSchedule.FeeSchedule n)

module EVM.Precompiled

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

module EVM.Types
data Word512
Word512 :: {-# UNPACK #-} !Word256 -> {-# UNPACK #-} !Word256 -> Word512
data Int512
Int512 :: {-# UNPACK #-} !Int256 -> {-# UNPACK #-} !Word256 -> Int512
truncateToAddr :: W256 -> Addr
data EType
Buf :: EType
Storage :: EType
Log :: EType
EWord :: EType
EAddr :: EType
EContract :: EType
Byte :: EType
End :: EType
data GVar (a :: EType)
[BufVar] :: Int -> GVar Buf
[StoreVar] :: Int -> GVar Storage

-- | Expr implements an abstract representation of an EVM program
--   
--   This type can give insight into the provenance of a term which is
--   useful, both for the aesthetic purpose of printing terms in a richer
--   way, but also to allow optimizations on the AST instead of letting the
--   SMT solver do all the heavy lifting.
--   
--   Memory, calldata, and returndata are all represented as a Buf.
--   Semantically speaking a Buf is a byte array with of size 2^256.
--   
--   Bufs have two base constructors: - AbstractBuf: all elements are fully
--   abstract values - ConcreteBuf bs: all elements past (length bs) are
--   zero
--   
--   Bufs can be read from with: - ReadByte idx buf: read the byte at idx
--   from buf - ReadWord idx buf: read the byte at idx from buf
--   
--   Bufs can be written to with: - WriteByte idx val buf: write val to idx
--   in buf - WriteWord idx val buf: write val to idx in buf - CopySlice
--   srcOffset dstOffset size src dst: overwrite dstOffset -> dstOffset
--   + size in dst with srcOffset -> srcOffset + size from src
--   
--   Note that the shared usage of <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 Expr (a :: EType)

-- | Literal words
[Lit] :: {-# UNPACK #-} !W256 -> Expr EWord

-- | Variables
[Var] :: Text -> Expr EWord

-- | variables introduced during the CSE pass
[GVar] :: GVar a -> Expr a
[LitByte] :: {-# UNPACK #-} !Word8 -> Expr Byte
[IndexWord] :: Expr EWord -> Expr EWord -> Expr Byte
[EqByte] :: Expr Byte -> Expr Byte -> Expr EWord
[JoinBytes] :: Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr EWord
[Partial] :: [Prop] -> Traces -> PartialExec -> Expr End
[Failure] :: [Prop] -> Traces -> EvmError -> Expr End
[Success] :: [Prop] -> Traces -> Expr Buf -> Map (Expr EAddr) (Expr EContract) -> Expr End
[ITE] :: Expr EWord -> Expr End -> Expr End -> Expr End
[Add] :: Expr EWord -> Expr EWord -> Expr EWord
[Sub] :: Expr EWord -> Expr EWord -> Expr EWord
[Mul] :: Expr EWord -> Expr EWord -> Expr EWord
[Div] :: Expr EWord -> Expr EWord -> Expr EWord
[SDiv] :: Expr EWord -> Expr EWord -> Expr EWord
[Mod] :: Expr EWord -> Expr EWord -> Expr EWord
[SMod] :: Expr EWord -> Expr EWord -> Expr EWord
[AddMod] :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
[MulMod] :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
[Exp] :: Expr EWord -> Expr EWord -> Expr EWord
[SEx] :: Expr EWord -> Expr EWord -> Expr EWord
[Min] :: Expr EWord -> Expr EWord -> Expr EWord
[Max] :: Expr EWord -> Expr EWord -> Expr EWord
[LT] :: Expr EWord -> Expr EWord -> Expr EWord
[GT] :: Expr EWord -> Expr EWord -> Expr EWord
[LEq] :: Expr EWord -> Expr EWord -> Expr EWord
[GEq] :: Expr EWord -> Expr EWord -> Expr EWord
[SLT] :: Expr EWord -> Expr EWord -> Expr EWord
[SGT] :: Expr EWord -> Expr EWord -> Expr EWord
[Eq] :: Expr EWord -> Expr EWord -> Expr EWord
[IsZero] :: Expr EWord -> Expr EWord
[And] :: Expr EWord -> Expr EWord -> Expr EWord
[Or] :: Expr EWord -> Expr EWord -> Expr EWord
[Xor] :: Expr EWord -> Expr EWord -> Expr EWord
[Not] :: Expr EWord -> Expr EWord
[SHL] :: Expr EWord -> Expr EWord -> Expr EWord
[SHR] :: Expr EWord -> Expr EWord -> Expr EWord
[SAR] :: Expr EWord -> Expr EWord -> Expr EWord
[Keccak] :: Expr Buf -> Expr EWord
[SHA256] :: Expr Buf -> Expr EWord
[Origin] :: Expr EWord
[BlockHash] :: Expr EWord -> Expr EWord
[Coinbase] :: Expr EWord
[Timestamp] :: Expr EWord
[BlockNumber] :: Expr EWord
[PrevRandao] :: Expr EWord
[GasLimit] :: Expr EWord
[ChainId] :: Expr EWord
[BaseFee] :: Expr EWord
[TxValue] :: Expr EWord
[Balance] :: Expr EAddr -> Expr EWord
[Gas] :: Int -> Expr EWord
[CodeSize] :: Expr EAddr -> Expr EWord
[CodeHash] :: Expr EAddr -> Expr EWord
[LogEntry] :: Expr EWord -> Expr Buf -> [Expr EWord] -> Expr Log
[C] :: ContractCode -> Expr Storage -> Expr EWord -> Maybe W64 -> Expr EContract
[SymAddr] :: Text -> Expr EAddr
[LitAddr] :: Addr -> Expr EAddr
[WAddr] :: Expr EAddr -> Expr EWord
[ConcreteStore] :: Map W256 W256 -> Expr Storage
[AbstractStore] :: Expr EAddr -> Maybe W256 -> Expr Storage
[SLoad] :: Expr EWord -> Expr Storage -> Expr EWord
[SStore] :: Expr EWord -> Expr EWord -> Expr Storage -> Expr Storage
[ConcreteBuf] :: ByteString -> Expr Buf
[AbstractBuf] :: Text -> Expr Buf
[ReadWord] :: Expr EWord -> Expr Buf -> Expr EWord
[ReadByte] :: Expr EWord -> Expr Buf -> Expr Byte
[WriteWord] :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf
[WriteByte] :: Expr EWord -> Expr Byte -> Expr Buf -> Expr Buf
[CopySlice] :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf -> Expr Buf
[BufLength] :: Expr Buf -> Expr EWord
data SomeExpr
SomeExpr :: Expr a -> SomeExpr
toNum :: Typeable a => Expr a -> Int
data Prop
[PEq] :: forall a. Typeable a => Expr a -> Expr a -> Prop
[PLT] :: Expr EWord -> Expr EWord -> Prop
[PGT] :: Expr EWord -> Expr EWord -> Prop
[PGEq] :: Expr EWord -> Expr EWord -> Prop
[PLEq] :: Expr EWord -> Expr EWord -> Prop
[PNeg] :: Prop -> Prop
[PAnd] :: Prop -> Prop -> Prop
[POr] :: Prop -> Prop -> Prop
[PImpl] :: Prop -> Prop -> Prop
[PBool] :: Bool -> Prop
(.&&) :: Prop -> Prop -> Prop
infixr 3 .&&
(.||) :: Prop -> Prop -> Prop
infixr 2 .||
(.<) :: Expr EWord -> Expr EWord -> Prop
infix 4 .<
(.<=) :: Expr EWord -> Expr EWord -> Prop
infix 4 .<=
(.>) :: Expr EWord -> Expr EWord -> Prop
infix 4 .>
(.>=) :: Expr EWord -> Expr EWord -> Prop
infix 4 .>=
(.==) :: Typeable a => Expr a -> Expr a -> Prop
infix 4 .==
(./=) :: Typeable a => Expr a -> Expr a -> Prop
infix 4 ./=
pand :: [Prop] -> Prop
por :: [Prop] -> Prop
isPBool :: Prop -> Bool

-- | Core EVM Error Types
data EvmError
BalanceTooLow :: Expr EWord -> Expr EWord -> EvmError
UnrecognizedOpcode :: Word8 -> EvmError
SelfDestruction :: EvmError
StackUnderrun :: EvmError
BadJumpDestination :: EvmError
Revert :: Expr Buf -> EvmError
OutOfGas :: Word64 -> Word64 -> EvmError
StackLimitExceeded :: EvmError
IllegalOverflow :: EvmError
StateChangeWhileStatic :: EvmError
InvalidMemoryAccess :: EvmError
CallDepthLimitReached :: EvmError
MaxCodeSizeExceeded :: W256 -> W256 -> EvmError
MaxInitCodeSizeExceeded :: W256 -> Expr EWord -> EvmError
InvalidFormat :: EvmError
PrecompileFailure :: EvmError
ReturnDataOutOfBounds :: EvmError
NonceOverflow :: EvmError
BadCheatCode :: FunctionSelector -> EvmError
NonexistentFork :: Int -> EvmError

-- | Sometimes we can only partially execute a given program
data PartialExec
UnexpectedSymbolicArg :: Int -> String -> [SomeExpr] -> PartialExec
[$sel:pc:UnexpectedSymbolicArg] :: PartialExec -> Int
[$sel:msg:UnexpectedSymbolicArg] :: PartialExec -> String
[$sel:args:UnexpectedSymbolicArg] :: PartialExec -> [SomeExpr]
MaxIterationsReached :: Int -> Expr EAddr -> PartialExec
[$sel:pc:UnexpectedSymbolicArg] :: PartialExec -> Int
[$sel:addr:UnexpectedSymbolicArg] :: PartialExec -> Expr EAddr
JumpIntoSymbolicCode :: Int -> Int -> PartialExec
[$sel:pc:UnexpectedSymbolicArg] :: PartialExec -> Int
[$sel:jumpDst:UnexpectedSymbolicArg] :: PartialExec -> Int

-- | Effect types used by the vm implementation for side effects &amp;
--   control flow
data Effect t s
[Query] :: Query t s -> Effect t s
[Choose] :: Choose s -> Effect Symbolic s

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

-- | Execution could proceed down one of two branches
data Choose s
[PleaseChoosePath] :: Expr EWord -> (Bool -> EVM Symbolic s ()) -> Choose s

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

-- | The possible result states of a VM
data VMResult (t :: VMType) s
[Unfinished] :: PartialExec -> VMResult Symbolic s
[VMFailure] :: EvmError -> VMResult t s
[VMSuccess] :: Expr Buf -> VMResult t s
[HandleEffect] :: Effect t s -> VMResult t s
data VMType
Symbolic :: VMType
Concrete :: VMType
type family Gas (t :: VMType) = r | r -> t

-- | The state of a stepwise EVM execution
data VM (t :: VMType) s
VM :: Maybe (VMResult t s) -> FrameState t s -> [Frame t s] -> Env -> Block -> TxState -> [Expr Log] -> TreePos Empty Trace -> Cache -> !Gas t -> Map CodeLocation (Int, [Expr EWord]) -> [Prop] -> RuntimeConfig -> Seq ForkState -> Int -> VM (t :: VMType) s
[$sel:result:VM] :: VM (t :: VMType) s -> Maybe (VMResult t s)
[$sel:state:VM] :: VM (t :: VMType) s -> FrameState t s
[$sel:frames:VM] :: VM (t :: VMType) s -> [Frame t s]
[$sel:env:VM] :: VM (t :: VMType) s -> Env
[$sel:block:VM] :: VM (t :: VMType) s -> Block
[$sel:tx:VM] :: VM (t :: VMType) s -> TxState
[$sel:logs:VM] :: VM (t :: VMType) s -> [Expr Log]
[$sel:traces:VM] :: VM (t :: VMType) s -> TreePos Empty Trace
[$sel:cache:VM] :: VM (t :: VMType) s -> Cache
[$sel:burned:VM] :: VM (t :: VMType) s -> !Gas t

-- | how many times we've visited a loc, and what the contents of the stack
--   were when we were there last
[$sel:iterations:VM] :: VM (t :: VMType) s -> Map CodeLocation (Int, [Expr EWord])
[$sel:constraints:VM] :: VM (t :: VMType) s -> [Prop]
[$sel:config:VM] :: VM (t :: VMType) s -> RuntimeConfig
[$sel:forks:VM] :: VM (t :: VMType) s -> Seq ForkState
[$sel:currentFork:VM] :: VM (t :: VMType) s -> Int
data ForkState
ForkState :: Env -> Block -> Cache -> String -> ForkState
[$sel:env:ForkState] :: ForkState -> Env
[$sel:block:ForkState] :: ForkState -> Block
[$sel:cache:ForkState] :: ForkState -> Cache
[$sel:urlOrAlias:ForkState] :: ForkState -> String

-- | Alias for the type of e.g. <tt>exec1</tt>.
type EVM (t :: VMType) s a = StateT (VM t s) (ST s) a

-- | The VM base state (i.e. should new contracts be created with abstract
--   balance / storage?)
data BaseState
EmptyBase :: BaseState
AbstractBase :: BaseState

-- | Configuration options that need to be consulted at runtime
data RuntimeConfig
RuntimeConfig :: Bool -> Maybe (Expr EAddr) -> BaseState -> RuntimeConfig
[$sel:allowFFI:RuntimeConfig] :: RuntimeConfig -> Bool
[$sel:overrideCaller:RuntimeConfig] :: RuntimeConfig -> Maybe (Expr EAddr)
[$sel:baseState:RuntimeConfig] :: RuntimeConfig -> BaseState

-- | An entry in the VM's "call/create stack"
data Frame (t :: VMType) s
Frame :: FrameContext -> FrameState t s -> Frame (t :: VMType) s
[$sel:context:Frame] :: Frame (t :: VMType) s -> FrameContext
[$sel:state:Frame] :: Frame (t :: VMType) s -> FrameState t s

-- | Call/create info
data FrameContext
CreationContext :: Expr EAddr -> Expr EWord -> Map (Expr EAddr) Contract -> SubState -> FrameContext
[$sel:address:CreationContext] :: FrameContext -> Expr EAddr
[$sel:codehash:CreationContext] :: FrameContext -> Expr EWord
[$sel:createreversion:CreationContext] :: FrameContext -> Map (Expr EAddr) Contract
[$sel:substate:CreationContext] :: FrameContext -> SubState
CallContext :: Expr EAddr -> Expr EAddr -> Expr EWord -> Expr EWord -> Expr EWord -> Maybe W256 -> Expr Buf -> Map (Expr EAddr) Contract -> SubState -> FrameContext
[$sel:target:CreationContext] :: FrameContext -> Expr EAddr
[$sel:context:CreationContext] :: FrameContext -> Expr EAddr
[$sel:offset:CreationContext] :: FrameContext -> Expr EWord
[$sel:size:CreationContext] :: FrameContext -> Expr EWord
[$sel:codehash:CreationContext] :: FrameContext -> Expr EWord
[$sel:abi:CreationContext] :: FrameContext -> Maybe W256
[$sel:calldata:CreationContext] :: FrameContext -> Expr Buf
[$sel:callreversion:CreationContext] :: FrameContext -> Map (Expr EAddr) Contract
[$sel:subState:CreationContext] :: FrameContext -> SubState

-- | The "accrued substate" across a transaction
data SubState
SubState :: [Expr EAddr] -> [Expr EAddr] -> Set (Expr EAddr) -> Set (Expr EAddr, W256) -> [(Expr EAddr, Word64)] -> SubState
[$sel:selfdestructs:SubState] :: SubState -> [Expr EAddr]
[$sel:touchedAccounts:SubState] :: SubState -> [Expr EAddr]
[$sel:accessedAddresses:SubState] :: SubState -> Set (Expr EAddr)
[$sel:accessedStorageKeys:SubState] :: SubState -> Set (Expr EAddr, W256)
[$sel:refunds:SubState] :: SubState -> [(Expr EAddr, Word64)]

-- | The "registers" of the VM along with memory and data stack
data FrameState (t :: VMType) s
FrameState :: Expr EAddr -> Expr EAddr -> ContractCode -> {-# UNPACK #-} !Int -> [Expr EWord] -> Memory s -> Word64 -> Expr Buf -> Expr EWord -> Expr EAddr -> !Gas t -> Expr Buf -> Bool -> FrameState (t :: VMType) s
[$sel:contract:FrameState] :: FrameState (t :: VMType) s -> Expr EAddr
[$sel:codeContract:FrameState] :: FrameState (t :: VMType) s -> Expr EAddr
[$sel:code:FrameState] :: FrameState (t :: VMType) s -> ContractCode
[$sel:pc:FrameState] :: FrameState (t :: VMType) s -> {-# UNPACK #-} !Int
[$sel:stack:FrameState] :: FrameState (t :: VMType) s -> [Expr EWord]
[$sel:memory:FrameState] :: FrameState (t :: VMType) s -> Memory s
[$sel:memorySize:FrameState] :: FrameState (t :: VMType) s -> Word64
[$sel:calldata:FrameState] :: FrameState (t :: VMType) s -> Expr Buf
[$sel:callvalue:FrameState] :: FrameState (t :: VMType) s -> Expr EWord
[$sel:caller:FrameState] :: FrameState (t :: VMType) s -> Expr EAddr
[$sel:gas:FrameState] :: FrameState (t :: VMType) s -> !Gas t
[$sel:returndata:FrameState] :: FrameState (t :: VMType) s -> Expr Buf
[$sel:static:FrameState] :: FrameState (t :: VMType) s -> Bool
data Memory s
ConcreteMemory :: MutableMemory s -> Memory s
SymbolicMemory :: !Expr Buf -> Memory s
type MutableMemory s = STVector s Word8

-- | The state that spans a whole transaction
data TxState
TxState :: W256 -> Word64 -> W256 -> Expr EAddr -> Expr EAddr -> Expr EWord -> SubState -> Bool -> Map (Expr EAddr) Contract -> TxState
[$sel:gasprice:TxState] :: TxState -> W256
[$sel:gaslimit:TxState] :: TxState -> Word64
[$sel:priorityFee:TxState] :: TxState -> W256
[$sel:origin:TxState] :: TxState -> Expr EAddr
[$sel:toAddr:TxState] :: TxState -> Expr EAddr
[$sel:value:TxState] :: TxState -> Expr EWord
[$sel:substate:TxState] :: TxState -> SubState
[$sel:isCreate:TxState] :: TxState -> Bool
[$sel:txReversion:TxState] :: TxState -> Map (Expr EAddr) Contract

-- | Various environmental data
data Env
Env :: Map (Expr EAddr) Contract -> W256 -> Int -> Int -> Env
[$sel:contracts:Env] :: Env -> Map (Expr EAddr) Contract
[$sel:chainId:Env] :: Env -> W256
[$sel:freshAddresses:Env] :: Env -> Int
[$sel:freshGasVals:Env] :: Env -> Int

-- | Data about the block
data Block
Block :: Expr EAddr -> Expr EWord -> W256 -> W256 -> Word64 -> W256 -> W256 -> FeeSchedule Word64 -> Block
[$sel:coinbase:Block] :: Block -> Expr EAddr
[$sel:timestamp:Block] :: Block -> Expr EWord
[$sel:number:Block] :: Block -> W256
[$sel:prevRandao:Block] :: Block -> W256
[$sel:gaslimit:Block] :: Block -> Word64
[$sel:baseFee:Block] :: Block -> W256
[$sel:maxCodeSize:Block] :: Block -> W256
[$sel:schedule:Block] :: Block -> FeeSchedule Word64

-- | Full contract state
data Contract
Contract :: ContractCode -> Expr Storage -> Expr Storage -> Expr EWord -> Maybe W64 -> Expr EWord -> Vector Int -> Vector (Int, Op) -> Bool -> Contract
[$sel:code:Contract] :: Contract -> ContractCode
[$sel:storage:Contract] :: Contract -> Expr Storage
[$sel:origStorage:Contract] :: Contract -> Expr Storage
[$sel:balance:Contract] :: Contract -> Expr EWord
[$sel:nonce:Contract] :: Contract -> Maybe W64
[$sel:codehash:Contract] :: Contract -> Expr EWord
[$sel:opIxMap:Contract] :: Contract -> Vector Int
[$sel:codeOps:Contract] :: Contract -> Vector (Int, Op)
[$sel:external:Contract] :: Contract -> Bool
class VMOps (t :: VMType)
burn' :: VMOps t => Gas t -> EVM t s () -> EVM t s ()
burnExp :: VMOps t => Expr EWord -> EVM t s () -> EVM t s ()
burnSha3 :: VMOps t => Expr EWord -> EVM t s () -> EVM t s ()
burnCalldatacopy :: VMOps t => Expr EWord -> EVM t s () -> EVM t s ()
burnCodecopy :: VMOps t => Expr EWord -> EVM t s () -> EVM t s ()
burnExtcodecopy :: VMOps t => Expr EAddr -> Expr EWord -> EVM t s () -> EVM t s ()
burnReturndatacopy :: VMOps t => Expr EWord -> EVM t s () -> EVM t s ()
burnLog :: VMOps t => Expr EWord -> Word8 -> EVM t s () -> EVM t s ()
initialGas :: VMOps t => Gas t
ensureGas :: VMOps t => Word64 -> EVM t s () -> EVM t s ()
gasTryFrom :: VMOps t => Expr EWord -> Either () (Gas t)
costOfCreate :: VMOps t => FeeSchedule Word64 -> Gas t -> Expr EWord -> Bool -> (Gas t, Gas t)
costOfCall :: VMOps t => FeeSchedule Word64 -> Bool -> Expr EWord -> Gas t -> Gas t -> Expr EAddr -> (Word64 -> Word64 -> EVM t s ()) -> EVM t s ()
reclaimRemainingGasAllowance :: VMOps t => VM t s -> EVM t s ()
payRefunds :: VMOps t => EVM t s ()
pushGas :: VMOps t => EVM t s ()
enoughGas :: VMOps t => Word64 -> Gas t -> Bool
subGas :: VMOps t => Gas t -> Word64 -> Gas t
toGas :: VMOps t => Word64 -> Gas t
whenSymbolicElse :: VMOps t => EVM t s a -> EVM t s a -> EVM t s a
partial :: VMOps t => PartialExec -> EVM t s ()
branch :: VMOps t => Expr EWord -> (Bool -> EVM t s ()) -> EVM t s ()

-- | A unique id for a given pc
type CodeLocation = (Expr EAddr, Int)

-- | The cache is data that can be persisted for efficiency: any expensive
--   query that is constant at least within a block.
data Cache
Cache :: Map Addr Contract -> Map (CodeLocation, Int) Bool -> Cache
[$sel:fetched:Cache] :: Cache -> Map Addr Contract
[$sel:path:Cache] :: Cache -> Map (CodeLocation, Int) Bool
unifyCachedContract :: Contract -> Contract -> Contract

-- | A contract is either in creation (running its "constructor") or
--   post-creation, and code in these two modes is treated differently by
--   instructions like <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

-- | Fully abstract code, keyed on an address to give consistent results
--   for e.g. extcodehash
UnknownCode :: Expr EAddr -> 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
data Trace
Trace :: Int -> Contract -> TraceData -> Trace
[$sel:opIx:Trace] :: Trace -> Int
[$sel:contract:Trace] :: Trace -> Contract
[$sel:tracedata:Trace] :: Trace -> TraceData
data TraceData
EventTrace :: Expr EWord -> Expr Buf -> [Expr EWord] -> TraceData
FrameTrace :: FrameContext -> TraceData
ErrorTrace :: EvmError -> TraceData
EntryTrace :: Text -> TraceData
ReturnTrace :: Expr Buf -> FrameContext -> TraceData

-- | Wrapper type containing vm traces and the context needed to pretty
--   print them properly
data Traces
Traces :: Forest Trace -> Map (Expr EAddr) Contract -> Traces
[$sel:traces:Traces] :: Traces -> Forest Trace
[$sel:contracts:Traces] :: Traces -> Map (Expr EAddr) Contract

-- | A specification for an initial VM state
data VMOpts (t :: VMType)
VMOpts :: Contract -> [(Expr EAddr, Contract)] -> (Expr Buf, [Prop]) -> BaseState -> Expr EWord -> W256 -> Expr EAddr -> Expr EAddr -> Expr EAddr -> Gas t -> Word64 -> W256 -> Expr EWord -> Expr EAddr -> W256 -> W256 -> Word64 -> W256 -> W256 -> FeeSchedule Word64 -> W256 -> Bool -> Map (Expr EAddr) [W256] -> Bool -> VMOpts (t :: VMType)
[$sel:contract:VMOpts] :: VMOpts (t :: VMType) -> Contract
[$sel:otherContracts:VMOpts] :: VMOpts (t :: VMType) -> [(Expr EAddr, Contract)]
[$sel:calldata:VMOpts] :: VMOpts (t :: VMType) -> (Expr Buf, [Prop])
[$sel:baseState:VMOpts] :: VMOpts (t :: VMType) -> BaseState
[$sel:value:VMOpts] :: VMOpts (t :: VMType) -> Expr EWord
[$sel:priorityFee:VMOpts] :: VMOpts (t :: VMType) -> W256
[$sel:address:VMOpts] :: VMOpts (t :: VMType) -> Expr EAddr
[$sel:caller:VMOpts] :: VMOpts (t :: VMType) -> Expr EAddr
[$sel:origin:VMOpts] :: VMOpts (t :: VMType) -> Expr EAddr
[$sel:gas:VMOpts] :: VMOpts (t :: VMType) -> Gas t
[$sel:gaslimit:VMOpts] :: VMOpts (t :: VMType) -> Word64
[$sel:number:VMOpts] :: VMOpts (t :: VMType) -> W256
[$sel:timestamp:VMOpts] :: VMOpts (t :: VMType) -> Expr EWord
[$sel:coinbase:VMOpts] :: VMOpts (t :: VMType) -> Expr EAddr
[$sel:prevRandao:VMOpts] :: VMOpts (t :: VMType) -> W256
[$sel:maxCodeSize:VMOpts] :: VMOpts (t :: VMType) -> W256
[$sel:blockGaslimit:VMOpts] :: VMOpts (t :: VMType) -> Word64
[$sel:gasprice:VMOpts] :: VMOpts (t :: VMType) -> W256
[$sel:baseFee:VMOpts] :: VMOpts (t :: VMType) -> W256
[$sel:schedule:VMOpts] :: VMOpts (t :: VMType) -> FeeSchedule Word64
[$sel:chainId:VMOpts] :: VMOpts (t :: VMType) -> W256
[$sel:create:VMOpts] :: VMOpts (t :: VMType) -> Bool
[$sel:txAccessList:VMOpts] :: VMOpts (t :: VMType) -> Map (Expr EAddr) [W256]
[$sel:allowFFI:VMOpts] :: VMOpts (t :: VMType) -> Bool
type Op = GenericOp (Expr EWord)
data GenericOp a
OpStop :: GenericOp a
OpAdd :: GenericOp a
OpMul :: GenericOp a
OpSub :: GenericOp a
OpDiv :: GenericOp a
OpSdiv :: GenericOp a
OpMod :: GenericOp a
OpSmod :: GenericOp a
OpAddmod :: GenericOp a
OpMulmod :: GenericOp a
OpExp :: GenericOp a
OpSignextend :: GenericOp a
OpLt :: GenericOp a
OpGt :: GenericOp a
OpSlt :: GenericOp a
OpSgt :: GenericOp a
OpEq :: GenericOp a
OpIszero :: GenericOp a
OpAnd :: GenericOp a
OpOr :: GenericOp a
OpXor :: GenericOp a
OpNot :: GenericOp a
OpByte :: GenericOp a
OpShl :: GenericOp a
OpShr :: GenericOp a
OpSar :: GenericOp a
OpSha3 :: GenericOp a
OpAddress :: GenericOp a
OpBalance :: GenericOp a
OpOrigin :: GenericOp a
OpCaller :: GenericOp a
OpCallvalue :: GenericOp a
OpCalldataload :: GenericOp a
OpCalldatasize :: GenericOp a
OpCalldatacopy :: GenericOp a
OpCodesize :: GenericOp a
OpCodecopy :: GenericOp a
OpGasprice :: GenericOp a
OpExtcodesize :: GenericOp a
OpExtcodecopy :: GenericOp a
OpReturndatasize :: GenericOp a
OpReturndatacopy :: GenericOp a
OpExtcodehash :: GenericOp a
OpBlockhash :: GenericOp a
OpCoinbase :: GenericOp a
OpTimestamp :: GenericOp a
OpNumber :: GenericOp a
OpPrevRandao :: GenericOp a
OpGaslimit :: GenericOp a
OpChainid :: GenericOp a
OpSelfbalance :: GenericOp a
OpBaseFee :: GenericOp a
OpPop :: GenericOp a
OpMload :: GenericOp a
OpMstore :: GenericOp a
OpMstore8 :: GenericOp a
OpSload :: GenericOp a
OpSstore :: GenericOp a
OpJump :: GenericOp a
OpJumpi :: GenericOp a
OpPc :: GenericOp a
OpMsize :: GenericOp a
OpGas :: GenericOp a
OpJumpdest :: GenericOp a
OpCreate :: GenericOp a
OpCall :: GenericOp a
OpStaticcall :: GenericOp a
OpCallcode :: GenericOp a
OpReturn :: GenericOp a
OpDelegatecall :: GenericOp a
OpCreate2 :: GenericOp a
OpRevert :: GenericOp a
OpSelfdestruct :: GenericOp a
OpDup :: !Word8 -> GenericOp a
OpSwap :: !Word8 -> GenericOp a
OpLog :: !Word8 -> GenericOp a
OpPush0 :: GenericOp a
OpPush :: a -> GenericOp a
OpUnknown :: Word8 -> GenericOp a

-- | 
--   <a>https://docs.soliditylang.org/en/v0.8.19/abi-spec.html#function-selector</a>
newtype FunctionSelector
FunctionSelector :: Word32 -> FunctionSelector
[$sel:unFunctionSelector:FunctionSelector] :: FunctionSelector -> Word32
newtype ByteStringS
ByteStringS :: ByteString -> ByteStringS
newtype W256
W256 :: Word256 -> W256
wordField :: Object -> Key -> Parser W256
newtype W64
W64 :: Word64 -> W64
word64Field :: Object -> Key -> Parser Word64
newtype Addr
Addr :: Word160 -> Addr
[$sel:addressWord160:Addr] :: Addr -> Word160
toChecksumAddress :: String -> String
addrField :: Object -> Key -> Parser Addr
addrFieldMaybe :: Object -> Key -> Parser (Maybe Addr)

-- | A four bit value
newtype Nibble
Nibble :: Word8 -> Nibble
toWord512 :: W256 -> Word512
fromWord512 :: Word512 -> W256
maybeLitByte :: Expr Byte -> Maybe Word8
maybeLitWord :: Expr EWord -> Maybe W256
maybeLitAddr :: Expr EAddr -> Maybe Addr
maybeConcreteStore :: Expr Storage -> Maybe (Map W256 W256)
word256 :: ByteString -> Word256
word :: ByteString -> W256
fromBE :: Integral a => ByteString -> a
asBE :: Integral a => a -> ByteString
word256Bytes :: W256 -> ByteString
word160Bytes :: Addr -> ByteString
hi :: Word8 -> Nibble
lo :: Word8 -> Nibble
toByte :: Nibble -> Nibble -> Word8
unpackNibbles :: ByteString -> [Nibble]
packNibbles :: [Nibble] -> ByteString
toWord64 :: W256 -> Maybe Word64
toInt :: W256 -> Maybe Int
bssToBs :: ByteStringS -> ByteString
keccakBytes :: ByteString -> ByteString
word32 :: [Word8] -> Word32
keccak :: Expr Buf -> Expr EWord
keccak' :: ByteString -> W256
abiKeccak :: ByteString -> FunctionSelector
internalError :: HasCallStack => [Char] -> a
concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
regexMatches :: Text -> Text -> Bool
readNull :: Read a => a -> String -> a
padLeft :: Int -> ByteString -> ByteString
padLeft' :: Int -> Vector (Expr Byte) -> Vector (Expr Byte)
padRight :: Int -> ByteString -> ByteString
padRight' :: Int -> String -> String
formatString :: ByteString -> String

-- | <a>paddedShowHex</a> displays a number in hexadecimal and pads the
--   number with 0 so that it has a minimum length of <tt>w</tt>.
paddedShowHex :: (Show a, Integral a) => Int -> a -> String
untilFixpoint :: Eq a => (a -> a) -> a -> a
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "allowFFI" k EVM.Types.RuntimeConfig EVM.Types.RuntimeConfig a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.BaseState, b GHC.Types.~ EVM.Types.BaseState) => Optics.Label.LabelOptic "baseState" k EVM.Types.RuntimeConfig EVM.Types.RuntimeConfig a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Maybe.Maybe (EVM.Types.Expr 'EVM.Types.EAddr), b GHC.Types.~ GHC.Maybe.Maybe (EVM.Types.Expr 'EVM.Types.EAddr)) => Optics.Label.LabelOptic "overrideCaller" k EVM.Types.RuntimeConfig EVM.Types.RuntimeConfig a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "baseFee" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "coinbase" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "gaslimit" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "maxCodeSize" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "number" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "prevRandao" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.FeeSchedule.FeeSchedule GHC.Word.Word64, b GHC.Types.~ EVM.FeeSchedule.FeeSchedule GHC.Word.Word64) => Optics.Label.LabelOptic "schedule" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "timestamp" k EVM.Types.Block EVM.Types.Block a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "chainId" k EVM.Types.Env EVM.Types.Env a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map (EVM.Types.Expr 'EVM.Types.EAddr) EVM.Types.Contract, b GHC.Types.~ Data.Map.Internal.Map (EVM.Types.Expr 'EVM.Types.EAddr) EVM.Types.Contract) => Optics.Label.LabelOptic "contracts" k EVM.Types.Env EVM.Types.Env a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Int, b GHC.Types.~ GHC.Types.Int) => Optics.Label.LabelOptic "freshAddresses" k EVM.Types.Env EVM.Types.Env a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Int, b GHC.Types.~ GHC.Types.Int) => Optics.Label.LabelOptic "freshGasVals" k EVM.Types.Env EVM.Types.Env a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "balance" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.ContractCode, b GHC.Types.~ EVM.Types.ContractCode) => Optics.Label.LabelOptic "code" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Vector.Vector (GHC.Types.Int, EVM.Types.Op), b GHC.Types.~ Data.Vector.Vector (GHC.Types.Int, EVM.Types.Op)) => Optics.Label.LabelOptic "codeOps" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "codehash" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "external" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Maybe.Maybe EVM.Types.W64, b GHC.Types.~ GHC.Maybe.Maybe EVM.Types.W64) => Optics.Label.LabelOptic "nonce" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Vector.Storable.Vector GHC.Types.Int, b GHC.Types.~ Data.Vector.Storable.Vector GHC.Types.Int) => Optics.Label.LabelOptic "opIxMap" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Storage, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Storage) => Optics.Label.LabelOptic "origStorage" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Storage, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Storage) => Optics.Label.LabelOptic "storage" k EVM.Types.Contract EVM.Types.Contract a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ GHC.Maybe.Maybe EVM.Types.W256, b GHC.Types.~ GHC.Maybe.Maybe EVM.Types.W256) => Optics.Label.LabelOptic "abi" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "address" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf) => Optics.Label.LabelOptic "calldata" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ Data.Map.Internal.Map (EVM.Types.Expr 'EVM.Types.EAddr) EVM.Types.Contract, b GHC.Types.~ Data.Map.Internal.Map (EVM.Types.Expr 'EVM.Types.EAddr) EVM.Types.Contract) => Optics.Label.LabelOptic "callreversion" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "codehash" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "context" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ Data.Map.Internal.Map (EVM.Types.Expr 'EVM.Types.EAddr) EVM.Types.Contract, b GHC.Types.~ Data.Map.Internal.Map (EVM.Types.Expr 'EVM.Types.EAddr) EVM.Types.Contract) => Optics.Label.LabelOptic "createreversion" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "offset" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "size" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.SubState, b GHC.Types.~ EVM.Types.SubState) => Optics.Label.LabelOptic "subState" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.SubState, b GHC.Types.~ EVM.Types.SubState) => Optics.Label.LabelOptic "substate" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.An_AffineTraversal, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "target" k EVM.Types.FrameContext EVM.Types.FrameContext a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.FrameContext, b GHC.Types.~ EVM.Types.FrameContext) => Optics.Label.LabelOptic "context" k (EVM.Types.Frame t s) (EVM.Types.Frame t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.FrameState t1 s1, b GHC.Types.~ EVM.Types.FrameState t2 s2) => Optics.Label.LabelOptic "state" k (EVM.Types.Frame t1 s1) (EVM.Types.Frame t2 s2) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "address" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "allowFFI" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "baseFee" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.BaseState, b GHC.Types.~ EVM.Types.BaseState) => Optics.Label.LabelOptic "baseState" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "blockGaslimit" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ (EVM.Types.Expr 'EVM.Types.Buf, [EVM.Types.Prop]), b GHC.Types.~ (EVM.Types.Expr 'EVM.Types.Buf, [EVM.Types.Prop])) => Optics.Label.LabelOptic "calldata" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "caller" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "chainId" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "coinbase" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Contract, b GHC.Types.~ EVM.Types.Contract) => Optics.Label.LabelOptic "contract" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "create" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Gas t1, b GHC.Types.~ EVM.Types.Gas t2) => Optics.Label.LabelOptic "gas" k (EVM.Types.VMOpts t1) (EVM.Types.VMOpts t2) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "gaslimit" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "gasprice" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "maxCodeSize" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "number" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "origin" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [(EVM.Types.Expr 'EVM.Types.EAddr, EVM.Types.Contract)], b GHC.Types.~ [(EVM.Types.Expr 'EVM.Types.EAddr, EVM.Types.Contract)]) => Optics.Label.LabelOptic "otherContracts" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "prevRandao" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "priorityFee" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.FeeSchedule.FeeSchedule GHC.Word.Word64, b GHC.Types.~ EVM.FeeSchedule.FeeSchedule GHC.Word.Word64) => Optics.Label.LabelOptic "schedule" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "timestamp" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map (EVM.Types.Expr 'EVM.Types.EAddr) [EVM.Types.W256], b GHC.Types.~ Data.Map.Internal.Map (EVM.Types.Expr 'EVM.Types.EAddr) [EVM.Types.W256]) => Optics.Label.LabelOptic "txAccessList" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "value" k (EVM.Types.VMOpts t) (EVM.Types.VMOpts t) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Contract, b GHC.Types.~ EVM.Types.Contract) => Optics.Label.LabelOptic "contract" k EVM.Types.Trace EVM.Types.Trace a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Int, b GHC.Types.~ GHC.Types.Int) => Optics.Label.LabelOptic "opIx" k EVM.Types.Trace EVM.Types.Trace a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.TraceData, b GHC.Types.~ EVM.Types.TraceData) => Optics.Label.LabelOptic "tracedata" k EVM.Types.Trace EVM.Types.Trace a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract, b GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr EVM.Types.Contract) => Optics.Label.LabelOptic "fetched" k EVM.Types.Cache EVM.Types.Cache a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map (EVM.Types.CodeLocation, GHC.Types.Int) GHC.Types.Bool, b GHC.Types.~ Data.Map.Internal.Map (EVM.Types.CodeLocation, GHC.Types.Int) GHC.Types.Bool) => Optics.Label.LabelOptic "path" k EVM.Types.Cache EVM.Types.Cache a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Set.Internal.Set (EVM.Types.Expr 'EVM.Types.EAddr), b GHC.Types.~ Data.Set.Internal.Set (EVM.Types.Expr 'EVM.Types.EAddr)) => Optics.Label.LabelOptic "accessedAddresses" k EVM.Types.SubState EVM.Types.SubState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Set.Internal.Set (EVM.Types.Expr 'EVM.Types.EAddr, EVM.Types.W256), b GHC.Types.~ Data.Set.Internal.Set (EVM.Types.Expr 'EVM.Types.EAddr, EVM.Types.W256)) => Optics.Label.LabelOptic "accessedStorageKeys" k EVM.Types.SubState EVM.Types.SubState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [(EVM.Types.Expr 'EVM.Types.EAddr, GHC.Word.Word64)], b GHC.Types.~ [(EVM.Types.Expr 'EVM.Types.EAddr, GHC.Word.Word64)]) => Optics.Label.LabelOptic "refunds" k EVM.Types.SubState EVM.Types.SubState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Expr 'EVM.Types.EAddr], b GHC.Types.~ [EVM.Types.Expr 'EVM.Types.EAddr]) => Optics.Label.LabelOptic "selfdestructs" k EVM.Types.SubState EVM.Types.SubState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Expr 'EVM.Types.EAddr], b GHC.Types.~ [EVM.Types.Expr 'EVM.Types.EAddr]) => Optics.Label.LabelOptic "touchedAccounts" k EVM.Types.SubState EVM.Types.SubState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "gaslimit" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "gasprice" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "isCreate" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "origin" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "priorityFee" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.SubState, b GHC.Types.~ EVM.Types.SubState) => Optics.Label.LabelOptic "substate" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "toAddr" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map (EVM.Types.Expr 'EVM.Types.EAddr) EVM.Types.Contract, b GHC.Types.~ Data.Map.Internal.Map (EVM.Types.Expr 'EVM.Types.EAddr) EVM.Types.Contract) => Optics.Label.LabelOptic "txReversion" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "value" k EVM.Types.TxState EVM.Types.TxState a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf) => Optics.Label.LabelOptic "calldata" k (EVM.Types.FrameState t s) (EVM.Types.FrameState t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "caller" k (EVM.Types.FrameState t s) (EVM.Types.FrameState t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EWord) => Optics.Label.LabelOptic "callvalue" k (EVM.Types.FrameState t s) (EVM.Types.FrameState t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.ContractCode, b GHC.Types.~ EVM.Types.ContractCode) => Optics.Label.LabelOptic "code" k (EVM.Types.FrameState t s) (EVM.Types.FrameState t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "codeContract" k (EVM.Types.FrameState t s) (EVM.Types.FrameState t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.EAddr) => Optics.Label.LabelOptic "contract" k (EVM.Types.FrameState t s) (EVM.Types.FrameState t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Gas t1, b GHC.Types.~ EVM.Types.Gas t2) => Optics.Label.LabelOptic "gas" k (EVM.Types.FrameState t1 s) (EVM.Types.FrameState t2 s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Memory s1, b GHC.Types.~ EVM.Types.Memory s2) => Optics.Label.LabelOptic "memory" k (EVM.Types.FrameState t s1) (EVM.Types.FrameState t s2) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Word.Word64, b GHC.Types.~ GHC.Word.Word64) => Optics.Label.LabelOptic "memorySize" k (EVM.Types.FrameState t s) (EVM.Types.FrameState t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Int, b GHC.Types.~ GHC.Types.Int) => Optics.Label.LabelOptic "pc" k (EVM.Types.FrameState t s) (EVM.Types.FrameState t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Buf) => Optics.Label.LabelOptic "returndata" k (EVM.Types.FrameState t s) (EVM.Types.FrameState t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Expr 'EVM.Types.EWord], b GHC.Types.~ [EVM.Types.Expr 'EVM.Types.EWord]) => Optics.Label.LabelOptic "stack" k (EVM.Types.FrameState t s) (EVM.Types.FrameState t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "static" k (EVM.Types.FrameState t s) (EVM.Types.FrameState t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Block, b GHC.Types.~ EVM.Types.Block) => Optics.Label.LabelOptic "block" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Gas t, b GHC.Types.~ EVM.Types.Gas t) => Optics.Label.LabelOptic "burned" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Cache, b GHC.Types.~ EVM.Types.Cache) => Optics.Label.LabelOptic "cache" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.RuntimeConfig, b GHC.Types.~ EVM.Types.RuntimeConfig) => Optics.Label.LabelOptic "config" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Prop], b GHC.Types.~ [EVM.Types.Prop]) => Optics.Label.LabelOptic "constraints" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Types.Int, b GHC.Types.~ GHC.Types.Int) => Optics.Label.LabelOptic "currentFork" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.Env, b GHC.Types.~ EVM.Types.Env) => Optics.Label.LabelOptic "env" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Sequence.Internal.Seq EVM.Types.ForkState, b GHC.Types.~ Data.Sequence.Internal.Seq EVM.Types.ForkState) => Optics.Label.LabelOptic "forks" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Frame t s], b GHC.Types.~ [EVM.Types.Frame t s]) => Optics.Label.LabelOptic "frames" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Map.Internal.Map EVM.Types.CodeLocation (GHC.Types.Int, [EVM.Types.Expr 'EVM.Types.EWord]), b GHC.Types.~ Data.Map.Internal.Map EVM.Types.CodeLocation (GHC.Types.Int, [EVM.Types.Expr 'EVM.Types.EWord])) => Optics.Label.LabelOptic "iterations" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ [EVM.Types.Expr 'EVM.Types.Log], b GHC.Types.~ [EVM.Types.Expr 'EVM.Types.Log]) => Optics.Label.LabelOptic "logs" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ GHC.Maybe.Maybe (EVM.Types.VMResult t s), b GHC.Types.~ GHC.Maybe.Maybe (EVM.Types.VMResult t s)) => Optics.Label.LabelOptic "result" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.FrameState t s, b GHC.Types.~ EVM.Types.FrameState t s) => Optics.Label.LabelOptic "state" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ Data.Tree.Zipper.TreePos Data.Tree.Zipper.Empty EVM.Types.Trace, b GHC.Types.~ Data.Tree.Zipper.TreePos Data.Tree.Zipper.Empty EVM.Types.Trace) => Optics.Label.LabelOptic "traces" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance (k GHC.Types.~ Optics.Internal.Optic.Types.A_Lens, a GHC.Types.~ EVM.Types.TxState, b GHC.Types.~ EVM.Types.TxState) => Optics.Label.LabelOptic "tx" k (EVM.Types.VM t s) (EVM.Types.VM t s) a b
instance GHC.Generics.Generic EVM.Types.Word512
instance Data.Data.Data EVM.Types.Word512
instance GHC.Generics.Generic EVM.Types.Int512
instance Data.Data.Data EVM.Types.Int512
instance GHC.Show.Show EVM.Types.BranchCondition
instance GHC.Show.Show EVM.Types.BaseState
instance GHC.Base.Functor EVM.Types.GenericOp
instance GHC.Classes.Ord a => GHC.Classes.Ord (EVM.Types.GenericOp a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (EVM.Types.GenericOp a)
instance GHC.Show.Show a => GHC.Show.Show (EVM.Types.GenericOp a)
instance GHC.Real.Integral EVM.Types.FunctionSelector
instance GHC.Enum.Enum EVM.Types.FunctionSelector
instance GHC.Real.Real EVM.Types.FunctionSelector
instance GHC.Classes.Ord EVM.Types.FunctionSelector
instance GHC.Classes.Eq EVM.Types.FunctionSelector
instance GHC.Num.Num EVM.Types.FunctionSelector
instance GHC.Bits.Bits EVM.Types.FunctionSelector
instance GHC.Generics.Generic EVM.Types.ByteStringS
instance GHC.Classes.Eq EVM.Types.ByteStringS
instance GHC.Enum.Bounded EVM.Types.W256
instance GHC.Classes.Eq EVM.Types.W256
instance GHC.Enum.Enum EVM.Types.W256
instance GHC.Bits.FiniteBits EVM.Types.W256
instance GHC.Generics.Generic EVM.Types.W256
instance GHC.Bits.Bits EVM.Types.W256
instance GHC.Classes.Ord EVM.Types.W256
instance GHC.Real.Real EVM.Types.W256
instance GHC.Real.Integral EVM.Types.W256
instance GHC.Num.Num EVM.Types.W256
instance GHC.Enum.Bounded EVM.Types.W64
instance GHC.Classes.Eq EVM.Types.W64
instance GHC.Enum.Enum EVM.Types.W64
instance GHC.Bits.FiniteBits EVM.Types.W64
instance GHC.Bits.Bits EVM.Types.W64
instance GHC.Generics.Generic EVM.Types.W64
instance GHC.Classes.Ord EVM.Types.W64
instance GHC.Real.Real EVM.Types.W64
instance GHC.Real.Integral EVM.Types.W64
instance GHC.Num.Num EVM.Types.W64
instance GHC.Bits.FiniteBits EVM.Types.Addr
instance GHC.Bits.Bits EVM.Types.Addr
instance GHC.Generics.Generic EVM.Types.Addr
instance GHC.Classes.Eq EVM.Types.Addr
instance GHC.Enum.Enum EVM.Types.Addr
instance GHC.Classes.Ord EVM.Types.Addr
instance GHC.Real.Real EVM.Types.Addr
instance GHC.Real.Integral EVM.Types.Addr
instance GHC.Num.Num EVM.Types.Addr
instance GHC.Classes.Ord EVM.Types.PartialExec
instance GHC.Classes.Eq EVM.Types.PartialExec
instance GHC.Show.Show EVM.Types.PartialExec
instance GHC.Classes.Ord EVM.Types.EvmError
instance GHC.Classes.Eq EVM.Types.EvmError
instance GHC.Show.Show EVM.Types.EvmError
instance GHC.Show.Show EVM.Types.SubState
instance GHC.Classes.Ord EVM.Types.SubState
instance GHC.Classes.Eq EVM.Types.SubState
instance GHC.Classes.Ord EVM.Types.RuntimeCode
instance GHC.Classes.Eq EVM.Types.RuntimeCode
instance GHC.Show.Show EVM.Types.RuntimeCode
instance GHC.Classes.Ord EVM.Types.ContractCode
instance GHC.Classes.Eq EVM.Types.ContractCode
instance GHC.Show.Show EVM.Types.ContractCode
instance GHC.Classes.Ord EVM.Types.Contract
instance GHC.Classes.Eq EVM.Types.Contract
instance GHC.Show.Show EVM.Types.Contract
instance GHC.Generics.Generic EVM.Types.FrameContext
instance GHC.Show.Show EVM.Types.FrameContext
instance GHC.Classes.Ord EVM.Types.FrameContext
instance GHC.Classes.Eq EVM.Types.FrameContext
instance GHC.Generics.Generic EVM.Types.TraceData
instance GHC.Show.Show EVM.Types.TraceData
instance GHC.Classes.Ord EVM.Types.TraceData
instance GHC.Classes.Eq EVM.Types.TraceData
instance GHC.Generics.Generic EVM.Types.Trace
instance GHC.Show.Show EVM.Types.Trace
instance GHC.Classes.Ord EVM.Types.Trace
instance GHC.Classes.Eq EVM.Types.Trace
instance GHC.Generics.Generic EVM.Types.Traces
instance GHC.Show.Show EVM.Types.Traces
instance GHC.Classes.Ord EVM.Types.Traces
instance GHC.Classes.Eq EVM.Types.Traces
instance GHC.Generics.Generic EVM.Types.Cache
instance GHC.Show.Show EVM.Types.Cache
instance GHC.Generics.Generic EVM.Types.Block
instance GHC.Show.Show EVM.Types.Block
instance GHC.Generics.Generic EVM.Types.Env
instance GHC.Show.Show EVM.Types.Env
instance GHC.Generics.Generic EVM.Types.ForkState
instance GHC.Show.Show EVM.Types.ForkState
instance GHC.Generics.Generic (EVM.Types.FrameState t s)
instance GHC.Show.Show EVM.Types.TxState
instance GHC.Show.Show EVM.Types.RuntimeConfig
instance GHC.Generics.Generic (EVM.Types.VM t s)
instance GHC.Generics.Generic EVM.Types.Nibble
instance GHC.Enum.Bounded EVM.Types.Nibble
instance GHC.Classes.Eq EVM.Types.Nibble
instance GHC.Enum.Enum EVM.Types.Nibble
instance GHC.Classes.Ord EVM.Types.Nibble
instance GHC.Real.Real EVM.Types.Nibble
instance GHC.Real.Integral EVM.Types.Nibble
instance GHC.Num.Num EVM.Types.Nibble
instance GHC.Show.Show (EVM.Types.GVar a)
instance GHC.Classes.Eq (EVM.Types.GVar a)
instance GHC.Classes.Ord (EVM.Types.GVar a)
instance GHC.Show.Show (EVM.Types.Expr a)
instance GHC.Classes.Eq (EVM.Types.Expr a)
instance GHC.Classes.Ord (EVM.Types.Expr a)
instance GHC.Show.Show EVM.Types.SomeExpr
instance GHC.Show.Show EVM.Types.Prop
instance GHC.Show.Show (EVM.Types.Effect t s)
instance GHC.Show.Show (EVM.Types.VMResult t s)
instance GHC.Show.Show (EVM.Types.VM 'EVM.Types.Symbolic s)
instance GHC.Show.Show (EVM.Types.VM 'EVM.Types.Concrete s)
instance GHC.Show.Show (EVM.Types.Frame 'EVM.Types.Symbolic s)
instance GHC.Show.Show (EVM.Types.Frame 'EVM.Types.Concrete s)
instance GHC.Show.Show (EVM.Types.FrameState 'EVM.Types.Symbolic s)
instance GHC.Show.Show (EVM.Types.FrameState 'EVM.Types.Concrete s)
instance GHC.Show.Show (EVM.Types.VMOpts 'EVM.Types.Symbolic)
instance GHC.Show.Show (EVM.Types.VMOpts 'EVM.Types.Concrete)
instance Witch.From.From EVM.Types.Nibble GHC.Types.Int
instance GHC.Show.Show EVM.Types.Nibble
instance GHC.Show.Show (EVM.Types.Query t s)
instance GHC.Show.Show (EVM.Types.Choose s)
instance GHC.Show.Show (EVM.Types.Memory s)
instance GHC.Base.Semigroup EVM.Types.Cache
instance GHC.Base.Monoid EVM.Types.Cache
instance GHC.Classes.Eq EVM.Types.SomeExpr
instance GHC.Classes.Ord EVM.Types.SomeExpr
instance GHC.Classes.Eq EVM.Types.Prop
instance GHC.Classes.Ord EVM.Types.Prop
instance GHC.Base.Semigroup EVM.Types.Traces
instance GHC.Base.Monoid EVM.Types.Traces
instance Witch.From.From EVM.Types.Addr GHC.Num.Integer.Integer
instance Witch.From.From EVM.Types.Addr EVM.Types.W256
instance Witch.TryFrom.TryFrom GHC.Num.Integer.Integer EVM.Types.Addr
instance Witch.TryFrom.TryFrom EVM.Types.W256 EVM.Types.Addr
instance GHC.Read.Read EVM.Types.Addr
instance GHC.Show.Show EVM.Types.Addr
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Types.Addr
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Types.Addr
instance Data.Aeson.Types.ToJSON.ToJSONKey EVM.Types.Addr
instance Data.Aeson.Types.FromJSON.FromJSONKey EVM.Types.Addr
instance Options.Generic.ParseField EVM.Types.Addr
instance Options.Generic.ParseFields EVM.Types.Addr
instance Options.Generic.ParseRecord EVM.Types.Addr
instance Witch.From.From EVM.Types.W64 EVM.Types.W256
instance Witch.TryFrom.TryFrom EVM.Types.W256 EVM.Types.W64
instance GHC.Read.Read EVM.Types.W64
instance GHC.Show.Show EVM.Types.W64
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Types.W64
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Types.W64
instance Witch.From.From EVM.Types.W256 GHC.Num.Integer.Integer
instance Witch.From.From GHC.Word.Word8 EVM.Types.W256
instance Witch.From.From GHC.Word.Word32 EVM.Types.W256
instance Witch.From.From GHC.Word.Word64 EVM.Types.W256
instance Witch.From.From Data.DoubleWord.Word256 EVM.Types.W256
instance Witch.TryFrom.TryFrom GHC.Types.Int EVM.Types.W256
instance Witch.TryFrom.TryFrom Data.DoubleWord.Int256 EVM.Types.W256
instance Witch.TryFrom.TryFrom GHC.Num.Integer.Integer EVM.Types.W256
instance Witch.TryFrom.TryFrom EVM.Types.W256 EVM.Types.FunctionSelector
instance Witch.TryFrom.TryFrom EVM.Types.W256 GHC.Types.Int
instance Witch.TryFrom.TryFrom EVM.Types.W256 GHC.Int.Int64
instance Witch.TryFrom.TryFrom EVM.Types.W256 Data.DoubleWord.Int256
instance Witch.TryFrom.TryFrom EVM.Types.W256 GHC.Word.Word8
instance Witch.TryFrom.TryFrom EVM.Types.W256 GHC.Word.Word32
instance Witch.TryFrom.TryFrom EVM.Types.W256 GHC.Word.Word64
instance Witch.TryFrom.TryFrom EVM.Types.Word512 EVM.Types.W256
instance GHC.Read.Read EVM.Types.W256
instance GHC.Show.Show EVM.Types.W256
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Types.W256
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Types.W256
instance Data.Aeson.Types.FromJSON.FromJSONKey EVM.Types.W256
instance Options.Generic.ParseField EVM.Types.W256
instance Options.Generic.ParseFields EVM.Types.W256
instance Options.Generic.ParseRecord EVM.Types.W256
instance GHC.Show.Show EVM.Types.ByteStringS
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Types.ByteStringS
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Types.ByteStringS
instance GHC.Show.Show EVM.Types.FunctionSelector
instance Data.BinaryWord.BinaryWord EVM.Types.Word512
instance Data.DoubleWord.Base.DoubleWord EVM.Types.Int512
instance GHC.Classes.Eq EVM.Types.Int512
instance GHC.Classes.Ord EVM.Types.Int512
instance GHC.Enum.Bounded EVM.Types.Int512
instance GHC.Enum.Enum EVM.Types.Int512
instance GHC.Num.Num EVM.Types.Int512
instance GHC.Real.Real EVM.Types.Int512
instance GHC.Real.Integral EVM.Types.Int512
instance GHC.Show.Show EVM.Types.Int512
instance GHC.Read.Read EVM.Types.Int512
instance Data.Hashable.Class.Hashable EVM.Types.Int512
instance GHC.Ix.Ix EVM.Types.Int512
instance GHC.Bits.Bits EVM.Types.Int512
instance GHC.Bits.FiniteBits EVM.Types.Int512
instance Data.BinaryWord.BinaryWord EVM.Types.Int512
instance Data.DoubleWord.Base.DoubleWord EVM.Types.Word512
instance GHC.Classes.Eq EVM.Types.Word512
instance GHC.Classes.Ord EVM.Types.Word512
instance GHC.Enum.Bounded EVM.Types.Word512
instance GHC.Enum.Enum EVM.Types.Word512
instance GHC.Num.Num EVM.Types.Word512
instance GHC.Real.Real EVM.Types.Word512
instance GHC.Real.Integral EVM.Types.Word512
instance GHC.Show.Show EVM.Types.Word512
instance GHC.Read.Read EVM.Types.Word512
instance Data.Hashable.Class.Hashable EVM.Types.Word512
instance GHC.Ix.Ix EVM.Types.Word512
instance GHC.Bits.Bits EVM.Types.Word512
instance GHC.Bits.FiniteBits EVM.Types.Word512
instance Witch.From.From Data.DoubleWord.Int256 GHC.Num.Integer.Integer
instance Witch.From.From GHC.Word.Word8 Data.DoubleWord.Word256
instance Witch.From.From GHC.Word.Word32 Data.DoubleWord.Word256
instance Witch.From.From GHC.Word.Word32 Data.ByteString.Internal.Type.ByteString
instance Witch.From.From Data.DoubleWord.Word256 GHC.Num.Integer.Integer
instance Witch.TryFrom.TryFrom GHC.Types.Int Data.DoubleWord.Word256
instance Witch.TryFrom.TryFrom Data.DoubleWord.Word160 GHC.Word.Word8
instance Witch.TryFrom.TryFrom Data.DoubleWord.Word256 GHC.Types.Int
instance Witch.TryFrom.TryFrom Data.DoubleWord.Word256 Data.DoubleWord.Int256
instance Witch.TryFrom.TryFrom Data.DoubleWord.Word256 GHC.Word.Word8
instance Witch.TryFrom.TryFrom Data.DoubleWord.Word256 GHC.Word.Word32


module EVM.Traversals
foldProp :: forall b. Monoid b => (forall a. Expr a -> b) -> b -> Prop -> b
foldEContract :: forall b. Monoid b => (forall a. Expr a -> b) -> b -> Expr EContract -> b
foldContract :: forall b. Monoid b => (forall a. Expr a -> b) -> b -> Contract -> b
foldCode :: forall b. Monoid b => (forall a. Expr a -> b) -> ContractCode -> 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
mapProp' :: (Prop -> Prop) -> Prop -> Prop
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
mapEContractM :: Monad m => (forall a. Expr a -> m (Expr a)) -> Expr EContract -> m (Expr EContract)
mapContractM :: Monad m => (forall a. Expr a -> m (Expr a)) -> Contract -> m Contract
mapCodeM :: Monad m => (forall a. Expr a -> m (Expr a)) -> ContractCode -> m ContractCode

-- | Generic operations over AST terms
class TraversableTerm a
mapTerm :: TraversableTerm a => (forall b. Expr b -> Expr b) -> a -> a
foldTerm :: forall c. (TraversableTerm a, Monoid c) => (forall b. Expr b -> c) -> c -> a -> c
instance EVM.Traversals.TraversableTerm (EVM.Types.Expr a)
instance EVM.Traversals.TraversableTerm EVM.Types.Prop

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


-- | Helper functions for working with Expr instances. All functions here
--   will return a concrete result if given a concrete input.
module EVM.Expr
maxLit :: W256
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 expression if necessary. 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 expression will be returned.
bufLength :: Expr Buf -> Expr EWord
bufLengthEnv :: Map Int (Expr Buf) -> Bool -> Expr Buf -> Expr EWord

-- | Return the minimum possible length of a buffer. In the case of an
--   abstract buffer, it is the largest write that is made on a concrete
--   location. Parameterized by an environment for buffer variables.
minLength :: Map Int (Expr Buf) -> Expr Buf -> Maybe Integer
concretePrefix :: Expr Buf -> Vector Word8
word256At :: Expr EWord -> Lens (Expr Buf) (Expr Buf) (Expr EWord) (Expr EWord)

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

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

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

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

-- | 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 Storage -> Maybe (Expr EWord)
pattern MappingSlot :: ByteString -> Expr EWord -> Expr EWord
pattern Keccak64Bytes :: Expr EWord
pattern ArraySlotWithOffset :: ByteString -> Expr EWord -> Expr EWord
pattern ArraySlotZero :: ByteString -> Expr EWord
idsDontMatch :: ByteString -> ByteString -> Bool
slotPos :: Word8 -> ByteString

-- | Turns Literals into keccak(bytes32(id)) + offset (i.e. writes to
--   arrays)
structureArraySlots :: Expr a -> Expr a
litToArrayPreimage :: W256 -> Maybe (Word8, W256)

-- | 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 Storage -> Expr Storage
getAddr :: Expr Storage -> Maybe (Expr EAddr)
getLogicalIdx :: Expr Storage -> Maybe W256
data StorageType
SmallSlot :: StorageType
Array :: StorageType
Map :: StorageType
Mixed :: StorageType
UNK :: StorageType
safeToDecompose :: Expr a -> Bool

-- | Splits storage into logical sub-stores if (1) all SLoad-&gt;SStore*
--   chains are one of: (1a) Lit &lt; 256, (1b) MappingSlot, (1c)
--   ArraySlotWithOffset, (1d) ArraySlotZero and (2) there is no mixing of
--   different types (e.g. Map with Array) within the same SStore -&gt;
--   SLoad* chain, and (3) there is no mixing of different array/map slots.
--   
--   Mixing (2) and (3) are attempted to be prevented (if possible) as part
--   of the rewrites done by the <a>readStorage</a> function that is ran
--   before this. If there is still mixing here, we abort with a Nothing.
--   
--   We do NOT rewrite stand-alone <a>SStore</a>-s (i.e. SStores that are
--   not read), since they are often used to describe a post-state, and are
--   not dispatched as-is to the solver
decomposeStorage :: Expr a -> Maybe (Expr a)

-- | Simple recursive match based AST simplification Note: may not
--   terminate!
simplify :: Expr a -> Expr a
simplifyProps :: [Prop] -> [Prop]

-- | Evaluate the provided proposition down to its most concrete result
--   Also simplifies the inner Expr, if it exists
simplifyProp :: Prop -> Prop
flattenProps :: [Prop] -> [Prop]
remRedundantProps :: [Prop] -> [Prop]
litAddr :: Addr -> Expr EWord
exprToAddr :: Expr EWord -> Maybe Addr
wordToAddr :: Expr EWord -> Maybe (Expr EAddr)
litCode :: ByteString -> [Expr Byte]
to512 :: W256 -> Word512
isLitByte :: Expr Byte -> Bool
isLitWord :: Expr EWord -> Bool
isSuccess :: Expr End -> Bool
isFailure :: Expr End -> Bool
isPartial :: Expr End -> Bool

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

-- | Converts a list of bytes into a W256. TODO: semantics if the input is
--   too large?
bytesToW256 :: [Word8] -> W256
padBytesLeft :: Int -> [Expr Byte] -> [Expr Byte]
joinBytes :: [Expr Byte] -> Expr EWord
eqByte :: Expr Byte -> Expr Byte -> Expr EWord
min :: Expr EWord -> Expr EWord -> Expr EWord
max :: Expr EWord -> Expr EWord -> Expr EWord
numBranches :: Expr End -> Int
allLit :: [Expr Byte] -> Bool

-- | True if the given expression contains any node that satisfies the
--   input predicate
containsNode :: (forall a. Expr a -> Bool) -> Expr b -> Bool
inRange :: Int -> Expr EWord -> Prop

-- | images of keccak(bytes32(x)) where 0 &lt;= x &lt; 256
preImages :: [(W256, Word8)]
data ConstState
ConstState :: Map (Expr EWord) W256 -> Bool -> ConstState
[$sel:values:ConstState] :: ConstState -> Map (Expr EWord) W256
[$sel:canBeSat:ConstState] :: ConstState -> Bool

-- | Folds constants
constFoldProp :: [Prop] -> Bool
concKeccakSimpExpr :: Expr a -> Expr a
concKeccakProps :: [Prop] -> [Prop]
concKeccakOnePass :: Expr a -> Expr a
instance GHC.Classes.Eq EVM.Expr.StorageType
instance GHC.Show.Show EVM.Expr.StorageType
instance GHC.Show.Show EVM.Expr.ConstState
instance GHC.Base.Semigroup (EVM.Types.Expr 'EVM.Types.Buf)
instance GHC.Base.Monoid (EVM.Types.Expr 'EVM.Types.Buf)

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


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

module EVM.Concrete
byteStringSliceWithDefaultZeroes :: Int -> Int -> ByteString -> ByteString
sliceMemory :: W256 -> W256 -> ByteString -> ByteString
writeMemory :: ByteString -> W256 -> W256 -> W256 -> ByteString -> ByteString
createAddress :: Addr -> W64 -> Expr EAddr
create2Address :: Addr -> W256 -> ByteString -> Expr EAddr


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.Assembler
assemble :: [Op] -> Vector (Expr Byte)

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

-- | A method name, and the (ordered) types of it's arguments
data Sig
Sig :: Text -> [AbiType] -> Sig
putAbi :: AbiValue -> Put
getAbi :: AbiType -> Get AbiValue

-- | Decode a sequence type (e.g. tuple / array). Will fail for non
--   sequence types
getAbiSeq :: Int -> [AbiType] -> Get (Vector AbiValue)
genAbiValue :: AbiType -> Gen AbiValue
abiValueType :: AbiValue -> AbiType
abiTypeSolidity :: AbiType -> Text
abiMethod :: Text -> AbiValue -> ByteString
emptyAbi :: AbiValue
encodeAbiValue :: AbiValue -> ByteString
decodeAbiValue :: AbiType -> ByteString -> AbiValue
decodeBuf :: [AbiType] -> Expr Buf -> AbiVals
decodeStaticArgs :: Int -> Int -> Expr Buf -> [Expr EWord]
formatString :: ByteString -> String
parseTypeName :: Vector AbiType -> Text -> Maybe AbiType
makeAbiValue :: AbiType -> String -> AbiValue
parseAbiValue :: AbiType -> ReadP AbiValue
selector :: Text -> ByteString
instance Data.Data.Data EVM.ABI.AbiType
instance GHC.Generics.Generic EVM.ABI.AbiType
instance GHC.Classes.Ord EVM.ABI.AbiType
instance GHC.Classes.Eq EVM.ABI.AbiType
instance GHC.Read.Read EVM.ABI.AbiType
instance GHC.Generics.Generic EVM.ABI.AbiValue
instance GHC.Classes.Ord EVM.ABI.AbiValue
instance GHC.Classes.Eq EVM.ABI.AbiValue
instance GHC.Read.Read EVM.ABI.AbiValue
instance GHC.Classes.Eq EVM.ABI.Sig
instance GHC.Show.Show EVM.ABI.Sig
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 :: MonadUnliftIO m => Text -> Text -> m (Maybe ByteString)
solcRuntime :: MonadUnliftIO m => Text -> Text -> m (Maybe ByteString)
yul :: Text -> Text -> IO (Maybe ByteString)
yulRuntime :: Text -> Text -> IO (Maybe ByteString)
data JumpType
JumpInto :: JumpType
JumpFrom :: JumpType
JumpRegular :: JumpType
data SolcContract
SolcContract :: W256 -> W256 -> ByteString -> ByteString -> Text -> [(Text, AbiType)] -> Map FunctionSelector Method -> Map W256 Event -> Map W256 SolError -> Map W256 [Reference] -> Maybe (Map Text StorageItem) -> Seq SrcMap -> Seq SrcMap -> SolcContract
[$sel:runtimeCodehash:SolcContract] :: SolcContract -> W256
[$sel:creationCodehash:SolcContract] :: SolcContract -> W256
[$sel:runtimeCode:SolcContract] :: SolcContract -> ByteString
[$sel:creationCode:SolcContract] :: SolcContract -> ByteString
[$sel:contractName:SolcContract] :: SolcContract -> Text
[$sel:constructorInputs:SolcContract] :: SolcContract -> [(Text, AbiType)]
[$sel:abiMap:SolcContract] :: SolcContract -> Map FunctionSelector Method
[$sel:eventMap:SolcContract] :: SolcContract -> Map W256 Event
[$sel:errorMap:SolcContract] :: SolcContract -> Map W256 SolError
[$sel:immutableReferences:SolcContract] :: SolcContract -> Map W256 [Reference]
[$sel:storageLayout:SolcContract] :: SolcContract -> Maybe (Map Text StorageItem)
[$sel:runtimeSrcmap:SolcContract] :: SolcContract -> Seq SrcMap
[$sel:creationSrcmap:SolcContract] :: SolcContract -> Seq SrcMap

-- | A mapping from contract identifiers (filepath:name) to a SolcContract
--   object
newtype Contracts
Contracts :: Map Text SolcContract -> Contracts

-- | The various project types understood by hevm
data ProjectType
DappTools :: ProjectType
CombinedJSON :: ProjectType
Foundry :: ProjectType
FoundryStdLib :: ProjectType
data BuildOutput
BuildOutput :: Contracts -> SourceCache -> BuildOutput
[$sel:contracts:BuildOutput] :: BuildOutput -> Contracts
[$sel:sources:BuildOutput] :: BuildOutput -> SourceCache
data StorageItem
StorageItem :: SlotType -> Int -> Int -> StorageItem
[$sel:slotType:StorageItem] :: StorageItem -> SlotType
[$sel:offset:StorageItem] :: StorageItem -> Int
[$sel:slot:StorageItem] :: StorageItem -> Int
data SourceCache
SourceCache :: Map Int (FilePath, ByteString) -> Map Int (Vector ByteString) -> Map Text Value -> SourceCache
[$sel:files:SourceCache] :: SourceCache -> Map Int (FilePath, ByteString)
[$sel:lines:SourceCache] :: SourceCache -> Map Int (Vector ByteString)
[$sel:asts:SourceCache] :: SourceCache -> Map Text Value
data SrcMap
SM :: {-# UNPACK #-} !Int -> {-# UNPACK #-} !Int -> {-# UNPACK #-} !Int -> JumpType -> {-# UNPACK #-} !Int -> SrcMap
[$sel:offset:SM] :: SrcMap -> {-# UNPACK #-} !Int
[$sel:length:SM] :: SrcMap -> {-# UNPACK #-} !Int
[$sel:file:SM] :: SrcMap -> {-# UNPACK #-} !Int
[$sel:jump:SM] :: SrcMap -> JumpType
[$sel:modifierDepth:SM] :: SrcMap -> {-# UNPACK #-} !Int
data CodeType
Creation :: CodeType
Runtime :: CodeType
data Method
Method :: [(Text, AbiType)] -> [(Text, AbiType)] -> Text -> Text -> Mutability -> Method
[$sel:output:Method] :: Method -> [(Text, AbiType)]
[$sel:inputs:Method] :: Method -> [(Text, AbiType)]
[$sel:name:Method] :: Method -> Text
[$sel:methodSignature:Method] :: Method -> Text
[$sel:mutability:Method] :: Method -> Mutability
data SlotType
StorageMapping :: NonEmpty AbiType -> AbiType -> SlotType
StorageValue :: AbiType -> SlotType
data Reference
Reference :: Int -> Int -> Reference
[$sel:start:Reference] :: Reference -> Int
[$sel:length:Reference] :: Reference -> Int
data Mutability

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

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

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

-- | function accepts Ether
Payable :: Mutability

-- | Reads all solc output json files found under the provided filepath and
--   returns them merged into a BuildOutput
readBuildOutput :: FilePath -> ProjectType -> IO (Either String BuildOutput)
functionAbi :: Text -> IO Method
makeSrcMaps :: Text -> Maybe (Seq SrcMap)
readSolc :: ProjectType -> FilePath -> FilePath -> IO (Either String BuildOutput)
readJSON :: ProjectType -> Text -> Text -> Maybe (Contracts, Asts, Sources)

-- | Parses the standard json output from solc
readStdJSON :: Text -> Maybe (Contracts, Asts, Sources)

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

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


module EVM.Sign
deriveAddr :: Integer -> Maybe Addr
sign :: W256 -> Integer -> (Word8, W256, W256)

-- | We don't want to introduce the machinery needed to sign with a random
--   nonce, so we just use the same nonce every time (420). This is
--   obviously very insecure, but fine for testing purposes.
ethsign :: PrivateKey -> Digest Keccak_256 -> Signature
ecrec :: W256 -> W256 -> W256 -> W256 -> Maybe Addr

module EVM.Dapp
data DappInfo
DappInfo :: FilePath -> Map Text SolcContract -> Map W256 (CodeType, SolcContract) -> [(Code, SolcContract)] -> SourceCache -> [(Text, [Sig])] -> Map FunctionSelector Method -> Map W256 Event -> Map W256 SolError -> Map Int Value -> (SrcMap -> Maybe Value) -> DappInfo
[$sel:root:DappInfo] :: DappInfo -> FilePath
[$sel:solcByName:DappInfo] :: DappInfo -> Map Text SolcContract
[$sel:solcByHash:DappInfo] :: DappInfo -> Map W256 (CodeType, SolcContract)
[$sel:solcByCode:DappInfo] :: DappInfo -> [(Code, SolcContract)]
[$sel:sources:DappInfo] :: DappInfo -> SourceCache
[$sel:unitTests:DappInfo] :: DappInfo -> [(Text, [Sig])]
[$sel:abiMap:DappInfo] :: DappInfo -> Map FunctionSelector Method
[$sel:eventMap:DappInfo] :: DappInfo -> Map W256 Event
[$sel:errorMap:DappInfo] :: DappInfo -> Map W256 SolError
[$sel:astIdMap:DappInfo] :: DappInfo -> Map Int Value
[$sel:astSrcMap:DappInfo] :: DappInfo -> SrcMap -> Maybe Value

-- | bytecode modulo immutables, to identify contracts
data Code
Code :: ByteString -> [Reference] -> Code
[$sel:raw:Code] :: Code -> ByteString
[$sel:immutableLocations:Code] :: Code -> [Reference]
data DappContext
DappContext :: DappInfo -> Map (Expr EAddr) Contract -> DappContext
[$sel:info:DappContext] :: DappContext -> DappInfo
[$sel:env:DappContext] :: DappContext -> Map (Expr EAddr) Contract
dappInfo :: FilePath -> BuildOutput -> DappInfo
emptyDapp :: DappInfo
unitTestMarkerAbi :: FunctionSelector
findAllUnitTests :: [SolcContract] -> [(Text, [Sig])]
mkSig :: Method -> Maybe Sig
findUnitTests :: Text -> [SolcContract] -> [(Text, [Sig])]
unitTestMethodsFiltered :: (Text -> Bool) -> SolcContract -> [Sig]
unitTestMethods :: SolcContract -> [Sig]
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
srcMapCodePos :: SourceCache -> SrcMap -> Maybe (FilePath, Int)
srcMapCode :: SourceCache -> SrcMap -> Maybe ByteString
instance GHC.Show.Show EVM.Dapp.Code

module EVM
blankState :: VMOps t => ST s (FrameState t s)

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

-- | Initialize an abstract contract with unknown code
unknownContract :: Expr EAddr -> Contract

-- | Initialize an abstract contract with known code
abstractContract :: ContractCode -> Expr EAddr -> Contract

-- | Initialize an empty contract without code
emptyContract :: Contract

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

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

-- | Executes the EVM one step
exec1 :: forall (t :: VMType) s. VMOps t => EVM t s ()
transfer :: VMOps t => Expr EAddr -> Expr EAddr -> Expr EWord -> EVM t s ()

-- | Checks a *CALL for failure; OOG, too many callframes, memory access
--   etc.
callChecks :: forall (t :: VMType) s. (?op :: Word8, VMOps t) => Contract -> Gas t -> Expr EAddr -> Expr EAddr -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr EWord] -> (Gas t -> EVM t s ()) -> EVM t s ()
precompiledContract :: (?op :: Word8, VMOps t) => Contract -> Gas t -> Addr -> Addr -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr EWord] -> EVM t s ()
executePrecompile :: (?op :: Word8, VMOps t) => Addr -> Gas t -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr EWord] -> EVM t s ()
truncpadlit :: Int -> ByteString -> ByteString
lazySlice :: W256 -> W256 -> ByteString -> ByteString
parseModexpLength :: ByteString -> (W256, W256, W256)
isZero :: W256 -> W256 -> ByteString -> Bool
asInteger :: ByteString -> Integer
noop :: Monad m => m ()
pushTo :: MonadState s m => Lens s s [a] [a] -> a -> m ()
pushToSequence :: MonadState s m => Setter s s (Seq a) (Seq a) -> a -> m ()
getCodeLocation :: VM t s -> CodeLocation
query :: Query t s -> EVM t s ()
choose :: Choose s -> EVM Symbolic s ()

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

-- | Loads the selected contract as the current contract to execute
loadContract :: Expr EAddr -> State (VM t s) ()
limitStack :: VMOps t => Int -> EVM (t :: VMType) s () -> EVM t s ()
notStatic :: VMOps t => EVM t s () -> EVM t s ()
forceAddr :: VMOps t => Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s ()
forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()
forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()
forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s ()
forceConcrete2 :: VMOps t => (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s ()
forceConcreteBuf :: VMOps t => Expr Buf -> String -> (ByteString -> EVM t s ()) -> EVM t s ()
refund :: Word64 -> EVM t s ()
unRefund :: Word64 -> EVM t s ()
touchAccount :: Expr EAddr -> EVM t s ()
selfdestruct :: Expr EAddr -> EVM t s ()
accessAndBurn :: VMOps t => Expr EAddr -> EVM t s () -> EVM t s ()

-- | 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 :: Expr EAddr -> EVM t s 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 :: Expr EAddr -> Expr EWord -> EVM t s Bool
cheatCode :: Expr EAddr
cheat :: (?op :: Word8, VMOps t) => (Expr EWord, Expr EWord) -> (Expr EWord, Expr EWord) -> EVM t s ()
type CheatAction t s = Expr EWord -> Expr EWord -> Expr Buf -> EVM t s ()
cheatActions :: VMOps t => Map FunctionSelector (CheatAction t s)
delegateCall :: (VMOps t, ?op :: Word8) => Contract -> Gas t -> Expr EAddr -> Expr EAddr -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr EWord] -> (Expr EAddr -> EVM t s ()) -> EVM t s ()
collision :: Maybe Contract -> Bool
create :: forall t s. (?op :: Word8, VMOps t) => Expr EAddr -> Contract -> Expr EWord -> Gas t -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM t s ()

-- | Parses a raw Buf into an InitCode
--   
--   solidity implements constructor args by appending them to the end of
--   the initcode. we support this internally by treating initCode as a
--   concrete region (initCode) followed by a potentially symbolic region
--   (arguments).
--   
--   when constructing a contract that has symbolic constructor args, we
--   need to apply some heuristics to convert the (unstructured) initcode
--   in memory into this structured representation. The (unsound, bad,
--   hacky) way that we do this, is by: looking for the first potentially
--   symbolic byte in the input buffer and then splitting it there into
--   code / data.
parseInitCode :: Expr Buf -> Maybe ContractCode

-- | Replace a contract's code, like when CREATE returns from the
--   constructor code.
replaceCode :: Expr EAddr -> ContractCode -> EVM t s ()
replaceCodeOfSelf :: ContractCode -> EVM t s ()
resetState :: VMOps t => EVM t s ()
vmError :: VMOps t => EvmError -> EVM t s ()
wrap :: Typeable a => [Expr a] -> [SomeExpr]
underrun :: VMOps t => EVM t s ()

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

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

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

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

-- | This function defines how to pop the current stack frame in either of
--   the ways specified by <a>FrameResult</a>.
--   
--   It also handles the case when the current stack frame is the only one;
--   in this case, we set the final <tt>_result</tt> of the VM execution.
finishFrame :: VMOps t => FrameResult -> EVM t s ()
accessUnboundedMemoryRange :: VMOps t => Word64 -> Word64 -> EVM t s () -> EVM t s ()
accessMemoryRange :: VMOps t => Expr EWord -> Expr EWord -> EVM t s () -> EVM t s ()
accessMemoryWord :: VMOps t => Expr EWord -> EVM t s () -> EVM t s ()
copyBytesToMemory :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM t s ()
copyCallBytesToMemory :: Expr Buf -> Expr EWord -> Expr EWord -> EVM t s ()
readMemory :: Expr EWord -> Expr EWord -> EVM t s (Expr Buf)
withTraceLocation :: TraceData -> EVM t s Trace
pushTrace :: TraceData -> EVM t s ()
insertTrace :: TraceData -> EVM t s ()
popTrace :: EVM t s ()
zipperRootForest :: TreePos Empty a -> Forest a
traceForest :: VM t s -> Forest Trace
traceForest' :: Expr End -> Forest Trace
traceContext :: Expr End -> Map (Expr EAddr) Contract
traceTopLog :: [Expr Log] -> EVM t s ()
push :: W256 -> EVM t s ()
pushSym :: Expr EWord -> EVM t s ()
pushAddr :: Expr EAddr -> EVM t s ()
stackOp1 :: (?op :: Word8, VMOps t) => Word64 -> (Expr EWord -> Expr EWord) -> EVM t s ()
stackOp2 :: (?op :: Word8, VMOps t) => Word64 -> (Expr EWord -> Expr EWord -> Expr EWord) -> EVM t s ()
stackOp3 :: (?op :: Word8, VMOps t) => Word64 -> (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord) -> EVM t s ()
checkJump :: VMOps t => Int -> [Expr EWord] -> EVM t s ()
noJumpIntoInitData :: VMOps t => Int -> EVM t s () -> EVM t s ()
isValidJumpDest :: VM t s -> Int -> Bool
opSize :: Word8 -> Int
mkOpIxMap :: ContractCode -> Vector Int
vmOp :: VM t s -> Maybe Op
vmOpIx :: VM t s -> Maybe Int
mkCodeOps :: ContractCode -> Vector (Int, Op)
concreteModexpGasFee :: ByteString -> Word64
costOfPrecompile :: FeeSchedule Word64 -> Addr -> Expr Buf -> Word64
memoryCost :: FeeSchedule Word64 -> Word64 -> Word64
hashcode :: ContractCode -> Expr EWord

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

-- | The length of the code including any constructor args. This can return
--   an abstract value
codelen :: ContractCode -> Expr EWord
toBuf :: ContractCode -> Maybe (Expr Buf)
codeloc :: EVM t s CodeLocation
createAddress :: Expr EAddr -> Maybe W64 -> EVM t s (Expr EAddr)
create2Address :: Expr EAddr -> W256 -> ByteString -> EVM t s (Expr EAddr)
freshSymAddr :: EVM t s (Expr EAddr)
isPrecompileAddr :: Expr EAddr -> Bool
ceilDiv :: (Num a, Integral a) => a -> a -> a
allButOne64th :: (Num a, Integral a) => a -> a
log2 :: FiniteBits b => b -> Int
writeMemory :: MutableMemory s -> Int -> ByteString -> EVM t s ()
freezeMemory :: MutableMemory s -> EVM t s (Expr Buf)
symbolify :: VM Concrete s -> VM Symbolic s
symbolifyFrameState :: FrameState Concrete s -> FrameState Symbolic s
symbolifyFrame :: Frame Concrete s -> Frame Symbolic s
symbolifyResult :: VMResult Concrete s -> VMResult Symbolic s
forceLit :: Expr EWord -> W256
burn :: VMOps t => Word64 -> EVM t s () -> EVM t s ()
instance GHC.Show.Show EVM.FrameResult
instance EVM.Types.VMOps 'EVM.Types.Symbolic
instance EVM.Types.VMOps 'EVM.Types.Concrete

module EVM.Format
formatExpr :: Expr a -> Text
formatSomeExpr :: SomeExpr -> Text
formatPartial :: PartialExec -> Text
formatProp :: Prop -> 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 t s -> Text
showTraceTree' :: DappInfo -> Expr End -> Text
showValues :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
prettyvmresult :: Expr End -> String
showCall :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
showWordExact :: Integral i => i -> Text
showWordExplanation :: W256 -> DappInfo -> Text
parenthesise :: [Text] -> Text
showValue :: (?context :: DappContext) => AbiType -> Expr Buf -> Text
textValues :: (?context :: DappContext) => [AbiType] -> Expr Buf -> [Text]
showAbiValue :: (?context :: DappContext) => AbiValue -> Text
prettyIfConcreteWord :: Expr EWord -> Text
formatBytes :: ByteString -> Text
formatBinary :: ByteString -> Text
indent :: Int -> Text -> Text
strip0x :: ByteString -> ByteString
strip0x' :: String -> String
hexByteString :: String -> ByteString -> ByteString
hexText :: Text -> ByteString
bsToHex :: ByteString -> String
showVal :: AbiValue -> Text
instance GHC.Show.Show EVM.Format.Signedness

module EVM.Transaction
data AccessListEntry
AccessListEntry :: Addr -> [W256] -> AccessListEntry
[$sel:address:AccessListEntry] :: AccessListEntry -> Addr
[$sel:storageKeys:AccessListEntry] :: AccessListEntry -> [W256]
data TxType
LegacyTransaction :: TxType
AccessListTransaction :: TxType
EIP1559Transaction :: TxType
data Transaction
Transaction :: ByteString -> Word64 -> Maybe W256 -> W256 -> W256 -> W256 -> Maybe Addr -> W256 -> W256 -> TxType -> [AccessListEntry] -> Maybe W256 -> Maybe W256 -> W256 -> Transaction
[$sel:txdata:Transaction] :: Transaction -> ByteString
[$sel:gasLimit:Transaction] :: Transaction -> Word64
[$sel:gasPrice:Transaction] :: Transaction -> Maybe W256
[$sel:nonce:Transaction] :: Transaction -> W256
[$sel:r:Transaction] :: Transaction -> W256
[$sel:s:Transaction] :: Transaction -> W256
[$sel:toAddr:Transaction] :: Transaction -> Maybe Addr
[$sel:v:Transaction] :: Transaction -> W256
[$sel:value:Transaction] :: Transaction -> W256
[$sel:txtype:Transaction] :: Transaction -> TxType
[$sel:accessList:Transaction] :: Transaction -> [AccessListEntry]
[$sel:maxPriorityFeeGas:Transaction] :: Transaction -> Maybe W256
[$sel:maxFeePerGas:Transaction] :: Transaction -> Maybe W256
[$sel:chainId:Transaction] :: Transaction -> W256
emptyTransaction :: Transaction

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

-- | Increments origin nonce and pays gas deposit
setupTx :: Expr EAddr -> Expr EAddr -> W256 -> Word64 -> Map (Expr EAddr) Contract -> Map (Expr EAddr) 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 t s -> VM t s
instance GHC.Generics.Generic EVM.Transaction.AccessListEntry
instance GHC.Show.Show EVM.Transaction.AccessListEntry
instance GHC.Generics.Generic EVM.Transaction.TxType
instance GHC.Classes.Eq EVM.Transaction.TxType
instance GHC.Show.Show EVM.Transaction.TxType
instance GHC.Generics.Generic EVM.Transaction.Transaction
instance GHC.Show.Show EVM.Transaction.Transaction
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Transaction.Transaction
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Transaction.Transaction
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Transaction.TxType
instance Data.Aeson.Types.ToJSON.ToJSON EVM.Transaction.AccessListEntry
instance Data.Aeson.Types.FromJSON.FromJSON EVM.Transaction.AccessListEntry

module EVM.Exec
ethrunAddress :: Addr
vmForEthrunCreation :: VMOps t => ByteString -> ST s (VM t s)
exec :: VMOps t => EVM t s (VMResult t s)
run :: VMOps t => EVM t s (VM t s)
execWhile :: (VM t s -> Bool) -> State (VM t s) Int


-- | This module contains custom app specific mtl style effects for hevm
--   These are written in the style of the ReaderT over IO pattern [1].
--   Right now we only have a single <a>ReadConfig</a> effect, but over
--   time hope to migrate most usages of IO into custom effects here.
--   
--   This framework would allow us to have multiple interpretations for
--   effects (e.g. a pure version for tests), but for now we interpret
--   everything in IO only.
--   
--   <ul>
--   <li><i>1</i>
--   <a>https://www.fpcomplete.com/blog/readert-design-pattern/</a></li>
--   </ul>
module EVM.Effects
class Monad m => ReadConfig m
readConfig :: ReadConfig m => m Config
data Config
Config :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Integer -> Bool -> Config
[$sel:dumpQueries:Config] :: Config -> Bool
[$sel:dumpExprs:Config] :: Config -> Bool
[$sel:dumpEndStates:Config] :: Config -> Bool
[$sel:debug:Config] :: Config -> Bool
[$sel:abstRefineArith:Config] :: Config -> Bool
[$sel:abstRefineMem:Config] :: Config -> Bool
[$sel:dumpTrace:Config] :: Config -> Bool
[$sel:numCexFuzz:Config] :: Config -> Integer
[$sel:onlyCexFuzz:Config] :: Config -> Bool
defaultConfig :: Config
class Monad m => TTY m
writeOutput :: TTY m => Text -> m ()
writeErr :: TTY m => Text -> m ()
writeTraceDapp :: App m => DappInfo -> VM t RealWorld -> m ()
writeTrace :: App m => VM t RealWorld -> m ()
newtype Env
Env :: Config -> Env
[$sel:config:Env] :: Env -> Config
defaultEnv :: Env
runEnv :: Env -> ReaderT Env m a -> m a
type App m = (MonadUnliftIO m, ReadConfig m, TTY m)
runApp :: ReaderT Env m a -> m a
instance GHC.Classes.Eq EVM.Effects.Config
instance GHC.Show.Show EVM.Effects.Config
instance GHC.Base.Monad m => EVM.Effects.ReadConfig (Control.Monad.Trans.Reader.ReaderT EVM.Effects.Env m)
instance (GHC.Base.Monad m, Control.Monad.IO.Class.MonadIO m) => EVM.Effects.TTY (Control.Monad.Trans.Reader.ReaderT EVM.Effects.Env m)


module EVM.SMT

-- | Data that we need to construct a nice counterexample
data CexVars
CexVars :: [Text] -> [Text] -> Map Text (Expr EWord) -> Map (Expr EAddr, Maybe W256) (Set (Expr EWord)) -> [Text] -> [Text] -> CexVars

-- | variable names that we need models for to reconstruct calldata
[$sel:calldata:CexVars] :: CexVars -> [Text]

-- | symbolic address names
[$sel:addrs:CexVars] :: CexVars -> [Text]

-- | buffer names and guesses at their maximum size
[$sel:buffers:CexVars] :: CexVars -> Map Text (Expr EWord)

-- | reads from abstract storage
[$sel:storeReads:CexVars] :: CexVars -> Map (Expr EAddr, Maybe W256) (Set (Expr EWord))

-- | the names of any block context variables
[$sel:blockContext:CexVars] :: CexVars -> [Text]

-- | the names of any tx context variables
[$sel:txContext:CexVars] :: CexVars -> [Text]

-- | A model for a buffer, either in it's compressed form (for storing
--   parsed models from a solver), or as a bytestring (for presentation to
--   users)
data BufModel
Comp :: CompressedBuf -> BufModel
Flat :: ByteString -> BufModel

-- | This representation lets us store buffers of arbitrary length without
--   exhausting the available memory, it closely matches the format used by
--   smt-lib when returning models for arrays
data CompressedBuf
Base :: Word8 -> W256 -> CompressedBuf
[$sel:byte:Base] :: CompressedBuf -> Word8
[$sel:length:Base] :: CompressedBuf -> W256
Write :: Word8 -> W256 -> CompressedBuf -> CompressedBuf
[$sel:byte:Base] :: CompressedBuf -> Word8
[$sel:idx:Base] :: CompressedBuf -> W256
[$sel:next:Base] :: CompressedBuf -> CompressedBuf

-- | a final post shrinking cex, buffers here are all represented as
--   concrete bytestrings
data SMTCex
SMTCex :: Map (Expr EWord) W256 -> Map (Expr EAddr) Addr -> Map (Expr Buf) BufModel -> Map (Expr EAddr) (Map W256 W256) -> Map (Expr EWord) W256 -> Map (Expr EWord) W256 -> SMTCex
[$sel:vars:SMTCex] :: SMTCex -> Map (Expr EWord) W256
[$sel:addrs:SMTCex] :: SMTCex -> Map (Expr EAddr) Addr
[$sel:buffers:SMTCex] :: SMTCex -> Map (Expr Buf) BufModel
[$sel:store:SMTCex] :: SMTCex -> Map (Expr EAddr) (Map W256 W256)
[$sel:blockContext:SMTCex] :: SMTCex -> Map (Expr EWord) W256
[$sel:txContext:SMTCex] :: SMTCex -> Map (Expr EWord) W256

-- | Used for abstraction-refinement of the SMT formula. Contains
--   assertions that make our query fully precise. These will be added to
--   the assertion stack if we get <tt>sat</tt> with the abstracted query.
data RefinementEqs
RefinementEqs :: [Builder] -> [Prop] -> RefinementEqs
flattenBufs :: SMTCex -> Maybe SMTCex

-- | Attempts to collapse a compressed buffer representation down to a
--   flattened one
collapse :: BufModel -> Maybe BufModel
getVar :: SMTCex -> Text -> W256
data SMT2
SMT2 :: [Builder] -> RefinementEqs -> CexVars -> [Prop] -> SMT2
formatSMT2 :: SMT2 -> Text

-- | Reads all intermediate variables from the builder state and produces
--   SMT declaring them as constants
declareIntermediates :: BufEnv -> StoreEnv -> SMT2
data AbstState
AbstState :: Map (Expr EWord) Int -> Int -> AbstState
[$sel:words:AbstState] :: AbstState -> Map (Expr EWord) Int
[$sel:count:AbstState] :: AbstState -> Int
abstractAwayProps :: Config -> [Prop] -> ([Prop], AbstState)
smt2Line :: Builder -> SMT2
assertProps :: Config -> [Prop] -> SMT2
assertPropsNoSimp :: Config -> [Prop] -> SMT2
referencedAbstractStores :: TraversableTerm a => a -> Set Builder
referencedWAddrs :: TraversableTerm a => a -> Set Builder
referencedBufs :: TraversableTerm a => a -> [Builder]
referencedVars :: TraversableTerm a => a -> [Builder]
referencedFrameContext :: TraversableTerm a => a -> [(Builder, [Prop])]
referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])]

-- | This function overapproximates the reads from the abstract storage.
--   Potentially, it can return locations that do not read a slot directly
--   from the abstract store but from subsequent writes on the store (e.g,
--   SLoad addr idx (SStore addr idx val AbstractStore)). However, we
--   expect that most of such reads will have been simplified away.
findStorageReads :: Prop -> Map (Expr EAddr, Maybe W256) (Set (Expr EWord))
findBufferAccess :: TraversableTerm a => [a] -> [(Expr EWord, Expr EWord, Expr Buf)]

-- | Asserts that buffer reads beyond the size of the buffer are equal to
--   zero. Looks for buffer reads in the a list of given predicates and the
--   buffer and storage environments.
assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop]

-- | Finds the maximum read index for each abstract buffer in the input
--   props
discoverMaxReads :: [Prop] -> BufEnv -> StoreEnv -> Map Text (Expr EWord)

-- | Returns an SMT2 object with all buffers referenced from the input
--   props declared, and with the appropriate cex extraction metadata
--   attached
declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2
declareVars :: [Builder] -> SMT2
declareAddrs :: [Builder] -> SMT2
declareFrameContext :: [(Builder, [Prop])] -> SMT2
declareAbstractStores :: [Builder] -> SMT2
declareBlockContext :: [(Builder, [Prop])] -> SMT2
prelude :: SMT2
exprToSMT :: Expr a -> Builder
sp :: Builder -> Builder -> Builder
zero :: Builder
one :: Builder
propToSMT :: Prop -> Builder

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

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

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

-- | Concatenates a list of bytes into a larger bitvector
writeBytes :: ByteString -> Expr Buf -> Builder
encodeConcreteStore :: Map W256 W256 -> Builder
storeName :: Expr EAddr -> Maybe W256 -> Builder
formatEAddr :: Expr EAddr -> Builder
parseAddr :: SpecConstant -> Addr
parseW256 :: SpecConstant -> W256
parseInteger :: SpecConstant -> Integer
parseW8 :: SpecConstant -> Word8
parseSC :: (Num a, Eq a) => SpecConstant -> a
parseErr :: Show a => a -> b
parseVar :: Text -> Expr EWord
parseEAddr :: Text -> Expr EAddr
parseBlockCtx :: Text -> Expr EWord
parseTxCtx :: Text -> Expr EWord
getAddrs :: (Text -> Expr EAddr) -> (Text -> IO Text) -> [Text] -> IO (Map (Expr EAddr) Addr)
getVars :: (Text -> Expr EWord) -> (Text -> IO Text) -> [Text] -> IO (Map (Expr EWord) W256)
getOne :: (SpecConstant -> a) -> (Text -> IO Text) -> Map Text a -> Text -> IO (Map Text a)

-- | Queries the solver for models for each of the expressions representing
--   the max read index for a given buffer
queryMaxReads :: (Text -> IO Text) -> Map Text (Expr EWord) -> IO (Map Text W256)

-- | Gets the initial model for each buffer, these will often be much too
--   large for our purposes
getBufs :: (Text -> IO Text) -> [Text] -> IO (Map (Expr Buf) BufModel)

-- | Takes a Map containing all reads from a store with an abstract base,
--   as well as the concrete part of the storage prestate and returns a
--   fully concretized storage
getStore :: (Text -> IO Text) -> Map (Expr EAddr, Maybe W256) (Set (Expr EWord)) -> IO (Map (Expr EAddr) (Map W256 W256))

-- | Ask the solver to give us the concrete value of an arbitrary abstract
--   word
queryValue :: (Text -> IO Text) -> Expr EWord -> IO W256

-- | Interpret an N-dimensional array as a value of type a. Parameterized
--   by an interpretation function for array values.
interpretNDArray :: (Map Symbol Term -> Term -> a) -> Map Symbol Term -> Term -> W256 -> a

-- | Interpret an 1-dimensional array as a function
interpret1DArray :: Map Symbol Term -> Term -> W256 -> W256
instance GHC.Show.Show EVM.SMT.CexVars
instance GHC.Classes.Eq EVM.SMT.CexVars
instance GHC.Show.Show EVM.SMT.CompressedBuf
instance GHC.Classes.Eq EVM.SMT.CompressedBuf
instance GHC.Show.Show EVM.SMT.BufModel
instance GHC.Classes.Eq EVM.SMT.BufModel
instance GHC.Show.Show EVM.SMT.SMTCex
instance GHC.Classes.Eq EVM.SMT.SMTCex
instance GHC.Show.Show EVM.SMT.RefinementEqs
instance GHC.Classes.Eq EVM.SMT.RefinementEqs
instance GHC.Show.Show EVM.SMT.SMT2
instance GHC.Classes.Eq EVM.SMT.SMT2
instance GHC.Show.Show EVM.SMT.AbstState
instance GHC.Base.Semigroup EVM.SMT.SMT2
instance GHC.Base.Monoid EVM.SMT.SMT2
instance GHC.Base.Semigroup EVM.SMT.RefinementEqs
instance GHC.Base.Monoid EVM.SMT.RefinementEqs
instance GHC.Base.Semigroup EVM.SMT.CexVars
instance GHC.Base.Monoid EVM.SMT.CexVars


module EVM.Fuzz
tryCexFuzz :: [Prop] -> Integer -> Maybe SMTCex
filterCorrectKeccak :: [Prop] -> [Prop]
substituteEWord :: Map (Expr EWord) W256 -> Prop -> Prop
substituteBuf :: Map (Expr Buf) BufModel -> Prop -> Prop
substituteStores :: Map (Expr 'EAddr) (Map W256 W256) -> Prop -> Prop
data CollectVars
CollectVars :: Set (Expr EWord) -> Set W256 -> CollectVars
[$sel:vars:CollectVars] :: CollectVars -> Set (Expr EWord)
[$sel:vals:CollectVars] :: CollectVars -> Set W256
initVarsState :: CollectVars
findVarProp :: Prop -> State CollectVars Prop
extractVars :: [Prop] -> CollectVars
newtype CollectBufs
CollectBufs :: Set (Expr Buf) -> CollectBufs
[$sel:bufs:CollectBufs] :: CollectBufs -> Set (Expr Buf)
initBufsState :: CollectBufs
extractBufs :: [Prop] -> [Expr Buf]
findBufProp :: Prop -> State CollectBufs Prop
data CollectStorage
CollectStorage :: Set (Expr EAddr, Maybe W256) -> Set W256 -> Set W256 -> CollectStorage
[$sel:addrs:CollectStorage] :: CollectStorage -> Set (Expr EAddr, Maybe W256)
[$sel:keys:CollectStorage] :: CollectStorage -> Set W256
[$sel:vals:CollectStorage] :: CollectStorage -> Set W256
initStorageState :: CollectStorage
extractStorage :: [Prop] -> CollectStorage
findStoragePropComp :: Prop -> State CollectStorage Prop
findStoragePropInner :: Prop -> State CollectStorage Prop
getvals :: CollectVars -> Gen (Map (Expr EWord) W256)
getStores :: CollectStorage -> Gen (Map (Expr EAddr) (Map W256 W256))
getBufs :: [Expr Buf] -> Gen (Map (Expr Buf) BufModel)
getRndW256 :: Gen W256
instance GHC.Show.Show EVM.Fuzz.CollectVars
instance GHC.Show.Show EVM.Fuzz.CollectBufs
instance GHC.Show.Show EVM.Fuzz.CollectStorage
instance GHC.Base.Semigroup EVM.Fuzz.CollectStorage


module EVM.Solvers

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

-- | A running solver instance
data SolverInstance
SolverInstance :: Solver -> Handle -> Handle -> ProcessHandle -> SolverInstance
[$sel:solvertype:SolverInstance] :: SolverInstance -> Solver
[$sel:stdin:SolverInstance] :: SolverInstance -> Handle
[$sel:stdout:SolverInstance] :: SolverInstance -> Handle
[$sel:process:SolverInstance] :: SolverInstance -> ProcessHandle

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

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

-- | The result of a call to (check-sat)
data CheckSatResult
Sat :: SMTCex -> CheckSatResult
Unsat :: CheckSatResult
Unknown :: CheckSatResult
Error :: Text -> CheckSatResult
isSat :: CheckSatResult -> Bool
isErr :: CheckSatResult -> Bool
isUnsat :: CheckSatResult -> Bool
checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult
writeSMT2File :: SMT2 -> Int -> String -> IO ()
withSolvers :: App m => Solver -> Natural -> Maybe Natural -> (SolverGroup -> m a) -> m a
getModel :: SolverInstance -> CexVars -> IO SMTCex
mkTimeout :: Maybe Natural -> Text

-- | Arguments used when spawning 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 instance
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 ())
checkCommand :: SolverInstance -> Text -> IO ()

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

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

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

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

-- | Reads lines from h until we have a balanced sexpr
readSExpr :: Handle -> IO [Text]
splitSExpr :: [Text] -> [Text]
data Par
LPar :: Par
RPar :: Par
getSExpr :: Text -> (Text, Text)
instance GHC.Classes.Eq EVM.Solvers.CheckSatResult
instance GHC.Show.Show EVM.Solvers.CheckSatResult
instance GHC.Show.Show EVM.Solvers.Solver

module EVM.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 W64
[QuerySlot] :: Addr -> W256 -> RpcQuery W256
[QueryChainId] :: RpcQuery W256
data BlockNumber
Latest :: BlockNumber
BlockNumber :: W256 -> BlockNumber
type RpcInfo = Maybe (BlockNumber, Text)
rpc :: String -> [Value] -> Value
class ToRPC a
toRPC :: ToRPC a => a -> Value
readText :: Read a => Text -> a
fetchQuery :: Show a => BlockNumber -> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
parseBlock :: (AsValue s, Show s) => s -> Maybe Block
fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value)
fetchContractWithSession :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchSlotWithSession :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe W256)
fetchBlockWithSession :: BlockNumber -> Text -> Session -> IO (Maybe Block)
fetchBlockFrom :: BlockNumber -> Text -> IO (Maybe Block)
fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchSlotFrom :: BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256)
fetchChainIdFrom :: Text -> IO (Maybe W256)
http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher t m s
zero :: Natural -> Maybe Natural -> Fetcher t m s
oracle :: SolverGroup -> RpcInfo -> Fetcher t m s
type Fetcher t m s = App m => Query t s -> m (EVM t s ())

-- | 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 :: App m => SolverGroup -> Prop -> Prop -> m BranchCondition
instance GHC.Classes.Eq EVM.Fetch.BlockNumber
instance GHC.Show.Show EVM.Fetch.BlockNumber
instance GHC.Show.Show (EVM.Fetch.RpcQuery a)
instance EVM.Fetch.ToRPC EVM.Types.Addr
instance EVM.Fetch.ToRPC EVM.Types.W256
instance EVM.Fetch.ToRPC GHC.Types.Bool
instance EVM.Fetch.ToRPC EVM.Fetch.BlockNumber

module EVM.Stepper

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

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

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

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

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

-- | Perform an IO action
[IOAct] :: IO a -> Action t s a

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

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

-- | Run the VM until its final state
runFully :: Stepper t s (VM t s)
wait :: Query t s -> Stepper t s ()
ask :: Choose s -> Stepper Symbolic s ()
evm :: EVM t s a -> Stepper t s a
evmIO :: IO a -> Stepper t s a
enter :: Text -> Stepper t s ()
interpret :: forall m a. App m => Fetcher Concrete m RealWorld -> VM Concrete RealWorld -> Stepper Concrete RealWorld a -> m a

module EVM.SymExec
data LoopHeuristic
Naive :: LoopHeuristic
StackBased :: LoopHeuristic
data ProofResult a b c
Qed :: a -> ProofResult a b c
Cex :: b -> ProofResult a b c
Timeout :: c -> ProofResult a b c
type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End)
type EquivResult = ProofResult () (SMTCex) ()
isTimeout :: ProofResult a b c -> Bool
isCex :: ProofResult a b c -> Bool
isQed :: ProofResult a b c -> Bool
data VeriOpts
VeriOpts :: Bool -> Maybe Integer -> Integer -> LoopHeuristic -> RpcInfo -> VeriOpts
[$sel:simp:VeriOpts] :: VeriOpts -> Bool
[$sel:maxIter:VeriOpts] :: VeriOpts -> Maybe Integer
[$sel:askSmtIters:VeriOpts] :: VeriOpts -> Integer
[$sel:loopHeuristic:VeriOpts] :: VeriOpts -> LoopHeuristic
[$sel:rpcInfo:VeriOpts] :: VeriOpts -> RpcInfo
defaultVeriOpts :: VeriOpts
rpcVeriOpts :: (BlockNumber, Text) -> VeriOpts
extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
bool :: Expr EWord -> Prop

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

-- | Generates calldata matching given type signature, optionally
--   specialized with concrete arguments. Any argument given as
--   "<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])
isSt :: CalldataFragment -> Bool
abstractVM :: (Expr Buf, [Prop]) -> ByteString -> Maybe (Precondition s) -> Bool -> ST s (VM Symbolic s)
loadSymVM :: ContractCode -> Expr EWord -> (Expr Buf, [Prop]) -> Bool -> ST s (VM Symbolic s)

-- | Interpreter which explores all paths at branching points. Returns an
--   'Expr End' representing the possible executions.
interpret :: forall m. App m => Fetcher Symbolic m RealWorld -> Maybe Integer -> Integer -> LoopHeuristic -> VM Symbolic RealWorld -> Stepper Symbolic RealWorld (Expr End) -> m (Expr End)
maxIterationsReached :: VM Symbolic s -> Maybe Integer -> Maybe Bool
askSmtItersReached :: VM Symbolic s -> Integer -> Bool

-- | Loop head detection heuristic
--   
--   The main thing we wish to differentiate between, are actual loop
--   heads, and branch points inside of internal functions that are called
--   multiple times.
--   
--   One way to do this is to observe that for internal functions, the
--   compiler must always store a stack item representing the location that
--   it must jump back to. If we compare the stack at the time of the
--   previous visit, and the time of the current visit, and notice that
--   this location has changed, then we can guess that the location is a
--   jump point within an internal function instead of a loop (where such
--   locations should be constant between iterations).
--   
--   This heuristic is not perfect, and can certainly be tricked, but
--   should generally be good enough for most compiler generated and non
--   pathological user generated loops.
isLoopHead :: LoopHeuristic -> VM Symbolic s -> Maybe Bool
type Precondition s = VM Symbolic s -> Prop
type Postcondition s = VM Symbolic s -> Expr End -> Prop
checkAssert :: App m => SolverGroup -> [Word256] -> ByteString -> Maybe Sig -> [String] -> VeriOpts -> m (Expr End, [VerifyResult])
getExpr :: App m => SolverGroup -> ByteString -> Maybe Sig -> [String] -> VeriOpts -> m (Expr End)

-- | 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 s

-- | By default hevm only checks for user-defined assertions
defaultPanicCodes :: [Word256]
allPanicCodes :: [Word256]

-- | Produces the revert message for solc &gt;=0.8 assertion violations
panicMsg :: Word256 -> ByteString

-- | Builds a buffer representing calldata from the provided method
--   description and concrete arguments
mkCalldata :: Maybe Sig -> [String] -> (Expr Buf, [Prop])
verifyContract :: App m => SolverGroup -> ByteString -> Maybe Sig -> [String] -> VeriOpts -> Maybe (Precondition RealWorld) -> Maybe (Postcondition RealWorld) -> m (Expr End, [VerifyResult])

-- | Stepper that parses the result of Stepper.runFully into an Expr End
runExpr :: Stepper Symbolic RealWorld (Expr End)
toEContract :: Contract -> Expr EContract

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

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

-- | Extract constraints stored in Expr End nodes
extractProps :: Expr End -> [Prop]
isPartial :: Expr a -> Bool
getPartials :: [Expr End] -> [PartialExec]

-- | Symbolically execute the VM and check all endstates against the
--   postcondition, if available.
verify :: App m => SolverGroup -> VeriOpts -> VM Symbolic RealWorld -> Maybe (Postcondition RealWorld) -> m (Expr End, [VerifyResult])
expandCex :: VM Symbolic s -> SMTCex -> SMTCex
type UnsatCache = TVar [Set Prop]

-- | Compares two contract runtimes for trace equivalence by running two
--   VMs and comparing the end states.
--   
--   We do this by asking the solver to find a common input for each pair
--   of endstates that satisfies the path conditions for both sides and
--   produces a differing output. If we can find such an input, then we
--   have a clear equivalence break, and since we run this check for every
--   pair of end states, the check is exhaustive.
equivalenceCheck :: forall m. App m => SolverGroup -> ByteString -> ByteString -> VeriOpts -> (Expr Buf, [Prop]) -> m [EquivResult]
equivalenceCheck' :: forall m. App m => SolverGroup -> [Expr End] -> [Expr End] -> m [EquivResult]
both' :: (a -> b) -> (a, a) -> (b, b)
produceModels :: App m => SolverGroup -> Expr End -> m [(Expr End, CheckSatResult)]
showModel :: Expr Buf -> (Expr End, CheckSatResult) -> IO ()
formatCex :: Expr Buf -> Maybe Sig -> SMTCex -> Text
prettyCalldata :: SMTCex -> Expr Buf -> Text -> [AbiType] -> Text

-- | If the expression contains any symbolic values, default them to some
--   concrete value The intuition here is that if we still have symbolic
--   values in our calldata expression after substituting in our cex, then
--   they can have any value and we can safely pick a random value. This is
--   a bit unsatisfying, we should really be doing smth like:
--   <a>https://github.com/ethereum/hevm/issues/334</a> but it's probably
--   good enough for now
defaultSymbolicValues :: Expr a -> Expr a

-- | Takes an expression and a Cex and replaces all abstract values in the
--   buf with concrete ones from the Cex.
subModel :: SMTCex -> Expr a -> Expr a
subVars :: Map (Expr EWord) W256 -> Expr a -> Expr a
subAddrs :: Map (Expr EAddr) Addr -> Expr a -> Expr a
subBufs :: Map (Expr Buf) ByteString -> Expr a -> Expr a
subStores :: Map (Expr EAddr) (Map W256 W256) -> Expr a -> Expr a
getCex :: ProofResult a b c -> Maybe b
getTimeout :: ProofResult a b c -> Maybe c
instance GHC.Generics.Generic EVM.SymExec.LoopHeuristic
instance Options.Generic.ParseRecord EVM.SymExec.LoopHeuristic
instance Options.Generic.ParseFields EVM.SymExec.LoopHeuristic
instance Options.Generic.ParseField EVM.SymExec.LoopHeuristic
instance GHC.Read.Read EVM.SymExec.LoopHeuristic
instance GHC.Show.Show EVM.SymExec.LoopHeuristic
instance GHC.Classes.Eq EVM.SymExec.LoopHeuristic
instance (GHC.Classes.Eq a, GHC.Classes.Eq b, GHC.Classes.Eq c) => GHC.Classes.Eq (EVM.SymExec.ProofResult a b c)
instance (GHC.Show.Show a, GHC.Show.Show b, GHC.Show.Show c) => GHC.Show.Show (EVM.SymExec.ProofResult a b c)
instance GHC.Show.Show EVM.SymExec.VeriOpts
instance GHC.Classes.Eq EVM.SymExec.VeriOpts
instance GHC.Classes.Eq EVM.SymExec.CalldataFragment
instance GHC.Show.Show EVM.SymExec.CalldataFragment

module EVM.UnitTest
data UnitTestOptions s
UnitTestOptions :: RpcInfo -> SolverGroup -> Maybe Int -> Maybe Integer -> Integer -> Maybe Natural -> Maybe Text -> Text -> DappInfo -> TestVMParams -> Bool -> UnitTestOptions s
[$sel:rpcInfo:UnitTestOptions] :: UnitTestOptions s -> RpcInfo
[$sel:solvers:UnitTestOptions] :: UnitTestOptions s -> SolverGroup
[$sel:verbose:UnitTestOptions] :: UnitTestOptions s -> Maybe Int
[$sel:maxIter:UnitTestOptions] :: UnitTestOptions s -> Maybe Integer
[$sel:askSmtIters:UnitTestOptions] :: UnitTestOptions s -> Integer
[$sel:smtTimeout:UnitTestOptions] :: UnitTestOptions s -> Maybe Natural
[$sel:solver:UnitTestOptions] :: UnitTestOptions s -> Maybe Text
[$sel:match:UnitTestOptions] :: UnitTestOptions s -> Text
[$sel:dapp:UnitTestOptions] :: UnitTestOptions s -> DappInfo
[$sel:testParams:UnitTestOptions] :: UnitTestOptions s -> TestVMParams
[$sel:ffiAllowed:UnitTestOptions] :: UnitTestOptions s -> Bool
data TestVMParams
TestVMParams :: Expr EAddr -> Expr EAddr -> Expr EAddr -> Word64 -> Word64 -> W256 -> W256 -> W256 -> Expr EAddr -> W256 -> W256 -> Word64 -> W256 -> W256 -> W256 -> W256 -> TestVMParams
[$sel:address:TestVMParams] :: TestVMParams -> Expr EAddr
[$sel:caller:TestVMParams] :: TestVMParams -> Expr EAddr
[$sel:origin:TestVMParams] :: TestVMParams -> Expr EAddr
[$sel:gasCreate:TestVMParams] :: TestVMParams -> Word64
[$sel:gasCall:TestVMParams] :: TestVMParams -> Word64
[$sel:baseFee:TestVMParams] :: TestVMParams -> W256
[$sel:priorityFee:TestVMParams] :: TestVMParams -> W256
[$sel:balanceCreate:TestVMParams] :: TestVMParams -> W256
[$sel:coinbase:TestVMParams] :: TestVMParams -> Expr EAddr
[$sel:number:TestVMParams] :: TestVMParams -> W256
[$sel:timestamp:TestVMParams] :: TestVMParams -> W256
[$sel:gaslimit:TestVMParams] :: TestVMParams -> Word64
[$sel:gasprice:TestVMParams] :: TestVMParams -> W256
[$sel:maxCodeSize:TestVMParams] :: TestVMParams -> W256
[$sel:prevrandao:TestVMParams] :: TestVMParams -> W256
[$sel:chainId:TestVMParams] :: TestVMParams -> W256
defaultGasForCreating :: Word64
defaultGasForInvoking :: Word64
defaultBalanceForTestContract :: W256
defaultMaxCodeSize :: W256
type ABIMethod = Text

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

-- | Top level CLI endpoint for hevm test
unitTest :: App m => UnitTestOptions RealWorld -> Contracts -> m 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 s -> SolcContract -> Stepper Concrete s ()
runUnitTestContract :: App m => UnitTestOptions RealWorld -> Map Text SolcContract -> (Text, [Sig]) -> m [Bool]

-- | Define the thread spawner for symbolic tests
symRun :: App m => UnitTestOptions RealWorld -> VM Concrete RealWorld -> Sig -> m (Text, Either Text Text)
allBranchRev :: Text -> Text
symFailure :: UnitTestOptions RealWorld -> Text -> Expr Buf -> [AbiType] -> [(Expr End, SMTCex)] -> Text
execSymTest :: UnitTestOptions RealWorld -> ABIMethod -> (Expr Buf, [Prop]) -> Stepper Symbolic RealWorld (Expr End)
checkSymFailures :: VMOps t => UnitTestOptions RealWorld -> Stepper t RealWorld (VM t RealWorld)
indentLines :: Int -> Text -> Text
passOutput :: VM t s -> UnitTestOptions s -> Text -> Text
failOutput :: VM t s -> UnitTestOptions s -> Text -> Text
formatTestLogs :: (?context :: DappContext) => Map W256 Event -> [Expr Log] -> Text
formatTestLog :: (?context :: DappContext) => Map W256 Event -> Expr Log -> Maybe Text
abiCall :: VMOps t => TestVMParams -> Either (Text, AbiValue) ByteString -> EVM t s ()
makeTxCall :: VMOps t => TestVMParams -> (Expr Buf, [Prop]) -> EVM t s ()
initialUnitTestVm :: VMOps t => UnitTestOptions s -> SolcContract -> ST s (VM t s)
paramsFromRpc :: RpcInfo -> IO TestVMParams
tick :: Text -> IO ()