* Update hevm and enable arithmetic abstraction internally
* Test arithmetic abstraction on multiplication monotonicity
* Optimize hevm while preserving symbolic Keccak preimages
Integrate the optimization settings and conditional preimage recording from PR #1621. Keep recording throughout symbolic campaigns and verify that both solvers recover earlier transaction inputs after replaying a symbolic counterexample.
transactions[].arguments used ppAbiValue for every argument, so bytes,
bytesN and string were the Haskell `show` rendering (\NUL, \DEL, decimal
escapes, \&) and arrays/tuples were stringified. Encode bytes/bytesN as
0x-hex, string as a JSON string (hex if not UTF-8), arrays/tuples as JSON
arrays. Scalars are unchanged.
Co-authored-by: Claude Sonnet 5.5 <[email protected]>
* feat: add a call-sequence syntax for MCP clients
Something driving a campaign from outside it needs a way to name a
sequence of calls, and the natural one is how the calls would be written
in Solidity, with a hole wherever the fuzzer should choose:
approve(0x10, ?); transferFrom(?, ?, 100)
Echidna.MCP.Parse reads that into the list of SolCallPrototypes the
preceding commits taught the fuzzer to generate from. Parsing stops at an
argument's shape rather than its type -- an integer becomes a uint256, an
0x-prefixed literal an address -- because an argument left open carries no
type to compare against anyway, so a prototype is resolved against the
ABI by name and arity either way.
It is a module of its own rather than part of the server that will use
it. This is the one piece of the interface with a set of edge cases worth
enumerating, and Tests.MCPParse enumerates them without needing a
campaign to run against.
Three things differ from the version this is adapted from. `foo(1` no
longer parses as a call with no arguments: the closing parenthesis is
checked rather than assumed, which is what that silently relied on. An
empty sequence is rejected instead of accepted as a sequence of no calls.
And splitting on `;` is Data.List.Split's job rather than a hand-rolled
splitter's -- the bracket-aware split of an argument list still needs its
own, since a comma inside `[1,2]` does not separate arguments.
Nothing parses a sequence yet; the MCP server that does arrives next.
Co-authored-by: gustavo-grieco <[email protected]>
* feat: replace the events server with an MCP server
--server PORT has run a Server-Sent Events server: a one-way stream of
campaign events, enough to watch a campaign with but not to ask it
anything. Replace it with a Model Context Protocol server on the same
flag and the same port, so what is on the other end can both read the
campaign and steer it.
Nine tools. Four report: status (corpus size, iterations, coverage,
tests, optimization values, how long since the last coverage, the
functions that found it, and whatever is being sampled), target,
show_coverage and dump_lcov. Five act: inject_fuzz_transactions and
clear_fuzz_priorities aim the fuzzer at an ordering, sample starts and
stops recording what a function does, execute_sequence replays a concrete
sequence without disturbing the campaign, and reload_corpus picks up
whatever was written to the corpus directory since it started.
The five that act do so over the inter-worker bus, which is why this
comes last: the commands they send, the sampling they switch on and the
replay they ask for all landed in the preceding commits with nothing to
send them. AgentId gains ServerId to say where they come from.
Retiring SSE is the point of the commit rather than a side effect of it.
Echidna.Server had no other caller, so it goes, and wai-extra with it.
The "Waiting until all SSE are received..." drain at the end of a
non-interactive run goes too, and with no reader left the MVar the SIGINT
handler filled goes as well. --server and the `server` config key keep
their names and their meaning -- a port to serve the campaign on -- so
there is no point at which the flag does nothing.
On the dependency: mcp-server comes from Hackage at 0.2.0.1, not from the
personal fork this was prototyped against. Upstream has since released
the two fixes that fork existed for (202 with no body for a notification,
405 for a server-stream GET), so there is no reason to carry a fork of a
library in the closure of a security tool. It needs http-types >= 0.12.6,
which nixpkgs and lts-23.24 both predate: only that version re-exports
`hOrigin` from the umbrella Network.HTTP.Types module that mcp-server
imports unqualified, and http-types has to move for the whole package set
rather than for mcp-server alone, since wai and warp exchange its Status
type with it. Everything in the closure builds against 0.12.6.
Some notes on the shape of it:
The server runs mcpApplication under Warp directly instead of
runMcpServerHttpWithConfig, which announces itself with a bare putStrLn.
Going through a ServerLog event instead keeps the line timestamped and
prefixed like every other one, and leaves Warp's settings to us -- which
matters for binding to loopback.
Origin validation is on with an empty allow-list. The campaign is
reachable from a browser on the same machine, and a page must not be able
to drive a fuzzer through DNS rebinding; a client that sends no Origin at
all, which is every CLI agent, is unaffected.
A tool that cannot do what it was asked answers with an MCP error result
rather than with a report whose text begins "Error:", so a model does not
have to read prose to notice. That is what the Either in ToolRun is.
reload_corpus reads the same two directories the campaign read at
startup, through loadInitialCorpus, rather than the corpus directory
itself -- what is directly in there is those directories, and reading one
as a file is an exception. It decides what is new and adds it inside a
single atomicModifyIORef', because workers are adding to the corpus while
it runs and a read followed by a write would drop whatever arrived in
between. Sequences from disk take the weight of the best entry already
there, never zero, which selectFromCorpus would never draw.
The upstream version's Env.sourceCache is not here: DappInfo already
carries the source cache, so env.dapp.sources is the same thing without a
second copy in Env. Its DumpLcov bus command is not here either -- the
tool calls saveLcovSnapshot directly, and a command with no sender is
what the earlier commits have been leaving out. Its markLines change is
not here: dropping the line number and column separator to save an
agent's tokens would have regressed every text and HTML coverage report
Echidna writes, and an agent that cannot cite a line number is worse off
than one reading a few more tokens.
The recently-covered functions are kept with takeStrict, not take. They
are appended to on every coverage event and read only when a client asks,
so a lazy tail would retain every sequence the campaign ever found
coverage with -- the same trap the sampling state was written around.
One limitation worth knowing: execute_sequence sends every call to the
contract under test, so a sequence naming a function of some other
deployed contract goes to the wrong address. The sequence syntax has no
way to spell an address, so there is nothing to fix it with yet.
Co-authored-by: gustavo-grieco <[email protected]>
* fix: coerce concrete MCP arguments to ABI parameter types
Resolve concrete replay calls against the ABI before constructing SolCall values, and coerce fixed arguments in fuzz prototypes. Preserve signed and full-width literals, validate bounds and array lengths, and reject ambiguous replay overloads.
Add parser, coercion, mixed-prototype and Solidity replay regressions. The focused 63-test suite and live MCP probe pass; restoring the original call construction fails all four call-site regression tests.
* test: cover bytes32 literals in mixed MCP calls
Exercise asymmetric 32-byte words through generic mixed-parameter replay and injected prototypes. Check leading-zero padding, the zero word, and oversized literal rejection for G3, whose implementation is covered by the B1 coercion fix.
Validation: targeted HLint and git diff --check pass. Execution testing is deferred to GitHub CI.
* fix: start MCP only after workers are ready
---------
Co-authored-by: gustavo-grieco <[email protected]>
* feat: replay a concrete sequence and report on it
Add ExecuteSequence, the command that answers "what does this sequence
of calls actually do?". A caller hands a worker a concrete sequence and
gets back a JSON report: what each call was, whether it completed,
reverted or failed an assertion, the gas it burned and the events it
emitted, then the block number and timestamp the sequence ended on and,
if asked for, the EVM trace.
The replay goes through execTx rather than callseq, so the campaign is
left exactly as it was: no coverage recorded, nothing added to the
corpus, no test falsified. Answering a question about the contract must
not change what the campaign does next, and a test pins that down.
The report summarises the sequence by its worst transaction rather than
its first failure. An assertion failure anywhere outranks a revert, even
one that happened earlier -- reverts are common enough in a random
sequence that reporting one would bury the thing the caller was looking
for. Assertion failures are recognised with checkAssertionEvent and
checkPanicEvent, the same pair an assertion test uses, so both the
emit-AssertionFailed convention and solc's Panic(1) are covered; the
tests exercise one path each.
The command is addressed to a single worker, which answers through a
one-shot Reply channel. The replay runs on that worker's own thread, so
it stops fuzzing for as long as the caller is waiting on it.
Nothing sends this command yet; the MCP server that does arrives next.
Co-authored-by: gustavo-grieco <[email protected]>
* fix: drop a partial head from the replay tests
GHC 9.8 turned head into a -Wall warning, and CI builds the test suite
with -Werror, so the single-transaction assertion in the Panic(1) test
failed the Windows and Linux builds.
Match on the list instead. The test replays exactly one transaction, so
pinning that down says what the assertion already assumed and reports a
useful failure if it ever stops holding.
---------
Co-authored-by: gustavo-grieco <[email protected]>
* refactor: factor the shared tail out of genTx
genTx does three things in sequence: resolve the deployed contracts to
the ABIs Echidna knows how to call, pick one of them and generate a call
to it, then wrap that call in a transaction with a random sender, value
and delay. Only the middle step is about choosing what to call; the two
ends are the same for any generator that has already decided.
Split them into callableContracts, genRandomCall and toTx, leaving genTx
as the composition of the three. No behaviour changes -- this is the
groundwork for a generator that picks its own call and reuses both ends
rather than repeating them.
Co-authored-by: gustavo-grieco <[email protected]>
* feat: generate a transaction from a call prototype
A prototype is a SolCall with holes: a function name and an argument
list where Nothing marks an argument left for the fuzzer to fill in. It
is how something outside the campaign says "call transfer, I don't care
with what", or "call transfer with this recipient and any amount".
genTxFromPrototype resolves one against the deployed contracts and hands
the result to the same tail genTx uses. Matching is on name and arity
only: an argument left open carries no type to compare against, so
same-arity overloads all qualify and one is picked at random.
matchingContracts cuts each contract down to just the signatures that
match, which keeps the subsequent pick total -- there is no filtered
list that can turn out to be empty after a contract was already chosen.
When nothing deployed exposes such a function it falls back to a fully
random transaction, so a prototype naming a function that isn't there
costs diversity rather than stalling the worker.
Nothing produces prototypes yet; the command that injects them follows.
Co-authored-by: gustavo-grieco <[email protected]>
* feat: prioritize injected call sequences during fuzzing
Add the other half of prototypes: a worker can be handed a sequence of
them together with a probability, and will fuzz that sequence instead of
a corpus-mutated one that often. This is what lets something outside the
campaign spend part of a worker's budget on a specific ordering -- an
ordering it has reason to believe is interesting, but that the corpus
mutators are unlikely to stumble into.
FuzzSequence and ClearPrioritization join the commands a fuzzing worker
accepts over the bus, and what they inject accumulates in
WorkerState.prioritizedSequences. randseq now chooses between the
prioritized path and the standard one; its previous body moves to
genStandardSeq unchanged.
genPrioritizedSeq turns a sequence of prototypes into a real one. The
calls are generated in order with up to maxInterleavedTxs random
transactions between consecutive ones, so what gets pinned is the
ordering rather than the whole sequence. It is then prefixed with the
start of a corpus entry, so the ordering also runs from a state the
campaign has already reached -- except on worker 0, which always takes
the empty prefix so the initial state stays covered. The result is
padded with random transactions, or truncated, to respect seqLen.
Nothing sends these commands yet; the client that does arrives with the
MCP server.
Co-authored-by: gustavo-grieco <[email protected]>
---------
Co-authored-by: gustavo-grieco <[email protected]>
* feat: sample per-function call statistics
A worker can now be asked to watch a handful of functions and keep, for
each of them, how often it was called, how often the call did not return
successfully, the range its return value spanned, and a short tail of
revert summaries. This is what an outside observer needs to answer "is
this function reachable, and what does it do when it is" without reading
the corpus.
The state hangs off WorkerState.sampledFunctions, keyed by canonical
signature. Nothing populates that map yet -- the command that enables
sampling arrives with the inter-worker bus -- so callseq's cost is a
Map.null check per sequence, and the per-call work only happens for
functions someone asked about.
The interesting part is the per-event algebra, so it is factored out of
the worker: applySampleEvent folds one call result into a SampleStats,
abiCompare gives the partial ordering the range tracking needs, and
mergeSampleStats combines two workers' views. All three are pure and
covered by Tests.Sample; updateSampleStats in Worker/Sequence.hs is left
with just the decode-and-dispatch.
Every SampleStats field is strict, and the revert list is built with a
take that forces its spine and elements. These are updated on the fuzzing
hot path and only read when a client asks, so a lazy field would quietly
retain the entire call history: a plain `take n (new : old)` keeps `old`
alive through its unevaluated tail, and `old` keeps the one before it.
Co-authored-by: gustavo-grieco <[email protected]>
* feat: add an inter-worker message bus
Workers have so far been able to communicate in exactly one direction:
each pushes events onto the campaign's event queue, which the UI and the
listener read. Nothing can talk back to a running worker, and a worker
cannot tell another one what it just learned.
Add a bus to Env alongside the event queue: a broadcast STM channel, so
readers take their own dupTChan of it and every reader sees every
message rather than racing for it. Echidna.Types.InterWorker holds the
protocol -- a message, its sender, and the commands a fuzzing worker
accepts.
Two things use it. callseq broadcasts NewCoverageInfo whenever a
sequence finds coverage, carrying the sequence and whether it came from
replaying the corpus, which is the new argument threaded through
callseq's callers. And a fuzzing worker checks the bus once per loop
iteration for commands addressed to it, which is how sampling gets
turned on and off.
The two commands land here rather than with a sender because they are
what makes the bus worth having; the client that issues them, and the
listener for NewCoverageInfo, arrive with the MCP server. Everything
else in the upstream protocol -- symbolic commands, request/response,
the other broadcasts -- has neither a sender nor a reader, so it is left
out until it has both.
The command handler lives in its own module rather than in another
where-block inside runFuzzWorker, which is the shape the preceding
decomposition was aiming for and the natural home for the handlers that
follow.
Two details worth calling out:
checkMessages drains its queue rather than taking one message per
iteration. Every broadcast is copied to every worker's duplicate, so
with N workers finding coverage a worker receives roughly N messages per
iteration; consuming one would let the queue grow without bound during
the early phase of a campaign, when almost every sequence is new
coverage. Commands come from outside the campaign at human pace, so
there is nothing to starve fuzzing with.
The broadcast's sender is resolved through workerIDToType, the same way
pushWorkerEvent decides which worker type to attribute an event to. The
symbolic worker calls callseq too, and it is not a fuzzer.
Co-authored-by: gustavo-grieco <[email protected]>
---------
Co-authored-by: gustavo-grieco <[email protected]>
* Revert "Drain campaign event queue to fix root-cursor memory leak (#1587)"
This reverts commit 58d7fc5860.
* Use broadcast TChan for campaign events
Replace the campaign event queue with an STM broadcast TChan so subscribers
keep the existing events-after-subscribe behavior without the Chan root
cursor retention issue. Producers now write through STM, and campaign/UI/SSE
listeners subscribe with dupTChan/readTChan.
Avoid retaining full VM snapshots in queued TestFalsified/TestOptimized
events by publishing VM-free EchidnaTest copies. The canonical testRefs
state still keeps the VM so shrinking, reports, traces, and final JSON
continue to work.
* refactor: replace runWorker dispatch with an Agent typeclass
runWorker dispatched on WorkerType and threaded eight positional
arguments down to runFuzzWorker/runSymWorker, so every caller had to
supply arguments the other worker discards: testLimit for the symbolic
worker, the selected contract name for the fuzzer.
Replace it with Echidna.Types.Agent:
class Agent a where
runAgent :: a -> Env -> IO WorkerStopReason
FuzzerAgent and SymbolicAgent each carry exactly the parameters their
worker needs plus the IORef WorkerState they publish through, and
Echidna.Campaign shrinks to isSuccessful.
runAgent returns the stop reason rather than pushing a WorkerStopped
event: an agent killed by the campaign timeout never reaches its own
last line, so only spawnWorker knows the real reason, and it has to
emit that event exactly once per worker -- listeners count those events
to decide when the campaign is over.
Two details come along with the move:
The agents announce themselves through the generic Log event, so
"Starting FuzzerAgent N" shows up in the same stream as the rest of the
worker output.
runAgent publishes the final worker state to stateRef before returning.
The callback publishes as the worker goes but not from every exit path
-- verification mode never runs it -- and src/test/Common.hs now reads
the state back from that ref instead of from runWorker's return value,
so the ref has to be authoritative.
Co-authored-by: gustavo-grieco <[email protected]>
* refactor: retire Echidna.Campaign, move isSuccessful to Types.Test
With runWorker gone, Echidna.Campaign held a single pure predicate over a
list of tests and had a single caller. The name no longer described the
contents: nothing about a campaign was left in it.
Echidna.Types.Test already collects the EchidnaTest state predicates --
isOpen, isPassed, isVerified, didFail, isConclusiveFailure,
needsShrinking -- and isSuccessful is the same kind of thing, one level
up on a list. It needs no import that module does not already have, so
move it there and drop Echidna.Campaign.
Echidna.Test.State was the other candidate and is the wrong fit: it is
about reading and updating Env.testRefs in a monad, while isSuccessful
is pure and takes the list directly.
The function is moved verbatim. It does not treat Unsolvable as a
success, so a fully verified run exits non-zero; that is a separate
behaviour change and gets its own commit.
Co-authored-by: gustavo-grieco <[email protected]>
* fix: count verified tests as a success in the exit code
In verification mode a run where every test was formally verified still
exited 1. isSuccessful accepted only Passed and Open, and Unsolvable --
the state symbolic execution sets once it proves an assertion cannot be
reached -- fell through to False. The better verification did, the more
likely the run was to "fail": a test that could not be verified stays
Open and counted as a success, while one that was verified did not.
Every other consumer of the state already treats Unsolvable as a
success: ppTS prints "verified", tsWidget shows VERIFIED!, and the JSON
encoder maps it to Verified. Only the exit code disagreed, which made it
useless for gating CI on a verification run.
Say it with the sibling predicates it now sits next to, so the three
accepted states are visible in one line.
Fixes#1602
* refactor: make Agent a sum type instead of a typeclass
The class had two instances and nothing ever abstracted over it: both
call sites matched on WorkerType and then named a concrete instance, so
it bought a shared method name and no polymorphism.
A closed set of two worker kinds with per-kind behaviour at several
sites is what a sum type is for. Echidna.Types.Agent now holds one
Agent with a constructor per worker, and Echidna.Agent holds runAgent,
sitting above both worker modules exactly where runWorker used to.
That is the real shape of the original problem: runWorker took a tag
plus the union of both workers' parameters. The fix was never a class,
it was a sum of records, one per worker, each carrying only its own
arguments.
Falls out of it:
WorkerType is now derived from the agent via workerTypeOf rather than
carried alongside it, so spawnWorker picks the constructor once and
everything else follows.
The corpus split moves into that choice. "if workerType ==
SymbolicWorker then initialCorpus else corpusChunk" is gone; each
constructor is simply built with the corpus its worker wants.
Adding a third worker kind is now a compile error at every site that
has to care, which the class would not have given us.
* refactor: stop passing the symbolic worker a corpus it discards
runSymWorker has bound its initialCorpus parameter to _ since #1394
(c2671049), which removed the "void $ replayCorpus vm initialCorpus"
call but left the parameter and every caller feeding it. replayCorpus
now has exactly one caller, in Worker/Fuzz.hs.
So the argument was threaded from UI.hs, through the agent, into a
function that dropped it. Worse, UI.hs had a branch specifically to hand
the symbolic worker the *whole* corpus instead of a chunk, and a comment
claiming "the symbolic worker always replays the full corpus", which has
not been true for a year.
Drop the parameter, the SymbolicAgent field, and the special case, and
correct the comment. Behaviour cannot change: the value was already
being discarded.
This also restores the premise of the Agent constructors, that each one
carries only what its own worker needs.
---------
Co-authored-by: gustavo-grieco <[email protected]>
* feat: name the function that found new coverage
ppWorkerEvent already receives the transaction sequence behind a
NewCoverage event but only reported the aggregate counters. Append the
last transaction's call to the log line so it is visible which function
is making progress.
Co-authored-by: gustavo-grieco <[email protected]>
* feat: add generic log events
Add a WorkerEvent Log constructor for free-form worker messages and a
CampaignEvent ServerLog for messages that are not attributable to any
worker, reported with a [Server] prefix in the text UI and as a
server_log SSE event.
All four exhaustive matches over these types (the ToJSON instances, the
pretty printers and the SSE event names) land together so the compiler
stays happy.
Co-authored-by: gustavo-grieco <[email protected]>
* fix(tests): return the flag from flags.sol set0/set1
Both functions are declared 'returns (bool)' but fall off the end, so
solc warns and they silently return false.
Co-authored-by: gustavo-grieco <[email protected]>
* chore: gitignore Python artifacts
Co-authored-by: gustavo-grieco <[email protected]>
* fix(worker): avoid hlint false positive on record-dot access
CI runs bare `hlint lib src`, which does not read echidna.cabal and so
does not know OverloadedRecordDot is on. It parsed `(last txs).call` as
function composition and flagged the parens as a redundant bracket.
Taking that suggestion would have broken the build: under
OverloadedRecordDot, `last txs.call` parses as `last (txs.call)`.
Bind the last transaction first so the expression needs no parens and
reads identically to hlint and to GHC.
---------
Co-authored-by: gustavo-grieco <[email protected]>
* feat: add explicit verification test mode
* fix: respect sequence length in Foundry filtering
* test: use explicit verification mode for symbolic assertions
* refactor: decompose campaign execution
* refactor: narrow exports of decomposed campaign modules
* refactor: move listenerLoop to Echidna.Worker
listenerLoop is event-bus plumbing, not transaction execution: it reads
CampaignEvents off a Chan and counts WorkerStopped events. Echidna.Worker
already owns the write side of that bus (pushWorkerEvent,
pushCampaignEvent) and the worker accounting it depends on (getNWorkers,
workerIDToType), so the reader belongs there too.
This also drops Echidna.Execution from Campaign's imports, and narrows
Agent.Symbolic's dependency on Execution to the three call-sequence
functions it actually uses.
Pure move: the function body is unchanged.
* refactor: move MonadThrow (RandT) orphan to its own module
Both worker bodies run in RandT g (StateT WorkerState m) and call
callseq/replayCorpus, which carry a MonadThrow constraint, so they need
this instance. exceptions covers the standard transformers, but
MonadRandom's RandT is a newtype over StateT that derives nothing from
exceptions, so the instance is missing and we have to supply it.
It lived in Echidna.Execution, which has no use for it: that module only
mentions MonadThrow as a polymorphic constraint and compiles fine without
the instance. Meanwhile the two modules that do need it never named it --
they resolved it transitively through their Echidna.Execution import, and
-fno-warn-orphans kept GHC quiet about the arrangement. Narrowing or
dropping that import would have produced a "Could not deduce MonadThrow
(RandT ...)" error pointing at callseq, far from the cause.
Echidna.Orphans.Rand now holds it, alongside Echidna.Orphans.JSON, and
Agent.Fuzzer and Agent.Symbolic import it explicitly so the dependency is
visible where it is relied upon. Named for the type rather than the class,
following the same rule as Orphans.JSON: name the axis that stays fixed
while the other varies. JSON fixes the class family and accumulates types;
this module fixes RandT and would accumulate classes (MonadCatch or
MonadMask, should a worker ever need bracket).
Verified by deleting the instance outright: the only two failures were
Agent/Fuzzer.hs (replayCorpus) and Agent/Symbolic.hs (callseq).
* refactor: extract worker-agnostic test-set ops into Echidna.Test.State
updateTests and findFailedTests both declared MonadState WorkerState but
never touched it -- they only read Env.testRefs. Move them to a module that
says so, dropping the vestigial constraint.
updateOpenTest stays private next to its only caller evalSeq: it is genuinely
worker-scoped (stamps test.workerId, emits worker events).
Also replaces the symbolic worker's two inline "mark the assertion test for
this method signature" blocks with setAssertionTestState, which skips the
IORef write for non-matching tests instead of rewriting them unchanged.
* refactor: move the worker modules under Echidna.Worker
Echidna.Execution sat next to Echidna.Exec with a name that did not
distinguish them. Its remaining contents are worker-scoped call-sequence
machinery, so they move to Echidna.Worker.Sequence, alongside the two worker
strategies -- which also drop the "Agent" spelling for the "Worker" vocabulary
the rest of the codebase uses.
Echidna.Execution -> Echidna.Worker.Sequence
Echidna.Agent.Fuzzer -> Echidna.Worker.Fuzz
Echidna.Agent.Symbolic -> Echidna.Worker.Symbolic
* refactor: put spawnListener next to listenerLoop, share the shrink loop
spawnListener was in Echidna.Campaign calling listenerLoop in Echidna.Worker;
they are one mechanism, so both now live in Echidna.Worker. Echidna.Campaign is
left as what it is: the worker dispatcher. It has to stay above Worker.Fuzz and
Worker.Symbolic -- folding runWorker into Echidna.Worker would cycle, since both
workers import it for pushWorkerEvent.
The two workers also had byte-identical copies of "shrink the tests this worker
falsified", which is now Echidna.Shrink.shrinkWorkerTests.
* refactor: reuse initialWorkerState, name the stopOnFail predicate
Both workers hand-rolled the WorkerState record that Echidna.Types.Campaign
already provides as initialWorkerState, and both carried an identical local
'final' predicate whose name did not explain why a falsified test still being
shrunk (Large) must not trip stopOnFail. That is now isConclusiveFailure,
next to the other test-state predicates.
* refactor: share one shrinkable predicate between the workers
The two workers disagreed: the fuzzer bounded shrinking with n < shrinkLimit,
the symbolic worker returned True for any Large test on this worker. Only the
fuzzer's version is safe on its own terms. shrinkTest never moves an
optimization test to Solved -- it keeps reporting Large (i + 1) -- so without
the bound a loop over shrinkable tests cannot terminate. The symbolic worker
gets away with it because its shrink branch of shrinkAndRandomlyExplore
recurses on the same n and would spin, but an optimization test never carries
the symbolic worker's id: updateOpenTest only stamps workerId on BoolValue
False, and optimization tests get theirs from the fuzzer's
closeOptimizationTest.
So the two predicates agree on every reachable state today, and the bounded
one is strictly more conservative. Sharing it as Echidna.Shrink.isShrinkable
keeps the divergence from silently reappearing now that the workers live in
separate modules.
---------
Co-authored-by: Emilio López <[email protected]>
* feat: add explicit verification test mode
* fix: respect sequence length in Foundry filtering
* test: use explicit verification mode for symbolic assertions
* foundry fixes
* test: add missing testFail regression test files
The contract and config used by the "foundry/TestFail.sol" test case were
left out of the previous commit, making the test fail on CI with a missing
config file.
Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>
Claude-Session: https://claude.ai/code/session_01GWXznupnma5sEUJ7NrLDvi
* fix: fuzz check and prove functions in Foundry mode
"check" and "prove" functions are symbolic entry points, but a Foundry mode
campaign is a fuzzing campaign: symbolic execution is only used when it is
enabled, so these functions must be fuzzed like any other test function.
Before this, a stateless Foundry campaign (seqLen == 1) would neither call
nor check them, silently testing nothing for contracts whose properties all
use those prefixes.
Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>
Claude-Session: https://claude.ai/code/session_01GWXznupnma5sEUJ7NrLDvi
* test: cover stateful and reverting check/prove functions
The stateless case was the only one covered: add a stateful campaign, where
parameterless "check" and "prove" functions are checked after each
transaction, and a "check" function that reverts, which is a failure like it
is for any other test function.
Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>
Claude-Session: https://claude.ai/code/session_01GWXznupnma5sEUJ7NrLDvi
---------
Co-authored-by: Claude Opus 5 (1M context) <[email protected]>
* allow to disable testing of view/pure function, except prefix ones in property mode
* removed unused import
* test/config: fix remaining CI failures for excludeViewPure
- default.yaml: add excludeViewPure (the config test requires every option be
listed; it was failing with 'unset options: fromList ["excludeViewPure"]')
- Tests/Integration: pin basic/excludeviewpure.sol to solc >= 0.8.0 (pragma
^0.8.0), so it is skipped on the <0.8 solc CI matrix instead of failing to
compile.
Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
* test: prove view/pure functions are excluded, using notPresent
Addresses review feedback: excludeviewpure.sol gains a view function with
a planted assert(false), and a new assertion-mode run checks that no
assertion test is created for any view/pure function (via the previously
unused notPresent helper), so the planted assert can never fire. A control
run without excludeViewPure proves the assert IS found otherwise and pins
the test names the notPresent checks look up.
Co-Authored-By: Claude Fable 5 <[email protected]>
---------
Co-authored-by: Claude Opus 4.8 (1M context) <[email protected]>
Every consumer reads campaign events from its own dupChan, so the
original Chan's read end is never advanced and pins every event ever
written, keeping the whole campaign's event history (including full VM
snapshots) alive. Drain the original queue from a dedicated thread so
the GC can reclaim delivered events, and publish VM-free, strictly
forced copies of falsified/optimized tests so queued events can't
retain a VM through a lazy thunk.
The corpus distribution introduced in 92b90d4a uses integer divMod by
nFuzzWorkers, which throws on workers: 0 (symbolic-only mode, where the
sym worker is the only worker and forces the corpus chunks). Guard the
nFuzzWorkers == 0 case explicitly: there are no fuzz workers to
distribute to, and the symbolic worker replays the full corpus anyway.
* Fix suitableForSymExec precedence inversion
`not $ null m.inputs && ...` parsed as `not (null m.inputs && ...)`,
negating the whole conjunction: the dynamic-argument guard never fired
(so bytes/string/dynamic-array methods were handed to the symbolic
encoder, which throws).
Bind `not` to the emptiness check alone so the filter means what it
says: explore methods that have arguments, none dynamic, not opted out.
* updated to new hevm
* dynamic array handling
* Update hevm in flake.nix
---------
Co-authored-by: gustavo-grieco <[email protected]>
Every call sequence updates the constants dictionary with the lazy
Data.Map's `unionWith Set.union`, which allocates a suspended
`Set.union old new` per colliding key. Such a suspension is only forced
when the generator samples that key's AbiType (genWithDict), and only
the argument types of fuzzed functions are ever sampled. Since callseq
unconditionally inserts an AbiAddressType entry into the additions map
(even when no contract was created), any target ABI without an
`address`-typed parameter accumulates a never-forced chain of union
thunks: one per call sequence per worker, for the campaign lifetime.
On a minimal one-function contract this leaks ~0.4 B/call (~31 kB/s at
~75k calls/s), 100% of live-heap growth: the heap census shows a
single monotonically growing THUNK band, info-table profiling points at
the Map.unionWith specialization's collision branch, and retainer
profiling roots it at callseq's WorkerState.genDict. Note this is
distinct from the dictionary's known value growth -- it happens even
when no new constants are harvested at all.
Use Data.Map.Strict.unionWith so per-key sets are forced as they are
unioned. Measured on the reproducer: live-heap slope drops from
~31,010 B/s to ~3 B/s over 93M calls, with identical coverage and
corpus behavior.
Co-authored-by: Claude <[email protected]>
* Fix shrinking desync between reproducer and vm traces
* Root cause fix
* Proper fix by Emilio
* Add regression test for time-advance-on-revert
A reverting transaction must still advance the block clock; only EVM
state rolls back on a revert, not time. This test exercises that: f()
reverts at og+1 and asserts at og+2, so the assertion is reachable only
if the reverting step still advanced time. With maxTimeDelay=1 and
seqLen=2, the assert is solved iff the fix is present (found in 15/15
seeds at testLimit 500 with the fix, 0/5 at testLimit 10000 without it).
Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
* removed txDelay variable
---------
Co-authored-by: gustavo-grieco <[email protected]>
Co-authored-by: Claude Opus 4.8 (1M context) <[email protected]>
* Fix genDelay to use 0 as lower bound for random delay
genDelay used getRandomR(1, maxDelay) which caused undefined behavior
when maxDelay was 0 (inverted bounds). In practice this leaked delay=1
even when the user configured maxTimeDelay or maxBlockDelay to 0.
Change the lower bound to 0, which fixes the inverted bounds issue and
also allows zero delays naturally (consecutive txs in same block/time),
consistent with how genValue already uses getRandomR(0, ...).
* tests: add no-delay test for maxTimeDelay/maxBlockDelay = 0
Test that with maxTimeDelay: 0 and maxBlockDelay: 0, block numbers
and timestamps remain consistent across transactions (no delay leaks).
* Improve identification of CBOR bytecode metadata
* pick the last prefix if several are present, to work in bytecode-in-bytecode scenarios
(e.g., a contract that deploys other contracts)
* identify CBOR length and drop other trailing data (typically constructor arguments)
* Try CBOR metadata matches from end backwards, pick first valid
In bytecode-in-bytecode scenarios (e.g. a contract deploying another),
the child contract's CBOR prefix can appear in the middle of the parent
bytecode. Previously we only tried the last prefix match and fell back
to full bytecode if it was invalid. Now we try all matches from end to
start and return the first one with a valid CBOR length.
* improved support for foundry tests
* Extend Foundry support testing (#1512)
* Fix lint failures
* ci: bump python version to 3.10, clone submodules
* some fixes when using foundry mode
* Update hevm to `542986dea3bec4f5898731ff48877a7a21811bf4`
* Fix bugs in Foundry test generation (#1516)
* Fix fallback function bug in Foundry test generation
* Fix null byte in argument bug in Foundry test generation
* Remove unnecessary config file
* Remove unused/redundant imports
* Disable Slither in Foundry test gen tests
* Conditionally run forge-std tests based on the solc version
* Reduce unnecessary test grouping and improve failed assertion messages
---------
Co-authored-by: Emilio López <[email protected]>
* Update hevm to `41e6d1304411749ea8c816d131991663b5dca67a`
* Fix linter and build errors (#1521)
* improve foundry stateful invariant testing
* fix
* Fix foundry test generation linter hints and tests (#1522)
* Foundry updates (#1525)
* Rename dapptest to foundry and support foundry assertX in assertion mode
* Rename basic foundry test contracts dir to `foundry-basic`
* Add testing modes to `README`
* fixes
* fixes
* Add support for Foundry assume (#1528)
* flake: sync hevm version with stack.yaml
* Clarify `optimization` test mode in `README` (#1529)
* IS_TEST fix
---------
Co-authored-by: Radu Bahmata <[email protected]>
Co-authored-by: Emilio López <[email protected]>
Co-authored-by: Emilio López <[email protected]>
Sample contracts to test with sourcemaps:
- 0x924fa68a0fc644485b8df8abfa0a41c2e7744444
Single brace, direct format, chainid=56 (BSC)
- 0x58d97b57bb95320f9a05dc918aef65434969c2b2
Double brace, nested format, chainid=1 (Ethereum)
- 0x54261774905f3e6e9718f2abb10ed6555cae308a
Raw source code, chainid=56 (BSC)
* Initial Sourcify support
* Refactor onchain support
* Clean up implementation
* Fix conformance with Sourcify
* Clean up implementation
* Reduce amount of fields requested to Sourcify
* Do not request metadata from Sourcify
* Allow disabling Sourcify and Etherscan
This adds a new config option, `disableOnchainSources`, and a new
CLI flag, `--disable-onchain-sources` that allows disabling coverage
reports for onchain contracts.
* do not fetch if etherscan key is not available and support different chain ids
* etherscan: add support for source maps on other chains
* etherscan: move cache away from Env
* etherscan: remove extra & on URLs
* onchain: remove dead code
---------
Co-authored-by: Emilio López <[email protected]>
* Upgrade `hevm` to `95b5e074c9f27f970011ed53f38f1643d70c3c8a`
* Refactor cache use after hevm upgrade
* fixes
* Added rpc cache serialization code and fixes
* fixes
* fixes
* fixes
* refactor verification code to make sure tests are correctly labeled when the verifiction finishes
* revert b899481b65
* disable RPC logs
* update to the latest hevm
* updated flake
* updated flake
* avoid crashing when trying to do symbolic execution in fallback
* silence RPC warning when there is no RPC configured
* hlint fixes
* switch to stack based loop detection
* Clean up comment, whitespace
---------
Co-authored-by: Emilio López <[email protected]>
* Add cli option to include shrinking status in status lines
A worker event is also logged showing the shrinking operation and the sequence
length before and after each successful step.
* Add `logShrinking` flag to `default.yaml`
* Remove last shrinking op from status line
* Always display shrinking info in status line
* Comment cleanup
* Remove shrinking step log and `logShrinking` flag
* Compute status line reproducer length on demand
* Log per-worker shrinking status
* Display shrinking status when shrinking and active shrinking workers data
Gustavo Grieco