Invariant campaign can report complete when Recon smart-filter drops a generated property #519

Problem

A completed invariant campaign can silently omit a generated public property_* function from Recon's effective test set while still reporting the campaign as complete and usable.

In an Aave v4 invariant-only run, the generated and compiled Properties.sol ABI contained nine public property_* functions. Recon v0.4.17 logged:

Found 57 fuzzable functions (smart filtered from 58 total, 37 view/pure with assertions)
Created 58 tests for mode 'assertion'

The admitted test list contained only eight property_* functions. It silently omitted:

property_hub_asset_accounting_matches_formula()

That function is public, appears in the compiled ABI, and contains assertions through internal helper calls. The final campaign artifacts nevertheless reported:

• campaign_outcome: complete
• usable_results: true
• 58 passing entries
• zero failures

The 58 entries were eight properties, 49 targets, and Recon's generic AssertionFailed(..) entry.

Impact

A property can be marked implemented in the implementation ledger and exist in the generated suite, yet never execute in the final fuzzer campaign. This creates an undiagnosed false-negative risk and makes "campaign complete" overstate the effective property suite.

Suggested invariant

Before accepting a campaign as complete, compare the intended public property entrypoints (preferably from the compiled target ABI or a sealed suite manifest) with the backend's admitted/passing entry names.

If any intended property is absent, the campaign should:

• emit a precise diagnostic naming each omitted property; and
• become partial/blocked, or otherwise explicitly mark property-suite coverage incomplete.

Improving generation so public property entrypoints contain directly discoverable assertions may help, but a deterministic runtime/artifact gate is still needed because backend filtering behavior can change.

This is a generic campaign-integrity check; it should not depend on Aave-specific prompts or property names.