[TS PBT] Refute compiler-owned local relations and replay full original properties

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

@@ -833,6 +833,21 @@ 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`);
@@ -846,10 +861,9 @@ function validateCompilerLocal(
     && 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';
+    && 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`);

usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts

@@ -3,10 +3,11 @@ import { performance } from 'node:perf_hooks';
 import fc from 'fast-check';
 import { adapterDiagnostic } from './diagnostics.js';
 import { EntryPointInvocationError, isNamedCheckFailure, loadEntryPoint, sourceHashMatches, type LoadedEntryPoint } from './entry-point.js';
-import { describeNamedCheckFailure, describePropertyFailure, invokePropertyOnce, validateRequest, type FastCheckFailureDetails } from './execute-property.js';
+import { describeNamedCheckFailure, describePropertyFailure, invokePropertyOnce, validateCompilerLocalBinding, validateRequest, type FastCheckFailureDetails } from './execute-property.js';
 import { decodeJsValue, encodeJsValue, ProtocolError, protocolError, type JsConcreteValue, type TaggedJsValue } from './js-value.js';
 import { buildPropertyArbitrary } from './property-arbitrary.js';
 import { stringifyProtocolJson } from './protocol-json.js';
+import type { CompilerNumericLocalBinding } from './observe-property.js';
 import { inWitnessSupport } from './witness-support.js';
 
 export interface WitnessBinding {
@@ -16,11 +17,19 @@ export interface WitnessBinding {
   occurrence: number;
 }
 
+interface DslNumericLocalRelation {
+  compiler: CompilerNumericLocalBinding;
+  inputIndex: number;
+  resultIsLeft: boolean;
+  template: 'STRICT_EQUAL' | 'LESS_OR_EQUAL';
+}
+
 export interface WitnessTarget {
   id: string;
   role: 'PROPERTY' | 'COVERAGE' | 'HYPOTHESIS';
   binding?: WitnessBinding;
   expectedOutcome?: 'FALSE' | 'THREW';
+  dslNumericLocalRelation?: DslNumericLocalRelation;
   entryRelation?: {
     leftInputIndex: number;
     rightInputIndex: number;
@@ -68,7 +77,15 @@ export interface WitnessExecutionSuccess {
   witnessReduction?: WitnessReduction;
 }
 
-interface WitnessContext { events: WitnessEvent[]; active: boolean; contractError?: string }
+interface WitnessContext {
+  events: WitnessEvent[];
+  active: boolean;
+  contractError?: string;
+  compilerTarget: WitnessTarget | undefined;
+  compilerInput: number | undefined;
+  compilerCallbacks: number;
+  compilerDiagnostic?: string;
+}
 const contexts = new AsyncLocalStorage<WitnessContext>();
 
 /** A passive hook: evaluate the original guard/relation first; return its boolean without substituting an oracle. */
@@ -78,6 +95,11 @@ export function installWitnessHook(): void {
     value: (pointId: string, contextId: string, revision: string, guard: boolean, holds: boolean): boolean => {
       const context = contexts.getStore();
       if (context?.active) {
+        const protectedBinding = context.compilerTarget?.binding;
+        const compilerPoint = protectedBinding?.pointId === pointId && protectedBinding.contextId === contextId
+          && protectedBinding.revision === revision;
+        if (compilerPoint) return holds;
+
         const valid = [pointId, contextId, revision].every((value) => typeof value === 'string' && value.length > 0)
           && typeof guard === 'boolean' && typeof holds === 'boolean';
         if (!valid || context.events.length >= 256) {
@@ -102,6 +124,12 @@ export async function executeWitness(value: unknown): Promise<WitnessExecutionSu
   const operation = validateOperation((value as Record<string, unknown>).witness, request.manifest.inputs.length);
   const identity = { witnessPropertyId: request.manifest.propertyId, witnessTarget: operation.target };
   const target = operation.target;
+  const compilerRelation = target.dslNumericLocalRelation;
+  if (compilerRelation !== undefined) {
+    compilerRelation.compiler = validateCompilerLocalBinding(
+      compilerRelation.compiler, request.manifest, operation.sources, 'witness.target.dslNumericLocalRelation',
+    );
+  }
   const declaredCheck = request.manifest.assertions?.some((check) => check.id === target.id) === true;
   const diagnosticCheck = request.manifest.predicate.checkResultExportName !== undefined && declaredCheck;
   const originalCheckObservation = operation.mode === 'replay' && target.binding === undefined
@@ -151,6 +179,10 @@ export async function executeWitness(value: unknown): Promise<WitnessExecutionSu
   }
   const predicate = await loadEntryPoint(
     request.manifest.predicate, request.sourceRoots, 'manifest.predicate', request.tsconfig,
+    compilerRelation === undefined ? undefined : {
+      binding: compilerRelation.compiler,
+      observe: captureCompilerLocal,
+    },
   );
   const precondition = request.manifest.precondition === undefined ? undefined
     : await loadEntryPoint(
@@ -248,10 +280,19 @@ async function replayOnce(
   values: JsConcreteValue[], target: WitnessTarget, predicate: LoadedEntryPoint, precondition: LoadedEntryPoint | undefined,
   diagnosticCheck: boolean,
 ): Promise<WitnessNativeReplay> {
-  const context: WitnessContext = { events: [], active: false };
+  const localRelation = target.dslNumericLocalRelation;
+  const localInput = localRelation === undefined ? undefined : values[localRelation.inputIndex];
+  const context: WitnessContext = {
+    events: [], active: false, compilerCallbacks: 0,
+    compilerTarget: localRelation === undefined ? undefined : target,
+    compilerInput: typeof localInput === 'number' ? localInput : undefined,
+  };
   const result: WitnessNativeReplay = {
     admission: 'ADMITTED', outcome: 'HOLDS', targetMatched: false, events: context.events, runtimeVersion: process.version,
   };
+  if (localRelation !== undefined && typeof localInput !== 'number') {
+    return { ...result, admission: 'UNKNOWN', outcome: 'UNKNOWN', diagnostic: 'compiler-local-numeric-required' };
+  }
   const relation = target.entryRelation;
   const left = relation === undefined ? undefined : values[relation.leftInputIndex];
   const right = relation === undefined ? undefined : values[relation.rightInputIndex];
@@ -288,27 +329,57 @@ async function replayOnce(
       result.diagnostic = error instanceof ProtocolError ? error.code : describePropertyFailure(error).message;
     }
   }
+  context.active = false;
   if (context.contractError !== undefined) {
     result.admission = 'ERROR';
     result.outcome = 'ERROR';
     result.diagnostic = context.contractError;
   }
 
+  const requiresCompilerPoint = localRelation !== undefined && result.admission === 'ADMITTED';
+  const validCompilerPoint = !requiresCompilerPoint
+    || context.compilerCallbacks === 1 && context.compilerDiagnostic === undefined;
+  if (!validCompilerPoint) {
+    result.diagnostic = context.compilerDiagnostic ?? 'compiler-local-point-missing';
+  }
   const event = target.binding === undefined ? undefined
     : context.events.find((entry) => sameBinding(entry.binding, target.binding as WitnessBinding));
   const propertyFailed = result.outcome === 'FALSE' || result.outcome === 'THREW';
   const guardedEvent = event !== undefined && event.guard;
   const checkMatched = diagnosticCheck
     ? result.failure?.checkId === target.id
     : result.failure?.checkId === undefined || result.failure.checkId === target.id;
-  result.targetMatched = result.admission === 'ADMITTED' && (target.role === 'PROPERTY'
+  result.targetMatched = validCompilerPoint && result.admission === 'ADMITTED' && (target.role === 'PROPERTY'
     ? propertyFailed && checkMatched && (target.expectedOutcome === undefined || target.expectedOutcome === result.outcome)
       && (target.binding === undefined || (guardedEvent && !event.holds))
     : guardedEvent && (target.role === 'COVERAGE' || !event.holds));
 
   return result;
 }
 
+/** Only the callback passed to the selected companion can produce this protected event. */
+function captureCompilerLocal(nodeId: number, localName: string, value: unknown): void {
+  const context = contexts.getStore();
+  const target = context?.compilerTarget;
+  const relation = target?.dslNumericLocalRelation;
+  if (context === undefined || !context.active || relation === undefined) return;
+
+  context.compilerCallbacks += 1;
+  const valid = context.compilerCallbacks === 1 && nodeId === relation.compiler.nodeId
+    && localName === relation.compiler.localName && typeof value === 'number' && context.compilerInput !== undefined;
+  if (!valid) {
+    context.compilerDiagnostic = 'compiler-local-callback-mismatch';
+
+    return;
+  }
+  const left = relation.resultIsLeft ? value : context.compilerInput;
+  const right = relation.resultIsLeft ? context.compilerInput : value;
+  context.events.push({
+    binding: target!.binding!, guard: true,
+    holds: relation.template === 'STRICT_EQUAL' ? left === right : (left as number) <= (right as number),
+  });
+}
+
 export function sameTarget(actual: WitnessNativeReplay, expected: WitnessNativeReplay): boolean {
   return actual.admission === 'ADMITTED' && actual.targetMatched && actual.outcome === expected.outcome
     && actual.failure?.checkId === expected.failure?.checkId
@@ -341,12 +412,17 @@ function validateOperation(value: unknown, arity: number): WitnessOperation {
     && Number.isInteger(relation.leftInputIndex) && relation.leftInputIndex >= 0 && relation.leftInputIndex < arity
     && Number.isInteger(relation.rightInputIndex) && relation.rightInputIndex >= 0 && relation.rightInputIndex < arity
     && ['STRICT_EQUAL', 'LESS_OR_EQUAL'].includes(relation.template));
+  const local = target?.dslNumericLocalRelation;
+  const validLocal = local === undefined || (local !== null && typeof local === 'object' && !Array.isArray(local)
+    && relation === undefined && target?.role === 'HYPOTHESIS' && binding?.contextId === 'original-compiler-local'
+    && binding.occurrence === 0 && Number.isInteger(local.inputIndex) && local.inputIndex >= 0 && local.inputIndex < arity
+    && typeof local.resultIsLeft === 'boolean' && ['STRICT_EQUAL', 'LESS_OR_EQUAL'].includes(local.template));
   const valid = operation !== undefined && ['replay', 'reduce'].includes(operation.mode)
     && Array.isArray(operation.inputs) && operation.inputs.length === arity
     && typeof target?.id === 'string' && target.id.length > 0
     && ['PROPERTY', 'COVERAGE', 'HYPOTHESIS'].includes(target.role)
     && (target.expectedOutcome === undefined || ['FALSE', 'THREW'].includes(target.expectedOutcome))
-    && validBinding && validEntryRelation && (target.role === 'PROPERTY' || binding !== undefined)
+    && validBinding && validEntryRelation && validLocal && (target.role === 'PROPERTY' || binding !== undefined)
     && Array.isArray(operation.sources) && operation.sources.length > 0
     && operation.sources.every((source) => source !== null && typeof source === 'object' && typeof source.module === 'string'
       && typeof source.sha256 === 'string' && /^[0-9a-f]{64}$/.test(source.sha256));

usvm-ts-fast-check/fast-check-adapter/test/compiler-local-capture.test.ts

@@ -4,6 +4,7 @@ import { mkdtemp, realpath, rm, writeFile } from 'node:fs/promises';
 import { tmpdir } from 'node:os';
 import path from 'node:path';
 import test from 'node:test';
+import { executeWitness, type WitnessTarget } from '../src/external-witness.js';
 import { executeProperty } from '../src/execute-property.js';
 import { encodeJsValue, ProtocolError } from '../src/js-value.js';
 import type { CompilerNumericLocalBinding, ObservationPointRequest } from '../src/observe-property.js';
@@ -186,3 +187,85 @@ test('changed selected source and incompatible companion signature cannot supply
       error instanceof ProtocolError && error.code === 'protocol.request.invalid');
   }, '', false);
 });
+
+function witnessRequest(request: ReturnType<typeof buildRequest>, input = 7) {
+  const target: WitnessTarget = {
+    id: 'compiler-result', role: 'HYPOTHESIS',
+    binding: { pointId: 'compiler-result', contextId: 'original-compiler-local', revision: 'v1', occurrence: 0 },
+    dslNumericLocalRelation: {
+      compiler: request.observationRequest.points[0]!.compilerLocal!,
+      inputIndex: 0, resultIsLeft: true, template: 'STRICT_EQUAL',
+    },
+  };
+
+  return { ...request, witness: {
+    mode: 'replay', target, inputs: [encodeJsValue(input)], sources: request.observationRequest.sources,
+  } };
+}
+
+test('compiler witness callback compares original numeric snapshots with JavaScript semantics', async () => {
+  await fixture(async (request) => {
+    for (const input of [Number.NaN, -0, Number.NEGATIVE_INFINITY, Number.POSITIVE_INFINITY]) {
+      const initial = witnessRequest(request, input);
+      const selected = { ...initial, manifest: { ...initial.manifest, inputs: [{ name: 'value', domain: {
+        kind: 'number', min: { value: 'negative-infinity' }, max: { value: 'positive-infinity' }, allowNaN: true,
+      } }] } };
+
+      const replay = (await executeWitness(selected)).witnessReplay;
+
+      assert.equal(replay?.outcome, 'HOLDS');
+      assert.equal(replay?.targetMatched, Number.isNaN(input));
+      assert.deepEqual(replay?.events.map((event) => event.binding), [initial.witness.target.binding]);
+    }
+  });
+});
+
+test('missing wrong repeated and nonnumeric compiler witness receipts retain the original oracle', async () => {
+  const callbacks = [
+    '', "observer?.(5, 'result', result);", "observer?.(4, 'other', result);",
+    "observer?.(4, 'result', 'unsupported');",
+    "observer?.(4, 'result', result); observer?.(4, 'result', result);",
+  ];
+  for (const callback of callbacks) {
+    await fixture(async (request) => {
+      const replay = (await executeWitness(witnessRequest(request))).witnessReplay;
+
+      assert.equal(replay?.outcome, 'HOLDS');
+      assert.equal(replay?.admission, 'ADMITTED');
+      assert.equal(replay?.targetMatched, false);
+      assert.ok(replay?.diagnostic?.startsWith('compiler-local-'));
+    }, callback);
+  }
+});
+
+test('public witness hook cannot impersonate the compiler callback', async () => {
+  await fixture(async (request) => {
+    const replay = (await executeWitness(witnessRequest(request))).witnessReplay;
+
+    assert.equal(replay?.outcome, 'HOLDS');
+    assert.equal(replay?.targetMatched, false);
+    assert.deepEqual(replay?.events, []);
+    assert.equal(replay?.diagnostic, 'compiler-local-point-missing');
+  }, `(globalThis as any)[Symbol.for('org.usvm.ts.pbt.witness')]?.(
+    'compiler-result', 'original-compiler-local', 'v1', true, false);`);
+});
+
+test('compiler witness validates input index direction context and declared compiler authority', async () => {
+  await fixture(async (request) => {
+    const initial = witnessRequest(request);
+    const target = initial.witness.target;
+    const local = target.dslNumericLocalRelation!;
+    const badTargets = [
+      { ...target, dslNumericLocalRelation: { ...local, inputIndex: 1 } },
+      { ...target, dslNumericLocalRelation: { ...local, resultIsLeft: 'true' } },
+      { ...target, dslNumericLocalRelation: { ...local, template: 'COERCING_EQUAL' } },
+      { ...target, binding: { ...target.binding!, contextId: 'helper' } },
+      { ...target, dslNumericLocalRelation: { ...local, compiler: { ...local.compiler, producer: 'source-line' } } },
+      { ...target, dslNumericLocalRelation: { ...local, compiler: { ...local.compiler, sourceSha256: '0'.repeat(64) } } },
+    ];
+    for (const changed of badTargets) {
+      await assert.rejects(executeWitness({ ...initial, witness: { ...initial.witness, target: changed } }),
+        (error: unknown) => error instanceof ProtocolError && error.code === 'protocol.request.invalid');
+    }
+  });
+});

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

@@ -310,6 +310,11 @@ internal class FastCheckWitnessCoordinator(
             if (!numericInputs) return WitnessReplayStatus.UNSUPPORTED_REPLAY
         }
 
+        val localRelation = candidate.target.dslNumericLocalRelation
+        if (localRelation != null && inputs.getOrNull(localRelation.inputIndex) !is JsConcreteValue.Number) {
+            return WitnessReplayStatus.UNSUPPORTED_REPLAY
+        }
+
         val sourceModules = candidate.sources.mapTo(hashSetOf()) { source -> source.module }
         val requiredModules = listOfNotNull(property.predicate.module, property.precondition?.module)
         val validSources = candidate.sources.all { source -> source.sha256.matches(SHA256_REGEX) } &&