h&C      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 ! Safe-Inferred"%&($hevmThis is an easy way to force full evaluation of a value inside of the IO monad, being essentially just the composition of evaluate and force. Safe-Inferred"%&($2?543210/.-,+*)('&%$#"!  6789:;<=>?@?543210/.-,+*)('&%$#"!  6789:;<=>?@ Safe-Inferred"%&()BhevmB renders a  as a multi-line  complete with addressing, hex digits, and ASCII representation. Sample output Length: 100 (0x64) bytes 0000: 4b c1 ad 8a 5b 47 d7 57 48 64 e7 cc 5e b5 2f 6e K...[G.WHd..^./n 0010: c5 b3 a4 73 44 3b 97 53 99 2d 54 e7 1b 2f 91 12 ...sD;.S.-T../.. 0020: c8 1a ff c4 3b 2b 72 ea 97 e2 9f e2 93 ad 23 79 ....;+r.......#y 0030: e8 0f 08 54 02 14 fa 09 f0 2d 34 c9 08 6b e1 64 ...T.....-4..k.d 0040: d1 c5 98 7e d6 a1 98 e2 97 da 46 68 4e 60 11 15 ...~......FhN`.. 0050: d8 32 c6 0b 70 f5 2e 76 7f 8d f2 3b ed de 90 c6 .2..p..v...;.... 0060: 93 12 9c e1 ....hevm displays a number in hexidecimal and pads the number with 0 so that it has a minimum length of w.ChevmC converts a  to a - showing the octets grouped in 32-bit words. Sample output 4b c1 ad 8a 5b 47 d7 57hevm returns  for non-control ascii characters. These characters will all fit in a single character when rendered.hevm( breaks up a list into sublists of size n&. The last group may be smaller than n elements. When n8 less not positive the list is returned as one sublist.BCBC Safe-Inferred"%&(+?hevm8Opaque representation of the C library's context struct.Dhevm5Run a given precompiled contract using the C library.Dhevm&The number of the precompiled contracthevmThe input bufferhevmThe desired output sizehevmHopefully, the output bufferDD Safe-Inferred"%&(,bEhevmTurn a list state value into a widget given an item drawing function.Ehevm1Rendering function, True for the selected elementhevmWhether the list has focushevmThe List to be renderedhevmrendered widgetEFEF Safe-Inferred"%&()1<6hevm=Expr implements an abstract respresentation of an EVM programThis 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 zeroBufs can be read from with: - ReadByte idx buf: read the byte at idx from buf - ReadWord idx buf: read the byte at idx from bufBufs 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 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 Y, , 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.hevmRight padding / truncating truncpad :: Int -> [SWord 8] -> [SWord 8] truncpad n xs = if m > n then take n xs else mappend xs (replicate (n - m) 0) where m = length xsGHIKJLMNWUTSRQPOVX~}|wutrnlkjhfec_^]\[d`sybYZoz{igmxavqpX~}|wutrnlkjhfec_^]\[d`sybYZoz{igmxavqpNWUTSRQPOVLMIKJGH32444444.Generic traversal functions for Expr datatypes Safe-Inferred "%&(1; hevmRecursively 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 hasslehevmRecursively applies a given function to every node in a given expr instance Recursion schemes do this & a lot more, but defining them over GADT's isn't worth the hassle  Safe-Inferred"%&(;R  Safe-Inferred"%&(  Safe-Inferred "%&(1IhevmIf 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 expresion if nescessary. Note that a Buf is an infinite structure, so reads outside of the bounds of a ConcreteBuf return 0. This is inline with the semantics of calldata and memory, but not of returndata.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 expresion will be returned.hevm=If a buffer has a concrete prefix, we return it's length herehevm 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.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.hevmSimple recursive match based AST simplification Note: may not terminate!hevm,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? Safe-Inferred "%&(J-Common subexpression elimination for Expr ast Safe-Inferred "%&(1LXhevm.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 PropUtilities for building and executing SMT queries from Expr instances Safe-Inferred "%&()1Rhevm#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 writtenhevm)A channel representing a group of solvershevmA running solver instancehevmSupported solvershevmReads all intermediate variables from the builder state and produces SMT declaring them as constantshevm-Arguments used when spawing a solver instancehevmSpawns a solver instance, and sets the various global config options that we use for our querieshevm*Cleanly shutdown a running solver instnacehevmSends 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 bufferhevmSends a string to the solver and appends a newline, returns the first available line from the output bufferhevmSends a string to the solver and appends a newline, doesn't return stdouthevmReturns a string representation of the model for the requested variablehevm1Reads lines from h until we have a balanced sexprhevmStores a region of src into dsthevm:Unrolls an exponentiation into a series of multiplicationshevm4Concatenates a list of bytes into a larger bitvectorhevm4Concatenates a list of bytes into a larger bitvector Safe-Inferred "%&(1ThevmDecode a sequence type (e.g. tuple / array). Will fail for non sequence typeshevmPretty-print some .99 Safe-Inferred"%&(1=Yhevm&specified to not read blockchain statehevm,specified to not modify the blockchain statehevm,function does not accept Ether - the defaulthevmfunction accepts EtherhevmWhen 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. Safe-Inferred"%&()1n0/hevmData about the blockhevmVarious environmental datahevmWhen doing symbolic execution, we have three different ways to model the storage of contracts. This determines not only the initial contract storage model but also how RPC or state fetched contracts will be modeled.hevmUses  Storage. Reading / Writing from abstract locations causes a runtime failure. Can be nicely combined with RPC.hevmUses  Storage. Reading / Writing never reaches RPC, but always done using an SMT array with no default value.hevmUses  Storage. Reading / Writing never reaches RPC, but always done using an SMT array with 0 as the default value.hevmA contract can either have concrete or symbolic storage depending on what type of execution we are doing data Storage = Concrete (Map Word Expr EWord) | Symbolic [(Expr EWord, Expr EWord)] (SArray (WordN 256) (WordN 256)) deriving (Show)The state of a contracthevmWe 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...hevm Constructor code, during contract creationhevmInstance code, after contract creationhevm+The "accrued substate" across a transactionhevm(The state that spans a whole transactionhevm:The "registers" of the VM along with memory and data stackhevmCall/create infohevm(An entry in the VM's "call/create stack"hevm$A way to specify an initial VM statehevmThe cache is data that can be persisted for efficiency: any expensive query that is constant at least within a block.hevm5The possible return values of a `is unique` SMT queryhevm)The possible return values of a SMT queryhevmAlias for the type of e.g. exec1.hevmQueries halt execution until resolved through RPC calls or SMT querieshevm%The state of a stepwise EVM executionhevm"The possible result states of a VMhevmAn operation failedhevm$Reached STOP, RETURN, or end-of-codehevmEVM failure modes 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. 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 hevm2Burn gas, failing if insufficient gas is available 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 hevmWe don't wanna introduce the machinery needed to sign with a random nonce, so we just use the same nonce every time (420). This is obviusly very insecure, but fine for testing purposes. 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  of the VM execution. hevmReads 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 hevmContract addresshevmStorage slot keyhevm Continuation    Safe-Inferred"%&(un 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 hevm/Abstract representation of an RPC fetch request hevmChecks 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  "%&(1x/   Safe-Inferred"%&(x   Safe-Inferred"%&(y   Safe-Inferred "%&()1{J hevm'Type alias for an operational monad of Action hevm-The instruction type of the operational monad hevm6Keep executing until an intermediate result is reached hevm5Keep executing until an intermediate state is reached hevmWait for a query to be resolved hevmMultiple things can happen hevmEmbed a VM state transformation hevmPerform an IO action hevm4Run the VM until final result, resolving all queries hevm Run the VM until its final state   Safe-Inferred"%&({  Safe-Inferred "%&(|Y hevm1bytecode modulo immutables, to identify contracts5 5  Safe-Inferred"%&(}]  Safe-Inferred "%&(1}   Safe-Inferred "%&(1/ hevm%Abstract calldata argument generation hevmGenerates 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 representing the possible executions 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-require hevmBy default hevm checks for all assertions except those which result from arithmetic overflow hevm?Produces the revert message for solc >=0.8 assertion violations hevmStepper that parses the result of Stepper.runFully into an Expr End hevmConverts 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 properly hevmEvaluate the provided proposition down to its most concrete result hevm,Extract contraints stored in Expr End nodes hevmSymbolically 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. hevmTakes a buffer and a Cex and replaces all abstract values in the buf with concrete ones from the Cex7 7  Safe-Inferred "%&(1P hevm*This is like an unresolved source mapping. hevm&Generate VeriOpts from UnitTestOptions hevm$Top level CLI endpoint for dapp-test hevmAssuming a constructor is loaded, this stepper will run the constructor to create the test contract, give it an initial balance, and run `setUp()'. hevmAssuming a test contract is loaded and initialized, this stepper will run the specified test method and return whether it succeeded. hevm;Randomly generates the calldata arguments and runs the test hevmRuns an invariant test, calls the invariant before execution begins hevm/Define the thread spawner for normal test cases hevm2Define the thread spawner for property based tests hevm,Define the thread spawner for symbolic tests $Helpers for repl driven hevm hacking Safe-Inferred "%&(1S hevm1Builds the Expr for the given evm bytecode object  ! Safe-Inferred "%&(  Safe-Inferred "%&(1 hevmEach step command in the terminal should finish immediately with one of these outcomes. hevmProgram finished hevmTook one step; more steps to go hevmRun a specific number of steps hevm Finish when a VM predicate holds hevm This turns a Stepper into a state action usable from within the TTY loop, yielding a  StepOutcome depending on the StepMode.  "#$%&''()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijjkklmmnopqrstuvwxyz{|}~{                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              !!!!!!!!hevm-0.50.2-inplace EVM.Format EVM.DemandEVM.FeeSchedule EVM.HexdumpEVM.PrecompiledEVM.TTYCenteredList EVM.TypesEVM.TraversalsEVM.RLP EVM.PatriciaEVM.Op EVM.KeccakEVM.Expr EVM.ConcreteEVM.CSEEVM.SMTEVM.ABI EVM.SolidityEVMEVM.Transaction EVM.Fetch EVM.Facts EVM.Facts.GitEVM.Exec EVM.Stepper EVM.DebugEVM.DappEVM.StorageLayout EVM.SymExec EVM.UnitTestEVM.DevEVM.TTY Paths_hevm&tree-view-0.5.1-JWemnWBJYU254eYiAWWoizData.Tree.ViewshowTreedemandEIP FeeScheduleg_zerog_base g_verylowg_lowg_midg_high g_extcode g_balanceg_sload g_jumpdestg_ssetg_sresetr_sclearg_selfdestructg_selfdestruct_newaccountr_selfdestructg_create g_codedepositg_call g_callvalue g_callstipend g_newaccountg_exp g_expbyteg_memory g_txcreate g_txdatazerog_txdatanonzero g_transactiong_log g_logdata g_logtopicg_sha3 g_sha3wordg_copy g_blockhash g_extcodehash g_quaddivisorg_ecaddg_ecmulg_pairing_pointg_pairing_baseg_froundr_block g_cold_sloadg_cold_account_accessg_warm_storage_readg_access_list_addressg_access_list_storage_keyeip150eip160 homestead metropoliseip1108eip1884eip2028eip2200istanbuleip2929berlin$fShowFeeSchedule prettyHex simpleHexexecute renderListdrawListElementsNibbleAddraddressWord160 ByteStringSPropPEqPLTPGTPGEqPLEqPNegPAndPOrPBoolExprLitVarGVarLitByte IndexWordEqByte JoinBytesRevertFailureReturnITEAddSubMulDivSDivModSModAddModMulModExpSExMinLTGTLEqGEqSLTSGTEqIsZeroAndOrXorNotSHLSHRSARKeccakSHA256Origin BlockHashCoinbase Timestamp BlockNumber PrevRandaoGasLimitChainIdBaseFee CallValueCallerAddressBalance SelfBalanceGasCodeSize ExtCodeHashLogEntryCreateCreate2CallCallCode DelegeateCall EmptyStore ConcreteStore AbstractStoreSLoadSStore ConcreteBuf AbstractBufReadWordReadByte WriteWord WriteByte CopySlice BufLengthBufVarStoreVarErrorInvalidIllegalOverflowStackLimitExceededInvalidMemoryAccessBadJumpDestination SelfDestructTmpErrETypeBufStorageLogEWordByteEndW256Int512Word512.&&.||.<.<=.>.>=.==./=unlit unlitByte maybeLitWordtoChecksumAddressstrip0xstrip0x' hexByteStringhexTextreadNreadNull wordField word64Field addrFieldaddrFieldMaybe dataField toWord512 fromWord512numpadLeft padLeftStrpadRight padRight'padLeft'word256wordbyteAtfromBEasBE word256Bytes word160ByteshilotoByte unpackNibbles packNibblestoWord64toInt keccakBytesword32keccakkeccak' abiKeccak concatMapM regexMatches$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$fParseRecordW256$fParseFieldsW256$fParseFieldW256$fFromJSONKeyW256$fFromJSONW256 $fToJSONW256 $fShowW256 $fReadW256 $fOrdProp$fEqProp$fToJSONByteStringS$fShowByteStringS$fParseRecordAddr$fParseFieldsAddr$fParseFieldAddr$fFromJSONKeyAddr$fFromJSONAddr $fShowAddr $fReadAddr $fShowNibble $fNumNibble$fIntegralNibble $fRealNibble $fOrdNibble $fEnumNibble $fEqNibble$fBoundedNibble$fGenericNibble $fNumAddr$fIntegralAddr $fRealAddr $fOrdAddr $fEnumAddr$fEqAddr $fGenericAddr $fBitsAddr$fFiniteBitsAddr$fEqByteStringS $fShowError $fEqError $fOrdError $fNumW256$fIntegralW256 $fRealW256 $fOrdW256 $fGenericW256 $fBitsW256$fFiniteBitsW256 $fEnumW256$fEqW256 $fBoundedW256 $fDataInt512$fGenericInt512 $fDataWord512$fGenericWord512 $fShowProp $fOrdExpr$fEqExpr $fShowExpr $fOrdGVar$fEqGVar $fShowGVarfoldPropfoldExprmapPropmapExprmapExprMmapPropMRLPBSListsliceitemInfo rlpdecode rlplengths rlpencode encodeLenrlpListoctets octetsFull octets160 rlpWord256 rlpWordFull rlpAddrFull rlpWord160 $fShowRLP$fEqRLPMapDBTrieNodeDBNodeEmptyShortcutFullRefHashLiteralPathDBKVPutGetinsertDBlookupDBrunDB encodePathrlpRefrlpNodeputNodegetNode lookupPathgetValemptyRef emptyRefs addPrefix insertRefupdatedeleteinsertlookupInrunTrierunMapDB insertValuescalcRoot $fShowRef$fShowDB $fShowNode$fEqNode$fEqRef $fFunctorDB$fApplicativeDB $fMonadDB $fFunctorKVOpOpStopOpAddOpMulOpSubOpDivOpSdivOpModOpSmodOpAddmodOpMulmodOpExp OpSignextendOpLtOpGtOpSltOpSgtOpEqOpIszeroOpAndOpOrOpXorOpNotOpByteOpShlOpShrOpSarOpSha3 OpAddress OpBalanceOpOriginOpCaller OpCallvalueOpCalldataloadOpCalldatasizeOpCalldatacopy OpCodesize OpCodecopy OpGasprice OpExtcodesize OpExtcodecopyOpReturndatasizeOpReturndatacopy OpExtcodehash OpBlockhash OpCoinbase OpTimestampOpNumber OpPrevRandao OpGaslimit OpChainid OpSelfbalanceOpPopOpMloadOpMstore OpMstore8OpSloadOpSstoreOpJumpOpJumpiOpPcOpMsizeOpGas OpJumpdestOpCreateOpCall OpStaticcall OpCallcodeOpReturnOpDelegatecall OpCreate2OpRevertOpSelfdestructOpDupOpSwapOpLogOpPush OpUnknownopString$fShowOp$fEqOpkeccakAssumptions$fShowBuilderStateop1op2op3normArgsaddsubmuldivsdivmodsmodaddmodmulmodexpsexltgtleqgeqsltsgteqiszeroandorxornotshlshrsarreadByte readBytesreadWordreadWordFromBytesmaxBytes copySlice writeByte writeWord bufLength concPrefix word256AttakedroptoListfromList simplifyReads stripWrites readStorage readStorage' writeStoragesimplifylitAddrlitCodeto512 isLitByte isLitWord indexWordpadByte bytesToW256 padBytesLeft joinByteseqBytemin numBranchesallLit $fMonoidExpr$fSemigroupExprwordAtreadByteOrZero byteStringSliceWithDefaultZeroes sliceMemory writeMemory^ createAddresscreate2AddressStoreEnvBufEnv eliminateExpreliminatePropsCheckSatResultSatUnsatUnknownTaskscript resultChan SolverGroupSolverInstance_type_stdin_stdout_stderr_processSolverZ3CVC5BitwuzlaCustomSMT2SMTCexvarsbuffers blockContext txContextCexVars calldataVbuffersV blockContextV txContextVgetVar formatSMT2declareIntermediates assertPropsprelude declareBufsreferencedBufsreferencedBufs'referencedVars'referencedFrameContext'referencedBlockContext' declareVarsreferencedVarsdeclareFrameContextreferencedFrameContextdeclareBlockContextreferencedBlockContext exprToSMTspzeroone propToSMTisSatisErrisUnsatcheckSat parseW256 parseIntegerparseW8parseErrparseVar parseBlockCtx parseFrameCtxgetVarsgetBufsparseSC withSolvers solverArgs spawnSolver stopSolver sendScript sendCommandsendLine sendLine'getValue readSExpr expandExp concatBytes writeBytesencodeConcreteStore$fMonoidCexVars$fSemigroupCexVars $fMonoidSMT2$fSemigroupSMT2 $fShowSolver$fShowCheckSatResult$fEqCheckSatResult$fEqSMT2 $fShowSMT2 $fEqSMTCex $fShowSMTCex $fEqCexVars $fShowCexVarsAbiValsNoValsCAbiSAbiSolErrorEventIndexed NotIndexed Anonymity Anonymous NotAnonymousAbiKindDynamicStaticAbiType AbiUIntType AbiIntTypeAbiAddressType AbiBoolType AbiBytesTypeAbiBytesDynamicType AbiStringTypeAbiArrayDynamicType AbiArrayType AbiTupleTypeAbiValueAbiUIntAbiInt AbiAddressAbiBoolAbiBytesAbiBytesDynamic AbiStringAbiArrayDynamicAbiArrayAbiTuple formatStringabiKind abiValueTypeabiTypeSoliditygetAbiputAbi getAbiSeqencodeAbiValuedecodeAbiValueselector abiMethod parseTypeNameemptyAbi genAbiValue makeAbiValue parseAbiValue decodeBufdecodeStaticArgs$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$fReadAbiValue $fEqAbiValue $fOrdAbiValue$fGenericAbiValue $fReadAbiType $fEqAbiType $fOrdAbiType$fGenericAbiTypeCodeTypeCreationRuntimeSrcMapSM srcMapOffset srcMapLength srcMapFile srcMapJumpsrcMapModifierDepthJumpTypeJumpIntoJumpFrom JumpRegular Reference _refStart _refLength SourceCache _sourceFiles _sourceLines _sourceAsts MutabilityPureView NonPayablePayableMethod _methodOutput _methodInputs _methodName_methodSignature_methodMutability SolcContract_runtimeCodehash_creationCodehash _runtimeCode _creationCode _contractName_constructorInputs_abiMap _eventMap _errorMap_immutableReferences_storageLayout_runtimeSrcmap_creationSrcmapSlotTypeStorageMapping StorageValue StorageItem_offset_slot$fReadSlotType$fShowSlotType$fMonoidSourceCache$fSemigroupSourceCache$fFromJSONReference$fShowCodeType $fEqCodeType $fOrdCodeType$fShowSrcMapParseState$fShowSolcContract$fEqSolcContract$fGenericSolcContract $fShowSrcMap $fEqSrcMap $fOrdSrcMap$fGenericSrcMap$fShowJumpType $fEqJumpType $fOrdJumpType$fGenericJumpType$fShowReference $fEqReference$fShowSourceCache$fEqSourceCache$fGenericSourceCache $fShowMethod $fEqMethod $fOrdMethod$fGenericMethod$fShowMutability$fEqMutability$fOrdMutability$fGenericMutability$fShowStorageItem$fEqStorageItem $fEqSlotTypeabiMapconstructorInputs contractName creationCodecreationCodehashcreationSrcmaperrorMapeventMapimmutableReferences runtimeCoderuntimeCodehash runtimeSrcmap storageLayout sourceAsts sourceFiles sourceLinesLanguageSolidityYul methodInputsmethodMutability methodName methodOutputmethodSignature makeSrcMapsmakeSourceCache lineSubrangereadSolcyul yulRuntimesolidity solcRuntime functionAbireadJSONreadCombinedJSON readStdJSON signatureparseMethodInputcontainsLinkerHole solidity'yul'solcstdjsonstripBytecodeMetadatastripBytecodeMetadataSymastIdMap astSrcMap$fToJSONStandardJSON$fShowLanguageBlock _coinbase _timestamp_number _prevRandao _gaslimit_baseFee _maxCodeSize _scheduleEnv _contracts_chainId_storage _origStorage _sha3Crack StorageModel ConcreteS SymbolicSInitialSContract _contractcode_balance_nonce _codehash_opIxMap_codeOps _external RuntimeCodeConcreteRuntimeCodeSymbolicRuntimeCode ContractCodeInitCodeSubState_selfdestructs_touchedAccounts_accessedAddresses_accessedStorageKeys_refundsTxState _gasprice _txgaslimit_txPriorityFee_origin_toAddr_value _substate _isCreate _txReversion FrameState _contract _codeContract_code_pc_stack_memory _memorySize _calldata _callvalue_caller_gas _returndata_static FrameContextCreationContext CallContextcreationContextAddresscreationContextCodehashcreationContextReversioncreationContextSubstatecallContextTargetcallContextContextcallContextOffsetcallContextSizecallContextCodehashcallContextAbicallContextDatacallContextReversioncallContextSubStateFrame _frameContext _frameStateVMOpts vmoptContract vmoptCalldatavmoptStorageBase vmoptValuevmoptPriorityFee vmoptAddress vmoptCaller vmoptOriginvmoptGas vmoptGaslimit vmoptNumbervmoptTimestamp vmoptCoinbasevmoptPrevRandaovmoptMaxCodeSizevmoptBlockGaslimit vmoptGasprice vmoptBaseFee vmoptSchedule vmoptChainId vmoptCreatevmoptTxAccessList vmoptAllowFFI StorageBaseConcreteSymbolicCache_fetchedContracts_fetchedStorage_pathIsUniqueUniqueMultiple InconsistentUTimeoutUBranchConditionCase Inconsistent CodeLocationChoosePleaseChoosePathQueryPleaseFetchContractPleaseFetchSlot PleaseAskSMT PleaseDoFFI TraceData EventTrace FrameTrace QueryTrace ErrorTrace EntryTrace ReturnTraceTrace _traceOpIx_traceContract _traceDataVM_result_state_frames_env_block_tx_logs_traces_cache_burned _iterations _constraints _keccakEqs _allowFFIVMResult VMFailure VMSuccess BalanceTooLowUnrecognizedOpcodeSelfDestruction StackUnderrunOutOfGas BadCheatCodeStateChangeWhileStaticCallDepthLimitReachedMaxCodeSizeExceeded InvalidFormatPrecompileFailureUnexpectedSymbolicArgDeadPath NotUnique SMTTimeoutFFI NonceOverflow blankState$fEqContractCode$fParseFieldStorageModel $fShowChoose $fShowQuery$fShowVM $fShowTrace$fShowTraceData $fShowBlock $fShowEnv$fReadStorageModel$fShowStorageModel $fShowCache $fShowVMOpts $fShowFrame$fShowFrameContext $fShowTxState$fShowFrameState$fShowContractCode$fShowRuntimeCode$fEqRuntimeCode$fOrdRuntimeCode$fShowSubState$fShowStorageBase$fEqStorageBase$fShowIsUnique$fShowBranchCondition$fShowContract$fOrdContractCode$fShowVMResultcalldatacaller callvaluecode codeContractcontractgasmemory memorySizepc returndatastackstatic frameContext frameStatebaseFeecoinbasegaslimit maxCodeSizenumber prevRandaoschedule timestampgaspriceisCreateoriginsubstatetoAddr txPriorityFee txReversion txgaslimitvalueaccessedAddressesaccessedStorageKeysrefunds selfdestructstouchedAccountsbalancecodeOpscodehash contractcodeexternalnonceopIxMapchainId contracts origStorage sha3CrackstoragefetchedContractsfetchedStoragepath traceContract traceData traceOpIx FrameResult FrameReturned FrameReverted FrameErrored CheatActionallowFFIblockburnedcache constraintsenvframes iterations keccakEqslogsresultstatetracestxbytecodeunifyCachedStorageunifyCachedContractcurrentContractmakeVminitialContractnextexec1transfer callChecksprecompiledContractexecutePrecompile truncpadlit lazySliceparseModexpLengthisZero asIntegernooppushTopushToSequencegetCodeLocationbranch fetchAccount accessStorage accountExists accountEmptyfinalize loadContract limitStack notStaticburn forceConcreteforceConcrete2forceConcrete3forceConcrete4forceConcrete5forceConcrete6forceConcreteBufrefundunRefund touchAccount selfdestruct accessAndBurnaccessAccountForGasaccessStorageForGas cheatCodecheat cheatActionsethsign delegateCall collisioncreate replaceCodereplaceCodeOfSelf resetStatevmErrorunderrun finishFrameaccessUnboundedMemoryRangeaccessMemoryRangeaccessMemoryWordcopyBytesToMemorycopyCallBytesToMemory readMemorywithTraceLocation pushTrace insertTracepopTracezipperRootForest traceForest traceTopLogpushpushSymstackOp1stackOp2stackOp3 checkJumpopSize mkOpIxMapvmOpvmOpIxopParamsreadOp mkCodeOps costOfCall costOfCreateconcreteModexpGasFeecostOfPrecompile memoryCostceilDiv allButOne64thlog2hashcodeopslencodelentoBufcodeloc $fMonoidCache$fSemigroupCache$fShowFrameResult TransactiontxData txGasLimit txGasPricetxNoncetxRtxStxToAddrtxVtxValuetxType txAccessListtxMaxPriorityFeeGastxMaxFeePerGasTxTypeLegacyTransactionAccessListTransactionEIP1559TransactionAccessListEntry accessAddressaccessStorageKeys txAccessMapecrecsender signingDataaccessListPrice txGasCost accountAt newAccountsetupTxinitTx$fFromJSONAccessListEntry$fFromJSONTransaction$fShowTransaction $fShowTxType $fEqTxType$fShowAccessListEntryFetcherToRPCtoRPCRpcInfoLatestRpcQuery QueryCode QueryBlock QueryBalance QueryNonce QuerySlot QueryChainIdrpcreadText fetchQuery parseBlockfetchWithSessionfetchContractWithSessionfetchSlotWithSessionfetchBlockWithSessionfetchBlockFromfetchContractFrom fetchSlotFromhttporacle checkBranch$fToRPCBlockNumber $fToRPCBool $fToRPCW256 $fToRPCAddr$fShowBlockNumber$fEqBlockNumber$fShowRpcQueryFilefilePathfileDataData dataASCIIFact BalanceFact NonceFact StorageFactCodeFactaddrwhatwhichblob contractFacts cacheFactsvmFactsapply applyCache factToFile fileToFact $fOrdFact$fAsASCIIByteString $fAsASCIIW256 $fAsASCIIAddr$fEqFile $fOrdFile $fShowFile$fEqData $fOrdData $fShowData$fEqPath $fOrdPath $fShowPath$fEqFact $fShowFactRepoAt saveFacts loadFacts $fEqRepoAt $fOrdRepoAt $fShowRepoAt ethrunAddressvmForEthrunCreationexecrun execWhileStepperActionExecRunWaitAskIOActwaitaskevmevmIO execFullyrunFullyenteringenter interpretModeDebug JsonTraceobjectprettyContractprettyContracts srcMapCodePos srcMapCode$fEqMode $fShowModeTest ConcreteTest SymbolicTest InvariantTest DappContext _contextInfo _contextEnvCoderawimmutableLocationsDappInfo _dappRoot_dappSolcByName_dappSolcByHash_dappSolcByCode _dappSources_dappUnitTests _dappAbiMap _dappEventMap _dappErrorMap _dappAstIdMap_dappAstSrcMap $fShowCode dappAbiMap dappAstIdMap dappAstSrcMap dappErrorMap dappEventMapdappRootdappSolcByCodedappSolcByHashdappSolcByName dappSources dappUnitTests contextEnv contextInfodappInfo emptyDappunitTestMarkerAbifindAllUnitTestsmkTest findUnitTestsunitTestMethodsFilteredunitTestMethods extractSig traceSrcMapsrcMapfindSrc lookupCode compareCodeshowTraceLocation $fShowTestfindContractDefinitionstorageVariablesForContractnodeIsisStorageVariableDeclarationslotTypeForDeclarationgrokDeclarationTypegrokMappingType grokValueType showWordExactshowWordExplanationprettyIfConcreteWord showAbiValue textValues parenthesise showValues showValueshowCall showError formatBytes formatBinary showTraceTree unindexedcontractNamePartcontractPathPartprettyvmresultindent formatExpr$fShowSignedness Postcondition PreconditionCalldataFragmentStDyCompVeriOptssimpdebugmaxIter askSmtItersrpcInfoEquivalenceResult VerifyResult ProofResultQedCexTimeoutisQed containsAdefaultVeriOpts rpcVeriOpts debugVeriOpts extractCexinRangebool symAbiArg symCalldatacdLen writeSelectorcombineFragments abstractVM loadSymVMmaxIterationsReached checkAssertcheckAssertionsdefaultPanicCodes allPanicCodespanicMsgverifyContractpruneDeadPathsrunExpr flattenExpr reachableevalProp extractPropsverifyequivalenceCheckboth' produceModels showModel formatCexsubModel$fShowCalldataFragment$fEqCalldataFragment $fEqVeriOpts$fShowVeriOpts$fShowProofResult$fEqProofResult ExploreTx CoverageState OpLocation srcContractsrcOpIx ABIMethod TestVMParams testAddress testCaller testOrigin testGasCreate testGasCall testBaseFeetestPriorityFeetestBalanceCreate testCoinbase testNumber testTimestamp testGaslimit testGaspricetestMaxCodeSizetestPrevrandao testChainIdUnitTestOptionssolversverbosesmtDebugmaxDepth smtTimeoutsolvercovMatchmatchfuzzRunsreplay vmModifierdapp testParams ffiAlloweddefaultGasForCreatingdefaultGasForInvokingdefaultBalanceForTestContractdefaultMaxCodeSize makeVeriOptsdappTestinitializeUnitTest runUnitTestexecTestStepper exploreStep checkFailuresfuzzTestticksrcMapForOpLocationcurrentOpLocationexecWithCoveragerunWithCoverageinterpretWithCoveragecoverageReportcoverageForUnitTestContractrunUnitTestContractrunTest decodeCallsinitialExplorationStepperexplorationSteppergetTargetContracts exploreRunexecTestrunOnefuzzRunsymRun symFailureprettyCalldata showCalldatashowVal execSymTestcheckSymFailures indentLines passOutput failOutputformatTestLogs formatTestLog word32BytesabiCall makeTxCallinitialUnitTestVm%getParametersFromEnvironmentVariables$fOrdOpLocation$fEqOpLocation$fShowOpLocation checkEquiv runDappTesttestOptsdoTest analyzeDaidaiExpr analyzeVatanalyzeDeposit reachable'showExpr summaryStoresafeAdd testContractvatinitVm buildExprdaiUiStateViewVm ViewContracts ViewPickerViewHelpUiBrowserState_browserContractList _browserVmUiTestPickerState_testPickerList_testPickerDapp _testOpts UiVmState_uiVm_uiStep _uiSnapshots _uiStepper _uiShowMemory _uiTestOptsUiWidgetNameAbiPane StackPane BytecodePane TracePane SolidityPaneTestPickerPane BrowserPanePager$fEqName $fShowName $fOrdName uiShowMemory uiSnapshotsuiStep uiStepper uiTestOptsuiVmtestPickerDapptestPickerListbrowserContractList browserVm ContinuationStoppedContinueStepModeStep StepUntilPred_ViewVm_ViewContracts _ViewPicker _ViewHelpsnapshotInterval keepExecutingisUnitTestContractmkVty runFromVM initUiVmStatedebuggableTests isFuzzTestmaintakeStep backstepUntilbackstepappEventappinitialUiVmStateForTestmyThemedrawUi drawHelpViewdrawTestPicker drawVmBrowserdrawVm drawHelpBar stepOneOpcodeisNewTraceAddedisNextSourcePosition#isNextSourcePositionWithoutEnteringisExecutionHalted currentSrcMap drawStackPanemessagedrawBytecodePanedim withHighlightprettyIfConcrete drawTracePaneourWrap solidityListdrawSolidityPane ifTallEnoughopWidget selectedAttrdimAttrwordAttrboldAttr activeAttrbytestring-0.11.3.1Data.ByteString.Internal ByteStringbaseGHC.BaseString paddedShowHexisWorthPrintingghc-prim GHC.TypesTruegroup EthjetContext mtl-2.2.2Control.Monad.State.ClassputgeteliminateExpr'eliminateProp'eliminateProps'versiongetDataFileName getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDir