[TS PBT][Research] Assess and report the two-phase property-guided analysis #404

Scope agreed on 2026-10-16

One concrete PBT generation phase is followed by one USVM search phase. No return to random generation is required. Concrete replay and optional shrinking validate a USVM candidate; they are not a second PBT generation phase. This replaces the previous repeated-round acceptance.

Research scope

Describe and evaluate one PBT evidence-collection phase followed by USVM search over the same original property. Coverage and enabled one-time observed-relation guidance are the mechanisms under study. Iterative return-to-PBT generation, generator-choice search, dedicated multi-execution/stateful frameworks and helper summaries are not required contributions.

Work

• Compare primary sources on hybrid/concolic testing, coverage-guided PBT (including JQF/Zest), dynamic invariant inference and static/dynamic combinations. Do not claim novelty from the TypeScript language or from feature count alone.
• Explain which user properties, generator support, observations and branch facts are reused, and how they change actual USVM work.
• Use [TS PBT] Prepare real and artificial benchmarks for the two-phase analysis #356/[TS PBT] Compare two-phase evidence-guided USVM with equal-budget controls #357's preserved real/artificial evidence, controls and costs. Separate original implementation faults, false specifications, passing hypothesis refutations, mutants and unsupported execution.
• Maintain a claim/evidence mapping to pinned code, configurations and raw runs. The diagnostic three-class pilot does not establish superiority.
• Prepare manuscript/artifact material within confirmed capabilities. Negative results may require a narrower claim; they do not justify hidden benchmark selection.

Acceptance

Nearest-work boundaries, reproducible tables, limitations and the supported claim are ready for author review. This issue does not authorize external submission/publication. #400-#403 and repeated feedback rounds are not dependencies.

Delivery status (2026-10-17)

The authorized development campaign is complete on frozen local assembly c447392006cb72b06ead3d857b639a23d7e259c9: 108 scalar cells, 18 prefix/native attribution diagnostics and 144 class cells. #357 records the protocol, full results and exclusions. No further experiment tuning, reruns, replacements or families were introduced after outcomes.

The scalar branching mutant is officially confirmed in 3/3 RELATION_FEEDBACK and COMBINED_FEEDBACK runs versus 0/3 in each of the four original-objective controls. This does not demonstrate an additional contribution from learned PBT observations: all 18 independently checked prefix diagnostics are complete, and prefix/native-oracle execution reaches the same rare input 417 and both mutant failures without the learned equality. The prefix diagnostic has a different budget allocation; it is not a seventh fair control or an official witness confirmation. It establishes this concrete attribution failure, not an observation speedup estimate.

The checked original-class experiment has 89/144 full eligible cells and only 14/27 strict four-mode class-by-seed pairs. Every complete pair has zero coverage gain over PBT. Mailbox and CircularLinkedList provide complete genuine-class comparisons; SinglyLinkedList, DoublyLinkedList and CircularQueue do not. Their incomplete native verification/deadline/publication outcomes must not be relabeled unsupported-language misses or negative complete comparisons. The genuine SinglyLinkedList defect was known from corpus validation before the comparison. Both artificial mutants are found by every paired control. Variants, profiles and seeds are not independent programs/families.

The current supported claim is functional: one PBT evidence phase changes subsequent supported USVM work, original objectives remain available, exact auxiliary candidates are checked under the original oracle, and passing relation refutations stay separate from original named faults. The evidence does not support real-program coverage superiority or incremental learned-observation value.

Remaining author-review material must connect that narrow claim to nearest primary work, include the failed attribution, attrition, all charged costs and supported-subset limits, and distinguish open PR implementation from merged main. A future observation-value claim would require a separately approved fair observation-independent prefix/template comparison and independent program evidence; no new campaign is authorized by this status update. #354/#612/#613 track caller/inner deadline and artifact preservation separately. External submission/publication is not authorized.