[TS PBT] Confirm and shrink witnesses from two-phase property search #353

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

#506 provides original-runtime confirmation, typed evidence and target-preserving native reduction. #541 adds explicitly selected named DSL checks. Both remain useful for the two-phase design and are not merged yet. Basic DSL replay already exists in main.

Delivery acceptance scope

• Wire candidate confirmation through the ordinary DSL/campaign path, retaining the selected named check and false-versus-exception outcome without a second manually selected target.
• Reuse declared support, the original precondition and the complete original TypeScript oracle. Preserve the original candidate on failed validation, unsupported reduction, source drift or timeout.
• For an enabled observation-derived challenge from [TS PBT] Bind one-time observed relations to exact symbolic challenges #398, distinguish a passing original property with a refuted empirical relation from an original-property defect. Reuse exact executable bindings; do not invent context from a source line.
• Retain admitted, natively confirmed coverage and target outcomes in the existing result artifact. No returned-input generator, round lineage or cross-round session is required.

Acceptance

A public DSL/campaign test confirms and reduces an actual USVM candidate while preserving the same failed named check. Rejected admission, changed source, wrong check and failed final replay remain explicit. An enabled hypothesis target can be refuted while the original property holds. Confirmation/reduction consume the campaign deadline from #354.

Delivery status (2026-10-17)

The ordinary DSL/campaign path retains a selected named original check, native confirmation and target-preserving reduction through #506/#541/#566/#571/#572/#588, with exact entry/local hypothesis confirmation composed by #602/#603. A native refutation whose original property holds is CONFIRMED_HYPOTHESIS_REFUTATION; an actual original named-check failure is CONFIRMED_PROPERTY_VIOLATION. #603 stops auxiliary work on the first timely confirmed original fault and exposes it as the canonical confirmation. #610's retained-sample correction and #611's strict auxiliary-receipt consumption are published and integrated in frozen local assembly c447392006cb72b06ead3d857b639a23d7e259c9; 42 focused integration tests passed. These are open PRs, not merged-main functionality.

The completed 108-cell scalar protocol retained official original confirmations within a 60-second outer deadline. At input 417, the mutant returns 415 and fails original named check receipt; the captured bound check remains true. The correct variant returns 416: its observed result === input relation is refuted while the complete original oracle holds. These outcomes remain distinct. Prefix-only diagnostic replay is independently checked native evidence, not a USVM WitnessConfirmation and not an additional official treatment.

The class pilot also exposed incomplete original native verification: eight saved cells retain 94--251 unchecked symbolic inputs (one also hit the external runner deadline). Their partial native coverage and symbolic statuses are retained as incomplete; they cannot be counted as full checked-class results or successful no-finding runs. Caller/inner deadline origin and publication reserve belong to #354/#613, not a change to the witness target contract. No second PBT generation phase is needed.