[Epic][TS PBT] Integrate pluggable PBT engines with symbolic execution

Goal

Implement and evaluate a Kotlin-owned TypeScript property pipeline combining fast-check with USVM, using the same declared domains and original TypeScript predicates.

Research boundary

The question is whether combining PBT and symbolic search finds more faults or finds them earlier under the same total budget. The initial HYBRID mode in #354 is an explicitly defined sequential portfolio. It is a baseline, not evidence of coverage-guided search or runtime feedback. #355 evaluates optional feedback separately.

Unknown-call policy/model evaluation belongs to #360/#385; replay may be shared infrastructure without claiming the same result twice.

Scope

• Keep the property definition, value encoding and orchestration in Kotlin. Preserve a small backend interface so fast-check objects do not become the common model.
• Complete the shared execution contract and fixes in #384 before downstream integration is considered complete.
• Use the native JacoDB TypeScript frontend and original TypeScript runtime for concrete execution.
• Resolve entry points, construct supported symbolic inputs, search for property violations, replay candidates, and reuse backend shrinking.
• Treat coverage as optional. #382 is required only for c8/V8 branch-guided work; its absence does not block the property-directed baseline.
• Record actual tool/backend revisions, run settings and results in one run directory. Reuse existing artifacts and codecs; do not add version negotiation, a plugin platform or a second backend to prove hypothetical extensibility.
• Freeze a meaningful corpus and evaluate the baseline before retaining optional search hints.

Work and completion order

• Existing foundation: #346, #347, #348, #349.
• Mapping: #350.
• First-priority contract gate: #384.
• Symbolic projection/search/replay and baseline: #351, #352, #353, #354.
• Corpus: #356; selection and property authoring can proceed while implementation is completed.
• Optional hint experiment: #355, after the baseline and frozen corpus.
• Final evaluation: #357.
• Optional c8/V8 branch reconstruction: #382.

Definition of Done

• One command runs PBT_ONLY, SYMBOLIC_ONLY and the specified sequential HYBRID baseline on the same supported properties.
• Every final symbolic counterexample is confirmed against the original TypeScript predicate and domain.
• Preconditions, exceptions, mutation isolation and unsupported cases follow #384 consistently.
• A backend without coverage or shrinking yields an explicit partial capability, not failure of unrelated phases.
• Comparable total budgets include relevant startup, search, replay and shrinking costs.
• The frozen benchmark and raw per-run results support a conclusion about the marginal benefit and cost of USVM, including negative results.
• Runtime hints are evaluated or explicitly deferred; they do not block publication of the baseline comparison.
• Documentation states actual supported domains, backend capabilities and measured limits.

No stateful-testing framework, arbitrary object-domain system, dynamic scheduler, new frontend, or general invariant miner is required by this epic.

Start with the contract gate in #384, then read the existing foundations (#346-#349) and the symbolic projection, search, replay, and baseline work (#351-#354). Confirm how the native JacoDB TypeScript frontend and original runtime are used, then define the integration around the stated backend interface. Done means comparable PBT_ONLY, SYMBOLIC_ONLY, and HYBRID runs with replayed counterexamples, recorded results, and documented capabilities and limits.