[TS PBT][Checkpoint] Validate the two-phase handoff and assess its measured value #405

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.

Functional gate

• One real PBT generation phase exports bounded observations/outcomes and admitted coverage; one USVM phase consumes that evidence while preserving the original property/support/precondition.
• Independently changed real branch evidence changes symbolic exploration. Covered prefixes stay traversable and original-property search continues after coverage saturation.
• A reached candidate is checked in original TypeScript; eligible reduction preserves its exact failed check/target. Unsupported validation remains visible.
• The public runner uses one total deadline and preserves source identity, results, limitations and costs. PBT random generation is not restarted after USVM begins.
• For an enabled relation mode, demonstrate an observation-derived exact challenge and distinguish a passing hypothesis refutation from an original-property defect. This is a separate enabled capability, not an invented relation requirement for the coverage-only mode.

The previous two-PBT-round/two-symbolic-advance/returned-descendant gate is removed. No #481 session or #547 returned-input generator is required.

Development assessment

Use #356/#357's frozen real/artificial development cases and equal-budget controls. State the actual supported subset, retain negative results and record the next decision. A negative comparison can complete the assessment; an unimplemented public handoff cannot.

Existing evidence

The local 24-cell rerun completed with 5,511 native consistency checks, no mismatches and no domain violations. For PGOrbit the guided 30-second coverage increased from 67 to 78/104; the 120-second result stayed 79/104 versus PBT's 102/104. Processing/coverage accumulation became faster. Matrix and SegmentTree still did not enter symbolic class execution. This is limited diagnostic evidence, not completion of the product integration or a superiority claim.

Dependencies are #353/#354/#355/#382/#399, with #397/#398 only for the enabled relation capability. #400-#403 and repeated-round work are not required.

Delivery status (2026-10-17)

The functional supported handoff is implemented in published open PRs through #603, with #610 finite retained samples and #611 strict auxiliary replay consumption integrated in frozen local assembly c447392006cb72b06ead3d857b639a23d7e259c9. Forty-two focused integration tests passed. Actual original PBT evidence changes the next supported symbolic work; exact entry/local challenges retain original native outcomes; original property search remains available; no second random-generation phase is used. Open PR delivery, local integration, CI and merged main remain distinct.

The authorized development assessment is complete: 108/108 scalar artifacts eligible under the charged 60-second process budget; 18/18 complete prefix attribution diagnostics; 144 class cells with 89 full eligible and 55 incomplete outcomes. Strict four-mode pairing leaves 14/27 class-by-seed rows and zero checked original-statement gain on every complete row. Only Mailbox and CircularLinkedList provide complete genuine-class comparisons; no conclusion of zero gain is assigned to the other three genuine classes.

Relation modes confirm the branching mutant in 3/3 seeds versus 0/3 in the four original-objective controls. The prefix/native diagnostic reaches the same rare input without the learned equality, so the additional contribution of observations is not demonstrated. The artificial class mutants are found by all paired controls, and the genuine SinglyLinkedList defect was already known during native corpus validation. #357/#404 preserve these negative attribution and coverage results.

The frozen ordinary-CLI results expose a separate caller/inner deadline-origin and publication-reserve problem under #354. Their failures are not all assigned one cause: 47 external kills, 45 missing-artifact diagnostics, one unterminated JSON, eight saved native-incomplete cells (one also killed), and one Operation-not-permitted cell. The narrow #614 file-before-stdout fix and focused #615/#616 caller-cutoff/publication-reserve changes are now published, not left as unimplemented work. They remain open for user review/merge. A separate single delayed-launch functional check saved an explicit DEADLINE/CONFIRMATION artifact without an outer kill and correctly gave no credit to its 67 unchecked inputs; it is not an additional comparative cell or a positive coverage result. #613 retains exact receipt/timing evidence and the cooperative publication/IR cleanup/native-throughput boundary. Remaining work is review/merge of published slices, separate language support and honest research packaging. No additional comparative experiments or scope expansion are required for this assessment.