[TS PBT] Assemble the end-to-end PBT and USVM pipeline

Start by tracing the existing command, options, backend phases and phase artifacts, then review dependencies #353 and #384. Implement and test one reproducible command covering PBT_ONLY, SYMBOLIC_ONLY and sequential HYBRID with observable deadlines, statuses and reports. Done means the listed end-to-end paths, fixtures and documentation work without claiming unsupported coverage guidance.

Part of #345. Depends on #353 and #384.

Goal

Provide one reproducible command for PBT_ONLY, SYMBOLIC_ONLY and a precisely defined sequential HYBRID baseline.

Baseline algorithm

• Load and validate one common property definition and the selected backend capabilities.
• PBT_ONLY runs the concrete campaign and backend shrinking within its deadline.
• SYMBOLIC_ONLY runs USVM property-violation search and concrete validation. A concrete runtime is still required to confirm candidates, even though it performs no random generation.
• HYBRID first runs the concrete campaign up to its configured phase cap. If it finds a concrete violation, preserve and minimize that result as budget permits. Otherwise run USVM against the same property failure condition, then replay and optionally shrink its candidates.
• An unsupported engine phase can be skipped with an explicit status while the supported phase proceeds. Property-definition errors stop the affected property; they are not an invitation to run a different meaning of it.
• The initial hybrid is a sequential portfolio. Concrete coverage is collected/reported when available, but does not silently become a search constraint or an implemented residual-target scheduler.
• A later coverage-guided mode needs a separately specified target-selection algorithm, actual backend support and an ablation against this portfolio. It is not required to complete this baseline.

Budgets and configuration

• Use one monotonic total deadline per property and explicit caps for generation, symbolic search and concrete validation/shrinking whose sum does not exceed the total.
• Choose and freeze the phase allocation in the benchmark configuration before evaluation; no adaptive allocator is required.
• Unused earlier phase time may pass forward subject to the total deadline. Reserve validation time before starting symbolic search; stop producing candidates when validation cannot be attempted within the remaining budget.
• Count relevant startup, frontend/adapter work, search, replay and shrinking in total time. Report one-time shared setup separately and consistently between modes.
• Record selected properties, backend ID, actual backend/tool versions, phase caps, seeds and output directory using existing options.
• Use pinned dependencies and actual-version reporting. Do not add version-range resolution, backend compatibility negotiation, plugin discovery or a general configuration framework.

Results

Reuse existing phase artifacts in one run directory and produce a small per-property summary: mode, effective configuration, phase statuses/durations, optional source coverage, concrete result, symbolic candidates, replay results, final confirmed counterexample and limitations.

No violation found within the budget, confirmed violation, unsupported phase, timeout and tool/property-definition error remain distinct. If validation cannot run, retain an unconfirmed candidate; if only shrinking fails, retain the confirmed original.

Definition of Done

• One command exercises all three modes on the same example properties.
• A hybrid fixture demonstrates a USVM candidate confirmed by the original TypeScript predicate.
• A holding property is not reported as proved by bounded unsuccessful search.
• The no-coverage and no-shrinking paths work. #382 does not block this baseline.
• End-to-end tests cover a violation, no found violation, unsupported phase, timeout and backend failure.
• Total deadlines and phase allocation are observable and enforced.
• Reports identify the finding engine and concrete validation backend.
• The command and limited extension point are documented without claiming unimplemented feedback or coverage-guided behavior.