Skip to content

Concrete sequence replay with a JSON report - #1606

Open
elopez wants to merge 2 commits into
feat/prioritized-sequencesfrom
feat/sequence-replay
Open

Concrete sequence replay with a JSON report#1606
elopez wants to merge 2 commits into
feat/prioritized-sequencesfrom
feat/sequence-replay

Conversation

@elopez

@elopez elopez commented Aug 14, 2026

Copy link
Copy Markdown
Member

A caller hands a fuzzing worker a concrete sequence of transactions and gets back a JSON report of what it did. This is what lets something outside the campaign ask "what does this sequence actually do?" without guessing from coverage.

ExecuteSequence joins the commands a worker accepts over the bus. 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.

executeSeq lands in its own Echidna.Worker.Replay — nothing about it is fuzz-specific, and Worker/Fuzz.hs is not the place to accumulate it.

{"failed_tx_index":3,"final_block_number":"0x42ae50","final_timestamp":"0x5ae26348",
 "status":"assertion_failed","transaction_count":3,"transactions":[
   {"call":"Test.assert_revert(1)","gas_used":21609,"index":1,"logs":[],
    "result":"Stop","status":"completed"},
   {"call":"Test.assert_unreachable()","gas_used":21202,"index":2,"logs":[],
    "result":"ErrorRevert","status":"reverted"},
   {"call":"Test.assert_revert(200)","gas_used":23398,"index":3,
    "logs":["AssertionFailed(«error») from: 0xa329c0648769a73afac7f9381e08fb43dbea72"],
    "result":"ErrorRevert","status":"assertion_failed"}]}

Asking for the trace adds a trace field. Traces are cleared before each transaction unless allEvents is set, so in the usual case that is the last transaction's trace alone, which is what keeps the cost bounded — showTraceTree is not cheap.

Nothing sends this command yet; the MCP server that does is the next rung.

Notes for review

Four places where this deliberately departs from the dev-agents-3 original:

  • Assertion detection was dead code. The original matched "AssertFail" and "Panic(AbiUInt 256 1)"; neither string is ever produced. Echidna emits AssertionFailed(...), which does not contain AssertFail, and hevm's Show AbiValue renders AbiUInt _ n as just n, so the revert text is Panic(1). assertion_failed could never be reported. This uses checkAssertionEvent and checkPanicEvent "1" from Echidna.Test instead — the same pair checkAssertionFailure uses — and a test covers each path.
  • The summary reports the sequence's worst transaction, not its first failure. The original returns "reverted" for a sequence where tx 2 reverted and tx 3 failed an assertion. Reverts are routine in a random sequence, so first-failure buries the finding.
  • TxStatus/TxOutcome replace the four-tuple accumulator, whose mbFailed and mbFailedStatus were always set together for the same index, and the stringly-typed case mbFailedStatus of Just "assertion_failed" -> … that read them back. result uses TxResult's existing ToJSON rather than show.
  • The trace is ANSI-stripped with stripAnsiEscapeCodes, as UI/Widgets.hs already does for the same reason: whoever reads this report is not a terminal, so the escape codes are only tokens wasted.

Also dropped the original's when (workerId == 0) guard inside the handler — checkMessages already filters on tid == workerId, so exactly one worker ever replies.

Reply is a newtype over TMVar with an opaque Show, so FuzzerCmd keeps its derived Show instead of needing a hand-written instance that can drift as constructors are added.

Follow-up for the MCP rung

The worker replies on its own thread, so a replay stops that worker fuzzing while the caller waits. More importantly, if the addressed worker has already reached its test limit, nobody replies at all — the MCP tool needs a timeout rather than a bare takeTMVar.

Testing

  • cabal build clean, no warnings, no new dependencies.
  • cabal run tests — 195/195, including five new Sequence replay cases. One asserts the campaign's coverage stats and corpus size are unchanged across a replay; another checks solc's Panic(1) path, gated on solc ≥ 0.8.
  • hlint lib src clean for the files touched.
  • A 4-worker campaign on basic/flags.sol still runs and terminates, exercising the checkMessages signature change in the hot loop.

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 <gustavo.grieco+github@gmail.com>
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant