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

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 [TS PBT] Establish a clean integration baseline #346–[TS PBT] Map Kotlin property definitions and source coverage to EtsIR #350 and [TS PBT][P0] Align and simplify property execution semantics before integration #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 [TS PBT][P0] Align and simplify property execution semantics before integration #384 sample isolation; bounded stateful sequences explicitly preserve state only within one invocation.

Work packages

Execution order and orchestration

1. Start corpus selection ([TS PBT] Build a property-rich development and held-out benchmark with validated faults #356) and literature/claim design ([TS PBT][Research] Establish novelty and deliver the reproducible property-feedback paper #404) immediately. Preserve the already reviewed foundation and the narrow [TS PBT] Project properties and search violations with USVM #387 delivery; new research mechanisms land in their owning follow-ups.
2. Complete [TS PBT] Project property domains and preconditions into USVM #351/[TS PBT] Search for property violations with USVM #352 and implement [TS PBT] Confirm, classify and shrink symbolic property and hypothesis witnesses #353/[TS PBT] Provide campaign controls, shared budgets and extensible run artifacts #354. In parallel, establish [TS PBT] Reuse user properties, assertion structure and generator semantics #395, [TS PBT] Capture bounded property-scoped observations in original TypeScript #396 and [TS PBT] Integrate exact c8/EtsIR edge feedback into target selection #382.
3. Deliver the bounded [TS PBT] Infer property-relevant relational hypotheses from PBT observations #397/[TS PBT] Project observed relations and assertion goals into exact EtsIR bindings #398 contracts, then [TS PBT] Schedule assertion, coverage and hypothesis targets under one budget #399 and [TS PBT] Integrate the core iterative property-observation feedback loop #355's core repeated loop. Use the development manifest from [TS PBT] Build a property-rich development and held-out benchmark with validated faults #356 and protocol/nearest-work inputs from [TS PBT] Evaluate causal contributions of property-aware feedback and bounded extensions #357/[TS PBT][Research] Establish novelty and deliver the reproducible property-feedback paper #404 without waiting for those issues to close.
4. Complete [TS PBT][Checkpoint] Validate the bounded core feedback loop and assess its research value #405: check functional causality, run the equal-budget development comparisons, account for all overhead, and record the next decision. Do not make [TS PBT] Search bounded generator choices while preserving dependent input structure #400–[TS PBT] Challenge context-scoped observed function summaries during symbolic search #403 prerequisites for this checkpoint or expand the pilot to rescue an unfavorable result.
5. Use the pilot's diagnosis to implement and integrate [TS PBT] Search bounded generator choices while preserving dependent input structure #400, [TS PBT] Guide relational and metamorphic properties across multiple executions #401, [TS PBT] Reuse bounded command models and state invariants in hybrid search #402 and [TS PBT] Challenge context-scoped observed function summaries during symbolic search #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 [TS PBT] Evaluate causal contributions of property-aware feedback and bounded extensions #357 and complete [TS PBT][Research] Establish novelty and deliver the reproducible property-feedback paper #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 [TS PBT] Evaluate causal contributions of property-aware feedback and bounded extensions #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 ([Epic][TS Calls] Introduce explicit fallback policies and partial semantic models #360/[TS Calls] Evaluate fallback policies and models with concrete replay #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.