[TS PBT] Add core development corpus and pilot protocol

docs/ts-pbt/CORE_NEAREST_WORK.md

@@ -0,0 +1,27 @@
+# #404 nearest-work and provisional claim ledger
+
+Status: early input to #405, before pilot data or a comprehensive novelty review. `Yes` below means the cited primary source explicitly supports the stated mechanism; `unverified` means this pass did not establish its absence. Language alone is not a novelty argument.
+
+| Work / primary evidence | Reused test or input structure | Feedback / inference | Symbolic challenge and replay | Boundary for this roadmap |
+| --- | --- | --- | --- | --- |
+| [JQF/Zest, ISSTA 2019](https://doi.org/10.1145/3293882.3330576) and [JQF project](https://github.com/rohanpadhye/JQF) | Parameterized Java property tests and pluggable generators | Coverage and validity feedback guide semantically valid generation | No symbolic relation challenge established by the cited overview | Reusing PBT generators and feeding coverage back are prior work; compare beyond coverage. |
+| [Daikon project](https://plse.cs.washington.edu/daikon/) | Program execution traces | Reports **likely** point-specific invariants from observed values | No testing loop established by the cited overview | Observed relations are hypotheses, not facts or new by themselves. |
+| [DSD-Crasher, TOSEM 2008 abstract](https://plse.cs.washington.edu/daikon/pubs/CsallnerSX2008-abstract.html) | Program tests/observations | Dynamic invariants restrict static analysis; a final dynamic step confirms predictions | Yes: dynamic–static–dynamic testing | Dynamic invariant plus static search plus concrete confirmation is direct prior work. Our proposed distinction needs a measured, assertion-specific target/feedback mechanism, not a generic D–S–D claim. |
+| [QSYM, USENIX Security 2018](https://www.usenix.org/conference/usenixsecurity18/presentation/yun) | Fuzzer inputs for binaries | Hybrid fuzzing with concolic execution and fuzzer validation | Yes, bidirectional hybrid testing; not a user PBT oracle in the cited abstract | Returning symbolic inputs to a fuzzer and validating them is prior work. The intended TypeScript property/oracle semantics must show incremental value. |
+| [HypoFuzz project](https://hypofuzz.com/) | Existing Python Hypothesis tests | Fuzzing backend and coverage dashboard; finer mechanism requires source review | Symbolic relation challenge unverified here | Existing PBT reuse and coverage are established beyond JQF; do not claim those features as novel. |
+
+The supplied private 2026 Go/gopter + usvm-go thesis is **not redistributed** here. Its recorded mechanisms include uncovered-line guidance, input-corpus transfer and `behaviorKey` novelty filtering. Author/title/public citation must be verified with the owner before referencing it in a public paper. The output-novelty control in the pilot is required partly to test this boundary. The full #404 review must also inspect generator-choice search, metamorphic and stateful/model-based PBT, internal-context summaries, and newer property-directed testing against their primary papers; the table above is deliberately incomplete.
+
+## Claim → required evidence
+
+| Proposed statement | Evidence needed before making it | Current status |
+| --- | --- | --- |
+| The bounded core loop works | A real observation yields a nontrivial assertion-relevant relation; it changes an actual target; a replay-confirmed refutation changes later generated inputs; exact branch signal affects scheduling; all costs and mismatches are logged. | Unmeasured; fixtures and protocol only. |
+| It finds more distinct faults or confirms them faster than baselines | Paired equal-budget development results, then independently frozen held-out results, with original oracle, common support, uncertainty and regressions. Compare direct property search and sequential portfolio. | Unmeasured; superiority provisional. |
+| Assertion focus adds value beyond generic invariants | Focused versus unfocused inference, equal vocabulary/target budget and controlled target ordering. | Planned contrast only. |
+| Observed relations add value beyond coverage/templates/output novelty | Coverage-only, observation-independent templates and output-novelty controls on the same eligible cases and budget. | Planned contrast only. |
+| Extensions add value | End-to-end #400–#403 enable/disable comparisons on their supported strata after the core checkpoint. | Out of this early checkpoint. |
+| A concrete witness is valid | Original-runtime replay of that exact input against the original predicate, with admissibility and execution outcome recorded. This confirms the witness only. | No witness from a search campaign yet. |
+| Any bounded symbolic conclusion is sound | A separate argument for the model, supported semantics, binding/guards, solver assumptions and bounded scope; replay cannot establish general soundness or completeness, and finite unsuccessful search proves no property. | No proof claim or proof argument. |
+
+The final ledger must link each empirical statement to a pinned implementation revision, corpus manifest, raw run IDs and table-regeneration command. #405 may report a negative or inconclusive pilot without turning functional completion into an improvement claim. No manuscript or external publication is in this PR.

docs/ts-pbt/CORE_PILOT_PROTOCOL.md

@@ -0,0 +1,19 @@
+# #405 core development comparison: preregistration draft
+
+Status: protocol prepared before comparative runs. Use `usvm-ts-pbt/corpus/development/v1/manifest.json` as the initial development selection. #357's final held-out protocol will be frozen later; no results are claimed here. Record the implementation commit, corpus revision, property registration, configuration and machine/runtime versions with every campaign.
+
+## Common denominator and controls
+
+For each eligible case, retain the **same original TypeScript predicate/assertions**, declared support and precondition, exact input value semantics, and original-runtime confirmation in every mode. Fast-check distribution bias is measured separately from hard support. Case admission is per capability: only the intersection that all compared modes execute faithfully enters a paired comparison. Publish both that intersection and the full inventory with `supported`, `unsupported`, `UNKNOWN`, timeout and error counts. A hypothesis refutation that passes the predicate is not a fault. A false specification is a separate diagnosis.
+
+Run six core configurations under a common total wall-clock deadline per case and seed: `PBT_ONLY`, `SYMBOLIC_ONLY`, `SEQUENTIAL` (fixed PBT then symbolic allocation, no feedback), `COVERAGE_FEEDBACK` (exact branch signal), `RELATION_FEEDBACK` (observations and symbolic challenges), and `COMBINED_FEEDBACK` (coverage plus relation, replay and returned-input rounds). Freeze the scheduler, phase allocations and target tie-break rules before observing comparisons. All symbolic modes retain direct original-property search and concrete confirmation. Covered branches remain searchable when fault search needs them. Report the native fast-check suite run with identical oracle, generator support and deadline as a bridge-overhead control; record any distribution mismatch explicitly.
+
+Preplanned focused contrasts, on eligible cases only: (1) relation feedback versus observation-independent templates with **identical formula vocabulary and target budget**, preselected without observing outcomes; (2) property-focused versus unfocused observations/inference, fixed or randomized target ordering; (3) combined feedback versus a one-round/no-return variant; (4) combined feedback versus output-behavior novelty selection. These are planned contrasts, not a Cartesian product and not winner-dependent selections. #400–#403 get separate enable/disable comparisons in the final eligible strata. A relation-derived witness demonstrates functional causality only; compare it with direct original-property search before any advantage claim.
+
+## Time, sampling and analysis
+
+Set numeric deadlines, allocations, memory limit, observation points/templates, search bounds and seeds in a versioned run configuration **before** running the first comparison. For the pilot, start with at least ten independent campaign seeds per configuration and case; choose the final repetition count using development-only variance and save the change as a new protocol revision. Pair seeds across configurations, rotate/interleave run order, and record cold/warm setup. Predeclare whether shared build/setup is charged or amortized, then apply it uniformly. The total deadline includes frontend/adapter startup, instrumentation, observation, inference, mapping, solver search, original-runtime replay, returned-input generation and target-preserving shrinking. Report each cost and peak memory; retain interrupted runs as censored outcomes.
+
+Primary outcomes are distinct original-oracle-confirmed faulty implementations, time to first confirmation (censored at deadline), marginal faults and regressions. Count a fault once regardless of witnesses or properties. Keep real defects, validated mutants, source-authored controlled faults and curated functional cases in separate tables. Secondary outcomes include capability denominator, adaptation time, exact source branch coverage, output novelty, observation truncation, relation support/contradictions, target yield, replay acceptance, returned-seed usefulness, fallback, per-phase cost and memory. EtsIR target reach is not concrete source coverage. Analyze paired runs within case, then summarize at project/family level; do not treat 10 seeds or near-duplicate mutants as 10 independent projects. Give effect sizes and interval estimates, show no-gain cases, and state the multiple-comparison treatment before final inference. Never select the best seed as the result.
+
+The planned same-language coverage-guided comparator is a pilot research choice: assess an executable TypeScript/fast-check tool and freeze its version/settings before held-out runs, or document a concrete incompatibility. JQF/Zest is Java related work, not a directly comparable TypeScript score. Preserve raw inputs, lineage, observations, formulas, guards, mapping, attempted targets, solver outcomes, original replay, shrink steps, phase clocks and failure classifications. A future runner must offer one frozen-plan command and a separate raw-to-table regeneration command; neither exists at this early checkpoint.

usvm-ts-pbt/corpus/README.md

@@ -0,0 +1,30 @@
+# TypeScript PBT corpus: development checkpoint v1
+
+This is the early **development** input for #405, not the completed #356 benchmark. The machine-readable case and provenance inventory is [`development/v1/manifest.json`](development/v1/manifest.json). No comparative search run has used this version. The fixtures are TypeScript exports; #395 owns executable `PropertyManifest` registration. This metadata does not introduce another oracle language.
+
+## Reproduce the original-runtime checks
+
+From `usvm-ts-pbt/corpus/development/v1`:
+
+```sh
+npm ci --ignore-scripts --no-audit --no-fund
+npm run validate
+```
+
+The lockfile pins fast-check 4.9.0, tsx 4.23.12 and TypeScript 5.9.2. Validation uses 500 deterministic generated inputs per correct property with seed 20260930, plus explicit witnesses. This checks the intended-correct implementations and known constructed counterexamples; it does not validate symbolic admission, branch saturation, discovery likelihood, or comparative effectiveness. Keep the source's original generator and the bounded pilot generator separate in the manifest. The upper array/number bounds are pilot support choices, not facts inferred from observations.
+
+## Selection and analysis units
+
+The first source-linked family is es-toolkit's generated chunk property. It keeps all three assertions: flattened order, full non-last chunks, and nonempty chunks no larger than `size`. The second is fast-check's own duplicate-removal test. That upstream test intentionally uses a faulty identity implementation to check generation bias; its oracle is useful here, but the fault is **source-authored controlled**, not a real defect in fast-check. Our Set-based deduplicator is a locally authored correct baseline, not an upstream implementation. The two source projects each contribute one property family. The three curated scalar mechanisms are one constructed project and do not increase the count of independent real projects. The Boolean fixture translations preserve the stated oracle checks, but native suite registration/import through #395 remains unverified. There is no claim of representative sampling or a measured improvement.
+
+The pilot admits an upstream property only if its original predicate is meaningful, the relevant implementation and source license/revision are recoverable, and a bounded numeric/dense-array support can be represented without changing the assertion. We exclude oracle replacements such as no-throw checks, opaque generator construction, and cases needing #400–#403 from the **core direct-comparison denominator**, while preserving them in the full #356 inventory. A false specification is never scored as a faulty implementation. The `1.8` floating-point round trip is an excluded semantic diagnostic. The exact supported denominator is determined per mode after #395 registration and capability checks; missing modes are reported `unsupported`, never as no-fault results.
+
+The curated parity fixture has a controlled branchless numeric perturbation at input 7. Its parity oracle fails there after ordinary input 6 passes. It is a **candidate** saturated-coverage mechanism until #382 verifies exact real-runtime branch traces and #395/#352 verify symbolic support. The absolute-value fixture separates a passing hypothesis refutation from a property failure. The constant-output fixture must remain in the pilot even if feedback yields no benefit. Source-authored and curated faults are counted separately; no real-world implementation defect has been admitted yet. Each controlled fault has an explicit non-equivalence witness in the manifest; witnesses are validation only and must stay out of search seeds and relation training.
+
+## Split and revision rule
+
+All v1 fixtures, their witnesses, settings, outcomes and any future tuning are development data. Freeze a later held-out set by **project and property family** before inspecting its results; neither another mutant of these functions nor a later version of the same family can enter held-out. Select later projects by an outcome-independent published inventory and eligibility rule. Keep excluded/unsupported cases visible. Any change to v1 selection, bounds, oracle, mutant or seed plan creates v2, retaining v1 and its runs. Final held-out collection, #400–#403 strata, known real defects and validated mutants remain work for the full #356/#357 delivery.
+
+## License and adaptation boundary
+
+The es-toolkit implementation is adapted from its pinned MIT source. The fast-check test oracle is translated from a Vitest length assertion into equivalent Boolean equality; its deliberate faulty implementation comes from the source, while our Set-based correct implementation does not. The upstream license URLs and copyright notices are in the manifest. The `adaptation` entries record estimated manual glue and exact semantic changes; timed person-effort has **not** been measured. Before any published empirical comparison, register and execute the original assertion callback through #395, record actual edit time and annotations, and keep the same oracle/support across all eligible modes.

usvm-ts-pbt/corpus/THIRD_PARTY_LICENSES.md

@@ -0,0 +1,51 @@
+# Notices for adapted fixtures
+
+The fixture `development/v1/esToolkitChunk.ts` adapts `toss/es-toolkit` at revision `4504e985a433fe1e348d803a233b2c02d41e4b3c` (original `src/array/chunk.ts` and `src/array/chunk.spec.ts`). The fixture `development/v1/uniqueArray.ts` adapts the test oracle and deliberate faulty example from `dubzzz/fast-check` at revision `85eeab9e87c9d37e66cc7819260e3df1e72305ae` (original `packages/fast-check/test/arbitraries/ArrayArbitrary.spec.ts`). Both are MIT licensed.
+
+## es-toolkit
+
+MIT License
+
+Copyright (c) 2024 Viva Republica, Inc.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
+
+## fast-check
+
+MIT License
+
+Copyright (c) 2017 Nicolas DUBIEN
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

usvm-ts-pbt/corpus/development/v1/.gitignore

@@ -0,0 +1 @@
+node_modules/

usvm-ts-pbt/corpus/development/v1/esToolkitChunk.ts

@@ -0,0 +1,30 @@
+/** MIT licensed es-toolkit implementation; source and revision are pinned in manifest.json. */
+export function chunk(values: readonly number[], size: number): number[][] {
+    if (!Number.isInteger(size) || size <= 0) {
+        throw new Error('Size must be an integer greater than zero.');
+    }
+
+    const chunkLength = Math.ceil(values.length / size);
+    const result: number[][] = Array(chunkLength);
+
+    for (let index = 0; index < chunkLength; index++) {
+        const start = index * size;
+        const end = start + size;
+
+        result[index] = values.slice(start, end);
+    }
+
+    return result;
+}
+
+/** The three original assertions from es-toolkit's generated-input test. */
+export function originalChunkOracle(values: number[], size: number): boolean {
+    const chunks = chunk(values, size);
+    const flattened = chunks.flat();
+    const preservesOrder = flattened.length === values.length &&
+        flattened.every((value, index) => value === values[index]);
+    const fullExceptLast = chunks.every((item, index) => item.length === size || index === chunks.length - 1);
+    const nonemptyBounded = chunks.every(item => item.length > 0 && item.length <= size);
+
+    return preservesOrder && fullExceptLast && nonemptyBounded;
+}