Validate selected properties against executable backend oracles

Context

The completed Aave v4 invariant-only postmortem in #523 found that most ScFuzzBench failure observations had no semantically equivalent executable oracle in the generated suite: one exact inequality existed, two properties were partial analogues, and seven were absent, deferred, or ineffective. The immediate controlled rerun in #522 is intentionally limited to correcting the generic Recon sequence-length defect fixed by #521. We should not steer that rerun with benchmark-specific property text.

This issue tracks the later, generic property-specification and executable-oracle work separately.

Problem

The current workflow can record a high-priority property as selected or implemented without proving all of the following:

1. the executable assertion has the same semantics as the selected property;
2. the backend admits and invokes its entrypoint;
3. the prerequisite state and protocol call are reachable;
4. the backend can observe the intended failure mode.

For Recon assertion mode in particular, a direct typed call that unexpectedly reverts is discarded rather than reported as an assertion failure. A liveness property therefore needs selector-aware behavior: accept documented reverts and turn an unexpected selector into a Recon-detectable assertion failure. Merely removing broad try/catch blocks does not supply that oracle.

The Aave run also showed examples of selected temporal properties being deferred, supply/repay liveness being marked implemented without an effective unexpected-revert oracle, and handler preconditions making important protocol paths vacuous. These are motivating evidence, not a request to add Aave-specific benchmark names or formulas to stock prompts.

Scope

Implement generic validation between property selection, generated harness code, admitted backend targets, and runtime evidence. Coordinate with:

• #424 for persistent sequence-wide ghost/operation state;
• #519 for generated public properties omitted by Recon smart filtering;
• #523 for the run postmortem and reachability/coverage evidence;
• #522 for the sequence-only controlled rerun.

Acceptance criteria

• Every property recorded as implemented identifies its executable oracle and admitted backend entrypoint.
• Liveness properties encode documented allowed error selectors and convert unexpected selectors into backend-detectable failures.
• Regression coverage proves that a plain direct target revert in Recon assertion mode is not incorrectly treated as a liveness oracle.
• Property implementation evidence distinguishes exact, partial/weaker, and deferred semantics instead of treating source presence as equivalence.
• Handler/property evidence reports prerequisite-state and protocol-call reachability or an explicit blocker, so vacuous properties cannot pass silently.
• The mechanism is protocol-agnostic: do not place Aave v4 or ScFuzzBench-specific properties, names, selectors, or formulas in stock prompt templates.
• Re-evaluate the affected property families on a later sealed run only after the generic gates are in place.

Non-goal for the current rerun

Do not change property prompts or generated Aave harness code before the sequence-length-only experiment in #522. That run should isolate whether genuinely stateful sequences alone surface any existing assertion/property failures.

Start by reading the related issues #424, #519, #523, and #522, then trace the Recon assertion mode and the property-selection workflow they describe. Done means generic gates connect selected properties to admitted entrypoints, runtime oracle evidence, reachability, and exact or weaker/deferred semantics without adding Aave-specific prompt content.