Repository navigation
Description
Context
Split out of the Aave v4 postmortem (#523) so the remaining work is protocol-agnostic and
independently trackable. #523 is closed as the historical postmortem for
aave-v4-v056-gpt55-xhigh-invariant-only-20260811-full-timeout.
That run completed all 75 workflow nodes, ran its backend for the full configured timeout, passed
every artifact gate, and published a final report with zero protocol issues. It was nevertheless
structurally unable to observe the property families it was later evaluated against: temporal
share-price properties were deferred, the liquidation and withdraw oracles were deferred or
excluded debt-bearing states, and supply and repay liveness were marked implemented while their
executable handlers implemented no failure oracle and their protocol calls were unreachable.
Nothing in the run's own output said so. A backend that completes normally currently produces a
report that looks equally trustworthy whether or not the properties needed to falsify anything
were reachable.
Problem
Campaign completion and benchmark comparability are conflated. campaign_outcome: complete today
means "the backend ran to its configured end", but it is consumed as "this campaign's negative
result is meaningful". There is no verdict surface that says a completed campaign is only
partially comparable because required property families were deferred, had no executable oracle,
or were demonstrably unreachable.
Adjacent issues produce the inputs but stop short of the verdict:
- Invariant campaign can report complete when Recon smart-filter drops a generated property #519 marks a campaign partial only for the specific case of a smart-filter-omitted generated
property. - Validate selected properties against executable backend oracles #524 produces per-property executable-oracle and reachability evidence, but its acceptance
criteria end at evidence, not at a comparability classification.
Expected behavior
A campaign that completed its backend normally but could not observe required property families is
reported as semantically incomplete or partially comparable, distinctly from both a clean negative
result and an operational failure.
Acceptance criteria
- Campaign artifacts carry a comparability verdict separate from
campaign_outcome, with at
minimumcomparable/partially-comparable/not-comparableand a machine-readable
reason set. - The verdict is derived from declared inputs, not prose: deferred property families,
properties with no executable oracle, and properties whose entrypoint or protocol call is
demonstrably unreachable. It consumes Validate selected properties against executable backend oracles #524's evidence where available and fails closed when
that evidence is absent. -
report.mdandreport.jsonrender the verdict and its reasons; a partially-comparable
campaign cannot present a zero-finding result as an unqualified negative. - Eval scoring and the report bundle propagate the verdict, so a partially-comparable row is
reported as invalid rather than as zero. - The rule is protocol-agnostic and driven by the run's own declared property families.
- Regression coverage: a campaign that completes with every required family deferred or
unreachable is classifiednot-comparable; one with a subset deferred is
partially-comparable; one with full oracle and reachability evidence stayscomparable.
Activity
aviggiano commentedon Aug 12, 2026
Closing as it's not super important