[TS PBT] Evaluate PBT and hybrid configurations on the benchmark

Part of #345. Depends on #354 and #356. #355 is optional, not a blocker.

Goal

Measure the benefit and cost of adding USVM to a mature concrete PBT baseline on the same frozen property corpus.

Protocol

• Compare PBT_ONLY, SYMBOLIC_ONLY and the sequential HYBRID defined in #354, initially using fast-check.
• If #355 has a completed, justified hint configuration, evaluate it separately. Otherwise report it as deferred or rejected. Do not delay baseline evaluation for it.
• Do not claim the sequential portfolio is coverage-guided or uses runtime feedback. Such a claim requires an implemented mode and an ablation against the portfolio.
• Freeze the corpus, tool revisions, backend/runtime versions, seeds, repetitions, hardware, total/phase budgets and phase allocation before final runs.
• Use equal total budgets including relevant startup, frontend/adapter work, search, concrete replay and shrinking; account for shared setup consistently.
• Repeat runs, use a fixed or rotated execution order, and report variability. Fixing a seed does not make timeout-limited symbolic exploration exactly deterministic.

Primary outcomes

• Number and fraction of distinct validated faulty implementations/mutants found. Count a mutant once even if several properties or inputs expose it. Declare the common denominator and exclusions.
• Time to the first concrete-confirmed counterexample, with timeouts/unsolved cases treated as censored outcomes rather than dropped.
• Marginal faults found only, or earlier, with USVM; total hybrid cost.

All reported faults must reproduce in the original TypeScript runtime. A concrete PBT witness must remain reproducible; a symbolic candidate is counted only after replay.

Secondary outcomes

Report replay acceptance, unrepresentable/rejected candidates, minimized counterexample size under a declared metric, optional source coverage, and existing state/solver counters. Unsupported metrics are unavailable, not zero. Separate supported-only comparisons from the full corpus capability inventory.

Use the same instrumented source target definition if reporting coverage. EtsIR reached targets and real TypeScript coverage are separate measures; #382 is required only for claims using its branch mappings.

Definition of Done

• One command runs the frozen configurations and another regenerates summary tables from raw per-run results.
• Raw artifacts preserve configuration, phase statuses, candidate/replay distinctions and failures.
• Baseline findings answer whether and where USVM helps, including no-gain and regression cases.
• Unsupported cases, selection limits, possible budget bias and threats to validity are explicit.
• Correctness fixes discovered during evaluation are documented and applied consistently to all configurations before rerunning affected comparisons.
• No benchmark selection or hidden tuning based on the final results is introduced.

Start by reading #345, #354, and #356 to understand the benchmark scope and the PBT, symbolic, and hybrid configurations. Identify the existing benchmark entry points and result format, then implement the frozen-run and raw-artifact workflow; done means reproducible summary tables, replay-validated findings, and explicit limitations for unsupported cases and regressions.