fix(runtime): correct the assertion-mode revert guidance and warn about invariant checks that cannot fail (#687)

[mrthankyou]

Refs #687 (and the residual of #524 that moved there). Warn-only, as discussed on #524: nothing here fails a node.

Problem

Recon runs in assertion mode (recon fuzz --test-mode assertion): only a failed assert is a finding, and a call that reverts for any other reason is discarded. Four invariant prompts said the opposite, that every reached revert "is the signal the campaign records" (handlers.md:86-87, invariant-testing-campaign.md:86-90, coverage.md:69-71, implement-properties.md:109-110). That steers agents toward liveness checks and require post-conditions that can never fail. Nothing checked the generated Solidity, so a suite that could not fail looked like a clean campaign (#687: 7 of 12 implemented properties).

Changes

Prompts. The four passages now state assertion-mode behaviour, require assert for every invariant or correctness check, and describe the selector-aware liveness oracle: the typed call in try, catch (bytes memory reason) accepting only the selectors the catalog documents for that action, and assert(false) for any other selector, an empty reason or a panic. That is the only accepted try/catch around a protocol action; blanket try/catch stays an audit violation.

Warn-only checks (packages/artifacts/src/invariant-oracle-warnings.ts, gate invariant-oracle-falsifiability). The campaign node (the one declaring ultrafuzz/property-campaign@3) reads the test sources of the suite it ran, test/ and tests/ only, and warns about:

Code	Flags
INVARIANT_ORACLE_CONSTANT_TRUE	assert(true), t(true, …), assertEq(x, x), assert(a == a)
INVARIANT_ORACLE_REQUIRE_DISCARDED	a require after a call made for its effect (a statement call or try); a guard after a read such as x = vault.balanceOf(a) is not flagged
INVARIANT_ORACLE_BLANKET_CATCH	a catch whose body asserts nothing (rethrowing does not count: Recon discards the rethrown revert)
INVARIANT_ORACLE_IMPLEMENTATION_CALL	an assertion calling a library or contract imported from src/ or contracts/ (#687's MathLib case)

The final report reads warnings only from its direct dependencies, so the node that writes the finding lifecycle ledger (dedupe-findings, which depends on the campaign in every shipped topology) forwards them, keeping their artifacts/<campaign>/… location. The report's warnings companion lists them first under "Invariant checks that may not be able to fail (N)". report.md itself still renders no warnings, per the current report design; adding the count there is a separate call.

These are text heuristics, so they can miss a case and a flagged line can be deliberate; they mark a check for review rather than prove a property untested, which is why they warn rather than fail.

Evidence

All runs inside a Linux Podman container (Ubuntu 24.04 arm64), recon-fuzzer v0.4.17 built from its tag (the version the Modal image pins; there is no prebuilt Linux arm64 binary), with recon-generate@0.0.42, slither-analyzer==0.11.5 and the pinned covg-eval.

1. Recon's semantics, on a purpose-built seeded target

A small share vault with a plain-language spec and three ordinary-looking bugs (withdraw rounds up against a "round down" spec; a full exit reverts with an undocumented DustFloor(); collectFees() never zeroes feesAccrued), fuzzed with hand-written CryticTester harnesses (--test-mode assertion):

Harness	Expected	Recon
plain direct call to the reverting withdraw	no finding	passing (revert discarded)
selector-aware try/catch, undocumented selector → assert(false)	finding	failed
same pattern, only the documented InsufficientShares()	no finding	passing
oracle re-deriving the implementation's own formula	no finding	passing (cannot fail)
oracle from the spec ("rounded down")	finding	failed
require(balance >= assets + fees) after collectFees()	no finding	passing (discarded)
the same check with assert	finding	failed
arithmetic underflow (Panic(0x11))	—	passing (discarded too)

This is what the prompt text now states. The target and harnesses are not committed.

2. Before/after with Opus 4.8 (one pair, evidence not proof)

The same seeded target, a trimmed 21-node invariant-only topology (two property lanes, all five stateful stages), unstable prompts vs this branch:

	unstable	this PR
Properties implemented	12	17 (+1 blocked)
Seeded bugs the implementation agent reported	0 of 3	3 of 3
Generated suite fuzzed 15 min with Recon	catches all 3	catches all 3
Oracle warnings on the generated suite	0	1, a true positive (property_viewGettersNoRevert: view calls then t(true, …); it passed under Recon)

Neither run reached its campaign node because of an unrelated failure in the coverage stage on both branches (to be filed separately), so the "fuzzed" row is Recon run by hand on each agent's generated suite. On this small target Opus 4.8 wrote falsifiable suites under the old prompts too; the case for the prompt change is §1, not detection here. The analyzer raised no false positives across the 20 generated test files.

Tests

Linux container: @ultrafuzz/artifacts 336/336 (3 new analyzer tests: a falsifiable suite with guards, documented-selector catches, spec-derived bounds and require text inside strings produces no warnings; each #687 pattern is flagged at its line; only test sources are read), @ultrafuzz/prompts 62/62, runtime supporting suite all green except generated Smithers pinned source proof counts hidden unreachable commits…, which fails identically on unstable in the container; runtime.test.ts report / invariant / warning batches all pass. A new final-report-markdown test covers the counted section. Prompt wording is not pinned by a test, per prompt-structure.test.ts's stated policy; the warnings measure what agents actually produce instead.

Not in this PR

• Typed deferral blockers (blocker.code is free text): a schema change.
• Rejecting an expected-value expression token-equivalent to the observed implementation expression; the import check is the cheap proxy for now.
• Confirming whether Invariant implementation defers benchmark-critical properties without coverage gate #238's deferral gate regressed: needs a real campaign.
• Failing the artifact contract instead of warning, once false-positive rates are known from real runs.

🤖 Generated with Claude Code

Confidence Score: 5/5

The PR appears safe to merge, with a non-blocking performance issue in warning generation.

Findings

1.  Large suites slow verification ▶

Fix with agent prompt

### Issue 1
packages/artifacts/src/invariant-oracle-warnings.ts:264-266
`lineOf` scans from the start of the file for every warning. The analyzer also builds all warnings before `boundArtifactValidationWarnings` applies the limit. With files allowed to reach 16 MiB, many flagged checks can make campaign verification slow even though most warnings will be discarded.

Build a line-offset index once per file and stop collecting warnings when the warning budget is reached.

---

For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.

Summary

The PR corrects Recon assertion-mode guidance and adds advisory checks for generated invariants.

• Invariant prompts now explain how Recon reports failed checks.
• Invariant campaigns flag generated checks that may not produce findings.

Diagram

%%{init: {'theme': 'neutral'}}%%
flowchart LR
  A[Campaign suite test sources] --> B[Oracle warning checks]
  B --> C[Campaign verification marker]
  C --> D[dedupe-findings forwards warnings]
  D --> E[Final report warnings companion]

Loading

_{Reviews (3) · Last reviewed commit: "Merge unstable into invariant guidance f..." · Reviewed by Greptile}

[greptile-apps]

Large suites slow verification

lineOf scans from the start of the file for every warning. The analyzer also builds all warnings before boundArtifactValidationWarnings applies the limit. With files allowed to reach 16 MiB, many flagged checks can make campaign verification slow even though most warnings will be discarded.

Build a line-offset index once per file and stop collecting warnings when the warning budget is reached.

Prompt To Fix With AI

This is a comment left during a code review.
Path: packages/artifacts/src/invariant-oracle-warnings.ts
Line: 264-266

Comment:
**Large suites slow verification**

`lineOf` scans from the start of the file for every warning. The analyzer also builds all warnings before `boundArtifactValidationWarnings` applies the limit. With files allowed to reach 16 MiB, many flagged checks can make campaign verification slow even though most warnings will be discarded.

Build a line-offset index once per file and stop collecting warnings when the warning budget is reached.

---

For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.