[TS PBT] Pin capability-first real property candidate

docs/ts-pbt/CORE_CAPABILITY_SHORTLIST.md

@@ -0,0 +1,15 @@
+# #356 core corpus: capability-first source screening
+
+This is a read-only source inventory for a successor to development v1 (`ae7297699cc5036b54b8e3c54b1b42a2ca515705`). It was assembled before comparative outcomes. It does **not** add cases to the frozen v1 manifest, register a native suite, or assert direct symbolic support. Admission must follow original-runtime validation and a #395/#351–#352 capability result. Keep every v1 case and its outcomes on the development side.
+
+| Source, pinned revision, license | Original human-written assertion and generator | Operations / capability decision |
+| --- | --- | --- |
+| [helpers4 `isNonEmpty.spec.ts`](https://github.com/helpers4/typescript/blob/9deb33a6f6cdab3c03404217aa8e87626930733e/helpers/array/isNonEmpty.spec.ts), [`isNonEmpty.ts`](https://github.com/helpers4/typescript/blob/9deb33a6f6cdab3c03404217aa8e87626930733e/helpers/array/isNonEmpty.ts), [`LICENSE`](https://github.com/helpers4/typescript/blob/9deb33a6f6cdab3c03404217aa8e87626930733e/LICENSE) — `9deb33a6f6cdab3c03404217aa8e87626930733e`, LGPL-3.0-or-later, copyright 2025 baxyz | `fc.array(fc.anything(), { minLength: 1 })`; `expect(isNonEmpty(arr)).toBe(true)`. A second property uses `fc.array(fc.integer(), { minLength: 1 })`, then `if (isNonEmpty(arr)) expect(arr[0]).toBeDefined()`. | First oracle: original SUT checks `value != null && value.length > 0`; no dependent generator, Set, flat, every or Math. **Preferred numeric-array candidate** with bounded dense integer-array subset length 1..8. `anything` distribution and non-numeric original support remain native-only outside the common subset. Check `arr[0]` separately before admitting the second assertion. Vendoring requires LGPL license and modification notices; no source was copied in this inventory. |
+| [IgniteUI `math.property.spec.ts`](https://github.com/IgniteUI/igniteui-webcomponents/blob/d468f25bb12f72e05c5f27243fffd77c37e2107e/src/internals/utils/math.property.spec.ts), [`math.ts`](https://github.com/IgniteUI/igniteui-webcomponents/blob/d468f25bb12f72e05c5f27243fffd77c37e2107e/src/internals/utils/math.ts), [`orderedPair`](https://github.com/IgniteUI/igniteui-webcomponents/blob/d468f25bb12f72e05c5f27243fffd77c37e2107e/src/internals/testing/fast-check-setup.spec.ts), [`LICENSE`](https://github.com/IgniteUI/igniteui-webcomponents/blob/d468f25bb12f72e05c5f27243fffd77c37e2107e/LICENSE) — `d468f25bb12f72e05c5f27243fffd77c37e2107e`, MIT, copyright 2025 INFRAGISTICS | `fc.property(number, orderedPair(finite), (value,[min,max]) => expect(wrap(min,max,value)).to.be.within(min,max))`; `number` permits infinities but not NaN, `finite` excludes both, `orderedPair` sorts a generated tuple via `Math.min/Math.max`. | `wrap` SUT uses only `<`, `>` and argument returns; inclusive range oracle is meaningful. **Concrete-only under the current #395 contract**: the joint sorted-pair support is not registered/projected. A bounded integer subset must retain the declared `min <= max` relation and disclose changed distribution; inventing an unrelated precondition is not an import. `clamp` in the same suite also has idempotence and in-range preservation assertions, but its SUT uses `Math.min/Math.max`, so it is not a simpler core admission. |
+| [es-toolkit `chunk.spec.ts`](https://github.com/toss/es-toolkit/blob/4504e985a433fe1e348d803a233b2c02d41e4b3c/src/array/chunk.spec.ts) — MIT | Preserves order after flattening, non-last chunk size, and nonempty bounded chunks. | Existing v1 family; `flat`/`every` and array structure need explicit symbolic capability. Retain in inventory, possibly concrete-only. |
+| [fast-check `ArrayArbitrary.spec.ts`](https://github.com/dubzzz/fast-check/blob/85eeab9e87c9d37e66cc7819260e3df1e72305ae/packages/fast-check/test/arbitraries/ArrayArbitrary.spec.ts) — MIT | Deliberately faulty identity deduplicator; original `expect(filtered).toHaveLength(new Set(filtered).size)`. | Existing v1 family and #395 registration path; `Set` still requires symbolic capability. The local Set-based correct baseline is not an upstream implementation. |
+| [fleet-sdk `zigZag.spec.ts`](https://github.com/fleet-sdk/fleet/blob/8fd834a94a7534069ed78af3538f518068ca1e2e/packages/serializer/src/coders/zigZag.spec.ts) — MIT | `fc.integer({min:MIN_I32,max:MAX_I32})`; decode(encode(n)) equals n. | Exclude from core direct comparison: SUT uses BigInt conversion, shifts, bitwise operations and helper imports, beyond the current bounded numeric subset. Retain for later inventory. |
+
+## Admission rule for the next development revision
+
+Select the first original oracle whose **entire tested call and predicate** have supported semantics on an explicitly bounded common subset, based on APIs and language operations before viewing search outcomes. Keep the original native generator and assertion callback for a native control; record any bounded subset and changed distribution as an adaptation, not as original support. Run the intended-correct implementation with the original oracle, then check concrete replay and direct symbolic capability against the same subset. `UNSUPPORTED`, `UNKNOWN`, timeout and failed mapping never count as a negative fault result. If the preferred helpers4 source cannot be redistributed with its LGPL obligations or fails the direct symbolic check, keep it concrete-only and record the reason; do not silently replace its assertion with a weaker one. A later admitted set and settings become development v2, preserving v1 and all pilot traces. Final held-out eligibility is decided by project/family rules independent of these outcomes.

usvm-ts-pbt/corpus/README.md

@@ -25,6 +25,8 @@ The curated parity fixture has a controlled branchless numeric perturbation at i
 
 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.
 
+The separately versioned [`v2-candidate/helpers4`](development/v2-candidate/helpers4/README.md) is a source-pinned native runtime candidate selected by operation support, not a replacement for v1 or an admitted paired symbolic case. Its current capability status and exclusions are recorded with the fixture.
+
 ## 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/development/v2-candidate/helpers4/.gitignore

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

usvm-ts-pbt/corpus/development/v2-candidate/helpers4/README.md

@@ -0,0 +1,14 @@
+# helpers4 `isNonEmpty` development v2 candidate
+
+Source: [`helpers4/typescript` at `9deb33a6f6cdab3c03404217aa8e87626930733e`](https://github.com/helpers4/typescript/tree/9deb33a6f6cdab3c03404217aa8e87626930733e). `isNonEmpty.ts` and `upstream-isNonEmpty.spec.ts` are unchanged copies of the pinned [`isNonEmpty.ts`](https://github.com/helpers4/typescript/blob/9deb33a6f6cdab3c03404217aa8e87626930733e/helpers/array/isNonEmpty.ts) and [`isNonEmpty.spec.ts`](https://github.com/helpers4/typescript/blob/9deb33a6f6cdab3c03404217aa8e87626930733e/helpers/array/isNonEmpty.spec.ts); their Git blob IDs were checked against upstream and are recorded in [`candidate.json`](candidate.json). Copyright (C) 2025 baxyz; SPDX-License-Identifier: LGPL-3.0-or-later. The upstream LGPL license and the referenced GPL v3 text are included under `licenses/`. `bounded-isNonEmpty.spec.ts` is our clearly separate support restriction and does not modify the source assertion.
+
+Run from this directory:
+
+```sh
+npm ci --ignore-scripts --no-audit --no-fund
+npm run validate
+```
+
+The original suite checks (1) `isNonEmpty(arr) === true` for `fc.array(fc.anything(), {minLength:1})`, (2) false for an empty array, and (3) `arr[0]` is defined for nonempty integer arrays. The candidate **core subset is only the first assertion**, with dense integer arrays of length 1..8 and entries -16..16. The implementation is the unchanged upstream `value != null && value.length > 0`, including its TypeScript type-predicate annotation. This subset narrows support and changes the generator distribution; the native original suite is retained. The second assertion is not silently counted as supported: indexed access and `toBeDefined()` need separate #395 conformance. No fault or mutant is admitted for this case.
+
+Status: source and native runtime semantics pinned; direct EtsIR mapping and symbolic search of the original implementation/predicate are **unverified**. #395 can register the original one-assertion callback for the bounded subset, but input-domain projection alone does not establish execution capability. Until an exact capability check passes, classify the case `concrete-only/conditional`, outside the common paired symbolic denominator. This candidate is a simple control for capability and overhead, not evidence that relational feedback helps. It does not alter frozen development v1 or held-out membership.

usvm-ts-pbt/corpus/development/v2-candidate/helpers4/bounded-isNonEmpty.spec.ts

@@ -0,0 +1,19 @@
+import * as fc from 'fast-check';
+import { describe, expect, it } from 'vitest';
+import { isNonEmpty } from './isNonEmpty';
+
+describe('bounded core subset of the original isNonEmpty property', () => {
+  it('is always true for dense integer arrays with at least one element', () => {
+    const boundedNumericArray = fc.array(fc.integer({ min: -16, max: 16 }), {
+      minLength: 1,
+      maxLength: 8,
+    });
+
+    fc.assert(
+      fc.property(boundedNumericArray, (arr) => {
+        expect(isNonEmpty(arr)).toBe(true);
+      }),
+      { seed: 20260930, numRuns: 500 },
+    );
+  });
+});

usvm-ts-pbt/corpus/development/v2-candidate/helpers4/candidate.json

@@ -0,0 +1,26 @@
+{
+  "schemaVersion": 1,
+  "caseId": "helpers4-is-nonempty-original-property",
+  "status": "development-v2-candidate; concrete validated; direct symbolic execution unverified",
+  "source": {
+    "project": "helpers4/typescript",
+    "revision": "9deb33a6f6cdab3c03404217aa8e87626930733e",
+    "license": "LGPL-3.0-or-later; Copyright (C) 2025 baxyz",
+    "implementationUrl": "https://github.com/helpers4/typescript/blob/9deb33a6f6cdab3c03404217aa8e87626930733e/helpers/array/isNonEmpty.ts",
+    "implementationGitBlob": "c49099d8b4d1afb4bf16e24512742416ce1fd197",
+    "suiteUrl": "https://github.com/helpers4/typescript/blob/9deb33a6f6cdab3c03404217aa8e87626930733e/helpers/array/isNonEmpty.spec.ts",
+    "suiteGitBlob": "1b9a049b26eb562471baa6f3c0fb5964d99f6b28"
+  },
+  "family": "array-length-predicate",
+  "originalGenerator": "fc.array(fc.anything(), { minLength: 1 })",
+  "originalOracle": "expect(isNonEmpty(arr)).toBe(true)",
+  "boundedGenerator": "fc.array(fc.integer({ min: -16, max: 16 }), { minLength: 1, maxLength: 8 })",
+  "boundedSupport": "dense integer arrays, length 1..8, entries -16..16",
+  "operations": ["null/undefined comparison", "array.length", "integer comparison", "boolean conjunction"],
+  "correctImplementation": "unchanged pinned upstream isNonEmpty.ts; type-predicate annotation retained",
+  "faultClass": "none; correct/control case only",
+  "adaptation": "One additional bounded-subset test file, no modified original source or assertion; time and #395 registration annotation effort not measured",
+  "nativeConcrete": "original 3 tests plus bounded subset 1 test passed with locked fast-check 4.9.0 and Vitest 3.2.4",
+  "directSymbolicCapability": "unverified; do not include in common supported denominator until EtsIR mapping, execution and original-runtime replay pass",
+  "excludedFromCore": ["original fc.anything support outside dense numeric arrays", "original second assertion using arr[0] and toBeDefined, pending separate capability check"]
+}

usvm-ts-pbt/corpus/development/v2-candidate/helpers4/isNonEmpty.ts

@@ -0,0 +1,21 @@
+/**
+ * This file is part of helpers4.
+ * Copyright (C) 2025 baxyz
+ * SPDX-License-Identifier: LGPL-3.0-or-later
+ */
+
+/**
+ * Checks if an array is non-empty (has at least one element).
+ * `null` and `undefined` are treated as empty arrays and return `false`.
+ * @param value - The array to check
+ * @returns `true` if the array has at least one element; `false` for empty, `null`, or `undefined`
+ * @example
+ * isNonEmpty([1, 2, 3]) // => true
+ * isNonEmpty([])        // => false
+ * isNonEmpty(null)      // => false
+ * isNonEmpty(undefined) // => false
+ * @since 2.0.3
+ */
+export function isNonEmpty<T>(value: readonly T[] | null | undefined): value is readonly [T, ...T[]] {
+  return value != null && value.length > 0;
+}