[TS PBT] Confirm, classify and shrink symbolic property and hypothesis witnesses #353

Part of #345. Direct-counterexample delivery depends on #352/#384. The core contract includes hypothesis replay through #398 and is required by #405. Generator-choice and command-sequence reduction are later integrations owned by #400/#402; their acceptance gates do not block core completion.

Goal

Confirm every symbolic candidate in original TypeScript and reuse backend shrinking while preserving exactly what the witness demonstrates.

Scope

• Consume [TS PBT] Search for property violations with USVM #352's extracted JsConcreteValue inputs; reuse the current backend invocation, codecs and process supervision.
• Validate declared domain/generator support as applicable, execute the original precondition and original predicate using [TS PBT][P0] Align and simplify property execution semantics before integration #384.
• Keep outcomes distinct: confirmed original-property violation, confirmed hypothesis refutation with original property holding, no refutation/property holds, domain/precondition rejection, unrepresentable input, unsupported replay, nondeterminism, and property/engine/replay error.
• A hypothesis replay checks the same program point, context, guard and relation that generated the symbolic target. A different invocation/site does not confirm it. A full original oracle is still required even for an intermediate-prefix target.
• Preserve target/assertion/hypothesis identity and original input alongside replay status. An exception in a precondition is an error; predicate exceptions follow [TS PBT][P0] Align and simplify property execution semantics before integration #384. Hypothesis refutation alone is not counted as a program defect.
• Preserve special values, argument order and supported aliases/isolation without coercion. Generator-source/context revisions are pinned.
• Feed eligible external witnesses to backend shrinking; inspect canShrinkWithoutContext or retained native context as appropriate. Explicit-example execution and a zero shrink count are not proof of minimality.
• Use a target-specific reduction predicate: same original assertion failure, or same guarded hypothesis refutation. Recheck domain/admission and original predicate on the final result. Preserve the original confirmed witness if shrinking is unavailable, fails or times out.
• For [TS PBT] Search bounded generator choices while preserving dependent input structure #400, preserve dependent generator construction/choice validity. For [TS PBT] Reuse bounded command models and state invariants in hybrid search #402, reduce commands/arguments while retaining valid guards and the same failure. Add small adapters to backend facilities rather than a general custom shrinker.
• Return both confirmed failing inputs and useful non-failing behavioral witnesses to [TS PBT] Integrate the core iterative property-observation feedback loop #355 with provenance and a reproducible replay artifact. A replay token is not portable across arbitrary generator/backend revisions.
• Replay/reduction share [TS PBT] Provide campaign controls, shared budgets and extensible run artifacts #354's monotonic deadline. Reserve validation budget and retain unconfirmed candidates when it expires.

Definition of Done

• Real-runtime fixtures cover confirmed/spurious/rejected/unrepresentable inputs, exceptions, hypothesis-only refutation and unsupported shrinking.
• At least one external supported witness actually shrinks and still reproduces the same target-specific failure.
• Source/context mismatch, mutation isolation and core target-preserving reduction have explicit behavior tests. Generator-choice dependency and command-sequence reduction tests are delivered with [TS PBT] Search bounded generator choices while preserving dependent input structure #400/[TS PBT] Reuse bounded command models and state invariants in hybrid search #402.
• Artifacts retain original candidate, concrete classification, minimized result if any, reduction metric/attempts, backend revision and reproduction data.
• No candidate is reported as a final fault before original-oracle replay; no hypothesis-only witness is counted as an original-property violation.