-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Symbolic EVM Evaluator -- -- Symbolic EVM semantics in Haskell. @package hevm @version 0.54.2 -- | 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 ReadConfig 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. -- -- module EVM.Effects class Monad m => ReadConfig m readConfig :: ReadConfig m => m Config data Config Config :: Bool -> Bool -> Bool -> Bool -> Bool -> Integer -> Bool -> Bool -> Config [$sel:dumpQueries:Config] :: Config -> Bool [$sel:dumpExprs:Config] :: Config -> Bool [$sel:dumpEndStates:Config] :: Config -> Bool [$sel:debug:Config] :: Config -> Bool [$sel:dumpTrace:Config] :: Config -> Bool [$sel:numCexFuzz:Config] :: Config -> Integer [$sel:onlyCexFuzz:Config] :: Config -> Bool [$sel:decomposeStorage:Config] :: Config -> Bool defaultConfig :: Config class Monad m => TTY m writeOutput :: TTY m => Text -> m () writeErr :: TTY m => Text -> 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.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 Buf does allow for the -- construction of some badly typed Expr instances (e.g. an MSTORE on top -- of the contents of calldata instead of some previous instance of -- memory), we accept this for the sake of simplifying pattern matches -- against a Buf expression. -- -- Storage expressions are similar, but instead of writing regions of -- bytes, we write a word to a particular key in a given addresses -- storage. Note that as with a Buf, writes can be sequenced on top of -- concrete, empty and fully abstract starting states. -- -- One important principle is that of local context: e.g. each term -- representing a write to a Buf Storage Logs will always -- contain a copy of the state that is being added to, this ensures that -- all context relevant to a given operation is contained within the term -- that represents that operation. -- -- When dealing with Expr instances we assume that concrete expressions -- have been reduced to their smallest possible representation (i.e. a -- Lit, ConcreteBuf, or ConcreteStore). Failure to -- adhere to this invariant will result in your concrete term being -- treated as symbolic, and may produce unexpected errors. In the future -- we may wish to consider encoding the concreteness of a given term -- directly in the type of that term, since such type level shenanigans -- tends to complicate implementation, we skip this for now. 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] -> TraceContext -> PartialExec -> Expr End [Failure] :: [Prop] -> TraceContext -> EvmError -> Expr End [Success] :: [Prop] -> TraceContext -> 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 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 type Err a = Either String a getError :: Err a -> String getNonError :: Err a -> a -- | 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 :: String -> FunctionSelector -> EvmError NonexistentFork :: Int -> EvmError evmErrToString :: EvmError -> String -- | Sometimes we can only partially execute a given program data PartialExec UnexpectedSymbolicArg :: Int -> String -> String -> [SomeExpr] -> PartialExec [$sel:pc:UnexpectedSymbolicArg] :: PartialExec -> Int [$sel:opcode:UnexpectedSymbolicArg] :: PartialExec -> String [$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 & -- 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] -> Map String String -> (ByteString -> EVM t s ()) -> Query t s [PleaseReadEnv] :: String -> (String -> 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 -> Map Addr Text -> Map String String -> 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 [$sel:labels:VM] :: VM (t :: VMType) s -> Map Addr Text [$sel:osEnv:VM] :: VM (t :: VMType) s -> Map String String 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. exec1. 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 -> BaseState -> RuntimeConfig [$sel:allowFFI:RuntimeConfig] :: RuntimeConfig -> Bool [$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)] -> Set (Expr EAddr) -> 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)] [$sel:createdContracts:SubState] :: SubState -> Set (Expr EAddr) -- | 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 -> Maybe (Expr EAddr) -> 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 [$sel:overrideCaller:FrameState] :: FrameState (t :: VMType) s -> Maybe (Expr EAddr) [$sel:resetCaller: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 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:tStorage: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 EXTCODEHASH, so we distinguish these two -- code types. -- -- The definition follows the structure of code output by solc. We need -- to use some heuristics here to deal with symbolic data regions that -- may be present in the bytecode since the fully abstract case is -- impractical: -- -- -- -- 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 -- | Constructor code, during contract creation InitCode :: ByteString -> Expr Buf -> ContractCode -- | Instance 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 TraceContext TraceContext :: Forest Trace -> Map (Expr EAddr) Contract -> Map Addr Text -> TraceContext [$sel:traces:TraceContext] :: TraceContext -> Forest Trace [$sel:contracts:TraceContext] :: TraceContext -> Map (Expr EAddr) Contract [$sel:labels:TraceContext] :: TraceContext -> Map Addr Text -- | 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 -> Int -> W256 -> 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 [$sel:freshAddresses:VMOpts] :: VMOpts (t :: VMType) -> Int [$sel:beaconRoot:VMOpts] :: VMOpts (t :: VMType) -> W256 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 OpBlobhash :: GenericOp a OpBlobBaseFee :: GenericOp a OpPop :: GenericOp a OpMcopy :: GenericOp a OpMload :: GenericOp a OpMstore :: GenericOp a OpMstore8 :: GenericOp a OpSload :: GenericOp a OpSstore :: GenericOp a OpTload :: GenericOp a OpTstore :: 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 -- | -- https://docs.soliditylang.org/en/v0.8.19/abi-spec.html#function-selector 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 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 bssToBs :: ByteStringS -> ByteString keccakBytes :: ByteString -> ByteString word32 :: [Word8] -> Word32 keccak :: Expr Buf -> Expr EWord keccak' :: ByteString -> W256 abiKeccak :: ByteString -> FunctionSelector internalError :: HasCallStack => [Char] -> a concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] regexMatches :: Text -> Text -> Bool readNull :: Read a => a -> String -> a padLeft :: Int -> ByteString -> ByteString padLeft' :: Int -> Vector (Expr Byte) -> Vector (Expr Byte) padRight :: Int -> ByteString -> ByteString padRight' :: Int -> String -> String formatString :: ByteString -> String -- | paddedShowHex displays a number in hexadecimal and pads the -- number with 0 so that it has a minimum length of w. 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.~ 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.A_Lens, a GHC.Types.~ EVM.Types.Expr 'EVM.Types.Storage, b GHC.Types.~ EVM.Types.Expr 'EVM.Types.Storage) => Optics.Label.LabelOptic "tStorage" 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.A_Lens, 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.~ EVM.Types.W256, b GHC.Types.~ EVM.Types.W256) => Optics.Label.LabelOptic "beaconRoot" 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.~ GHC.Types.Int, b GHC.Types.~ GHC.Types.Int) => Optics.Label.LabelOptic "freshAddresses" 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.~ 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 "createdContracts" 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.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.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.~ GHC.Types.Bool, b GHC.Types.~ GHC.Types.Bool) => Optics.Label.LabelOptic "resetCaller" 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.~ Data.Map.Internal.Map EVM.Types.Addr Data.Text.Internal.Text, b GHC.Types.~ Data.Map.Internal.Map EVM.Types.Addr Data.Text.Internal.Text) => Optics.Label.LabelOptic "labels" 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.~ Data.Map.Internal.Map GHC.Base.String GHC.Base.String, b GHC.Types.~ Data.Map.Internal.Map GHC.Base.String GHC.Base.String) => Optics.Label.LabelOptic "osEnv" 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.Show.Show EVM.Types.RuntimeConfig 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.TraceContext instance GHC.Show.Show EVM.Types.TraceContext instance GHC.Classes.Ord EVM.Types.TraceContext instance GHC.Classes.Eq EVM.Types.TraceContext 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.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.TraceContext instance GHC.Base.Monoid EVM.Types.TraceContext 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 EVM.Types.W256 EVM.Types.Word512 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 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 & 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 mapPropM' :: forall m. Monad m => (Prop -> m Prop) -> Prop -> m Prop mapExpr :: (forall a. Expr a -> Expr a) -> Expr b -> Expr b mapExprM_ :: Monad m => (forall a. Expr a -> m ()) -> Expr b -> m () mapExprM :: Monad m => (forall a. Expr a -> m (Expr a)) -> Expr b -> m (Expr b) mapPropM_ :: Monad m => (forall a. Expr a -> m ()) -> Prop -> m () 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 peq :: Typeable a => Expr a -> Expr a -> Prop -- | 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 >= 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 maxWord256 :: 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. -- -- This does not strip writes that cannot possibly match a read, in case -- there are some write(s) in between that it cannot statically determine -- to be removable, because it will early-abort. So (load idx1 (store -- idx1 (store idx1 (store idx0)))) will not strip the idx0 store, in -- case things in between cannot be stripped. See -- simplify-storage-map-todo test for an example where this happens. Note -- that decomposition solves this, though late in the simplification -- lifecycle (just before SMT generation, which can be too late) readStorage :: Expr EWord -> Expr Storage -> Maybe (Expr EWord) pattern MappingSlot :: ByteString -> Expr EWord -> Expr EWord pattern ArraySlotWithOffs :: 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 safeToDecomposeProp :: Prop -> Bool safeToDecompose :: Expr a -> Maybe () -- | Splits storage into logical sub-stores if (1) all SLoad->SStore* -- chains are one of: (1a) Lit < 256, (1b) MappingSlot, (1c) -- ArraySlotWithOffs, (1d) ArraySlotZero and (2) there is no mixing of -- different types (e.g. Map with Array) within the same SStore -> -- SLoad* chain -- -- Mixing (2) and (3) are attempted to be prevented (if possible) as part -- of the rewrites done by the readStorage function that is ran -- before this. If there is still mixing here, we abort with a Nothing. -- -- We do NOT rewrite stand-alone SStore-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] 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 <= x < 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 -- | Checks if a conjunction of propositions is definitely unsatisfiable isUnsat :: [Prop] -> Bool concKeccakSimpExpr :: Expr a -> Expr a concKeccakProps :: [Prop] -> [Prop] concKeccakOnePass :: Expr a -> Expr a lhsConstHelper :: Expr a -> Maybe () checkLHSConstProp :: Prop -> Bool checkLHSConst :: Expr a -> Bool 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 OpBlobhash :: GenericOp a OpBlobBaseFee :: GenericOp a OpPop :: GenericOp a OpMcopy :: GenericOp a OpMload :: GenericOp a OpMstore :: GenericOp a OpMstore8 :: GenericOp a OpSload :: GenericOp a OpSstore :: GenericOp a OpTload :: GenericOp a OpTstore :: 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 showAlter :: ShowAlter a => a -> String 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 EVM.ABI.ShowAlter 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 :: App 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 CombinedJSON :: ProjectType Foundry :: 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 :: App m => FilePath -> ProjectType -> m (Either String BuildOutput) functionAbi :: Text -> IO Method makeSrcMaps :: Text -> Maybe (Seq SrcMap) readSolc :: App m => ProjectType -> FilePath -> FilePath -> m (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 -> Map Addr Text -> DappContext [$sel:info:DappContext] :: DappContext -> DappInfo [$sel:contracts:DappContext] :: DappContext -> Map (Expr EAddr) Contract [$sel:labels:DappContext] :: DappContext -> Map Addr Text 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. -- EXTCODEHASH. bytecode :: Getter Contract (Maybe (Expr Buf)) currentContract :: VM t s -> Maybe Contract makeVm :: VMOps t => VMOpts t -> ST s (VM t s) setEIP4788Storage :: VMOpts t -> VM t 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 () getOpW8 :: forall (t :: VMType) s. FrameState t s -> Word8 getOpName :: forall (t :: VMType) s. FrameState t s -> [Char] -- | 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 () accessTStorage :: VMOps t => Expr EAddr -> Expr EWord -> (Expr EWord -> EVM t s ()) -> EVM t s () clearTStorages :: 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) => Gas t -> (Expr EWord, Expr EWord) -> (Expr EWord, Expr EWord) -> [Expr EWord] -> EVM t s () type CheatAction t s = 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 FrameResult. -- -- It also handles the case when the current stack frame is the only one; -- in this case, we set the final _result 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 -> TraceContext 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 Tree 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 :: ByteString -> Maybe 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.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 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] -> CexVars -> [Prop] -> SMT2 formatSMT2 :: SMT2 -> Text -- | Reads all intermediate variables from the builder state and produces -- SMT declaring them as constants declareIntermediates :: BufEnv -> StoreEnv -> Err SMT2 data AbstState AbstState :: Map (Expr EWord) Int -> Int -> AbstState [$sel:words:AbstState] :: AbstState -> Map (Expr EWord) Int [$sel:count:AbstState] :: AbstState -> Int smt2Line :: Builder -> SMT2 assertProps :: Config -> [Prop] -> Err SMT2 assertPropsNoSimp :: [Prop] -> Err 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])] -> Err SMT2 declareAbstractStores :: [Builder] -> SMT2 declareBlockContext :: [(Builder, [Prop])] -> Err SMT2 assertSMT :: Prop -> Either String Builder prelude :: SMT2 exprToSMT :: Expr a -> Err Builder sp :: Builder -> Builder -> Builder zero :: Builder one :: Builder propToSMT :: Prop -> Err Builder -- | Stores a region of src into dst copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Err Builder -- | Unrolls an exponentiation into a series of multiplications expandExp :: Expr EWord -> W256 -> Err Builder -- | Concatenates a list of bytes into a larger bitvector concatBytes :: [Expr Byte] -> Err Builder -- | Concatenates a list of bytes into a larger bitvector writeBytes :: ByteString -> Expr Buf -> Err Builder encodeConcreteStore :: Map W256 W256 -> Err 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.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.SMTCex instance GHC.Base.Monoid EVM.SMT.SMTCex 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 :: String -> CheckSatResult Error :: String -> CheckSatResult isSat :: CheckSatResult -> Bool isUnsat :: CheckSatResult -> Bool checkSat :: SolverGroup -> Err SMT2 -> IO CheckSatResult writeSMT2File :: SMT2 -> Int -> IO () withSolvers :: App m => Solver -> Natural -> 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 -> Natural -> Maybe Natural -> [Text] -- | Spawns a solver instance, and sets the various global config options -- that we use for our queries spawnSolver :: Solver -> Natural -> 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 -- | Strips trailing r, if present stripCarriageReturn :: Text -> 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.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 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 Action 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 d Qed :: a -> ProofResult a b c d Cex :: b -> ProofResult a b c d Unknown :: c -> ProofResult a b c d Error :: d -> ProofResult a b c d type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End) String type EquivResult = ProofResult () (SMTCex) () String isUnknown :: ProofResult a b c d -> Bool isError :: ProofResult a b c d -> Bool isCex :: ProofResult a b c d -> Bool isQed :: ProofResult a b c d -> Bool groupIssues :: [ProofResult a b c String] -> [(Integer, String)] 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 -- "symbolic" 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) freezeVM :: VM Symbolic RealWorld -> ST RealWorld (VM Symbolic RealWorld) -- | 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: -- --
    --
  1. the invalid opcode (0xfe) (solc < 0.8)
    2. --
  2. a revert with a reason of the form -- `abi.encodeWithSelector("Panic(uint256)", code)`, where code is one of -- the following (solc >= 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 >= x.length or i < 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.
    3. --
-- -- see: -- https://docs.soliditylang.org/en/v0.8.6/control-structures.html?highlight=Panic#panic-via-assert-and-error-via-require checkAssertions :: [Word256] -> Postcondition s -- | By default hevm only checks for user-defined assertions defaultPanicCodes :: [Word256] allPanicCodes :: [Word256] -- | Produces the revert message for solc >=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: -- https://github.com/ethereum/hevm/issues/334 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 d -> Maybe b getUnknown :: ProofResult a b c d -> 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 d) => GHC.Classes.Eq (EVM.SymExec.ProofResult a b c d) instance (GHC.Show.Show a, GHC.Show.Show b, GHC.Show.Show c, GHC.Show.Show d) => GHC.Show.Show (EVM.SymExec.ProofResult a b c d) 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 -> 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 [$sel:checkFailBit: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 -- | Used in various places for dumping traces writeTraceDapp :: App m => DappInfo -> VM t RealWorld -> m () writeTrace :: App m => VM t RealWorld -> m () -- | 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 Bool allBranchRev :: Text symFailure :: UnitTestOptions RealWorld -> Text -> Expr Buf -> [AbiType] -> [(Expr End, SMTCex)] -> Text 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 ()