[TS PBT] Replay and shrink external witnesses with the original oracle

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/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/diagnostics.ts

@@ -19,6 +19,7 @@ const entryPoint = (code: string): AdapterDiagnosticDescriptor => ({
 export const adapterDiagnostic = {
   protocolJsonInvalid: invalidRequest('protocol.json.invalid'),
   protocolRequestInvalid: invalidRequest('protocol.request.invalid'),
+  witnessEventsInvalid: invalidRequest('witness.events.invalid'),
   protocolSeedInvalid: invalidRequest('protocol.seed.invalid'),
   protocolReplayPathInvalid: invalidRequest('protocol.replay-path.invalid'),
   protocolExamplesInvalid: invalidRequest('protocol.examples.invalid'),

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

@@ -143,9 +143,8 @@ export async function verifySourceHash(
   expectedSha256: string,
   sourceRoots: string[],
 ): Promise<void> {
-  const modulePath = await resolveModule(module, sourceRoots, 'observationRequest.sources');
-  const actual = createHash('sha256').update(await readFile(modulePath)).digest('hex');
-  if (actual !== expectedSha256) {
+  const matches = await sourceHashMatches(module, expectedSha256, sourceRoots);
+  if (!matches) {
     throw protocolError(
       adapterDiagnostic.entryPointSourceHashMismatch,
       `Selected TypeScript source changed: ${module}`,
@@ -154,6 +153,18 @@ export async function verifySourceHash(
   }
 }
 
+/** A replay may reject a stale source revision as an expected outcome before loading the original callback. */
+export async function sourceHashMatches(
+  module: string,
+  expectedSha256: string,
+  sourceRoots: string[],
+): Promise<boolean> {
+  const modulePath = await resolveModule(module, sourceRoots, 'observationRequest.sources');
+  const actual = createHash('sha256').update(await readFile(modulePath)).digest('hex');
+
+  return actual === expectedSha256;
+}
+
 async function resolveModule(
   module: string,
   sourceRoots: string[],

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

@@ -196,12 +196,13 @@ function buildProperty(
 }
 
 /** One invocation boundary; #353 exact replay uses the same shape after integration. */
-function invokePropertyOnce(
+export function invokePropertyOnce(
   values: JsConcreteValue[],
   predicate: LoadedEntryPoint,
   precondition: LoadedEntryPoint | undefined,
   recorder: ObservationRecorder | undefined,
   phase: 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown',
+  onPredicate?: () => void,
 ): boolean | null | Promise<boolean | null> {
   const invocationValues = cloneArguments(values);
   const invoke = (): boolean | null | Promise<boolean | null> => {
@@ -219,6 +220,7 @@ function invokePropertyOnce(
         }
 
         try {
+          onPredicate?.();
           const result = await predicate.invoke(invocationValues);
           recorder?.finish('admitted', result ? 'holds' : 'false');
 
@@ -242,6 +244,7 @@ function invokePropertyOnce(
     }
 
     try {
+      onPredicate?.();
       const result = predicate.invoke(invocationValues) as boolean;
       recorder?.finish('admitted', result ? 'holds' : 'false');
 
@@ -478,7 +481,7 @@ function failureDetails(details: RunDetails<[JsConcreteValue[]]>): FastCheckFail
   };
 }
 
-function describePropertyFailure(value: unknown): Pick<FastCheckFailureDetails, 'errorName' | 'message'> {
+export function describePropertyFailure(value: unknown): Pick<FastCheckFailureDetails, 'errorName' | 'message'> {
   try {
     if (value instanceof Error) {
       return {
@@ -506,7 +509,7 @@ function isFastCheckReplayFailure(error: unknown): boolean {
   return error instanceof Error && error.message.startsWith(FAST_CHECK_REPLAY_FAILURE_PREFIX);
 }
 
-function validateRequest(value: unknown): FastCheckExecutionRequest {
+export function validateRequest(value: unknown): FastCheckExecutionRequest {
   const request = requireRecord(
     value,
     adapterDiagnostic.protocolRequestInvalid,

usvm-ts-fast-check/fast-check-adapter/src/execution-cli.ts

@@ -2,6 +2,7 @@ import { adapterDiagnostic } from './diagnostics.js';
 import { startExecutionCoverage } from './execution-coverage.js';
 import { stringifyProtocolJson } from './protocol-json.js';
 import { executeProperty, type FastCheckExecutionSuccess } from './execute-property.js';
+import { executeWitness, type WitnessExecutionSuccess } from './external-witness.js';
 import { ProtocolError, protocolError } from './js-value.js';
 import type { ProtocolDiagnostic } from './js-value.js';
 
@@ -15,11 +16,12 @@ process.stdout.write = process.stderr.write.bind(process.stderr) as typeof proce
 
 const coverage = await startExecutionCoverage();
 try {
-  let response: FastCheckExecutionSuccess | FastCheckExecutionFailure;
+  let response: FastCheckExecutionSuccess | WitnessExecutionSuccess | FastCheckExecutionFailure;
   try {
     const request = parseRequest(await readStdin());
 
-    response = await executeProperty(request);
+    const isWitness = request !== null && typeof request === 'object' && 'witness' in request;
+    response = isWitness ? await executeWitness(request) : await executeProperty(request);
   } catch (error: unknown) {
     if (!(error instanceof ProtocolError)) throw error;
 
@@ -67,7 +69,7 @@ function protocolErrorResponse(error: ProtocolError): FastCheckExecutionFailure
   };
 }
 
-async function writeResponse(response: FastCheckExecutionSuccess | FastCheckExecutionFailure): Promise<void> {
+async function writeResponse(response: FastCheckExecutionSuccess | WitnessExecutionSuccess | FastCheckExecutionFailure): Promise<void> {
   const document = `${stringifyProtocolJson(response)}\n`;
 
   await new Promise<void>((resolve, reject) => {