[TS PBT] Integrate one PBT evidence phase followed by guided USVM search #355

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.

Goal

Implement the agreed product path: one PBT run exports its evidence, then one USVM analysis searches the unchanged original property. This issue replaces the earlier iterative feedback-loop task.

Implementation

• Reuse [TS PBT] Run two-phase campaigns with shared budgets and result artifacts #354's runner, configuration, total deadline and artifacts, plus the existing DSL and property model. Do not introduce another campaign engine.
• Collect bounded original inputs, original predicate/check outcomes, requested observations and admitted coverage in the PBT phase. Record truncation or missing capabilities instead of rerunning PBT to recover data.
• Prepare one compatible frontend/mapping and original-property analysis. Start with declared domains AND admitted precondition AND NOT(original property).
• Transfer exact admitted edge evidence through [TS PBT] Transfer exact admitted c8/EtsIR edges into one USVM search #382/[TS PBT] Prioritize original-property, uncovered-edge and optional relation goals in one USVM phase #399. Covered edges leave coverage goals but remain traversable; covered code remains eligible for finding a property violation.
• When explicitly enabled, infer/select relations once through [TS PBT] Infer bounded numeric hypotheses once from PBT observations #397 and bind/challenge them through [TS PBT] Bind one-time observed relations to exact symbolic challenges #398/[TS PBT] Prioritize original-property, uncovered-edge and optional relation goals in one USVM phase #399. Keep an unrestricted original-objective allocation; sampled relations are not hard program contracts.
• Validate each useful USVM candidate in original TypeScript through [TS PBT] Confirm and shrink witnesses from two-phase property search #353. A single-input replay or reduction may execute the oracle again, but must not restart random PBT generation.
• Retain all phase results and diagnostics in the same artifact.

Acceptance

• One command executes PBT -> evidence handoff -> USVM -> native candidate validation.
• Independently changing real admitted PBT edge evidence changes exploration of the same original symbolic query; saturated coverage does not stop original-property search.
• PBT generation is invoked once. No retained cross-round session, returned-input generator, repeated inference, hypothesis revision cache or second PBT batch is required.
• Source/support mismatch, missing evidence, unsupported mapping, failed replay and deadline exhaustion have explicit outcomes.
• For an enabled relation mode, real observations change an exact bound challenge and its native classification; the supported entry and explicit local/result binding paths are reported separately from unsupported arbitrary observations.

Dependencies

Coverage delivery: #354, #353, #382 and the coverage slice of #399. Observation delivery: #397/#398 and the corresponding scheduling slice. #481 and #400-#403 are outside the current project scope. Functional evidence and comparative benefit are assessed separately in #405/#357.

Delivery status (2026-10-17)

The one-way public handoff is implemented in the published campaign chain through #588 and optional relation coordinator #603. It reuses the original property/support/precondition, admitted coverage, exact source bindings and original-runtime confirmation. #602 composes exact entry and explicitly captured numeric local/result challenges; #603 selects once, challenges each selected relation at most once, keeps hypotheses distinct from the original objective and reserves time for unrestricted original search unless an original fault is confirmed.

#610 (f2c97a664f31cde9167fdb1ca04fe8e12f04ad1a) fixes usable finite retained samples without relaxing missing/corrupt/ambiguous evidence. #611 (ec2a4dc5a8f52781fb3cdbcc8aa56cb3ab63a994) consumes only timely, exact official auxiliary original-replay receipts for experiment coverage. Both are integrated in frozen local assembly c447392006cb72b06ead3d857b639a23d7e259c9, with 42 focused integration tests. No implementation gate for those two slices remains unpublished. All referenced PRs remain open and require user-controlled review/merge.

The completed 108 scalar / 18 prefix diagnostic / 144 class cells establish the implemented supported path and its limits, not comparative superiority. Four-mode paired original-class coverage has zero gain on all 14 eligible class-by-seed rows; three genuine classes have no complete paired result. The scalar relation-mode contrast is also reached by prefix/native-oracle execution without the learned equality. #357/#404 retain that attribution failure. The ordinary command-boundary deadline and artifact-publication gap is tracked in #354, with #612 for publication order and #613 for caller deadline origin/publication reserve. Selector policy is separately owned and unchanged here.