[TS PBT] Prepare real and artificial benchmarks for the two-phase analysis #356

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.

Goal

Build the two requested parts of the experiment: real programs with meaningful original properties, and separately reported artificial programs that isolate rare branches and useful property/observation signals.

Required preparation

• Freeze source revisions, licenses, original oracles, domains, class/scenario identity and the exact executable statement universe independently of which mode wins.
• Preflight concrete replay, frontend retention and the declared symbolic subset before freezing the eligible comparisons. Keep unsupported candidates and exclusion reasons visible.
• Reuse existing domains and supported joint constraints. Do not require symbolic fast-check choice tracing, a command-model framework, helper summaries or dedicated multi-execution infrastructure.
• Artificial cases should vary branch rarity and input structure, include correct/no-benefit controls, and have independently validated faults. Report them separately from real defects and validated mutants.
• For real classes, count original executable class statements; exclude wrappers, model bodies, comments and foreign classes. Credit only checked native hits. Keep the same denominator across modes.
• Use development data to settle bounds/settings; reserve separate projects/families for any held-out claims. Record adaptation effort and project concentration.

Historical diagnostic evidence

The earlier local three-class coverage pilot was diagnostic evidence, not the completed property-rich corpus. Its two-phase coverage signal was measured, but two classes were absent from IR. Track frontend retention in UnitTestBot/jacodb#447, runtime-limitation reporting in #555 and sparse array support in #388. Do not alter original class text to hide a frontend failure.

Acceptance

Pinned real/artificial manifests, original properties, validation commands and capability outcomes are available to #357. Supported and unsupported populations are reproducible. The former closed-without-merge corpus PRs #406/#408 do not count as delivered main code.

Delivery status (2026-10-17)

The pinned preparation preserves the original 61 cases (48 artificial and 13 real scenarios over eight classes), six separately named equivalent indexed-oracle ring wrappers, original provenance and unsupported dispositions. The equivalent ring wrappers were checked against the native oracle on 6,018 inputs. Frontend retention of 61/61 cases is not symbolic runtime support.

The final frozen class manifest contains 12 scenario profiles over five genuine original classes and two artificial families (separate control/mutant bodies yield nine class groups). All 12 preparation/native-smoke/frontend gates passed; runtime results remain separate. The source manifest SHA is df536cc014ec8305a2265139e72b1231ad90962a740f1fcdf06e4b86916aa513. Profiles include ordinary/wide SinglyLinkedList, DoublyLinkedList and CircularQueue; these profiles are not independent programs. No original class body was rewritten after outcomes.

The final scalar manifest is one artificial numeric-local family with six correct/mutant/no-benefit variants, three fast-check seeds and six treatments (108 cells), plus 18 predeclared prefix/native-oracle attribution diagnostics. Plan SHA: ad9ab6dfeefb7f4aedee82934d9ebab9755f055f82a5a4ba71f0f981963d0b4e. Variants/seeds are not additional independent families. Pure symbolic repeats use the same fixed BFS/randomSeed=0 configuration.

All authorized measurements are complete and frozen; no further tuning, replacements or new families were run after outcomes. #357 records 89/144 full class cells, 14 strict four-mode class-by-seed rows with zero coverage gain, and the scalar attribution limit. SinglyLinkedList's native invariant defect was discovered while validating the corpus (93 failures in 6,174 exhaustive native inputs), before the comparison; PBT and hybrids reproduce it, so it is not a new USVM discovery. DoublyLinkedList's 6,174 and CircularQueue's 768 native validation inputs hold. No upstream report was sent.

Remaining work is reviewable packaging and research assessment of this development population, plus separately tracked TypeScript support and review/merge of published #615/#616 command-boundary fixes under #354/#613. It is not a held-out or publication-ready superiority corpus. Original Adder/Float64Array limitations remain under #604; prior unsupported/truncated data remain preserved.