[Epic][TS PBT] Build and evaluate a property-aware PBT–USVM feedback system

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.

Intended result

Deliver the strongest evidence-backed version of the TypeScript PBT/USVM work: reuse human-written properties and generator semantics, infer property-relevant behavioral relations from concrete executions, challenge them symbolically, and return validated inputs to further generation and shrinking.

Coverage feedback is mandatory infrastructure. Observed relations are a central research mechanism. Generator-choice search, metamorphic relations, bounded command models and context-scoped helper summaries are included in the full delivery through bounded, working implementations and separate evaluation. They are not deferred as unspecified future work.

The full epic completes with an implemented, evaluated and reproducible result; scientific superiority is a hypothesis, not an acceptance criterion that permits hiding negative results.

Delivery stages

The full scope above is retained, but it is delivered through independently reviewable checkpoints. The first checkpoint does not wait for all extensions or the final benchmark corpus.

The core starts with supported bounded numeric/scalar inputs, tuples and dense bounded arrays; selected arguments, returns and explicit intermediate observation points; a small frozen relation vocabulary; and deterministic target scheduling. This is a declared capability boundary, not permission to approximate unsupported JavaScript behavior silently. Ordinary multi-call predicates remain usable wherever already supported; dedicated cross-execution inference belongs to #401.

#405 separates functional completion from evidence of benefit. A reproducible negative or inconclusive pilot can complete that checkpoint with a documented diagnosis and next decision; it cannot be called a demonstrated improvement. The full epic and its required extensions remain open. A later reduction of full scope must be an explicit roadmap change, never an inference from a negative run.

Dependencies are completion gates. Literature, corpus selection, protocol design and extension interface design may start early. Core component issues close on their stated bounded contracts; extension-specific implementation and acceptance are owned by #400–#403, not retroactively added to those core issues.

Semantic contract

• Kotlin owns common artifacts and orchestration; fast-check is the first concrete backend. Reuse completed #346–#350 and #384, the native TypeScript frontend, original TypeScript oracles and existing tagged values.
• Distinguish declared input support/preconditions, generator probability bias, concrete observations, empirical hypotheses and proved facts. Search for a violation of the declared predicate; never assume that predicate or a sampled relation as an unconditional fact.
• Challenge a hypothesis using declared domain AND admitted precondition AND reach(point/context) AND NOT(hypothesis). Preserve context/guards and value identity. Refuting a hypothesis is not automatically a defect.
• Every finding must replay in the original runtime. Unsupported execution, solver uncertainty, invalid models, timeouts and failed extraction remain visible. No finite unsuccessful search proves a property.
• Covered edges remain searchable. Input-dependent faults, relational behavior and different states on one path remain relevant after coverage plateaus.
• Speculative restrictions/substitutions are labeled experimental assumptions, with replay and a positive bounded unrestricted allocation under the same total deadline. Fallback alone is not a completeness guarantee.
• Preserve #384 sample isolation; bounded stateful sequences explicitly preserve state only within one invocation.

Work packages

Execution order and orchestration

1. Start corpus selection (#356) and literature/claim design (#404) immediately. Preserve the already reviewed foundation and the narrow #387 delivery; new research mechanisms land in their owning follow-ups.
2. Complete #351/#352 and implement #353/#354. In parallel, establish #395, #396 and #382.
3. Deliver the bounded #397/#398 contracts, then #399 and #355's core repeated loop. Use the development manifest from #356 and protocol/nearest-work inputs from #357/#404 without waiting for those issues to close.
4. Complete #405: check functional causality, run the equal-budget development comparisons, account for all overhead, and record the next decision. Do not make #400–#403 prerequisites for this checkpoint or expand the pilot to rescue an unfavorable result.
5. Use the pilot's diagnosis to implement and integrate #400, #401, #402 and #403 on the same budget/oracle contracts. Each remains required for the full epic, with a nonempty supported subset, conformance evidence and ablation. Their completion depends on the pilot assessment; early interface design is allowed.
6. Freeze final templates, bounds, scheduler, corpus exclusions and settings on development data, then execute #357 and complete #404. Final results do not tune the method or select favorable benchmarks.

Use one PR per independently reviewable contract/mechanism where practical, with linked issue, focused behavior tests, actual checked revision and reproduction commands. Keep the dependency graph acyclic; distinguish readiness to start work from gates on final integration. Do not mark an issue implemented solely because its plan or fixture exists.

Evaluation and completion gates

• Same original user oracles are used in PBT-only, symbolic-only, sequential, coverage-only, relations-only and combined modes. Add observation-independent template, unfocused-inference, no-return-loop, output-novelty and extension ablations in #357.
• Total budgets include observation/inference/mapping, frontend/adapter work, search, replay and reduction; report setup consistently. Measure distinct confirmed faults and time to confirmation, not coverage alone.
• Include held-out real properties, known defects and separately reported validated mutants; saturated-coverage, misleading-hypothesis, generator-dependence, metamorphic and stateful cases.
• Each required bounded extension works end to end. Unsupported-only placeholders or toy wins cannot stand in for the full scope or its evaluation.
• Raw artifacts expose observations, inferred expressions, evidence provenance, mappings, target decisions, replay outcomes, returned seeds, costs and limitations. Regeneration commands reproduce the paper's tables.
• Nearest-work analysis covers coverage-guided PBT, dynamic invariants, static/dynamic testing, hypothesis falsification, generator choices and model-based testing. The supplied Go/gopter thesis includes coverage, input corpora and behaviorKey novelty; reuse of values alone is not a novelty claim.
• Preserve negative results and distinguish functional completion from measured improvement. Keep unknown-call policy work (#360/#385), the ICCQ manuscript and IFDS/type-inference research separate.

Arbitrary JavaScript closure serialization, universal invariant discovery, arbitrary heap/environment modeling, concurrency/async schedule exploration and a general plugin platform are outside the required bounded implementation. This does not exclude the explicitly listed structured generators, metamorphic relations or within-invocation stateful command models.