Generate sequence-wide ghost and operation state in BeforeAfter scaffolds #424

Split from #405. Closing that analysis issue does not mean this engineering work has shipped.

Problem

The invariant setup prompt says only to initialize ghost or tracked state, and the handler prompt says only that updateGhosts must precede actor/admin modifiers. Neither defines the sequence-wide state needed by temporal or operation-conditioned properties.

R52 produced a 45-line BeforeAfter.sol containing a flat before/after snapshot for one active asset and actor. The ScFuzzBench reference additionally retained:

• maxima observed across the entire sequence;
• an Operation enum; and
• an isAnyUserLiquidatable flag.

Consequently, the generated suite could compare only adjacent wrapped steps. A handler on asset A that perturbed asset B could escape an active-asset snapshot, and the suite could not express “no operation other than a price change may make a user liquidatable.”

Expected behavior

For selected temporal or operation-conditioned properties, generated Recon/Chimera scaffolding should derive the persistent ghost state and operation identity needed to observe the property across the complete fuzz sequence.

This must be target-derived rather than Aave-specific. Depending on the property, it may include per-entity extrema, ever-observed flags, previous valid values, operation discriminants, or other sequence state. A universally quantified property must cover every relevant actor, asset, market, or position rather than only the currently active manager selection.

Setup, handler, coverage, and implementation handoffs must agree on which handlers update each ghost field and which operation identity surrounds each protocol action.

Acceptance criteria

• Setup and implementation prompts require persistent sequence-wide ghost state when a selected property cannot be expressed by one adjacent before/after pair.
• Handler generation assigns a stable operation discriminant to every mutable action relevant to an operation-conditioned property.
• Ghost and snapshot updates occur in a documented order around the protocol call while preserving the existing requirement that updateGhosts not consume the actor/admin prank.
• A property quantified over multiple entities tracks all relevant entities; changing the active manager does not make effects on inactive entities invisible.
• The handler coverage handoff identifies which handlers and operation labels update each required ghost field.
• An uninstrumented state-changing handler that can affect a selected temporal property produces an explicit coverage blocker instead of a falsely complete property.
• Regression coverage includes a sequence-wide extremum that remains observable after later operations, an operation-conditioned property that distinguishes a permitted operation from other actions, and a cross-entity effect where an action on one entity changes another.
• Recon constructor compatibility, natural failure propagation, and existing typed-call requirements remain intact.
• Suites without sequence-wide properties are not forced to add unrelated generic ghost state.

Non-goals

This does not hard-code Aave fields or require every invariant to become temporal. It supplies the scaffold required by properties whose catalogued semantics already span operations.