[TS PBT] Evaluate runtime-derived PBT hints for symbolic search

[CaelmBleidd]

Goal

Evaluate whether limited runtime observations from a concrete PBT backend can improve property-directed USVM search.

Why

Runtime-derived hints may help USVM prioritize likely input types and shapes, but they may also add overhead or steer the search away from counterexamples.

Observations are an optional PBT backend capability. The Kotlin orchestrator should consume a common observation artifact rather than depend on fast-check-specific callbacks or runtime objects.

The value of this feedback loop must be measured against the completed baseline pipeline before implementing a general invariant-mining subsystem.

Scope

• Define a versioned, backend-neutral runtime observation artifact.
• Collect a minimal set of observations at property boundaries through compatible PBT backends, initially fast-check:
  • runtime type;
  • null and undefined occurrence;
  • numeric ranges;
  • string length;
  • array length.
• Convert selected observations into temporary symbolic-search hints in Kotlin.
• Add an experimental HYBRID_WITH_RUNTIME_HINTS(pbtBackend, USVM) mode.
• Run the hinted symbolic attempt under a bounded part of the budget.
• Always run a hint-free fallback when the hinted attempt does not produce a confirmed violation.
• Attribute results to the PBT backend, hinted attempt, or fallback.
• Compare against HYBRID(pbtBackend, USVM) using the same concrete backend and:
  • time to counterexample;
  • reached targets;
  • explored states;
  • solver calls and solver time where available;
  • replay-confirmed violations;
  • fallback frequency.
• Report backends without observation support explicitly.
• Include cases where observations are useful and where they are misleading.
• Do not implement general object-shape or relational invariant mining in this issue.

Definition of Done

• The same Kotlin property set and PBT backend can be executed in HYBRID and HYBRID_WITH_RUNTIME_HINTS.
• fast-check observations are exposed through the common artifact rather than fast-check types.
• Hinted execution never replaces the mandatory hint-free fallback.
• Reports distinguish backend execution, hinted results, and fallback results.
• A misleading-observation fixture verifies that fallback preserves counterexample discovery.
• The experiment measures the overhead and benefit of each supported hint kind.
• Results state whether the tested hints improve, degrade, or do not affect symbolic search.
• Threats to validity and unsupported backend or observation capabilities are documented.
• A decision is recorded to either:
  • create a follow-up production feature;
  • keep only a smaller hint subset;
  • reject runtime-derived hints from the final pipeline.
• The experiment and its conclusions are delivered in a dedicated PR linked to this issue.