[TS PBT] Run one PBT phase followed by coverage-guided USVM

[CaelmBleidd]

A campaign can now run one bounded PBT generation phase, hand its admitted coverage and bounded original inputs/outcomes to USVM, and continue searching the unchanged original property. COVERAGE_FEEDBACK requires an explicit PBT allocation within the original monotonic total deadline. Frontend preparation, mapping, fixed-input native replay, confirmation and optional shrinking consume that same remaining budget. SEQUENTIAL remains an unguided control; PBT generation never restarts after the handoff.

Input-only observation capture reuses the existing request/artifact with an empty point list; explicit observation points remain supported. Initial source coverage still validates the current property/source identity independently of scoped entry metadata. A PBT phase timeout remains visible and makes CLI completion incomplete, even if later symbolic work completes. A confirmed original fault remains a finding. Saved artifacts retain the used allocation, shrinking control and complete portable guidance trace; stdout and file serialize the same completed run.

Own diff against #572: 10 files, approximately +480/-53; most added lines are the six real-backend campaign regressions, CLI regression and their fixtures. Immediate dependency: #572 at 2bc2ee8d4, which depends on #571 619d80f4b and #569 7e6d9b9c9. The frozen existing-dependency assembly is 342a042ef (#548/#524/#566/#560 on main e56cea501); its implementation is inherited and excluded from this diff. After those dependencies merge, move only this own campaign commit onto main and retarget. No merge to main is performed here.

Validation:

• Six real-backend regressions: changing admitted PBT evidence changes the next symbolic work for the same property; covered prefixes stay traversable; full initial coverage still finds and natively confirms an original defect; SEQUENTIAL passes no guidance; an expired PBT allocation retains an explicit outcome and leaves symbolic work possible; [TS PBT] Preserve runtime limitation reasons in property-search results #555 source/reason diagnostics survive artifact write/read.
• Public CLI regression verifies one PBT batch, bounded inputs/outcomes and identical stdout/file evidence. Native feedback, source-snapshot metadata and direct campaign/artifact controls passed focused checks, including source drift and replay failure.
• 216 Node adapter tests passed. Detekt main/test for both PBT modules reports zero findings after final cleanup; diff check is clean.

This delivers the coverage phase of #355/#354, not observation-derived relation guidance or comparative superiority. Independent SYMBOLIC_ONLY class coverage still needs bounded native replay of successful symbolic terminal inputs; an absent violation is not an absence of coverage.