[TS PBT] Run two-phase campaigns with shared budgets and result artifacts #354

Scope agreed on 2026-10-16

One concrete PBT generation phase is followed by one USVM search phase. No return to random generation is required. Concrete replay and optional shrinking validate a USVM candidate; they are not a second PBT generation phase. This replaces the previous repeated-round acceptance.

Existing implementation

The direct controls (#540), saved artifacts (#542), CLI (#545) and scoped metadata (#548) are implemented in open PRs. Retain these deliveries; do not replace their runner or serialization layer.

Contract

• Support PBT_ONLY, SYMBOLIC_ONLY and SEQUENTIAL controls. [TS PBT] Integrate one PBT evidence phase followed by guided USVM search #355 adds a guided two-phase mode using the same property, support, oracle, deadline and artifacts. SEQUENTIAL passes no PBT guidance into USVM.
• In the guided mode, run PBT once, retain its bounded inputs, outcomes, observations and coverage, then let USVM use the remaining allocation. Stop policy and the allocation are explicit configuration.
• One monotonic deadline includes collection, frontend/mapping, optional one-time inference, search, native validation and reduction. Retain actual elapsed time and overruns at cooperative boundaries.
• Preserve confirmed faults and incomplete results. Timeout, unsupported execution, invalid property, solver uncertainty and infrastructure errors remain distinct.
• Record the used controls, source/property identity, actual runtime versions, observation/coverage capability and available provenance. [TS PBT] Record scoped campaign metadata and observed Node versions #548 currently hashes entry modules and explicit tsconfig only; do not describe it as a complete imported-source/build identity.
• Keep artifacts usable without rerunning PBT. Omit session/round revision protocols, returned-input corpora and work-reuse counters from this delivery.

Acceptance

One ordinary command runs each direct control and the enabled two-phase mode without resetting the deadline or generating new random inputs after the USVM phase starts. The same completed artifact is printed/saved and can be read independently. No-feedback, no-observation and no-shrinking controls remain valid. The direct shell can be accepted before observation-derived challenges are implemented.