[TS PBT] Generate native integer neighborhoods from returned inputs

usvm-ts-fast-check/fast-check-adapter/package.json

@@ -9,7 +9,7 @@
     "build": "tsc --project tsconfig.json",
     "pretest": "npm run build",
     "test": "npm run test:compiled",
-    "test:compiled": "node --test dist/test/coverage-branches.test.js dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/observe-object.test.js dist/test/process-group-shutdown.test.js dist/test/process-supervisor.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js dist/test/source-replay.test.js dist/test/source-captures.test.js dist/test/local-source-closure.test.js dist/test/class-coverage-source.test.js"
+    "test:compiled": "node --test dist/test/coverage-branches.test.js dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/observe-object.test.js dist/test/process-group-shutdown.test.js dist/test/process-supervisor.test.js dist/test/project-domain.test.js dist/test/returned-input-generation.test.js dist/test/projection-cli.test.js dist/test/source-replay.test.js dist/test/source-captures.test.js dist/test/local-source-closure.test.js dist/test/class-coverage-source.test.js"
   },
   "dependencies": {
     "@jridgewell/trace-mapping": "0.3.31",

usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts

@@ -19,6 +19,8 @@ const entryPoint = (code: string): AdapterDiagnosticDescriptor => ({
 export const adapterDiagnostic = {
   protocolJsonInvalid: invalidRequest('protocol.json.invalid'),
   protocolRequestInvalid: invalidRequest('protocol.request.invalid'),
+  returnedGenerationInvalid: invalidRequest('generation.returned.invalid'),
+  returnedGenerationUnsupported: invalidRequest('generation.returned.unsupported'),
   protocolSeedInvalid: invalidRequest('protocol.seed.invalid'),
   protocolReplayPathInvalid: invalidRequest('protocol.replay-path.invalid'),
   protocolExamplesInvalid: invalidRequest('protocol.examples.invalid'),

usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts

@@ -22,10 +22,16 @@ import {
   protocolError,
   type TaggedJsValue,
 } from './js-value.js';
-import { buildPropertyArbitrary, PhaseTrackingArbitrary, validateJointGenerator } from './property-arbitrary.js';
+import { PhaseTrackingArbitrary, validateJointGenerator } from './property-arbitrary.js';
+import {
+  buildReturnedInputGeneration,
+  validateReturnedInputGeneration,
+  type ReturnedInputGeneration,
+} from './returned-input-generation.js';
 import {
   installObservationHook,
   ObservationRecorder,
+  type ReturnedInputMetadata,
   type ObservationArtifact,
   type ObservationPointRequest,
   type ObservationRequest,
@@ -76,6 +82,7 @@ export interface FastCheckExecutionRequest {
   timeoutMillis: number;
   examples: TaggedJsValue[][];
   observationRequest?: ObservationRequest;
+  returnedInputGeneration?: ReturnedInputGeneration;
 }
 
 export interface FastCheckFailureDetails {
@@ -126,13 +133,16 @@ export async function executeProperty(requestValue: unknown): Promise<FastCheckE
     : await loadEntryPoint(request.manifest.precondition, request.sourceRoots, 'manifest.precondition', request.tsconfig);
 
   const contractErrors: ContractErrorState = { first: undefined };
-  const baseArbitrary = buildPropertyArbitrary(request.manifest);
+  const generation = buildReturnedInputGeneration(request.manifest, request.returnedInputGeneration);
+  const baseArbitrary = generation.arbitrary;
   const tracker = recorder === undefined ? undefined : new PhaseTrackingArbitrary(baseArbitrary);
   const arbitrary = tracker ?? baseArbitrary;
   const phaseOf = (values: JsConcreteValue[]) => request.replayPath === undefined
     ? tracker?.phaseOf(values) ?? 'unknown'
     : 'replay';
-  const property = buildProperty(arbitrary, predicate, precondition, contractErrors, recorder, phaseOf);
+  const property = buildProperty(
+    arbitrary, predicate, precondition, contractErrors, recorder, phaseOf, generation.metadataOf,
+  );
   const parameters = buildParameters(request, tracker);
 
   const details = await checkProperty(property, parameters, request.replayPath);
@@ -158,6 +168,7 @@ function buildProperty(
   contractErrors: ContractErrorState,
   recorder: ObservationRecorder | undefined,
   phaseOf: (values: JsConcreteValue[]) => 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown',
+  metadataOf: (values: JsConcreteValue[]) => ReturnedInputMetadata | undefined,
 ): fc.IProperty<[JsConcreteValue[]]> | fc.IAsyncProperty<[JsConcreteValue[]]> {
   const asynchronous = predicate.executionKind === 'async' || precondition?.executionKind === 'async';
   let selectedCheckId: string | undefined;
@@ -166,7 +177,9 @@ function buildProperty(
     return fc.asyncProperty(arbitrary, (values: JsConcreteValue[]): Promise<boolean> => preserveAsyncContractError(
       contractErrors,
       async () => {
-        const result = await invokePropertyOnce(values, predicate, precondition, recorder, phaseOf(values));
+        const result = await invokePropertyOnce(
+          values, predicate, precondition, recorder, phaseOf(values), metadataOf(values),
+        );
         if (result === null) fc.pre(false);
 
         return result;
@@ -179,7 +192,9 @@ function buildProperty(
     () => {
       let result: boolean | null;
       try {
-        result = invokePropertyOnce(values, predicate, precondition, recorder, phaseOf(values)) as boolean | null;
+        result = invokePropertyOnce(
+          values, predicate, precondition, recorder, phaseOf(values), metadataOf(values),
+        ) as boolean | null;
       } catch (error: unknown) {
         if (isNamedCheckFailure(error)) {
           selectedCheckId ??= error.checkId;
@@ -202,6 +217,7 @@ function invokePropertyOnce(
   precondition: LoadedEntryPoint | undefined,
   recorder: ObservationRecorder | undefined,
   phase: 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown',
+  metadata?: ReturnedInputMetadata,
 ): boolean | null | Promise<boolean | null> {
   const invocationValues = cloneArguments(values);
   const invoke = (): boolean | null | Promise<boolean | null> => {
@@ -252,7 +268,7 @@ function invokePropertyOnce(
     }
   };
 
-  return recorder === undefined ? invoke() : recorder.run(values, phase, invoke);
+  return recorder === undefined ? invoke() : recorder.run(values, phase, invoke, metadata);
 }
 
 function predicateExceptionOutcome(error: unknown): 'false' | 'threw' {
@@ -586,6 +602,14 @@ function validateRequest(value: unknown): FastCheckExecutionRequest {
     validated.observationRequest = validateObservationRequest(request.observationRequest, manifest);
   }
 
+  if (request.returnedInputGeneration !== undefined) {
+    if (validated.observationRequest === undefined) {
+      throw protocolError(adapterDiagnostic.returnedGenerationInvalid,
+        'Returned generation requires bounded observations for lineage', 'returnedInputGeneration');
+    }
+    validated.returnedInputGeneration = validateReturnedInputGeneration(request.returnedInputGeneration, manifest);
+  }
+
   return validated;
 }
 

usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts

@@ -42,11 +42,17 @@ export interface ObservationValue {
   reason?: string;
 }
 
+export interface ReturnedInputMetadata {
+  origin: 'returned-seed' | 'returned-neighborhood';
+  returnedInput: { seedId: string; sourceRunId: string; sourceInvocationId: number };
+}
+
 interface InvocationRecord {
   invocationId: number;
   parentInvocationId: null;
   callSite: SourcePoint | null;
-  origin: 'fast-check';
+  origin: 'fast-check' | ReturnedInputMetadata['origin'];
+  returnedInput?: ReturnedInputMetadata['returnedInput'];
   phase: 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown';
   input: ObservationValue;
   admission: 'pending' | 'admitted' | 'rejected' | 'threw';
@@ -127,6 +133,7 @@ export class ObservationRecorder {
     values: unknown[],
     phase: InvocationRecord['phase'],
     invocation: () => T,
+    metadata?: ReturnedInputMetadata,
   ): T {
     if (this.artifact.invocations.length >= this.request.maxInvocations) {
       this.artifact.droppedInvocations = incrementCounter(this.artifact.droppedInvocations);
@@ -138,7 +145,8 @@ export class ObservationRecorder {
       invocationId: this.artifact.invocations.length,
       parentInvocationId: null,
       callSite: this.request.points[0]?.callSite ?? null,
-      origin: 'fast-check',
+      origin: metadata?.origin ?? 'fast-check',
+      ...(metadata === undefined ? {} : { returnedInput: metadata.returnedInput }),
       phase,
       input: this.snapshot(values),
       admission: 'pending',

usvm-ts-fast-check/fast-check-adapter/src/returned-input-generation.ts

@@ -0,0 +1,113 @@
+import fc from 'fast-check';
+import { adapterDiagnostic } from './diagnostics.js';
+import type { PropertyManifestWire } from './execute-property.js';
+import { decodeJsValue, type JsConcreteValue, type TaggedJsValue, protocolError } from './js-value.js';
+import type { ReturnedInputMetadata } from './observe-property.js';
+import { buildPropertyArbitrary } from './property-arbitrary.js';
+
+export interface ReturnedInputSeed {
+  id: string;
+  inputs: TaggedJsValue[];
+  sourceRunId: string;
+  sourceInvocationId: number;
+}
+
+export interface ReturnedInputGeneration {
+  seeds: ReturnedInputSeed[];
+  radius: number;
+}
+
+/** Reject unsupported support instead of replacing a joint or non-integer generator. */
+export function validateReturnedInputGeneration(value: unknown, manifest: PropertyManifestWire): ReturnedInputGeneration {
+  const request = asRecord(value);
+  const validRequest = request !== undefined && Array.isArray(request.seeds)
+    && request.seeds.length >= 1 && request.seeds.length <= MAX_SEEDS
+    && Number.isInteger(request.radius) && (request.radius as number) >= 1 && (request.radius as number) <= MAX_RADIUS;
+  if (!validRequest) throw invalid('Expected 1..8 returned seeds and integer radius 1..1024');
+
+  const integerSupport = manifest.generator === undefined
+    && manifest.inputs.length >= 1 && manifest.inputs.length <= MAX_INPUTS
+    && manifest.inputs.every((input) => asRecord(input.domain)?.kind === 'integer');
+  if (!integerSupport) {
+    throw protocolError(adapterDiagnostic.returnedGenerationUnsupported,
+      'Returned generation supports only independent integer inputs', 'returnedInputGeneration');
+  }
+
+  // Reuse ordinary projection validation before reading the supported integer bounds.
+  buildPropertyArbitrary(manifest);
+  const ids = new Set<string>();
+  const seeds = (request.seeds as unknown[]).map((value): ReturnedInputSeed => {
+    const seed = asRecord(value);
+    const validSeed = seed !== undefined && identifier(seed.id) && identifier(seed.sourceRunId)
+      && Number.isSafeInteger(seed.sourceInvocationId) && (seed.sourceInvocationId as number) >= 0
+      && Array.isArray(seed.inputs) && seed.inputs.length === manifest.inputs.length;
+    if (!validSeed) throw invalid('A returned seed requires identity, source invocation and the original input arity');
+    if (ids.has(seed.id as string)) throw invalid('Returned seed IDs must be unique');
+    ids.add(seed.id as string);
+
+    const inputs = seed.inputs as TaggedJsValue[];
+    inputs.forEach((tagged, index) => {
+      const number = decodeJsValue(tagged, `returnedInputGeneration.seeds.inputs[${index}]`);
+      const domain = asRecord(manifest.inputs[index]?.domain)!;
+      const inSupport = typeof number === 'number' && Number.isInteger(number) && !Object.is(number, -0)
+        && number >= (domain.min as number) && number <= (domain.max as number);
+      if (!inSupport) throw invalid('Returned seed is outside the original integer support');
+    });
+
+    return { id: seed.id as string, inputs, sourceRunId: seed.sourceRunId as string,
+      sourceInvocationId: seed.sourceInvocationId as number };
+  });
+
+  return { seeds, radius: request.radius as number };
+}
+
+/** Native oneof/tuple/integer supply generation and shrinking; the original branch retains half the probability. */
+export function buildReturnedInputGeneration(manifest: PropertyManifestWire, request?: ReturnedInputGeneration): {
+  arbitrary: fc.Arbitrary<JsConcreteValue[]>;
+  metadataOf(values: JsConcreteValue[]): ReturnedInputMetadata | undefined;
+} {
+  const original = buildPropertyArbitrary(manifest);
+  const metadata = new WeakMap<JsConcreteValue[], ReturnedInputMetadata>();
+  if (request === undefined) return { arbitrary: original, metadataOf: () => undefined };
+
+  const returned = request.seeds.map((seed) => {
+    const numbers = seed.inputs.map((value) => decodeJsValue(value) as number);
+    const components = numbers.map((number, index) => {
+      const domain = asRecord(manifest.inputs[index]?.domain)!;
+      const min = Math.max(domain.min as number, number - request.radius);
+      const max = Math.min(domain.max as number, number + request.radius);
+
+      return fc.integer({ min, max });
+    });
+
+    return fc.tuple(...components).map((values): JsConcreteValue[] => {
+      const exactSeed = values.every((number, index) => Object.is(number, numbers[index]));
+      metadata.set(values, {
+        origin: exactSeed ? 'returned-seed' : 'returned-neighborhood',
+        returnedInput: { seedId: seed.id, sourceRunId: seed.sourceRunId, sourceInvocationId: seed.sourceInvocationId },
+      });
+
+      return values;
+    });
+  });
+
+  return { arbitrary: fc.oneof(original, fc.oneof(...returned)), metadataOf: (values) => metadata.get(values) };
+}
+
+function identifier(value: unknown): value is string {
+  return typeof value === 'string' && value.length > 0 && value.length <= MAX_IDENTIFIER_LENGTH;
+}
+
+function asRecord(value: unknown): Record<string, unknown> | undefined {
+  return value !== null && typeof value === 'object' && !Array.isArray(value)
+    ? value as Record<string, unknown> : undefined;
+}
+
+function invalid(message: string): Error {
+  return protocolError(adapterDiagnostic.returnedGenerationInvalid, message, 'returnedInputGeneration');
+}
+
+const MAX_SEEDS = 8;
+const MAX_INPUTS = 8;
+const MAX_RADIUS = 1024;
+const MAX_IDENTIFIER_LENGTH = 128;