h)}R      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                0.53.0 Safe-Inferred "%&(1&@543210/.-,+*)('&%$#"!  5543210/.-,+*)('&%$#"!  5 Safe-Inferred "%&(1'hevm8Opaque representation of the C library's context struct.7hevm5Run a given precompiled contract using the C library.7hevm&The number of the precompiled contracthevmThe input bufferhevmThe desired output sizehevmHopefully, the output buffer77 Safe-Inferred "%&(1>k$8hevmA four bit valueChevm https://docs.soliditylang.org/en/v0.8.19/abi-spec.html#function-selectorhevm'A specification for an initial VM statehevmWrapper type containing vm traces and the context needed to pretty print them properlyhevmWe 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).hevmA contract is either in creation (running its "constructor") or post-creation, and code in these two modes is treated differently by instructions like  EXTCODEHASH+, so we distinguish these two code types.The definition follows the structure of code output by solc. We need to use some heuristics here to deal with symbolic data regions that may be present in the bytecode since the fully abstract case is impractical:initcode has concrete code, followed by an abstract data "section"runtimecode has a fixed length, but may contain fixed size symbolic regions (due to immutable)hopefully we do not have to deal with dynamic immutable before we get a real data section...hevmFully abstract code, keyed on an address to give consistent results for e.g. extcodehashhevm Constructor code, during contract creationhevmInstance code, after contract creationhevmThe cache is data that can be persisted for efficiency: any expensive query that is constant at least within a block.hevmA unique id for a given pchevmFull contract statehevmData about the blockhevmVarious environmental datahevm(The state that spans a whole transactionhevm:The "registers" of the VM along with memory and data stackhevm+The "accrued substate" across a transactionhevmCall/create infohevm(An entry in the VM's "call/create stack"hevm:Configuration options that need to be consulted at runtimehevmThe VM base state (i.e. should new contracts be created with abstract balance / storage?)hevmAlias for the type of e.g. exec1.hevm%The state of a stepwise EVM executionhevmhow many times we've visited a loc, and what the contents of the stack were when we were there lasthevm"The possible result states of a VMhevm)The possible return values of a SMT queryhevm0Execution could proceed down one of two brancheshevmQueries halt execution until resolved through RPC calls or SMT querieshevmEffect types used by the vm implementation for side effects & control flowhevm7Sometimes we can only partially execute a given programhevmCore EVM Error Typeshevm dstOffset + size in dst with srcOffset -> srcOffset + size from srcNote that the shared usage of  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 , , or ). 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.hevm Literal wordshevm Variableshevm(variables introduced during the CSE passhevm displays a number in hexadecimal and pads the number with 0 so that it has a minimum length of w.hevm$Execution could not continue furtherhevmAn operation failedhevm$Reached STOP, RETURN, or end-of-codehevm3An effect must be handled for execution to continue89:<;=>?@ABCEDF~}|{zyxwvutsrqponmlkjihgfedcba`_^]\[ZYXWVUTSRQPONMLKJIHGF~}|{zyxwvutsrqponmlkjihgfedcba`_^]\[ZYXWVUTSRQPONMLKJIHGCEDAB?@=>:<;8932444444.Generic traversal functions for Expr datatypes Safe-Inferred "%&(1Ghevm!Generic operations over AST termshevmRecursively 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 Safe-Inferred "%&(1G Safe-Inferred "%&(1WhevmIf 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.hevm.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.hevmReads n bytes starting from idx in buf and returns a left padded word*If n is >= 32 this is the same as readWordhevm1Reads the word starting at idx from the given bufhevmCopies a slice of src into dst.0 srcOffset srcOffset + size length src J--------------J------------------J-----------------J src: | | ------ sl ------ | | J--------------J------------------J-----------------J0 dstOffset dstOffset + size length dst J--------J------------------J-----------------J dst: | hd | | tl | J--------J------------------J-----------------Jhevm$Returns the length of a given bufferIf there are any writes to abstract locations, or CopySlices with an abstract size or dstOffset, an abstract expression will be returned.hevmReturn 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.hevm Returns the first n bytes of bufhevm/Returns everything but the first n bytes of bufhevm8Removes any irrelevant writes when reading from a bufferhevmStrips 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...hevmReads 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.hevmTurns Literals into keccak(bytes32(id)) + offset (i.e. writes to arrays)hevm0Writes 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.hevmSplits storage into logical sub-stores if (1) all SLoad->SStore* chains are one of: (1a) Lit < 256, (1b) MappingSlot, (1c) ArraySlotWithOffset, (1d) ArraySlotZero and (2) there is no mixing of different types (e.g. Map with Array) within the same SStore -> SLoad* chain, and (3) there is no mixing of different array/map slots.Mixing (2) and (3) are attempted to be prevented (if possible) as part of the rewrites done by the  function that is ran before this. If there is still mixing here, we abort with a Nothing.We do NOT rewrite stand-alone -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 solverhevmSimple recursive match based AST simplification Note: may not terminate!hevmEvaluate the provided proposition down to its most concrete result Also simplifies the inner Expr, if it existshevm,Returns the byte at idx from the given word.hevmConverts a list of bytes into a W256. TODO: semantics if the input is too large?hevmTrue if the given expression contains any node that satisfies the input predicatehevm/images of keccak(bytes32(x)) where 0 <= x < 256hevmFolds constants Safe-Inferred "%&(1YFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~FGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ +Expr passes to determine Keccak assumptions Safe-Inferred "%&(1Z  Safe-Inferred "%&(1[ -Common subexpression elimination for Expr ast Safe-Inferred "%&(1\hevm.Common subexpression elimination pass for Exprhevm.Common subexpression elimination pass for Prophevm6Common subexpression elimination pass for list of Prophevm6Common subexpression elimination pass for list of Prop ;Assembler for EVM opcodes used in the HEVM symbolic checker Safe-Inferred "%&(1]  Safe-Inferred "%&(1^hevm8A method name, and the (ordered) types of it's argumentshevmDecode a sequence type (e.g. tuple / array). Will fail for non sequence typeshevmPretty-print some .== Safe-Inferred"%&(1=?f  hevm,The various project types understood by hevmhevm5A mapping from source files to (maybe) their contentshevmSolidity source files are identified either by their location in the vfs, or by a src map identifierhevmA mapping from contract identifiers (filepath:name) to their ast json hevmA mapping from contract identifiers (filepath:name) to a SolcContract object hevm&specified to not read blockchain state hevm,specified to not modify the blockchain state hevm,function does not accept Ether - the default hevmfunction accepts Ether hevmReads all solc output json files found under the provided filepath and returns them merged into a BuildOutputhevmFinds all json files under the provided filepath, searches recursivelyhevmFilters out metadata json fileshevmReads a foundry json output hevm)Parses the standard json output from solc hevmWhen 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. hevmEvery 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.   for the EVM given a secret key Safe-Inferred "%&(1h hevmWe 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.   Safe-Inferred "%&(1i% hevm1bytecode modulo immutables, to identify contracts% %  Safe-Inferred "%&(1r hevm*A stack frame can be popped in three ways. hevmSTOP, RETURN, or no more code hevmREVERT hevmAny other error hevmAn "external" view of a contract's bytecode, appropriate for e.g.  EXTCODEHASH. hevm1Initialize an abstract contract with unknown code hevm/Initialize an abstract contract with known code hevm)Initialize an empty contract without code hevm)Initialize empty contract with given code hevmUpdate program counter hevmExecutes the EVM one step hevmChecks a *CALL for failure; OOG, too many callframes, memory access etc. hevm5Construct RPC Query and halt execution until resolved hevm>Loads the selected contract as the current contract to execute hevmreturns a wrapped boolean- if true, this address has been touched before in the txn (warm gas cost as in EIP 2929) otherwise cold hevmreturns a wrapped boolean- if true, this slot has been touched before in the txn (warm gas cost as in EIP 2929) otherwise cold hevm!Parses a raw Buf into an InitCodesolidity 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. hevmReplace a contract's code, like when CREATE returns from the constructor code. hevmThis function defines how to pop the current stack frame in either of the ways specified by  .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. hevmThe length of the code ignoring any constructor args. This represents the region that can contain executable opcodes hevmThe length of the code including any constructor args. This can return an abstract value  Safe-Inferred "%&(1t   Safe-Inferred "%&(1v hevmutility function for getting a more useful representation of accesslistentries duplicates only matter for gas computation hevm,Increments origin nonce and pays gas deposit hevmGiven a valid tx loaded into the vm state, subtract gas payment from the origin, increment the nonce and pay receiving address$ $  Safe-Inferred "%&(1w  Domain specific effects Safe-Inferred"%&()1?w  Utilities for building and executing SMT queries from Expr instances Safe-Inferred "%&(1L hevmUsed for abstraction-refinement of the SMT formula. Contains assertions that make our query fully precise. These will be added to the assertion stack if we get sat with the abstracted query. hevma final post shrinking cex, buffers here are all represented as concrete bytestrings hevmThis 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 hevmA 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) hevm4Data that we need to construct a nice counterexample hevm>variable names that we need models for to reconstruct calldata hevmsymbolic address names hevm.buffer names and guesses at their maximum size hevmreads from abstract storage hevm(the names of any block context variables hevm%the names of any tx context variables hevmAttempts to collapse a compressed buffer representation down to a flattened one hevmReads all intermediate variables from the builder state and produces SMT declaring them as constants hevmThis 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. hevmAsserts 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. hevmFinds the maximum read index for each abstract buffer in the input props hevmReturns an SMT2 object with all buffers referenced from the input props declared, and with the appropriate cex extraction metadata attached hevmStores a region of src into dst hevm:Unrolls an exponentiation into a series of multiplications hevm4Concatenates a list of bytes into a larger bitvector hevm4Concatenates a list of bytes into a larger bitvector hevmQueries the solver for models for each of the expressions representing the max read index for a given buffer hevmGets the initial model for each buffer, these will often be much too large for our purposes hevmTakes 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 hevmAsk the solver to give us the concrete value of an arbitrary abstract word hevmInterpret an N-dimensional array as a value of type a. Parameterized by an interpretation function for array values. hevm.Interpret an 1-dimensional array as a function Concrete Fuzzer of Exprs Safe-Inferred "%&(1   Solver orchestration Safe-Inferred "%&(1 hevm#The result of a call to (check-sat) hevmA 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 hevm)A channel representing a group of solvers hevmA running solver instance hevmSupported solvers hevm.Arguments used when spawning a solver instance hevmSpawns a solver instance, and sets the various global config options that we use for our queries hevm*Cleanly shutdown a running solver instance hevmSends a list of commands to the solver. Returns the first error, if there was one. hevmSends a single command to the solver, returns the first available line from the output buffer hevmSends a string to the solver and appends a newline, returns the first available line from the output buffer hevmSends a string to the solver and appends a newline, doesn't return stdout hevmReturns a string representation of the model for the requested variable hevm1Reads lines from h until we have a balanced sexpr- -  Safe-Inferred "%&(1[ hevm/Abstract representation of an RPC fetch requesthevmChecks 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.    Safe-Inferred "%&(1 hevm'Type alias for an operational monad of Actionhevm-The instruction type of the operational monadhevm6Keep executing until an intermediate result is reachedhevmWait for a query to be resolvedhevmMultiple things can happenhevmEmbed a VM state transformationhevmPerform an IO actionhevm4Run the VM until final result, resolving all querieshevm Run the VM until its final state Safe-Inferred "%&(1=hevm%Abstract calldata argument generationhevmGenerates calldata matching given type signature, optionally specialized with concrete arguments. Any argument given as " symbolic8" or omitted at the tail of the list are kept symbolic.hevmInterpreter which explores all paths at branching points. Returns an 'Expr End' representing the possible executions.hevmLoop head detection heuristicThe 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.hevm5Checks if an assertion violation has been encountered8hevm recognises the following as an assertion violation: &the invalid opcode (0xfe) (solc < 0.8)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.see: https://docs.soliditylang.org/en/v0.8.6/control-structures.html?highlight=Panic#panic-via-assert-and-error-via-requirehevm7By default hevm only checks for user-defined assertionshevm?Produces the revert message for solc >=0.8 assertion violationshevmBuilds a buffer representing calldata from the provided method description and concrete argumentshevmStepper that parses the result of Stepper.runFully into an Expr EndhevmConverts a given top level expr into a list of final states and the associated path conditions for each state.hevmStrips 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 properlyhevm,Extract constraints stored in Expr End nodeshevmSymbolically execute the VM and check all endstates against the postcondition, if available.hevmCompares 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.hevmIf 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 nowhevmTakes an expression and a Cex and replaces all abstract values in the buf with concrete ones from the Cex. Safe-Inferred "%&(1)hevm&Generate VeriOpts from UnitTestOptionshevm$Top level CLI endpoint for hevm testhevmAssuming a constructor is loaded, this stepper will run the constructor to create the test contract, give it an initial balance, and run `setUp()'.hevm,Define the thread spawner for symbolic tests77 Safe-Inferred "%&(1= !!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWWXXYZZ[[\\]]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    hevm-0.53.0-inplace EVM.FormatEVM.FeeScheduleEVM.Precompiled EVM.TypesEVM.TraversalsEVM.RLPEVM.ExprEVM.Op EVM.Keccak EVM.ConcreteEVM.CSE EVM.AssemblerEVM.ABI EVM.SolidityEVM.SignEVM.DappEVMEVM.TransactionEVM.Exec EVM.EffectsEVM.SMTEVM.Fuzz EVM.Solvers EVM.Fetch EVM.Stepper EVM.SymExec EVM.UnitTesthevm Paths_hevm&tree-view-0.5.1-BIZ7vC50x67GCHSkRNjc2cData.Tree.ViewshowTree FeeSchedule$sel:g_zero:FeeSchedule$sel:g_base:FeeSchedule$sel:g_verylow:FeeSchedule$sel:g_low:FeeSchedule$sel:g_mid:FeeSchedule$sel:g_high:FeeSchedule$sel:g_extcode:FeeSchedule$sel:g_balance:FeeSchedule$sel:g_sload:FeeSchedule$sel:g_jumpdest:FeeSchedule$sel:g_sset:FeeSchedule$sel:g_sreset:FeeSchedule$sel:r_sclear:FeeSchedule$sel:g_selfdestruct:FeeSchedule*$sel:g_selfdestruct_newaccount:FeeSchedule$sel:r_selfdestruct:FeeSchedule$sel:g_create:FeeSchedule$sel:g_codedeposit:FeeSchedule$sel:g_call:FeeSchedule$sel:g_callvalue:FeeSchedule$sel:g_callstipend:FeeSchedule$sel:g_newaccount:FeeSchedule$sel:g_exp:FeeSchedule$sel:g_expbyte:FeeSchedule$sel:g_memory:FeeSchedule$sel:g_txcreate:FeeSchedule$sel:g_txdatazero:FeeSchedule $sel:g_txdatanonzero:FeeSchedule$sel:g_transaction:FeeSchedule$sel:g_log:FeeSchedule$sel:g_logdata:FeeSchedule$sel:g_logtopic:FeeSchedule$sel:g_sha3:FeeSchedule$sel:g_sha3word:FeeSchedule$sel:g_initcodeword:FeeSchedule$sel:g_copy:FeeSchedule$sel:g_blockhash:FeeSchedule$sel:g_extcodehash:FeeSchedule$sel:g_quaddivisor:FeeSchedule$sel:g_ecadd:FeeSchedule$sel:g_ecmul:FeeSchedule $sel:g_pairing_point:FeeSchedule$sel:g_pairing_base:FeeSchedule$sel:g_fround:FeeSchedule$sel:r_block:FeeSchedule$sel:g_cold_sload:FeeSchedule&$sel:g_cold_account_access:FeeSchedule$$sel:g_warm_storage_read:FeeSchedule&$sel:g_access_list_address:FeeSchedule*$sel:g_access_list_storage_key:FeeSchedule feeSchedule$fShowFeeScheduleexecuteNibbleAddr$sel:addressWord160:AddrW64W256 ByteStringSFunctionSelector($sel:unFunctionSelector:FunctionSelector GenericOpOpStopOpAddOpMulOpSubOpDivOpSdivOpModOpSmodOpAddmodOpMulmodOpExp OpSignextendOpLtOpGtOpSltOpSgtOpEqOpIszeroOpAndOpOrOpXorOpNotOpByteOpShlOpShrOpSarOpSha3 OpAddress OpBalanceOpOriginOpCaller OpCallvalueOpCalldataloadOpCalldatasizeOpCalldatacopy OpCodesize OpCodecopy OpGasprice OpExtcodesize OpExtcodecopyOpReturndatasizeOpReturndatacopy OpExtcodehash OpBlockhash OpCoinbase OpTimestampOpNumber OpPrevRandao OpGaslimit OpChainid OpSelfbalance OpBaseFeeOpPopOpMloadOpMstore OpMstore8OpSloadOpSstoreOpJumpOpJumpiOpPcOpMsizeOpGas OpJumpdestOpCreateOpCall OpStaticcall OpCallcodeOpReturnOpDelegatecall OpCreate2OpRevertOpSelfdestructOpDupOpSwapOpLogOpPush0OpPush OpUnknownOpVMOpts$sel:contract:VMOpts$sel:otherContracts:VMOpts$sel:calldata:VMOpts$sel:baseState:VMOpts$sel:value:VMOpts$sel:priorityFee:VMOpts$sel:address:VMOpts$sel:caller:VMOpts$sel:origin:VMOpts$sel:gas:VMOpts$sel:gaslimit:VMOpts$sel:number:VMOpts$sel:timestamp:VMOpts$sel:coinbase:VMOpts$sel:prevRandao:VMOpts$sel:maxCodeSize:VMOpts$sel:blockGaslimit:VMOpts$sel:gasprice:VMOpts$sel:baseFee:VMOpts$sel:schedule:VMOpts$sel:chainId:VMOpts$sel:create:VMOpts$sel:txAccessList:VMOpts$sel:allowFFI:VMOptsTraces$sel:traces:Traces$sel:contracts:Traces TraceData EventTrace FrameTrace ErrorTrace EntryTrace ReturnTraceTrace$sel:opIx:Trace$sel:contract:Trace$sel:tracedata:Trace RuntimeCodeConcreteRuntimeCodeSymbolicRuntimeCode ContractCode UnknownCodeInitCodeCache$sel:fetched:Cache$sel:path:Cache CodeLocationVMOpsburn'burnExpburnSha3burnCalldatacopy burnCodecopyburnExtcodecopyburnReturndatacopyburnLog initialGas ensureGas gasTryFrom costOfCreate costOfCallreclaimRemainingGasAllowance payRefundspushGas enoughGassubGastoGaswhenSymbolicElsepartialbranchContract$sel:code:Contract$sel:storage:Contract$sel:origStorage:Contract$sel:balance:Contract$sel:nonce:Contract$sel:codehash:Contract$sel:opIxMap:Contract$sel:codeOps:Contract$sel:external:ContractBlock$sel:coinbase:Block$sel:timestamp:Block$sel:number:Block$sel:prevRandao:Block$sel:gaslimit:Block$sel:baseFee:Block$sel:maxCodeSize:Block$sel:schedule:BlockEnv$sel:contracts:Env$sel:chainId:Env$sel:freshAddresses:Env$sel:freshGasVals:EnvTxState$sel:gasprice:TxState$sel:gaslimit:TxState$sel:priorityFee:TxState$sel:origin:TxState$sel:toAddr:TxState$sel:value:TxState$sel:substate:TxState$sel:isCreate:TxState$sel:txReversion:TxState MutableMemoryMemoryConcreteMemorySymbolicMemory FrameState$sel:contract:FrameState$sel:codeContract:FrameState$sel:code:FrameState$sel:pc:FrameState$sel:stack:FrameState$sel:memory:FrameState$sel:memorySize:FrameState$sel:calldata:FrameState$sel:callvalue:FrameState$sel:caller:FrameState$sel:gas:FrameState$sel:returndata:FrameState$sel:static:FrameStateSubState$sel:selfdestructs:SubState$sel:touchedAccounts:SubState$sel:accessedAddresses:SubState!$sel:accessedStorageKeys:SubState$sel:refunds:SubState FrameContextCreationContext CallContext$sel:address:CreationContext$sel:codehash:CreationContext$$sel:createreversion:CreationContext$sel:substate:CreationContext$sel:target:CreationContext$sel:context:CreationContext$sel:offset:CreationContext$sel:size:CreationContext$sel:abi:CreationContext$sel:calldata:CreationContext"$sel:callreversion:CreationContext$sel:subState:CreationContextFrame$sel:context:Frame$sel:state:Frame RuntimeConfig$sel:allowFFI:RuntimeConfig!$sel:overrideCaller:RuntimeConfig$sel:baseState:RuntimeConfig BaseState EmptyBase AbstractBase ForkState$sel:env:ForkState$sel:block:ForkState$sel:cache:ForkState$sel:urlOrAlias:ForkStateVM$sel:result:VM $sel:state:VM$sel:frames:VM $sel:env:VM $sel:block:VM $sel:tx:VM $sel:logs:VM$sel:traces:VM $sel:cache:VM$sel:burned:VM$sel:iterations:VM$sel:constraints:VM$sel:config:VM $sel:forks:VM$sel:currentFork:VMGasVMTypeSymbolicConcreteVMResult Unfinished VMFailure VMSuccess HandleEffectBranchConditionCaseUnknownChoosePleaseChoosePathQueryPleaseFetchContractPleaseFetchSlot PleaseAskSMT PleaseDoFFIEffect PartialExecUnexpectedSymbolicArgMaxIterationsReachedJumpIntoSymbolicCode$sel:pc:UnexpectedSymbolicArg$sel:msg:UnexpectedSymbolicArg$sel:args:UnexpectedSymbolicArg$sel:addr:UnexpectedSymbolicArg"$sel:jumpDst:UnexpectedSymbolicArgEvmError BalanceTooLowUnrecognizedOpcodeSelfDestruction StackUnderrunBadJumpDestinationRevertOutOfGasStackLimitExceededIllegalOverflowStateChangeWhileStaticInvalidMemoryAccessCallDepthLimitReachedMaxCodeSizeExceededMaxInitCodeSizeExceeded InvalidFormatPrecompileFailureReturnDataOutOfBounds NonceOverflow BadCheatCodeNonexistentForkPropPEqPLTPGTPGEqPLEqPNegPAndPOrPImplPBoolSomeExprExprLitVarGVarLitByte IndexWordEqByte JoinBytesPartialFailureSuccessITEAddSubMulDivSDivModSModAddModMulModExpSExMinMaxLTGTLEqGEqSLTSGTEqIsZeroAndOrXorNotSHLSHRSARKeccakSHA256Origin BlockHashCoinbase Timestamp BlockNumber PrevRandaoGasLimitChainIdBaseFeeTxValueBalanceCodeSizeCodeHashLogEntryCSymAddrLitAddrWAddr ConcreteStore AbstractStoreSLoadSStore ConcreteBuf AbstractBufReadWordReadByte WriteWord WriteByte CopySlice BufLength $sel:code:Lit$sel:storage:Lit$sel:balance:Lit$sel:nonce:LitBufVarStoreVarETypeBufStorageLogEWordEAddr EContractByteEndInt512Word512truncateToAddrtoNum.&&.||.<.<=.>.>=.==./=pandporisPBoolunifyCachedContract wordField word64FieldtoChecksumAddress addrFieldaddrFieldMaybe toWord512 fromWord512 maybeLitByte maybeLitWord maybeLitAddrmaybeConcreteStoreword256wordfromBEasBE word256Bytes word160ByteshilotoByte unpackNibbles packNibblestoWord64toIntbssToBs keccakBytesword32keccakkeccak' abiKeccak internalError concatMapM regexMatchesreadNullpadLeftpadLeft'padRight padRight' formatString paddedShowHex untilFixpoint$fTryFromWord256Word32$fTryFromWord256Word8$fTryFromWord256Int256$fTryFromWord256Int$fTryFromWord160Word8$fTryFromIntWord256$fFromWord256Integer$fFromWord32ByteString$fFromWord32Word256$fFromWord8Word256$fFromInt256Integer$fFiniteBitsWord512 $fBitsWord512 $fIxWord512$fHashableWord512 $fReadWord512 $fShowWord512$fIntegralWord512 $fRealWord512 $fNumWord512 $fEnumWord512$fBoundedWord512 $fOrdWord512 $fEqWord512$fDoubleWordWord512$fBinaryWordInt512$fFiniteBitsInt512 $fBitsInt512 $fIxInt512$fHashableInt512 $fReadInt512 $fShowInt512$fIntegralInt512 $fRealInt512 $fNumInt512 $fEnumInt512$fBoundedInt512 $fOrdInt512 $fEqInt512$fDoubleWordInt512$fBinaryWordWord512$fShowFunctionSelector$fToJSONByteStringS$fFromJSONByteStringS$fShowByteStringS$fParseRecordW256$fParseFieldsW256$fParseFieldW256$fFromJSONKeyW256$fFromJSONW256 $fToJSONW256 $fShowW256 $fReadW256$fTryFromWord512W256$fTryFromW256Word64$fTryFromW256Word32$fTryFromW256Word8$fTryFromW256Int256$fTryFromW256Int64$fTryFromW256Int$fTryFromW256FunctionSelector$fTryFromIntegerW256$fTryFromInt256W256$fTryFromIntW256$fFromWord256W256$fFromWord64W256$fFromWord32W256$fFromWord8W256$fFromW256Integer $fFromJSONW64 $fToJSONW64 $fShowW64 $fReadW64$fTryFromW256W64 $fFromW64W256$fParseRecordAddr$fParseFieldsAddr$fParseFieldAddr$fFromJSONKeyAddr$fToJSONKeyAddr$fFromJSONAddr $fToJSONAddr $fShowAddr $fReadAddr$fTryFromW256Addr$fTryFromIntegerAddr$fFromAddrW256$fFromAddrInteger$fMonoidTraces$fSemigroupTraces $fOrdProp$fEqProp $fOrdSomeExpr $fEqSomeExpr $fMonoidCache$fSemigroupCache $fShowMemory $fShowChoose $fShowQuery $fShowNibble$fFromNibbleInt $fNumNibble$fIntegralNibble $fRealNibble $fOrdNibble $fEnumNibble $fEqNibble$fBoundedNibble$fGenericNibble $fGenericVM$fShowRuntimeConfig $fShowTxState$fGenericFrameState$fShowForkState$fGenericForkState $fShowEnv $fGenericEnv $fShowBlock$fGenericBlock $fShowCache$fGenericCache $fEqTraces $fOrdTraces $fShowTraces$fGenericTraces $fEqTrace $fOrdTrace $fShowTrace$fGenericTrace $fEqTraceData$fOrdTraceData$fShowTraceData$fGenericTraceData$fEqFrameContext$fOrdFrameContext$fShowFrameContext$fGenericFrameContext$fShowContract $fEqContract $fOrdContract$fShowContractCode$fEqContractCode$fOrdContractCode$fShowRuntimeCode$fEqRuntimeCode$fOrdRuntimeCode $fEqSubState $fOrdSubState$fShowSubState$fShowEvmError $fEqEvmError $fOrdEvmError$fShowPartialExec$fEqPartialExec$fOrdPartialExec $fNumAddr$fIntegralAddr $fRealAddr $fOrdAddr $fEnumAddr$fEqAddr $fGenericAddr $fBitsAddr$fFiniteBitsAddr$fNumW64 $fIntegralW64 $fRealW64$fOrdW64 $fGenericW64 $fBitsW64$fFiniteBitsW64 $fEnumW64$fEqW64 $fBoundedW64 $fNumW256$fIntegralW256 $fRealW256 $fOrdW256 $fBitsW256 $fGenericW256$fFiniteBitsW256 $fEnumW256$fEqW256 $fBoundedW256$fEqByteStringS$fGenericByteStringS$fBitsFunctionSelector$fNumFunctionSelector$fEqFunctionSelector$fOrdFunctionSelector$fRealFunctionSelector$fEnumFunctionSelector$fIntegralFunctionSelector$fShowGenericOp $fEqGenericOp$fOrdGenericOp$fFunctorGenericOp$fShowBaseState$fShowBranchCondition $fDataInt512$fGenericInt512 $fDataWord512$fGenericWord512 $fShowVMOpts $fShowVMOpts0$fShowFrameState$fShowFrameState0 $fShowFrame $fShowFrame0$fShowVM $fShowVM0$fShowVMResult $fShowEffect $fShowProp$fShowSomeExpr $fOrdExpr$fEqExpr $fShowExpr $fOrdGVar$fEqGVar $fShowGVar$fLabelOptic"tx"kVMVMab$fLabelOptic"traces"kVMVMab$fLabelOptic"state"kVMVMab$fLabelOptic"result"kVMVMab$fLabelOptic"logs"kVMVMab$fLabelOptic"iterations"kVMVMab$fLabelOptic"frames"kVMVMab$fLabelOptic"forks"kVMVMab$fLabelOptic"env"kVMVMab $fLabelOptic"currentFork"kVMVMab $fLabelOptic"constraints"kVMVMab$fLabelOptic"config"kVMVMab$fLabelOptic"cache"kVMVMab$fLabelOptic"burned"kVMVMab$fLabelOptic"block"kVMVMab+$fLabelOptic"static"kFrameStateFrameStateab*$fLabelOptic"stack"kFrameStateFrameStateab/$fLabelOptic"returndata"kFrameStateFrameStateab'$fLabelOptic"pc"kFrameStateFrameStateab/$fLabelOptic"memorySize"kFrameStateFrameStateab+$fLabelOptic"memory"kFrameStateFrameStateab($fLabelOptic"gas"kFrameStateFrameStateab-$fLabelOptic"contract"kFrameStateFrameStateab1$fLabelOptic"codeContract"kFrameStateFrameStateab)$fLabelOptic"code"kFrameStateFrameStateab.$fLabelOptic"callvalue"kFrameStateFrameStateab+$fLabelOptic"caller"kFrameStateFrameStateab-$fLabelOptic"calldata"kFrameStateFrameStateab$$fLabelOptic"value"kTxStateTxStateab*$fLabelOptic"txReversion"kTxStateTxStateab%$fLabelOptic"toAddr"kTxStateTxStateab'$fLabelOptic"substate"kTxStateTxStateab*$fLabelOptic"priorityFee"kTxStateTxStateab%$fLabelOptic"origin"kTxStateTxStateab'$fLabelOptic"isCreate"kTxStateTxStateab'$fLabelOptic"gasprice"kTxStateTxStateab'$fLabelOptic"gaslimit"kTxStateTxStateab0$fLabelOptic"touchedAccounts"kSubStateSubStateab.$fLabelOptic"selfdestructs"kSubStateSubStateab($fLabelOptic"refunds"kSubStateSubStateab4$fLabelOptic"accessedStorageKeys"kSubStateSubStateab2$fLabelOptic"accessedAddresses"kSubStateSubStateab$fLabelOptic"path"kCacheCacheab"$fLabelOptic"fetched"kCacheCacheab$$fLabelOptic"tracedata"kTraceTraceab$fLabelOptic"opIx"kTraceTraceab#$fLabelOptic"contract"kTraceTraceab"$fLabelOptic"value"kVMOptsVMOptsab)$fLabelOptic"txAccessList"kVMOptsVMOptsab&$fLabelOptic"timestamp"kVMOptsVMOptsab%$fLabelOptic"schedule"kVMOptsVMOptsab($fLabelOptic"priorityFee"kVMOptsVMOptsab'$fLabelOptic"prevRandao"kVMOptsVMOptsab+$fLabelOptic"otherContracts"kVMOptsVMOptsab#$fLabelOptic"origin"kVMOptsVMOptsab#$fLabelOptic"number"kVMOptsVMOptsab($fLabelOptic"maxCodeSize"kVMOptsVMOptsab%$fLabelOptic"gasprice"kVMOptsVMOptsab%$fLabelOptic"gaslimit"kVMOptsVMOptsab $fLabelOptic"gas"kVMOptsVMOptsab#$fLabelOptic"create"kVMOptsVMOptsab%$fLabelOptic"contract"kVMOptsVMOptsab%$fLabelOptic"coinbase"kVMOptsVMOptsab$$fLabelOptic"chainId"kVMOptsVMOptsab#$fLabelOptic"caller"kVMOptsVMOptsab%$fLabelOptic"calldata"kVMOptsVMOptsab*$fLabelOptic"blockGaslimit"kVMOptsVMOptsab&$fLabelOptic"baseState"kVMOptsVMOptsab$$fLabelOptic"baseFee"kVMOptsVMOptsab%$fLabelOptic"allowFFI"kVMOptsVMOptsab$$fLabelOptic"address"kVMOptsVMOptsab $fLabelOptic"state"kFrameFrameab"$fLabelOptic"context"kFrameFrameab/$fLabelOptic"target"kFrameContextFrameContextab1$fLabelOptic"substate"kFrameContextFrameContextab1$fLabelOptic"subState"kFrameContextFrameContextab-$fLabelOptic"size"kFrameContextFrameContextab/$fLabelOptic"offset"kFrameContextFrameContextab8$fLabelOptic"createreversion"kFrameContextFrameContextab0$fLabelOptic"context"kFrameContextFrameContextab1$fLabelOptic"codehash"kFrameContextFrameContextab6$fLabelOptic"callreversion"kFrameContextFrameContextab1$fLabelOptic"calldata"kFrameContextFrameContextab0$fLabelOptic"address"kFrameContextFrameContextab,$fLabelOptic"abi"kFrameContextFrameContextab($fLabelOptic"storage"kContractContractab,$fLabelOptic"origStorage"kContractContractab($fLabelOptic"opIxMap"kContractContractab&$fLabelOptic"nonce"kContractContractab)$fLabelOptic"external"kContractContractab)$fLabelOptic"codehash"kContractContractab($fLabelOptic"codeOps"kContractContractab%$fLabelOptic"code"kContractContractab($fLabelOptic"balance"kContractContractab#$fLabelOptic"freshGasVals"kEnvEnvab%$fLabelOptic"freshAddresses"kEnvEnvab $fLabelOptic"contracts"kEnvEnvab$fLabelOptic"chainId"kEnvEnvab$$fLabelOptic"timestamp"kBlockBlockab#$fLabelOptic"schedule"kBlockBlockab%$fLabelOptic"prevRandao"kBlockBlockab!$fLabelOptic"number"kBlockBlockab&$fLabelOptic"maxCodeSize"kBlockBlockab#$fLabelOptic"gaslimit"kBlockBlockab#$fLabelOptic"coinbase"kBlockBlockab"$fLabelOptic"baseFee"kBlockBlockab9$fLabelOptic"overrideCaller"kRuntimeConfigRuntimeConfigab4$fLabelOptic"baseState"kRuntimeConfigRuntimeConfigab3$fLabelOptic"allowFFI"kRuntimeConfigRuntimeConfigabTraversableTermmapTermfoldTermfoldProp foldEContract foldContractfoldCodefoldExprmapPropmapProp'mapExprmapExprMmapPropM mapEContractM mapContractMmapCodeM$fTraversableTermProp$fTraversableTermExprRLPBSListsliceitemInfo rlpdecode rlplengths rlpencode encodeLenrlpListoctets octetsFull octets160 rlpWord256 rlpWordFull rlpAddrFull rlpWord160 $fShowRLP$fEqRLP ConstState$sel:values:ConstState$sel:canBeSat:ConstState StorageType SmallSlotArrayMapMixedUNK ArraySlotZeroArraySlotWithOffset Keccak64Bytes MappingSlotmaxLitop1op2op3normArgsaddsubmuldivsdivmodsmodaddmodmulmodexpsexltgtleqgeqsltsgteqiszeroandorxornotshlshrsarreadByte readBytesreadWordreadWordFromBytesmaxBytes copySlice writeByte writeWord bufLength bufLengthEnv minLengthconcretePrefix word256AttakedroptoListfromList simplifyReads stripWrites readStorage' readStorage idsDontMatchslotPosstructureArraySlotslitToArrayPreimage writeStoragegetAddr getLogicalIdxsafeToDecomposedecomposeStoragesimplify simplifyProps simplifyProp flattenPropsremRedundantPropslitAddr exprToAddr wordToAddrlitCodeto512 isLitByte isLitWord isSuccess isFailure isPartial indexWordpadByte bytesToW256 padBytesLeft joinByteseqByteminmax numBranchesallLit containsNodeinRange preImages constFoldPropconcKeccakSimpExprconcKeccakPropsconcKeccakOnePass $fMonoidExpr$fSemigroupExpr$fShowConstState$fShowStorageType$fEqStorageType intToOpNameopStringreadOpgetOpkeccakAssumptions keccakCompute$fShowKeccakStore byteStringSliceWithDefaultZeroes sliceMemory writeMemory createAddresscreate2AddressStoreEnvBufEnv eliminateExpreliminateProps$fShowBuilderStateassembleAbiValsNoValsCAbiSAbiSolErrorEventIndexed NotIndexed Anonymity Anonymous NotAnonymousAbiKindDynamicStaticAbiType AbiUIntType AbiIntTypeAbiAddressType AbiBoolType AbiBytesTypeAbiBytesDynamicType AbiStringTypeAbiArrayDynamicType AbiArrayType AbiTupleTypeAbiFunctionTypeAbiValueAbiUIntAbiInt AbiAddressAbiBoolAbiBytesAbiBytesDynamic AbiStringAbiArrayDynamicAbiArrayAbiTuple AbiFunctionSigabiTypeSolidityabiKind abiValueTypegetAbiputAbi getAbiSeqencodeAbiValuedecodeAbiValueselector abiMethod parseTypeNameemptyAbi makeAbiValue parseAbiValue decodeBufdecodeStaticArgs genAbiValue$fArbitraryAbiType $fShowAbiType$fArbitraryAbiValue$fShowAbiValue $fReadBoolz $fShowAbiVals$fShowSolError $fOrdSolError $fEqSolError$fGenericSolError $fShowEvent $fOrdEvent $fEqEvent$fGenericEvent $fShowIndexed $fOrdIndexed $fEqIndexed$fGenericIndexed$fShowAnonymity$fOrdAnonymity $fEqAnonymity$fGenericAnonymity $fShowAbiKind $fReadAbiKind $fEqAbiKind $fOrdAbiKind$fGenericAbiKind $fShowSig$fEqSig$fReadAbiValue $fEqAbiValue $fOrdAbiValue$fGenericAbiValue $fReadAbiType $fEqAbiType $fOrdAbiType$fGenericAbiType $fDataAbiTypeLanguageSolidityYulCodeTypeCreationRuntimeSrcMapSM$sel:offset:SM$sel:length:SM $sel:file:SM $sel:jump:SM$sel:modifierDepth:SMJumpTypeJumpIntoJumpFrom JumpRegular Reference$sel:start:Reference$sel:length:Reference SourceCache$sel:files:SourceCache$sel:lines:SourceCache$sel:asts:SourceCache ProjectType DappTools CombinedJSONFoundry FoundryStdLib BuildOutput$sel:contracts:BuildOutput$sel:sources:BuildOutput Contracts MutabilityPureView NonPayablePayableMethod$sel:output:Method$sel:inputs:Method$sel:name:Method$sel:methodSignature:Method$sel:mutability:Method SolcContract!$sel:runtimeCodehash:SolcContract"$sel:creationCodehash:SolcContract$sel:runtimeCode:SolcContract$sel:creationCode:SolcContract$sel:contractName:SolcContract#$sel:constructorInputs:SolcContract$sel:abiMap:SolcContract$sel:eventMap:SolcContract$sel:errorMap:SolcContract%$sel:immutableReferences:SolcContract$sel:storageLayout:SolcContract$sel:runtimeSrcmap:SolcContract $sel:creationSrcmap:SolcContractSlotTypeStorageMapping StorageValue StorageItem$sel:slotType:StorageItem$sel:offset:StorageItem$sel:slot:StorageItem makeSrcMapsreadBuildOutputmakeSourceCache lineSubrangereadSolcyul yulRuntimesolidity solcRuntime functionAbireadJSON readStdJSON signatureparseMethodInputcontainsLinkerHolesolcstdjsonstripBytecodeMetadatastripBytecodeMetadataSymastIdMap astSrcMap$fReadSlotType$fShowSlotType$fMonoidSourceCache$fSemigroupSourceCache$fFromJSONReference$fMonoidBuildOutput$fSemigroupBuildOutput$fToJSONStandardJSON$fShowLanguage$fShowCodeType $fEqCodeType $fOrdCodeType$fShowSrcMapParseState$fShowBuildOutput$fEqBuildOutput$fShowContracts $fEqContracts$fSemigroupContracts$fMonoidContracts$fShowSolcContract$fEqSolcContract$fGenericSolcContract $fShowSrcMap $fEqSrcMap $fOrdSrcMap$fGenericSrcMap$fShowJumpType $fEqJumpType $fOrdJumpType$fGenericJumpType$fShowReference $fEqReference$fShowSourceCache$fEqSourceCache$fGenericSourceCache$fEqProjectType$fShowProjectType$fReadProjectType$fParseFieldProjectType $fShowSources $fEqSources$fSemigroupSources$fMonoidSources $fShowSrcFile $fEqSrcFile $fOrdSrcFile $fShowAsts$fEqAsts$fSemigroupAsts $fMonoidAsts $fShowMethod $fEqMethod $fOrdMethod$fGenericMethod$fShowMutability$fEqMutability$fOrdMutability$fGenericMutability$fShowStorageItem$fEqStorageItem $fEqSlotType deriveAddrsignethsignecrec DappContext$sel:info:DappContext$sel:env:DappContextCode $sel:raw:Code$sel:immutableLocations:CodeDappInfo$sel:root:DappInfo$sel:solcByName:DappInfo$sel:solcByHash:DappInfo$sel:solcByCode:DappInfo$sel:sources:DappInfo$sel:unitTests:DappInfo$sel:abiMap:DappInfo$sel:eventMap:DappInfo$sel:errorMap:DappInfo$sel:astIdMap:DappInfo$sel:astSrcMap:DappInfodappInfo emptyDappunitTestMarkerAbifindAllUnitTestsmkSig findUnitTestsunitTestMethodsFilteredunitTestMethods traceSrcMapsrcMapfindSrc lookupCode compareCodeshowTraceLocation srcMapCodePos srcMapCode $fShowCode FrameResult FrameReturned FrameReverted FrameErrored CheatAction blankStatebytecodecurrentContractmakeVmunknownContractabstractContract emptyContractinitialContract isCreationnextexec1transfer callChecksprecompiledContractexecutePrecompile truncpadlit lazySliceparseModexpLengthisZero asIntegernooppushTopushToSequencegetCodeLocationquerychoose fetchAccount accessStorage accountExists accountEmptyfinalize loadContract limitStack notStatic forceAddr forceConcreteforceConcreteAddrforceConcreteAddr2forceConcrete2forceConcreteBufrefundunRefund touchAccount selfdestruct accessAndBurnaccessAccountForGasaccessStorageForGas cheatCodecheat cheatActions delegateCall collisioncreate parseInitCode replaceCodereplaceCodeOfSelf resetStatevmErrorwrapunderrun finishFrameaccessUnboundedMemoryRangeaccessMemoryRangeaccessMemoryWordcopyBytesToMemorycopyCallBytesToMemory readMemorywithTraceLocation pushTrace insertTracepopTracezipperRootForest traceForest traceForest' traceContext traceTopLogpushpushSympushAddrstackOp1stackOp2stackOp3 checkJumpnoJumpIntoInitDataisValidJumpDestopSize mkOpIxMapvmOpvmOpIx mkCodeOpsconcreteModexpGasFeecostOfPrecompile memoryCosthashcodeopslencodelentoBufcodeloc freshSymAddrisPrecompileAddrceilDiv allButOne64thlog2 freezeMemory symbolifysymbolifyFrameStatesymbolifyFramesymbolifyResultforceLitburn$fVMOpsConcrete$fVMOpsSymbolic$fShowFrameResult showWordExactshowWordExplanationprettyIfConcreteWord showAbiValue textValues parenthesise showValues showValueshowCall showError formatBytes formatBinary showTraceTreeshowTraceTree'contractNamePartcontractPathPartprettyvmresultindent formatPartialformatSomeExpr formatExpr formatPropstrip0xstrip0x' hexByteStringhexTextbsToHexshowVal$fShowSignedness Transaction$sel:txdata:Transaction$sel:gasLimit:Transaction$sel:gasPrice:Transaction$sel:nonce:Transaction$sel:r:Transaction$sel:s:Transaction$sel:toAddr:Transaction$sel:v:Transaction$sel:value:Transaction$sel:txtype:Transaction$sel:accessList:Transaction"$sel:maxPriorityFeeGas:Transaction$sel:maxFeePerGas:Transaction$sel:chainId:TransactionTxTypeLegacyTransactionAccessListTransactionEIP1559TransactionAccessListEntry$sel:address:AccessListEntry $sel:storageKeys:AccessListEntryemptyTransaction txAccessMapsender signingDataaccessListPrice txGasCost accountAt newAccountsetupTxinitTx$fFromJSONAccessListEntry$fToJSONAccessListEntry$fToJSONTxType$fFromJSONTransaction$fToJSONTransaction$fShowTransaction$fGenericTransaction $fShowTxType $fEqTxType$fGenericTxType$fShowAccessListEntry$fGenericAccessListEntry ethrunAddressvmForEthrunCreationexecrun execWhileApp$sel:config:EnvTTY writeOutputwriteErrConfig$sel:dumpQueries:Config$sel:dumpExprs:Config$sel:dumpEndStates:Config$sel:debug:Config$sel:abstRefineArith:Config$sel:abstRefineMem:Config$sel:dumpTrace:Config$sel:numCexFuzz:Config$sel:onlyCexFuzz:Config ReadConfig readConfig defaultConfigwriteTraceDapp writeTrace defaultEnvrunEnvrunApp $fTTYReaderT$fReadConfigReaderT $fShowConfig $fEqConfig AbstState$sel:words:AbstState$sel:count:AbstStateSMT2 RefinementEqsSMTCex$sel:vars:SMTCex$sel:addrs:SMTCex$sel:buffers:SMTCex$sel:store:SMTCex$sel:blockContext:SMTCex$sel:txContext:SMTCex CompressedBufBaseWrite$sel:byte:Base$sel:length:Base $sel:idx:Base$sel:next:BaseBufModelCompFlatCexVars$sel:calldata:CexVars$sel:addrs:CexVars$sel:buffers:CexVars$sel:storeReads:CexVars$sel:blockContext:CexVars$sel:txContext:CexVars flattenBufscollapsegetVar formatSMT2declareIntermediatesabstractAwayPropssmt2Line assertPropsassertPropsNoSimpreferencedAbstractStoresreferencedWAddrsreferencedBufsreferencedVarsreferencedFrameContextreferencedBlockContextfindStorageReadsfindBufferAccess assertReadsdiscoverMaxReads declareBufs declareVars declareAddrsdeclareFrameContextdeclareAbstractStoresdeclareBlockContextprelude exprToSMTspzeroone propToSMT expandExp concatBytes writeBytesencodeConcreteStore storeName formatEAddr parseAddr parseW256 parseIntegerparseW8parseSCparseErrparseVar parseEAddr parseBlockCtx parseTxCtxgetAddrsgetVarsgetOne queryMaxReadsgetBufsgetStore queryValueinterpretNDArrayinterpret1DArray$fMonoidCexVars$fSemigroupCexVars$fMonoidRefinementEqs$fSemigroupRefinementEqs $fMonoidSMT2$fSemigroupSMT2$fShowAbstState$fEqSMT2 $fShowSMT2$fEqRefinementEqs$fShowRefinementEqs $fEqSMTCex $fShowSMTCex $fEqBufModel$fShowBufModel$fEqCompressedBuf$fShowCompressedBuf $fEqCexVars $fShowCexVarsCollectStorage$sel:addrs:CollectStorage$sel:keys:CollectStorage$sel:vals:CollectStorage CollectBufs$sel:bufs:CollectBufs CollectVars$sel:vars:CollectVars$sel:vals:CollectVars tryCexFuzzfilterCorrectKeccaksubstituteEWord substituteBufsubstituteStores initVarsState findVarProp extractVars initBufsState extractBufs findBufPropinitStorageStateextractStoragefindStoragePropCompfindStoragePropInnergetvals getStores getRndW256$fSemigroupCollectStorage$fShowCollectStorage$fShowCollectBufs$fShowCollectVarsParLParRParCheckSatResultSatUnsatErrorTask$sel:script:Task$sel:resultChan:Task SolverGroupSolverInstance$sel:solvertype:SolverInstance$sel:stdin:SolverInstance$sel:stdout:SolverInstance$sel:process:SolverInstanceSolverZ3CVC5BitwuzlaCustomisSatisErrisUnsatcheckSat writeSMT2File withSolversgetModel mkTimeout solverArgs spawnSolver stopSolver sendScript checkCommand sendCommandsendLine sendLine'getValue readSExpr splitSExprgetSExpr $fShowSolver$fShowCheckSatResult$fEqCheckSatResultFetcherToRPCtoRPCRpcInfoLatestRpcQuery QueryCode QueryBlock QueryBalance QueryNonce QuerySlot QueryChainIdrpcreadText fetchQuery parseBlockfetchWithSessionfetchContractWithSessionfetchSlotWithSessionfetchBlockWithSessionfetchBlockFromfetchContractFrom fetchSlotFromfetchChainIdFromhttporacle checkBranch$fToRPCBlockNumber $fToRPCBool $fToRPCW256 $fToRPCAddr$fShowBlockNumber$fEqBlockNumber$fShowRpcQueryStepperActionExecWaitAskIOActwaitaskevmevmIO execFullyrunFullyenter interpret UnsatCache Postcondition PreconditionCalldataFragmentStDyVeriOpts$sel:simp:VeriOpts$sel:maxIter:VeriOpts$sel:askSmtIters:VeriOpts$sel:loopHeuristic:VeriOpts$sel:rpcInfo:VeriOpts EquivResult VerifyResult ProofResultQedCexTimeout LoopHeuristicNaive StackBased isTimeoutisCexisQeddefaultVeriOpts rpcVeriOpts extractCexbool symAbiArg symCalldatacdLen writeSelectorcombineFragmentsisSt abstractVM loadSymVMmaxIterationsReachedaskSmtItersReached isLoopHead checkAssertgetExprcheckAssertionsdefaultPanicCodes allPanicCodespanicMsg mkCalldataverifyContractrunExpr toEContract flattenExpr reachable extractProps getPartialsverify expandCexequivalenceCheckequivalenceCheck'both' produceModels showModel formatCexprettyCalldatadefaultSymbolicValuessubModelsubVarssubAddrssubBufs subStoresgetCex getTimeout$fShowCalldataFragment$fEqCalldataFragment $fEqVeriOpts$fShowVeriOpts$fShowProofResult$fEqProofResult$fEqLoopHeuristic$fShowLoopHeuristic$fReadLoopHeuristic$fParseFieldLoopHeuristic$fParseFieldsLoopHeuristic$fParseRecordLoopHeuristic$fGenericLoopHeuristic ABIMethod TestVMParams$sel:address:TestVMParams$sel:caller:TestVMParams$sel:origin:TestVMParams$sel:gasCreate:TestVMParams$sel:gasCall:TestVMParams$sel:baseFee:TestVMParams$sel:priorityFee:TestVMParams$sel:balanceCreate:TestVMParams$sel:coinbase:TestVMParams$sel:number:TestVMParams$sel:timestamp:TestVMParams$sel:gaslimit:TestVMParams$sel:gasprice:TestVMParams$sel:maxCodeSize:TestVMParams$sel:prevrandao:TestVMParams$sel:chainId:TestVMParamsUnitTestOptions$sel:rpcInfo:UnitTestOptions$sel:solvers:UnitTestOptions$sel:verbose:UnitTestOptions$sel:maxIter:UnitTestOptions $sel:askSmtIters:UnitTestOptions$sel:smtTimeout:UnitTestOptions$sel:solver:UnitTestOptions$sel:match:UnitTestOptions$sel:dapp:UnitTestOptions$sel:testParams:UnitTestOptions$sel:ffiAllowed:UnitTestOptionsdefaultGasForCreatingdefaultGasForInvokingdefaultBalanceForTestContractdefaultMaxCodeSize makeVeriOptsunitTestinitializeUnitTestrunUnitTestContractsymRun allBranchRev symFailure execSymTestcheckSymFailures indentLines passOutput failOutputformatTestLogs formatTestLogabiCall makeTxCallinitialUnitTestVm paramsFromRpctick EthjetContexteliminateExpr'eliminateProp'eliminateProps'SourcesSrcFileAsts findJsonFilesfilterMetadatareadFoundryJSONversion getBinDir getLibDir getDynLibDir getDataDir getLibexecDirgetDataFileName getSysconfDir