[TS PBT] Capture compiler-owned numeric DSL results

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 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/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": {
     "@jridgewell/trace-mapping": "0.3.31",

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

@@ -30,6 +30,7 @@ import {
   type ObservationArtifact,
   type ObservationPointRequest,
   type ObservationRequest,
+  type CompilerNumericLocalBinding,
 } from './observe-property.js';
 
 export interface PropertyManifestInput {
@@ -121,7 +122,14 @@ export async function executeProperty(requestValue: unknown): Promise<FastCheckE
     installObservationHook();
   }
 
-  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);
@@ -791,6 +799,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;
   });
@@ -802,8 +813,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 (points.length === 0 || 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');
   }
@@ -818,6 +830,39 @@ 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 = 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
+    && point.source.module === manifest.predicate.module && point.callSite.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 && point.kind === 'return';
+  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;

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

@@ -14,6 +14,22 @@ export interface ObservationPointRequest {
   callSite: SourcePoint;
   kind: 'entry-argument' | 'argument' | 'return' | 'intermediate' | 'pre' | 'post';
   inputIndex?: number;
+  compilerLocal?: CompilerNumericLocalBinding;
+}
+
+/** Authority comes from the retained compiler program, not these source coordinates alone. */
+export interface CompilerNumericLocalBinding {
+  producer: string;
+  abi: string;
+  programId: string;
+  nodeId: number;
+  localName: string;
+  predicateExportName: string;
+  companionExportName: string;
+  predicateAssignment: SourcePoint;
+  companionAssignment: SourcePoint;
+  sourceSha256: string;
+  occurrence: number;
 }
 
 export interface SourcePoint {
@@ -123,6 +139,22 @@ export class ObservationRecorder {
     return this.artifact;
   }
 
+  get compilerLocalBinding(): CompilerNumericLocalBinding | undefined {
+    return this.request.points.find((point) => point.compilerLocal !== undefined)?.compilerLocal;
+  }
+
+  captureCompilerLocal(nodeId: number, localName: string, value: unknown): void {
+    const context = contexts.getStore();
+    const point = this.request.points.find((point) => point.compilerLocal !== undefined);
+    if (context?.recorder !== this || point === undefined) return;
+
+    const binding = point.compilerLocal!;
+    const identityMatches = nodeId === binding.nodeId && localName === binding.localName;
+    const reason = !identityMatches ? 'compiler-local-identity-mismatch'
+      : typeof value !== 'number' ? 'compiler-local-numeric-required' : undefined;
+    this.capturePoint(context.invocation, point, value, reason);
+  }
+
   run<T>(
     values: unknown[],
     phase: InvocationRecord['phase'],
@@ -172,8 +204,8 @@ export class ObservationRecorder {
 
   point(record: InvocationRecord, pointId: string, value: unknown): void {
     const point = this.pointsById.get(pointId);
-    // Entry snapshots belong to the adapter; user callbacks cannot replace or repeat them.
-    if (point?.kind === 'entry-argument') return;
+    // Adapter entry snapshots and compiler callbacks own these points; public hooks cannot replace them.
+    if (point?.kind === 'entry-argument' || point?.compilerLocal !== undefined) return;
     if (point === undefined) {
       this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints);
 
@@ -183,7 +215,7 @@ export class ObservationRecorder {
     this.capturePoint(record, point, value);
   }
 
-  private capturePoint(record: InvocationRecord, point: ObservationPointRequest, value: unknown): void {
+  private capturePoint(record: InvocationRecord, point: ObservationPointRequest, value: unknown, unsupportedReason?: string): void {
     if (record.points.length >= this.request.maxPointsPerInvocation) {
       this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints);
 
@@ -198,9 +230,10 @@ export class ObservationRecorder {
       callSite: point.callSite,
       kind: point.kind,
       ...(point.inputIndex === undefined ? {} : { inputIndex: point.inputIndex }),
+      ...(point.compilerLocal === undefined ? {} : { compilerLocal: point.compilerLocal }),
       occurrence: record.points.filter((event) => event.pointId === point.id).length,
       eventOrdinal: record.points.length,
-      value: this.snapshot(value),
+      value: unsupportedReason === undefined ? this.snapshot(value) : { status: 'unsupported', reason: unsupportedReason },
     });
     if (this.reservedArtifactBytes() > this.request.maxBytes) {
       record.points.pop();