[TS PBT] Register original assertions and bounded joint generator support

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

@@ -20,18 +20,40 @@ import {
   protocolError,
   type TaggedJsValue,
 } from './js-value.js';
-import { projectDomain } from './project-domain.js';
+import { buildPropertyArbitrary, validateJointGenerator } from './property-arbitrary.js';
 
 export interface PropertyManifestInput {
   name: string;
   domain: unknown;
+  generatorId?: string;
+}
+
+export interface PropertySourcePointWire {
+  module: string;
+  line: number;
+  column: number;
+}
+
+export interface PropertyAssertionWire {
+  id: string;
+  source: PropertySourcePointWire;
+  testedCall?: PropertySourcePointWire;
+  operands: Array<{ id: string; source: PropertySourcePointWire }>;
 }
 
 export interface PropertyManifestWire {
   propertyId: string;
   inputs: PropertyManifestInput[];
   predicate: TypeScriptEntryPointReference;
   precondition?: TypeScriptEntryPointReference;
+  assertions?: PropertyAssertionWire[];
+  sourceIdentity?: { sourceSha256: string; buildSha256: string; buildScope: string };
+  generator?: {
+    id: string;
+    kind: 'array-index';
+    arrayInputIndex: number;
+    indexInputIndex: number;
+  };
 }
 
 export interface FastCheckExecutionRequest {
@@ -78,10 +100,7 @@ export async function executeProperty(requestValue: unknown): Promise<FastCheckE
     ? undefined
     : await loadEntryPoint(request.manifest.precondition, request.sourceRoots, 'manifest.precondition');
 
-  const arbitrary = fc.tuple(
-    ...request.manifest.inputs.map((input, index) =>
-      projectDomain(input.domain, `manifest.inputs[${index}].domain`)),
-  );
+  const arbitrary = buildPropertyArbitrary(request.manifest);
   const contractErrors: ContractErrorState = { first: undefined };
   const property = buildProperty(arbitrary, predicate, precondition, contractErrors);
   const parameters = buildParameters(request);
@@ -248,6 +267,17 @@ function buildParameters(request: FastCheckExecutionRequest): Parameters<[JsConc
 
     const values = example.map((value, valueIndex) =>
       decodeJsValue(value, `examples[${exampleIndex}][${valueIndex}]`));
+    if (request.manifest.generator !== undefined) {
+      const [array, index] = values;
+      if (!Array.isArray(array) || typeof index !== 'number' || !Number.isInteger(index)
+        || index < 0 || index >= array.length) {
+        throw protocolError(
+          adapterDiagnostic.protocolExamplesInvalid,
+          'Explicit example violates declared joint generator support',
+          `examples[${exampleIndex}]`,
+        );
+      }
+    }
 
     return [values];
   });
@@ -457,7 +487,16 @@ function validateManifest(value: unknown): PropertyManifestWire {
       );
     }
 
-    return { name: input.name, domain: input.domain };
+    const validatedInput: PropertyManifestInput = { name: input.name, domain: input.domain };
+    if (input.generatorId !== undefined) {
+      if (typeof input.generatorId !== 'string' || input.generatorId.length === 0) {
+        throw protocolError(adapterDiagnostic.protocolManifestInputInvalid, 'Invalid generator ID', `manifest.inputs[${index}].generatorId`);
+      }
+
+      validatedInput.generatorId = input.generatorId;
+    }
+
+    return validatedInput;
   });
 
   const validated: PropertyManifestWire = {
@@ -470,9 +509,89 @@ function validateManifest(value: unknown): PropertyManifestWire {
     validated.precondition = validateEntryPoint(manifest.precondition, 'manifest.precondition');
   }
 
+  if (manifest.generator !== undefined) {
+    const generator = requireRecord(
+      manifest.generator,
+      adapterDiagnostic.protocolManifestInvalid,
+      'Generator must be an object',
+      'manifest.generator',
+    );
+    const validGenerator = typeof generator.id === 'string' && generator.id.length > 0
+      && generator.kind === 'array-index'
+      && generator.arrayInputIndex === 0 && generator.indexInputIndex === 1
+      && inputs.length === 2;
+    if (!validGenerator) {
+      throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Invalid joint generator', 'manifest.generator');
+    }
+
+    validated.generator = generator as unknown as NonNullable<PropertyManifestWire['generator']>;
+    validateJointGenerator(validated);
+  }
+
+  if (manifest.assertions !== undefined) {
+    if (!Array.isArray(manifest.assertions)) {
+      throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Assertions must be an array', 'manifest.assertions');
+    }
+
+    validated.assertions = manifest.assertions.map((value: unknown, index: number) =>
+      validateAssertion(value, `manifest.assertions[${index}]`));
+  }
+
+  if (manifest.sourceIdentity !== undefined) {
+    const identity = requireRecord(manifest.sourceIdentity, adapterDiagnostic.protocolManifestInvalid,
+      'Source identity must be an object', 'manifest.sourceIdentity');
+    if (typeof identity.sourceSha256 !== 'string' || typeof identity.buildSha256 !== 'string'
+      || typeof identity.buildScope !== 'string') {
+      throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Invalid source identity', 'manifest.sourceIdentity');
+    }
+
+    validated.sourceIdentity = {
+      sourceSha256: identity.sourceSha256,
+      buildSha256: identity.buildSha256,
+      buildScope: identity.buildScope,
+    };
+  }
+
   return validated;
 }
 
+function validateAssertion(value: unknown, path: string): PropertyAssertionWire {
+  const assertion = requireRecord(value, adapterDiagnostic.protocolManifestInvalid, 'Assertion must be an object', path);
+  if (typeof assertion.id !== 'string' || !Array.isArray(assertion.operands)) {
+    throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Invalid assertion identity or operands', path);
+  }
+
+  const operands = assertion.operands.map((value: unknown, index: number) => {
+    const operandPath = `${path}.operands[${index}]`;
+    const operand = requireRecord(value, adapterDiagnostic.protocolManifestInvalid, 'Operand must be an object', operandPath);
+    if (typeof operand.id !== 'string') {
+      throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Invalid operand ID', operandPath);
+    }
+
+    return { id: operand.id, source: validateSourcePoint(operand.source, `${operandPath}.source`) };
+  });
+  const result: PropertyAssertionWire = {
+    id: assertion.id,
+    source: validateSourcePoint(assertion.source, `${path}.source`),
+    operands,
+  };
+  if (assertion.testedCall !== undefined) {
+    result.testedCall = validateSourcePoint(assertion.testedCall, `${path}.testedCall`);
+  }
+
+  return result;
+}
+
+function validateSourcePoint(value: unknown, path: string): PropertySourcePointWire {
+  const point = requireRecord(value, adapterDiagnostic.protocolManifestInvalid, 'Source point must be an object', path);
+  if (typeof point.module !== 'string' || !Number.isInteger(point.line) || !Number.isInteger(point.column)
+    || (point.line as number) < 1 || (point.column as number) < 1) {
+    throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Invalid source point', path);
+  }
+
+  return { module: point.module, line: point.line as number, column: point.column as number };
+}
+
 function validateEntryPoint(value: unknown, entryPath: string): TypeScriptEntryPointReference {
   const entryPoint = requireRecord(
     value,

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

@@ -0,0 +1,59 @@
+import fc from 'fast-check';
+import { adapterDiagnostic } from './diagnostics.js';
+import type { JsConcreteValue } from './js-value.js';
+import { protocolError } from './js-value.js';
+import type { PropertyManifestWire } from './execute-property.js';
+import { projectDomain } from './project-domain.js';
+
+/** Constructs declared joint support; it does not interpret predicate or precondition behavior. */
+export function buildPropertyArbitrary(manifest: PropertyManifestWire): fc.Arbitrary<JsConcreteValue[]> {
+  const generator = manifest.generator;
+  if (generator === undefined) {
+    return fc.tuple(...manifest.inputs.map((input, index) =>
+      projectDomain(input.domain, `manifest.inputs[${index}].domain`)));
+  }
+
+  validateJointGenerator(manifest);
+
+  const array = projectDomain(manifest.inputs[0]?.domain, 'manifest.inputs[0].domain');
+
+  return array.chain((value) => {
+    if (!Array.isArray(value) || value.length === 0) {
+      throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Array-index generator requires a nonempty array', 'manifest.generator');
+    }
+
+    return fc.integer({ min: 0, max: value.length - 1 }).map((index): JsConcreteValue[] => [value, index]);
+  });
+}
+
+/** Checks the declared domains before a dependent arbitrary can sample outside either one. */
+export function validateJointGenerator(manifest: PropertyManifestWire): void {
+  const generator = manifest.generator;
+  if (generator === undefined) return;
+
+  const arrayDomain = manifest.inputs[0]?.domain;
+  const indexDomain = manifest.inputs[1]?.domain;
+  const array = asRecord(arrayDomain);
+  const index = asRecord(indexDomain);
+  const valid = generator.kind === 'array-index'
+    && generator.arrayInputIndex === 0 && generator.indexInputIndex === 1
+    && manifest.inputs.length === 2
+    && array?.kind === 'array' && Number.isInteger(array.minLength) && Number.isInteger(array.maxLength)
+    && (array.minLength as number) >= 1 && (array.maxLength as number) <= 32
+    && (array.minLength as number) <= (array.maxLength as number)
+    && index?.kind === 'integer' && index.min === 0
+    && index.max === (array.maxLength as number) - 1;
+  if (!valid) {
+    throw protocolError(
+      adapterDiagnostic.protocolManifestInvalid,
+      'Array-index generator requires a nonempty bounded array and index domain 0..maxLength-1',
+      'manifest.generator',
+    );
+  }
+}
+
+function asRecord(value: unknown): Record<string, unknown> | undefined {
+  return value !== null && typeof value === 'object' && !Array.isArray(value)
+    ? value as Record<string, unknown>
+    : undefined;
+}

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

@@ -4,13 +4,103 @@ import { tmpdir } from 'node:os';
 import path from 'node:path';
 import test from 'node:test';
 import { fileURLToPath } from 'node:url';
+import { tsImport } from 'tsx/esm/api';
 import { encodeJsValue, ProtocolError } from '../src/js-value.js';
 import {
   executeProperty,
   type FastCheckExecutionRequest,
   type FastCheckRunResult,
 } from '../src/execute-property.js';
 
+test('pinned fast-check callback shim preserves length assertion outcomes on bounded arrays', async () => {
+  const fixture = path.resolve(
+    path.dirname(fileURLToPath(import.meta.url)),
+    '../../../src/test/resources/properties/real/ArrayArbitraryProperty.ts',
+  );
+  const property = await tsImport(fixture, import.meta.url) as {
+    AssertionError: new (message: string) => Error;
+    expect(values: number[]): { toHaveLength(expected: number): void };
+    originalUniqueAssertion(values: number[]): void;
+    originalUniqueOracle(values: number[]): boolean;
+  };
+  const cases = [[], [0], [0, 1], [1, 1], [0, 1, 0], [10, 9, 8, 7], [10, 10, 10, 10]];
+
+  for (const values of cases) {
+    const expected = values.length === new Set(values).size;
+
+    if (expected) {
+      assert.equal(property.originalUniqueAssertion(values), undefined);
+      assert.equal(property.originalUniqueOracle(values), true);
+    } else {
+      assert.throws(() => property.originalUniqueAssertion(values), property.AssertionError);
+      assert.throws(() => property.originalUniqueOracle(values), property.AssertionError);
+    }
+  }
+});
+
+test('assertion shim evaluates expected operand before reading actual length and preserves thrown values', async () => {
+  const fixture = path.resolve(
+    path.dirname(fileURLToPath(import.meta.url)),
+    '../../../src/test/resources/properties/real/ArrayArbitraryProperty.ts',
+  );
+  const property = await tsImport(fixture, import.meta.url) as {
+    expect(values: number[]): { toHaveLength(expected: number): void };
+  };
+  const order: string[] = [];
+  const value = {
+    get length(): number {
+      order.push('actual');
+      return 1;
+    },
+  } as number[];
+  const expected = (): number => {
+    order.push('expected');
+    return 1;
+  };
+
+  property.expect(value).toHaveLength(expected());
+
+  assert.deepEqual(order, ['expected', 'actual']);
+
+  const thrown = new Error('length getter');
+  const throwing = {
+    get length(): number {
+      throw thrown;
+    },
+  } as number[];
+
+  assert.throws(() => property.expect(throwing).toHaveLength(1), (error) => error === thrown);
+});
+
+test('rejects array-index manifests that conflict with declared input domains before sampling', async () => {
+  await withPropertyModule(async (sourceRoot) => {
+    const array = (minLength: number, maxLength: number) => ({
+      kind: 'array',
+      element: { kind: 'integer', min: 0, max: 1 },
+      minLength,
+      maxLength,
+    });
+    const invalidDomains = [
+      [array(1, 3), { kind: 'integer', min: 99, max: 99 }],
+      [array(0, 3), { kind: 'integer', min: 0, max: 2 }],
+      [array(1, 33), { kind: 'integer', min: 0, max: 32 }],
+    ];
+
+    for (const inputDomains of invalidDomains) {
+      const request = executionRequest(sourceRoot, 'alwaysTrue', { inputDomains });
+      request.manifest.generator = {
+        id: 'values.valid-index',
+        kind: 'array-index',
+        arrayInputIndex: 0,
+        indexInputIndex: 1,
+      };
+
+      await assert.rejects(executeProperty(request), (error: unknown) =>
+        error instanceof ProtocolError && error.path === 'manifest.generator');
+    }
+  });
+});
+
 test('executes a synchronous TypeScript predicate with deterministic success details', async () => {
   await withPropertyModule(async (sourceRoot) => {
     const request = executionRequest(sourceRoot, 'alwaysTrue');

usvm-ts-fast-check/fast-check-adapter/test/project-domain.test.ts

@@ -5,6 +5,25 @@ import {
   projectDomain,
   projectionCapability,
 } from '../src/project-domain.js';
+import { buildPropertyArbitrary } from '../src/property-arbitrary.js';
+
+test('joint array-index generator keeps index within the generated array', () => {
+  const arbitrary = buildPropertyArbitrary({
+    propertyId: 'example.array-index',
+    predicate: { module: 'example.ts', exportName: 'property', executionKind: 'sync' },
+    inputs: [
+      { name: 'values', domain: { kind: 'array', element: { kind: 'integer', min: 0, max: 2 }, minLength: 1, maxLength: 4 } },
+      { name: 'index', domain: { kind: 'integer', min: 0, max: 3 } },
+    ],
+    generator: { id: 'values.valid-index', kind: 'array-index', arrayInputIndex: 0, indexInputIndex: 1 },
+  });
+
+  const samples = fc.sample(arbitrary, { seed: 42, numRuns: 100 });
+
+  assert.ok(samples.every(([values, index]) => Array.isArray(values)
+    && typeof index === 'number' && Number.isInteger(index) && index >= 0 && index < values.length));
+  assert.ok(samples.some(([values, index]) => Array.isArray(values) && values.length > 1 && index === 1));
+});
 
 test('bounded integers use a real fast-check arbitrary', () => {
   const samples = sample({ kind: 'integer', min: -3, max: 7 });

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt

@@ -9,6 +9,7 @@ import org.usvm.ts.pbt.manifest.toManifest
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.JsNumberKind
 import org.usvm.ts.pbt.model.PropertyDefinition
+import org.usvm.ts.pbt.model.accepts
 import org.usvm.ts.pbt.model.contains
 import org.usvm.ts.pbt.validation.requireValid
 import org.usvm.ts.pbt.validation.validatePropertyDefinition
@@ -96,6 +97,19 @@ class FastCheckBackend(
                     )
                 }
             }
+
+            validateJointExample(property, example, index)
+        }
+    }
+
+    private fun validateJointExample(property: PropertyDefinition, example: List<JsConcreteValue>, index: Int) {
+        if (property.generator?.accepts(example) == false) {
+            throw invalidRequest(
+                code = FastCheckDiagnosticCode.BACKEND_EXAMPLES_DOMAIN,
+                message = "Explicit example violates the declared joint generator support",
+                property = property,
+                path = "examples[$index]",
+            )
         }
     }