[TS PBT] Build a property-rich development and held-out benchmark with validated faults #356

Part of #345. Uses completed #347/#348/#384 and coordinates with #395. Corpus selection and authoring start immediately; they are not blocked by the final feedback implementation.

Goal

Provide a reproducible, independent test of what PBT-specific information adds beyond coverage and two-engine execution.

First checkpoint input

Deliver a versioned development manifest for #405 before the full corpus is complete. Start with supported numeric/scalar and bounded-array properties, at least two independent property families including an imported real fast-check suite, and declared inclusion/exclusion rules. Report project concentration and actual adaptation effort; a collection of near-duplicate mutants is not independent evidence.

Include a curated saturated-coverage fault fixture, a useful non-failing hypothesis-refutation fixture, a misleading/no-benefit case, and independent development cases for comparative runs. A constructed functional demonstration is reported separately from empirical results. Validate original oracles on intended-correct code; false mathematical specifications are not implementation defects.

Freeze the pilot selection and settings before comparative runs, retain no-gain/regression cases, and keep all pilot cases and tuning traces on the development side. Record later pilot revisions as new development versions. Final held-out selection follows outcome-independent project/family rules and cannot reuse pilot outcomes for tuning. #400–#403 strata remain required for final completion of this issue, but their absence does not block publication of the core development manifest.

Mandatory strata for the full corpus

• Original human-written properties from selected real open-source TypeScript/fast-check suites, with project revision, license, source links, rationale and adaptation/annotation effort. Do not replace meaningful oracles with a no-throw property.
• Relational/collection/pre-post properties exposing intermediate and input-to-result relationships, including saturated-coverage programs and misleading sample patterns.
• Difficult preconditions and dependent/structured generators for [TS PBT] Search bounded generator choices while preserving dependent input structure #400; record declared support separately from distribution and search-size limits.
• Round-trip/idempotence plus reference-equivalence or commutativity cases for [TS PBT] Guide relational and metamorphic properties across multiple executions #401.
• Bounded sequence-dependent faults with original command models for [TS PBT] Reuse bounded command models and state invariants in hybrid search #402.
• Internal helper relations with distinct call contexts for [TS PBT] Challenge context-scoped observed function summaries during symbolic search #403.
• JavaScript-semantic counterexamples (floating-point identities, special values, mutation/aliasing) and unsupported-prefix versus supported-prefix/unsupported-oracle cases.
• Correct implementations, real known defects where reproducibly available, and separately identified controlled mutants. Do not claim seeded defects are discovered real-world bugs.

Selection and freeze protocol

• Write inclusion/exclusion criteria and strata before seeing comparative outcomes. Use curated mechanisms only for explanation; report real-project and curated results separately.
• Split development and held-out cases by project/family where feasible, avoiding near-duplicate mutants or versions across the split. Keep final witnesses/results out of scheduler and template tuning.
• Phase A: freeze the core development manifest and initial held-out membership rules early enough for [TS PBT] Infer property-relevant relational hypotheses from PBT observations #397/[TS PBT] Schedule assertion, coverage and hypothesis targets under one budget #399 and [TS PBT][Checkpoint] Validate the bounded core feedback loop and assess its research value #405. Phase B: extend development strata for [TS PBT] Search bounded generator choices while preserving dependent input structure #400–[TS PBT] Challenge context-scoped observed function summaries during symbolic search #403 without contaminating held-out data, then freeze final revisions, original properties, generators, commands, mutants, bounds, exclusions and capabilities before [TS PBT] Evaluate causal contributions of property-aware feedback and bounded extensions #357. Phase A availability does not require this whole issue to be closed.
• Every counted mutant has a stable ID, exact source change, expected violated original property and a concrete non-equivalence witness. Screen equivalent/invalid mutants under a predefined rule. Keep witnesses outside generator/miner training.
• Validate original properties on intended-correct code and distinguish false specifications from implementation faults (e.g. exact floating-point round-trip equality).
• Record every selected case's capability and limitations, including author effort and required annotations. Keep unsupported cases in the full inventory and use explicit common supported subsets for direct comparisons.
• Reuse original predicates and native generator/command models through [TS PBT] Reuse user properties, assertion structure and generator semantics #395; all modes test the same declared support and oracle in each comparison.

Definition of Done

• Development and held-out manifests, revision/license pins, source-linked oracles and validation commands are committed.
• All mandatory strata have a nonempty meaningful subset, including actual reused user properties and sequence/dependence/relational examples; final selection is not based on the winning mode.
• Known faults and mutants are concretely validated and reported separately. Unavailable real defects or unsupported categories are disclosed rather than replaced with misleading claims.
• Corpus metadata supports per-family/project analysis, observation limits, source granularity, generator/sequence bounds and actual supported denominator.
• [TS PBT] Evaluate causal contributions of property-aware feedback and bounded extensions #357 can regenerate input selection and validate the same concrete semantics before running any search configuration.