Compose published relation consumers with the public PBT campaign

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/input-export.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 dist/test/external-witness.test.js"
+    "test:compiled": "node --test dist/test/coverage-branches.test.js dist/test/compiler-local-capture.test.js dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/input-export.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 dist/test/external-witness.test.js"
   },
   "dependencies": {
     "@bcoe/v8-coverage": "1.0.2",

usvm-ts-fast-check/fast-check-adapter/src/entry-point.ts

@@ -7,6 +7,7 @@ import { register } from 'tsx/esm/api';
 import { adapterDiagnostic } from './diagnostics.js';
 import type { JsConcreteValue } from './js-value.js';
 import { ProtocolError, protocolError } from './js-value.js';
+import type { CompilerNumericLocalBinding } from './observe-property.js';
 
 // Each adapter process uses one explicit resolver configuration for all nested imports.
 let registeredConfig: string | undefined;
@@ -60,14 +61,30 @@ export function isNamedCheckFailure(value: unknown): value is NamedCheckFailure
   return value !== null && typeof value === 'object' && namedCheckFailures.has(value);
 }
 
-type EntryPointFunction = (...args: JsConcreteValue[]) => unknown;
+type EntryPointFunction = (...args: unknown[]) => unknown;
+
+export interface CompilerNumericLocalCapture {
+  binding: CompilerNumericLocalBinding;
+  observe(nodeId: number, localName: string, value: unknown): void;
+}
 
 export async function loadEntryPoint(
   reference: TypeScriptEntryPointReference,
   sourceRoots: string[],
   referencePath: string,
   tsconfig?: string,
+  compilerCapture?: CompilerNumericLocalCapture,
 ): Promise<LoadedEntryPoint> {
+  if (compilerCapture !== undefined) {
+    const binding = compilerCapture.binding;
+    const validAbi = binding.producer === 'usvm-kotlin-dsl-v1' && binding.abi === 'numeric-local-callback-v1'
+      && binding.predicateExportName === reference.exportName
+      && binding.companionExportName === reference.checkResultExportName && reference.executionKind === 'sync';
+    if (!validAbi) {
+      throw protocolError(adapterDiagnostic.protocolRequestInvalid,
+        'Compiler local callback ABI does not match the selected predicate and companion', `${referencePath}.compilerLocal`);
+    }
+  }
   registerTypeScriptLoader(tsconfig);
   const modulePath = await resolveModule(reference.module, sourceRoots, referencePath);
   const moduleNamespace = await importTypeScriptModule(modulePath, referencePath);
@@ -101,7 +118,12 @@ export async function loadEntryPoint(
     return {
       executionKind: 'sync',
       invoke: (args) => {
-        const result = invokeEntryPoint(companion as EntryPointFunction, args);
+        if (compilerCapture !== undefined && companion.length !== args.length + 1) {
+          throw protocolError(adapterDiagnostic.protocolRequestInvalid,
+            'Compiler local companion has an incompatible callback signature', `${referencePath}.compilerLocal`);
+        }
+        const companionArgs = compilerCapture === undefined ? args : [...args, compilerCapture.observe];
+        const result = invokeEntryPoint(companion as EntryPointFunction, companionArgs);
         if (result === null || typeof result !== 'object' || isThenable(result)) {
           throw protocolError(adapterDiagnostic.entryPointResultInvalid,
             'A generated companion must return a check outcome', `${referencePath}.result`);
@@ -324,7 +346,7 @@ function buildInvocation(
   };
 }
 
-function invokeEntryPoint(entryPoint: EntryPointFunction, args: JsConcreteValue[]): unknown {
+function invokeEntryPoint(entryPoint: EntryPointFunction, args: unknown[]): unknown {
   try {
     return entryPoint(...args);
   } catch (error: unknown) {

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

@@ -31,6 +31,7 @@ import {
   type ObservationArtifact,
   type ObservationPointRequest,
   type ObservationRequest,
+  type CompilerNumericLocalBinding,
 } from './observe-property.js';
 import { InputExportRecorder, validateInputExportRequest, type InputExportArtifact, type InputExportRequest } from './input-export.js';
 
@@ -136,7 +137,14 @@ export async function executeProperty(requestValue: unknown, coverage?: Executio
     await verifySourceHash(source.module, source.sha256, request.sourceRoots);
   }
 
-  const predicate = await loadEntryPoint(request.manifest.predicate, request.sourceRoots, 'manifest.predicate', request.tsconfig);
+  const compilerBinding = recorder?.compilerLocalBinding;
+  const compilerCapture = compilerBinding === undefined ? undefined : {
+    binding: compilerBinding,
+    observe: (nodeId: number, localName: string, value: unknown) => recorder!.captureCompilerLocal(nodeId, localName, value),
+  };
+  const predicate = await loadEntryPoint(
+    request.manifest.predicate, request.sourceRoots, 'manifest.predicate', request.tsconfig, compilerCapture,
+  );
   const precondition = request.manifest.precondition === undefined
     ? undefined
     : await loadEntryPoint(request.manifest.precondition, request.sourceRoots, 'manifest.precondition', request.tsconfig);
@@ -839,7 +847,7 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi
     const point = requireRecord(value, adapterDiagnostic.protocolRequestInvalid, 'Point must be an object', path);
     if (typeof point.id !== 'string' || typeof point.assertionId !== 'string'
       || typeof point.operandId !== 'string'
-      || !['argument', 'return', 'intermediate', 'pre', 'post'].includes(point.kind as string)) {
+      || !['entry-argument', 'argument', 'return', 'intermediate', 'pre', 'post'].includes(point.kind as string)) {
       throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid point identity', path);
     }
 
@@ -851,7 +859,7 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi
       callSite: validateSourcePoint(point.callSite, `${path}.callSite`),
       kind: point.kind as ObservationPointRequest['kind'],
     };
-    if (point.kind === 'argument') {
+    if (point.kind === 'argument' || point.kind === 'entry-argument') {
       if (!Number.isInteger(point.inputIndex) || (point.inputIndex as number) < 0
         || (point.inputIndex as number) >= manifest.inputs.length) {
         throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid argument index', `${path}.inputIndex`);
@@ -860,6 +868,9 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi
     } else if (point.inputIndex !== undefined) {
       throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Only argument points may name an input index', path);
     }
+    if (point.compilerLocal !== undefined) {
+      validatedPoint.compilerLocal = validateCompilerLocal(point.compilerLocal, validatedPoint, manifest, sources, path);
+    }
 
     return validatedPoint;
   });
@@ -871,8 +882,9 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi
     assertion.id === point.assertionId && samePoint(assertion.testedCall, point.callSite)
       && assertion.operands.some((operand) =>
         operand.id === point.operandId && samePoint(operand.source, point.source))) ?? false);
+  const compilerPoints = points.filter((point) => point.compilerLocal !== undefined);
   if (uniquePoints.size !== points.length || uniqueSources.size !== sources.length
-    || !allSourcesPresent || !allPointsBound) {
+    || !allSourcesPresent || !allPointsBound || compilerPoints.length > 1) {
     throw protocolError(adapterDiagnostic.protocolRequestInvalid,
       'Observation points must bind to declared assertion operands and selected source hashes', 'observationRequest');
   }
@@ -887,6 +899,53 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi
   };
 }
 
+function validateCompilerLocal(
+  value: unknown, point: ObservationPointRequest, manifest: PropertyManifestWire,
+  sources: Array<{ module: string; sha256: string }>, path: string,
+): CompilerNumericLocalBinding {
+  const binding = validateCompilerLocalBinding(value, manifest, sources, path);
+  const originalPoint = point.kind === 'return' && point.source.module === manifest.predicate.module
+    && point.callSite.module === manifest.predicate.module;
+  if (!originalPoint) {
+    throw protocolError(adapterDiagnostic.protocolRequestInvalid,
+      'Compiler local requires an original return point', `${path}.compilerLocal`);
+  }
+
+  return binding;
+}
+
+export function validateCompilerLocalBinding(
+  value: unknown, manifest: PropertyManifestWire,
+  sources: Array<{ module: string; sha256: string }>, path: string,
+): CompilerNumericLocalBinding {
+  const binding = requireRecord(value, adapterDiagnostic.protocolRequestInvalid,
+    'Compiler local binding must be an object', `${path}.compilerLocal`);
+  const predicateAssignment = validateSourcePoint(binding.predicateAssignment, `${path}.compilerLocal.predicateAssignment`);
+  const companionAssignment = validateSourcePoint(binding.companionAssignment, `${path}.compilerLocal.companionAssignment`);
+  const source = sources.find((source) => source.module === manifest.predicate.module);
+  const valid = binding.producer === 'usvm-kotlin-dsl-v1' && binding.abi === 'numeric-local-callback-v1'
+    && binding.programId === manifest.propertyId && Number.isInteger(binding.nodeId) && (binding.nodeId as number) >= 0
+    && typeof binding.localName === 'string' && /^[A-Za-z_$][A-Za-z0-9_$]*$/.test(binding.localName)
+    && binding.predicateExportName === manifest.predicate.exportName
+    && binding.companionExportName === manifest.predicate.checkResultExportName
+    && manifest.predicate.checkResultExportName !== undefined && manifest.predicate.executionKind === 'sync'
+    && predicateAssignment.module === manifest.predicate.module && companionAssignment.module === manifest.predicate.module
+    && !samePoint(predicateAssignment, companionAssignment)
+    && typeof binding.sourceSha256 === 'string' && /^[0-9a-f]{64}$/.test(binding.sourceSha256)
+    && source?.sha256 === binding.sourceSha256 && binding.occurrence === 0;
+  if (!valid) {
+    throw protocolError(adapterDiagnostic.protocolRequestInvalid,
+      'Compiler local identity, callback ABI or selected source does not match', `${path}.compilerLocal`);
+  }
+
+  return {
+    producer: binding.producer as string, abi: binding.abi as string, programId: binding.programId as string,
+    nodeId: binding.nodeId as number, localName: binding.localName as string,
+    predicateExportName: binding.predicateExportName as string, companionExportName: binding.companionExportName as string,
+    predicateAssignment, companionAssignment, sourceSha256: binding.sourceSha256 as string, occurrence: 0,
+  };
+}
+
 function samePoint(left: PropertySourcePointWire | undefined, right: PropertySourcePointWire): boolean {
   return left !== undefined && left.module === right.module
     && left.line === right.line && left.column === right.column;