* 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.
* 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]>
Slither classifies seed() as a constant function (no state reads or
writes), so Echidna demotes it to the low-priority signature map, which
genTx samples with probability 1/1001. The test can only be solved by
harvesting seed()'s return value (1337 + 13337) into the dictionary and
then generating find(14674), so a campaign capped at 10000 transactions
failed whenever the RNG drew seed() too late or never (~0.8% of runs).
Add a dummy state write to seed() so it stays in the high-priority map
and is sampled like any other function. The value 14674 still exists
only as a runtime return value, so the test still exercises return
value harvesting. Modeled failure rate drops from ~1/120 to ~1/90000.
Same workaround precedent: values/contract.sol ("writes state to make
it non-pure and more likely for echidna to call").
* 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
* 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]>
* 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]>
* 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).
* 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]>
* 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.
* HTML coverage report improvements
This brings the coverage report improvements developed for Medusa
into Echidna.
* Fix file tree search behavior
Searching will now only open the file tree branches that contain matches.
Also clearing the search box will now properly clear the highlights and
close the file trees.
* Add timestamp to report
* Small report UI tweaks, linting
* Return to original coloring logic
* Fix hlint warnings
* Refactor report generation
* Add coverage report filtering option `coverageExcludes`
This option takes a list of globs and removes those files from
coverage reports. Example: `coverageExcludes: ["lib/**/*", "test/**/*"]`
Fixes: #1391
* Remove unused code
* removed old solc versions, use 0.8.x only instead
* fixed harvey test
* started to fix symexec using latest hevm
* added RPC support for symbolic execution + some clean up
* better constraints for block timestamp and number
* improved and simplified symexec code
* removed useless code
* some test fixes
* increase the number of random symbolic transaction if the corpus is empty
* added comments on why we only take one method from the shuffle list when doing symbolic exploration
* allow user to select smt solver
* use slither to filter functions with assert, if any
* started adding full verification mode for stateless campaigns
* refactored tons of code
* improved code for exploration/verification
* finished implementation and get back to hevm master
* fixed issue in addBlockConstraints and upgraded hevm
* disable debug mode when using interactive mode
* corrected array size in symbolic output
* fix decoding of negative numbers
* simplified code for decoding of negative numbers
* removed initialize field from default
* use verification mode for sym-assert test
* added some basic verification tests
* make the harvey test more reliable
* simplified exploration code and added shrinking
* added new test for exploration mode (but disabled so far)
* worker related refactoring code to allow other parts of the codebase to send events
* make sure symExecTarget is used to select methods
* keccak preimage support enabled
* reduced code duplication
* added documentation
* use new types in Types/Config.hs
* removed killed-related files
* modify callseq to store event changes into the corpus
* fixes#883
* chore: fix imports
* fix: simplify extractEventValues to take two vms and return the emmitted logs between them
* chore: remove redundant imports
* add test
* add campaign test to valueTests
* modify campaign test to take a seed value
* add campaign.yaml
* rename test from campaign to events
* reduce test limit
* fix ordering in callseq for computing additions and constants
* descending order is more efficient
* Map.unionsWith can elegantly replace foldl
Gustavo Grieco