[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.

Delivery status (2026-10-17)

The public runner/CLI/artifact chain is published through #588. #594 preserves bounded generated inputs at cooperative PBT allocation expiry; #597 consumes compact original receipts and keeps omissions explicit. #607 supports an explicit export up to 64 MiB while retaining the default 2 MiB export. #603 adds optional one-time relation guidance to the same runner and charges inference, challenges, original-native confirmation and an unrestricted-original reserve. #610/#611 are integrated in frozen local assembly c447392006cb72b06ead3d857b639a23d7e259c9, not merged main.

The final 108-cell scalar study completed with all 108 artifacts eligible under a 60-second outer monotonic process deadline, including JVM startup and DSL compilation. Its retained local typed launcher passes only actual remaining time after a one-second serialization reserve, explicitly sets the original-machine cap to 60 seconds, and leaves the existing runner's minimum-with-remaining behavior intact. First-fault timestamps were not measured; reported wall time ends at the completed receipt.

Frozen command-boundary evidence and published follow-up

The separate 144-cell class pilot used the ordinary installed CLI under a 30-second total caller budget, including preparation and eight seconds reserved for checked class replay. It produced 89 full eligible cells and 55 incomplete cells. Observations overlap: 47 external runner deadline kills (timedOut=true, exit -9), 45 missing-completed-artifact diagnostics, one unterminated campaign JSON, eight saved campaigns with unchecked native inputs, and one recorded [Errno 1] Operation not permitted. The permission error is one specific cell and does not explain the other failures.

One narrow publication-order failure is proved: SinglyLinkedList-wide / seed 16061113 / SYMBOLIC_ONLY has exactly 65,536 stdout bytes beginning with serialized result JSON, but no saved campaign file. The CLI currently serializes, appends JSON to stdout and then writes the file. The narrow file-before-stdout defect is tracked in #612; its repair is published as #614 (4c37ea13cd8d888e35db79a90a2c85c96315d63f) on the minimal public #581 parent. Four focused tests and strict Detekt pass locally. It is open, not merged, and is absent from all frozen c447 measurements. This does not establish why other cells have empty stdout or solve native-verification throughput.

In the frozen pilot, the caller started its deadline before JVM/CLI initialization and the inner runner created a fresh deadline later. Per-cell origin offsets and their causal contribution were not measured. The focused fix is now published as #615 (696e5e9946bb94c94339a1f4d45c6e0860c53736) and caller #616 (560b23d494509d726be2a6347e948b45e7dbf1aa) under #613. They retain original controls, convert the caller cutoff once, charge Popen, keep the class/publication reserves within the same allocation, and withhold credit from killed/late/incomplete results. They remain open/unmerged. The following acceptance is retained separately from the narrow #612/#614 output-order repair:

• Propagate a caller-established absolute deadline, or deduct measured startup/setup from the inner allocation, with observable deadline origin and actual remaining time at handoff.
• Reserve bounded time for serializing and publishing the completed artifact within the caller deadline. Preserve partial search/native-validation dispositions if work cannot finish.
• Test the installed command under a caller deadline, including slow/failing stdout and interrupted publication. Do not restart PBT, reset the budget, hide omitted inputs or retroactively rescore frozen measurements.

The class pilot's maximum original-query allocation was at most 20 seconds before preparation, so the CLI's existing default 20-second machine cap did not cause a shorter symbolic allocation in this protocol. No new round/session framework is required.

A separate one-off joint functional check with a two-second launcher delay inside 30 seconds saved a valid artifact without an outer kill: exit 2, DEADLINE/CONFIRMATION, 67 unchecked symbolic inputs, no coverage/primary credit. #613 records the pinned receipt and timing boundary. It is not another comparative cell and does not rescore frozen c447 evidence. Publication reserve, synchronous IR loading/filesystem work and cleanup remain cooperative; exact original phase offsets are not claimed.