From 32fab491c8f2a2423a71bef8ce03febc9bcab60f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 19:14:01 +0300 Subject: [PATCH 1/4] [TS PBT] Confirm and shrink external witnesses with original oracle replay --- .../fast-check-adapter/package.json | 2 +- .../src/execute-property.ts | 9 +- .../fast-check-adapter/src/execution-cli.ts | 8 +- .../src/external-witness.ts | 284 +++++++++++ .../fast-check-adapter/src/witness-support.ts | 46 ++ .../test/external-witness.test.ts | 161 +++++++ .../usvm/ts/pbt/fastcheck/FastCheckBackend.kt | 19 +- .../pbt/fastcheck/FastCheckCoverageSession.kt | 41 +- .../fastcheck/FastCheckExecutionProtocol.kt | 18 + .../pbt/fastcheck/FastCheckProcessClient.kt | 59 ++- .../fastcheck/FastCheckWitnessCoordinator.kt | 396 ++++++++++++++++ .../ts/pbt/fastcheck/ExternalWitnessTest.kt | 447 ++++++++++++++++++ .../usvm/PropertyExecutionConformanceTest.kt | 37 ++ .../properties/witness/CoverageWitness.ts | 11 + .../properties/witness/ExternalWitness.ts | 80 ++++ usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md | 129 +++++ usvm-ts-pbt/README.md | 4 + .../usvm/ts/pbt/backend/ExternalWitness.kt | 186 ++++++++ .../ts/pbt/backend/WitnessCandidateCapture.kt | 60 +++ 19 files changed, 1983 insertions(+), 14 deletions(-) create mode 100644 usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts create mode 100644 usvm-ts-fast-check/fast-check-adapter/src/witness-support.ts create mode 100644 usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts create mode 100644 usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt create mode 100644 usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt create mode 100644 usvm-ts-fast-check/src/test/resources/properties/witness/CoverageWitness.ts create mode 100644 usvm-ts-fast-check/src/test/resources/properties/witness/ExternalWitness.ts create mode 100644 usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/WitnessCandidateCapture.kt diff --git a/usvm-ts-fast-check/fast-check-adapter/package.json b/usvm-ts-fast-check/fast-check-adapter/package.json index 3fcbf35f61..953e7ddb10 100644 --- a/usvm-ts-fast-check/fast-check-adapter/package.json +++ b/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", diff --git a/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts b/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts index f4b8714dba..4af4985aae 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts +++ b/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 { const invocationValues = cloneArguments(values); const invoke = (): boolean | null | Promise => { @@ -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 { +export function describePropertyFailure(value: unknown): Pick { 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, diff --git a/usvm-ts-fast-check/fast-check-adapter/src/execution-cli.ts b/usvm-ts-fast-check/fast-check-adapter/src/execution-cli.ts index f9746a5bf3..62871dcfef 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/execution-cli.ts +++ b/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 { +async function writeResponse(response: FastCheckExecutionSuccess | WitnessExecutionSuccess | FastCheckExecutionFailure): Promise { const document = `${stringifyProtocolJson(response)}\n`; await new Promise((resolve, reject) => { diff --git a/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts b/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts new file mode 100644 index 0000000000..4c153b5fec --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts @@ -0,0 +1,284 @@ +import { AsyncLocalStorage } from 'node:async_hooks'; +import { performance } from 'node:perf_hooks'; +import fc from 'fast-check'; +import { adapterDiagnostic } from './diagnostics.js'; +import { EntryPointInvocationError, loadEntryPoint, verifySourceHash, type LoadedEntryPoint } from './entry-point.js'; +import { describePropertyFailure, invokePropertyOnce, 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 { inWitnessSupport } from './witness-support.js'; + +export interface WitnessBinding { + pointId: string; + contextId: string; + revision: string; + occurrence: number; +} + +export interface WitnessTarget { + id: string; + role: 'PROPERTY' | 'COVERAGE' | 'HYPOTHESIS'; + binding?: WitnessBinding; + expectedOutcome?: 'FALSE' | 'THREW'; +} + +export interface WitnessEvent { + binding: WitnessBinding; + guard: boolean; + holds: boolean; +} + +export interface WitnessNativeReplay { + admission: 'ADMITTED' | 'DOMAIN_REJECTED' | 'PRECONDITION_REJECTED' | 'ERROR'; + outcome: 'HOLDS' | 'FALSE' | 'THREW' | 'SKIPPED' | 'ERROR'; + targetMatched: boolean; + events: WitnessEvent[]; + failure?: FastCheckFailureDetails; + diagnostic?: string; + runtimeVersion?: string; +} + +export interface WitnessReduction { + status: 'UNSUPPORTED' | 'EXHAUSTED' | 'FAILED' | 'TIMEOUT'; + inputs?: TaggedJsValue[]; + attempts: number; + acceptedShrinks: number; + diagnostic?: string; +} + +export interface WitnessOperation { + mode: 'replay' | 'reduce'; + inputs: TaggedJsValue[]; + target: WitnessTarget; + sources: Array<{ module: string; sha256: string }>; + expected?: WitnessNativeReplay; +} + +export interface WitnessExecutionSuccess { + status: 'ok'; + witnessPropertyId: string; + witnessTarget: WitnessTarget; + witnessReplay?: WitnessNativeReplay; + witnessReduction?: WitnessReduction; +} + +interface WitnessContext { events: WitnessEvent[]; active: boolean; contractError?: ProtocolError } +const contexts = new AsyncLocalStorage(); + +/** A passive hook: evaluate the original guard/relation first; return its boolean without substituting an oracle. */ +export function installWitnessHook(): void { + Object.defineProperty(globalThis, Symbol.for('org.usvm.ts.pbt.witness'), { + configurable: true, + value: (pointId: string, contextId: string, revision: string, guard: boolean, holds: boolean): boolean => { + const context = contexts.getStore(); + if (context?.active) { + 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) { + context.contractError = protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid or unbounded witness events', 'witness.events'); + throw context.contractError; + } + + const occurrence = context.events.filter((event) => event.binding.pointId === pointId + && event.binding.contextId === contextId && event.binding.revision === revision).length; + context.events.push({ binding: { pointId, contextId, revision, occurrence }, guard, holds }); + } + + return holds; + }, + }); +} + +/** Uses the same invocation boundary, original entrypoints, codecs, and fast-check shrink stream as ordinary PBT. */ +export async function executeWitness(value: unknown): Promise { + const request = validateRequest(value); + const operation = validateOperation((value as Record).witness, request.manifest.inputs.length); + const identity = { witnessPropertyId: request.manifest.propertyId, witnessTarget: operation.target }; + const target = operation.target; + const validOriginalCheck = target.role !== 'PROPERTY' || (target.binding === undefined + ? (request.manifest.assertions?.length ?? 0) === 0 && target.id === request.manifest.predicate.exportName + : target.binding.pointId === target.id && request.manifest.assertions?.some((check) => check.id === target.id)); + if (!validOriginalCheck) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Original named check requires its executable binding', 'witness.target'); + } + for (const source of operation.sources) { + await verifySourceHash(source.module, source.sha256, request.sourceRoots); + } + const requiredModules = [request.manifest.predicate.module, request.manifest.precondition?.module] + .filter((module): module is string => module !== undefined); + if (!requiredModules.every((module) => operation.sources.some((source) => source.module === module))) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Witness sources must pin the original entrypoints', 'witness.sources'); + } + + installWitnessHook(); + const values = operation.inputs.map((input, index) => decodeJsValue(input, `witness.inputs[${index}]`)); + const arbitrary = buildPropertyArbitrary(request.manifest); + if (!inWitnessSupport(request.manifest, values)) { + if (operation.mode === 'reduce') { + return { status: 'ok', ...identity, witnessReduction: { + status: 'FAILED', attempts: 0, acceptedShrinks: 0, diagnostic: 'Input left declared support', + } }; + } + return { status: 'ok', ...identity, witnessReplay: { + admission: 'DOMAIN_REJECTED', outcome: 'SKIPPED', targetMatched: false, events: [], runtimeVersion: process.version, + } }; + } + const predicate = await loadEntryPoint(request.manifest.predicate, request.sourceRoots, 'manifest.predicate'); + const precondition = request.manifest.precondition === undefined ? undefined + : await loadEntryPoint(request.manifest.precondition, request.sourceRoots, 'manifest.precondition'); + const replay = (input: JsConcreteValue[]) => replayOnce(input, operation.target, predicate, precondition); + + if (operation.mode === 'replay') { + const first = await replay(values); + const second = await replay(values); + if (signature(first) !== signature(second)) first.diagnostic = 'nondeterministic'; + + return { status: 'ok', ...identity, witnessReplay: first }; + } + + if (!arbitrary.canShrinkWithoutContext(values)) { + return { status: 'ok', ...identity, witnessReduction: { + status: 'UNSUPPORTED', attempts: 0, acceptedShrinks: 0, + diagnostic: 'The backend arbitrary cannot shrink this external value without native context', + } }; + } + + const expected = operation.expected; + if (expected === undefined || !expected.targetMatched) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Reduction requires a confirmed target', 'witness.expected'); + } + const startedAt = performance.now(); + let attempts = 0; + let reductionError: unknown; + const property = fc.asyncProperty(new ExternalValueArbitrary(arbitrary, values), async (input) => { + attempts += 1; + try { + if (!inWitnessSupport(request.manifest, input)) return true; + const first = await replay(input); + const second = await replay(input); + if (signature(first) !== signature(second)) throw new Error('Nondeterministic shrinking invocation'); + if (first.outcome === 'ERROR') throw new Error(first.diagnostic ?? 'Original oracle error during reduction'); + + return !sameTarget(first, expected); + } catch (error: unknown) { + reductionError ??= error; + + return true; + } + }); + try { + const details = await fc.check(property, { + numRuns: 1, + seed: request.seed ?? 0, + interruptAfterTimeLimit: request.timeoutMillis, + markInterruptAsFailure: true, + }); + const timedOut = details.interrupted || performance.now() - startedAt >= request.timeoutMillis; + if (timedOut || reductionError !== undefined || details.counterexample === null) { + return { status: 'ok', ...identity, witnessReduction: { + status: timedOut ? 'TIMEOUT' : 'FAILED', attempts, acceptedShrinks: details.numShrinks, + diagnostic: reductionError === undefined ? 'Reduction did not retain the target' : describePropertyFailure(reductionError).message, + } }; + } + + return { status: 'ok', ...identity, witnessReduction: { + status: 'EXHAUSTED', inputs: details.counterexample[0].map(encodeJsValue), + attempts, acceptedShrinks: details.numShrinks, + } }; + } catch (error: unknown) { + return { status: 'ok', ...identity, witnessReduction: { + status: 'FAILED', attempts, acceptedShrinks: 0, diagnostic: describePropertyFailure(error).message, + } }; + } +} + +/** Only generation is replaced. All reduction comes from the backend's own arbitrary and retained shrink contexts. */ +class ExternalValueArbitrary extends fc.Arbitrary { + constructor(private readonly delegate: fc.Arbitrary, private readonly initial: JsConcreteValue[]) { + super(); + } + + generate(): fc.Value { return new fc.Value(structuredClone(this.initial), undefined); } + canShrinkWithoutContext(value: unknown): value is JsConcreteValue[] { return this.delegate.canShrinkWithoutContext(value); } + shrink(value: JsConcreteValue[], context: unknown): fc.Stream> { + return this.delegate.shrink(value, context); + } +} + +async function replayOnce( + values: JsConcreteValue[], target: WitnessTarget, predicate: LoadedEntryPoint, precondition: LoadedEntryPoint | undefined, +): Promise { + const context: WitnessContext = { events: [], active: false }; + const result: WitnessNativeReplay = { + admission: 'ADMITTED', outcome: 'HOLDS', targetMatched: false, events: context.events, runtimeVersion: process.version, + }; + try { + const holds = await contexts.run(context, () => invokePropertyOnce( + values, predicate, precondition, undefined, 'replay', () => { context.active = true; }, + )); + if (holds === null) { + result.admission = 'PRECONDITION_REJECTED'; + result.outcome = 'SKIPPED'; + } else { + result.outcome = holds ? 'HOLDS' : 'FALSE'; + } + } catch (error: unknown) { + if (error instanceof EntryPointInvocationError && context.contractError === undefined) { + result.outcome = 'THREW'; + result.failure = { kind: 'property', ...describePropertyFailure(error.thrownValue) }; + } else { + result.admission = 'ERROR'; + result.outcome = 'ERROR'; + result.diagnostic = context.contractError?.code + ?? (error instanceof ProtocolError ? error.code : describePropertyFailure(error).message); + } + } + 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; + result.targetMatched = result.admission === 'ADMITTED' && (target.role === 'PROPERTY' + ? propertyFailed && (target.expectedOutcome === undefined || target.expectedOutcome === result.outcome) + && (target.binding === undefined || (guardedEvent && !event.holds)) + : guardedEvent && (target.role === 'COVERAGE' || !event.holds)); + + return result; +} + +export function sameTarget(actual: WitnessNativeReplay, expected: WitnessNativeReplay): boolean { + return actual.admission === 'ADMITTED' && actual.targetMatched && actual.outcome === expected.outcome + && actual.failure?.errorName === expected.failure?.errorName; +} + +function sameBinding(left: WitnessBinding, right: WitnessBinding): boolean { + return left.pointId === right.pointId && left.contextId === right.contextId + && left.revision === right.revision && left.occurrence === right.occurrence; +} + +function signature(result: WitnessNativeReplay): string { return stringifyProtocolJson(result); } + +function validateOperation(value: unknown, arity: number): WitnessOperation { + if (value === null || typeof value !== 'object' || Array.isArray(value)) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Witness operation must be an object', 'witness'); + } + const operation = value as WitnessOperation | undefined; + const target = operation?.target; + const binding = target?.binding; + const validBinding = binding === undefined || (binding !== null && typeof binding.pointId === 'string' && binding.pointId.length > 0 + && typeof binding.contextId === 'string' && binding.contextId.length > 0 + && typeof binding.revision === 'string' && binding.revision.length > 0 + && Number.isInteger(binding.occurrence) && binding.occurrence >= 0); + 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 && (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)); + if (!valid) throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid external witness operation', 'witness'); + + return operation; +} diff --git a/usvm-ts-fast-check/fast-check-adapter/src/witness-support.ts b/usvm-ts-fast-check/fast-check-adapter/src/witness-support.ts new file mode 100644 index 0000000000..133e2e9796 --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/src/witness-support.ts @@ -0,0 +1,46 @@ +import type { PropertyManifestWire } from './execute-property.js'; +import { decodeJsNumber, decodeJsValue, type JsConcreteValue } from './js-value.js'; + +/** Admission checks the declared set independently of the arbitrary's ability to shrink external values. */ +export function inWitnessSupport(manifest: PropertyManifestWire, values: JsConcreteValue[]): boolean { + const domainsMatch = values.length === manifest.inputs.length + && manifest.inputs.every((input, index) => contains(input.domain, values[index])); + if (!domainsMatch) return false; + if (manifest.generator === undefined) return true; + + const [array, index] = values; + + return Array.isArray(array) && typeof index === 'number' && Number.isInteger(index) + && !Object.is(index, -0) && index >= 0 && index < array.length; +} + +function contains(domainValue: unknown, value: JsConcreteValue): boolean { + const domain = domainValue as Record; + switch (domain.kind) { + case 'boolean': return typeof value === 'boolean'; + case 'integer': return typeof value === 'number' && Number.isInteger(value) && !Object.is(value, -0) + && value >= (domain.min as number) && value <= (domain.max as number); + case 'number': return typeof value === 'number' && (Number.isNaN(value) + ? domain.allowNaN === true : value >= decodeJsNumber(domain.min) && value <= decodeJsNumber(domain.max)); + case 'string': return typeof value === 'string' && value.length >= (domain.minLength as number) + && value.length <= (domain.maxLength as number); + case 'constant': return Object.is(value, decodeJsValue(domain.value)); + case 'optional': return Object.is(value, decodeJsValue(domain.nil)) || contains(domain.value, value); + case 'array': return Array.isArray(value) && value.length >= (domain.minLength as number) + && value.length <= (domain.maxLength as number) && value.every((entry) => contains(domain.element, entry)); + case 'tuple': { + const elements = domain.elements as unknown[]; + + return Array.isArray(value) && value.length === elements.length + && elements.every((element, index) => contains(element, value[index])); + } + case 'object': { + const fields = domain.fields as Record; + + return value !== null && typeof value === 'object' && !Array.isArray(value) + && Object.keys(value).length === Object.keys(fields).length + && Object.entries(fields).every(([key, field]) => Object.hasOwn(value, key) && contains(field, value[key])); + } + default: return false; + } +} diff --git a/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts new file mode 100644 index 0000000000..da7c9578df --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts @@ -0,0 +1,161 @@ +import assert from 'node:assert/strict'; +import { createHash } from 'node:crypto'; +import { readFile } from 'node:fs/promises'; +import path from 'node:path'; +import { fileURLToPath } from 'node:url'; +import test from 'node:test'; +import { executeWitness, type WitnessNativeReplay, type WitnessTarget } from '../src/external-witness.js'; +import { encodeJsValue, ProtocolError } from '../src/js-value.js'; + +const root = path.resolve(path.dirname(fileURLToPath(import.meta.url)), '../../../src/test/resources'); +const module = 'properties/witness/ExternalWitness.ts'; +const sha256 = createHash('sha256').update(await readFile(path.join(root, module))).digest('hex'); +const binding = (pointId: string) => ({ pointId, contextId: 'original', revision: 'v1', occurrence: 0 }); + +function request(predicate: string, target: WitnessTarget = { id: predicate, role: 'PROPERTY' }, inputs = [encodeJsValue(80)]) { + return { + manifest: { + propertyId: 'witness.test', + predicate: { module, exportName: predicate, executionKind: 'sync' }, + inputs: [{ name: 'value', domain: { kind: 'integer', min: 0, max: 100 } }], + assertions: target.role === 'PROPERTY' && target.binding !== undefined + ? [{ id: target.id, source: { module, line: 1, column: 1 }, operands: [] }] : [], + }, + sourceRoots: [root], examples: [], numRuns: 1, timeoutMillis: 5000, + witness: { mode: 'replay', target, inputs, sources: [{ module, sha256 }] }, + }; +} + +async function reduced(predicate: string, target?: WitnessTarget) { + const replayRequest = request(predicate, target); + const original = (await executeWitness(replayRequest)).witnessReplay as WitnessNativeReplay; + const reductionRequest = { ...replayRequest, witness: { ...replayRequest.witness, mode: 'reduce', expected: original } }; + const result = (await executeWitness(reductionRequest)).witnessReduction; + + assert.equal(result?.status, 'EXHAUSTED'); + assert.ok(result.acceptedShrinks > 0); + assert.ok(result.attempts > 1); + + return result; +} + +test('external integer actually shrinks through native fast-check and retains the original failure', async () => { + const result = await reduced('threshold'); + + assert.deepEqual(result.inputs, [encodeJsValue(10)]); +}); + +test('a different failed named check cannot replace the target while shrinking', async () => { + const result = await reduced('namedChecks', { id: 'threshold-check', role: 'PROPERTY', binding: binding('threshold-check') }); + + assert.deepEqual(result.inputs, [encodeJsValue(15)]); +}); + +test('guarded hypothesis reduction keeps the complete original oracle holding', async () => { + const target: WitnessTarget = { id: 'hypothesis', role: 'HYPOTHESIS', binding: binding('hypothesis') }; + const result = await reduced('hypothesis', target); + const final = (await executeWitness(request('hypothesis', target, result.inputs))).witnessReplay; + + assert.deepEqual(result.inputs, [encodeJsValue(5)]); + assert.equal(final?.outcome, 'HOLDS'); + assert.equal(final?.targetMatched, true); +}); + +test('context revision occurrence and false guard must match exactly', async () => { + const target: WitnessTarget = { id: 'hypothesis', role: 'HYPOTHESIS', binding: binding('hypothesis') }; + for (const [predicate, selectedTarget, inputs] of [ + ['differentContext', target, [encodeJsValue(80)]], + ['hypothesis', { ...target, binding: { ...target.binding!, revision: 'v2' } }, [encodeJsValue(80)]], + ['hypothesis', target, [encodeJsValue(0)]], + ['repeatedHypothesis', target, [encodeJsValue(80)]], + ] as const) { + const result = (await executeWitness(request(predicate, selectedTarget, [...inputs]))).witnessReplay; + + assert.equal(result?.targetMatched, false); + } + + const matched = (await executeWitness(request('repeatedHypothesis', { + ...target, binding: { ...target.binding!, occurrence: 1 }, + }))).witnessReplay; + + assert.equal(matched?.targetMatched, true); +}); + +test('precondition and contract errors stay distinct from predicate exceptions', async () => { + const preconditionRequest = { ...request('threshold'), manifest: { + ...request('threshold').manifest, + precondition: { module, exportName: 'preconditionError', executionKind: 'sync' }, + } }; + const error = (await executeWitness(preconditionRequest)).witnessReplay; + const thrown = (await executeWitness(request('predicateError'))).witnessReplay; + const contract = (await executeWitness(request('contractError'))).witnessReplay; + + assert.equal(error?.outcome, 'ERROR'); + assert.equal(error?.targetMatched, false); + assert.equal(thrown?.outcome, 'THREW'); + assert.equal(thrown?.failure?.errorName, 'TypeError'); + assert.equal(contract?.outcome, 'ERROR'); +}); + +test('source drift and repeated outcome drift are retained explicitly', async () => { + const changed = request('threshold'); + changed.witness.sources[0]!.sha256 = '0'.repeat(64); + + await assert.rejects(executeWitness(changed), (error) => error instanceof ProtocolError + && error.code === 'entrypoint.source-hash.mismatch'); + + const replay = (await executeWitness(request('nondeterministic'))).witnessReplay; + + assert.equal(replay?.diagnostic, 'nondeterministic'); +}); + +test('native chained arbitrary without external context reports unsupported shrinking', async () => { + const base = request('supportedIndex', undefined, [encodeJsValue([80, 90]), encodeJsValue(1)]); + const dependent = { ...base, manifest: { ...base.manifest, + inputs: [ + { name: 'values', domain: { kind: 'array', element: { kind: 'integer', min: 0, max: 100 }, minLength: 1, maxLength: 3 } }, + { name: 'index', domain: { kind: 'integer', min: 0, max: 2 } }, + ], generator: { id: 'index', kind: 'array-index', arrayInputIndex: 0, indexInputIndex: 1 }, + } }; + const original = (await executeWitness(dependent)).witnessReplay; + const result = (await executeWitness({ ...dependent, witness: { ...dependent.witness, mode: 'reduce', expected: original } })).witnessReduction; + + assert.equal(result?.status, 'UNSUPPORTED'); + assert.equal(result?.attempts, 0); +}); + +test('each invocation isolates mutating input from replay and native shrinking', async () => { + const base = request('mutation', undefined, [encodeJsValue([80, 90, 100, 70])]); + const mutation = { ...base, manifest: { ...base.manifest, inputs: [{ name: 'values', domain: { + kind: 'array', element: { kind: 'integer', min: 0, max: 100 }, minLength: 0, maxLength: 5, + } }] } }; + const original = (await executeWitness(mutation)).witnessReplay; + const result = (await executeWitness({ ...mutation, witness: { ...mutation.witness, mode: 'reduce', expected: original } })).witnessReduction; + + assert.equal(original?.outcome, 'FALSE'); + assert.equal(original?.diagnostic, undefined); + assert.deepEqual(result?.inputs, [encodeJsValue([0, 0, 0])]); + assert.deepEqual(mutation.witness.inputs, [encodeJsValue([80, 90, 100, 70])]); +}); + +test('declared domain rejects values independently of shrinking capability', async () => { + for (const input of [encodeJsValue(101), encodeJsValue(-0), encodeJsValue(Number.NaN), encodeJsValue('80')]) { + const replay = (await executeWitness(request('threshold', undefined, [input]))).witnessReplay; + + assert.equal(replay?.admission, 'DOMAIN_REJECTED'); + assert.equal(replay?.outcome, 'SKIPPED'); + assert.equal(replay?.targetMatched, false); + } +}); + +test('malformed witness operation and wrong symbolic failure kind cannot confirm a target', async () => { + for (const witness of [null, [], {}, { ...request('threshold').witness, target: null }]) { + await assert.rejects(executeWitness({ ...request('threshold'), witness }), ProtocolError); + } + const replay = (await executeWitness(request('predicateError', { + id: 'predicateError', role: 'PROPERTY', expectedOutcome: 'FALSE', + }))).witnessReplay; + + assert.equal(replay?.targetMatched, false); + assert.equal(replay?.outcome, 'THREW'); +}); diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt index 3fc53edcbf..b69c2d6e0c 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt @@ -1,10 +1,15 @@ package org.usvm.ts.pbt.fastcheck import org.usvm.ts.pbt.FastCheckDiagnosticCode +import org.usvm.ts.pbt.backend.ExternalWitnessBackend +import org.usvm.ts.pbt.backend.ExternalWitnessCandidate import org.usvm.ts.pbt.backend.PropertyBasedTestingBackend import org.usvm.ts.pbt.backend.PropertyCoverageCapability import org.usvm.ts.pbt.backend.PropertyRunConfiguration import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.backend.WitnessEvidenceDelta +import org.usvm.ts.pbt.backend.WitnessReplayConfiguration +import org.usvm.ts.pbt.backend.WitnessReplayDeadline import org.usvm.ts.pbt.manifest.toManifest import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyDefinition @@ -23,7 +28,7 @@ class FastCheckBackend( nodeExecutable: String = "node", adapterEntryPoint: Path = FastCheckRuntime.executionEntryPoint(), private val tsconfig: Path? = null, -) : PropertyBasedTestingBackend { +) : PropertyBasedTestingBackend, ExternalWitnessBackend { override val coverageCapability: PropertyCoverageCapability = PropertyCoverageCapability.supported( backendId = FAST_CHECK_BACKEND_ID, backendVersion = FastCheckRuntimeMetadata.fastCheckVersion, @@ -61,6 +66,18 @@ class FastCheckBackend( return client.check(request) } + override fun confirmWitness( + property: PropertyDefinition, + candidate: ExternalWitnessCandidate, + configuration: WitnessReplayConfiguration, + deadline: WitnessReplayDeadline, + ): WitnessEvidenceDelta = FastCheckWitnessCoordinator(client = client, sourceRoots = sourceRoots).confirm( + property = property, + candidate = candidate, + configuration = configuration, + deadline = deadline, + ) + private fun validateConfiguration( property: PropertyDefinition, configuration: PropertyRunConfiguration, diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt index 25fd5c04f1..9755636050 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt @@ -14,6 +14,7 @@ import org.usvm.ts.pbt.coverage.decodeIstanbulCoverageReport import org.usvm.ts.pbt.coverage.inspectRawV8SourceMapDiagnostics import org.usvm.ts.pbt.coverage.mergeCoverageDiagnostics import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.PropertyId import java.io.IOException import java.nio.file.Files import java.nio.file.Path @@ -25,6 +26,7 @@ internal class FastCheckCoverageSession private constructor( private val request: FastCheckExecutionRequest, private val runtimeVersion: String, private val workspace: CoverageWorkspace, + private val remainingMillis: (() -> Long)?, ) : AutoCloseable { val adapterCommand: List get() = buildList { @@ -60,6 +62,10 @@ internal class FastCheckCoverageSession private constructor( } fun attachTo(result: PropertyRunResult): PropertyRunResult { + return result.copy(coverage = readArtifact()) + } + + fun readArtifact(): PropertyCoverageArtifact { val coverageRequest = requireNotNull(request.coverageRequest) val entryPointPaths = propertyEntryPointPaths() @@ -67,7 +73,7 @@ internal class FastCheckCoverageSession private constructor( val context = IstanbulCoverageContext( backendId = FastCheckBackend.FAST_CHECK_BACKEND_ID, backendVersion = FastCheckRuntimeMetadata.fastCheckVersion, - propertyId = result.propertyId, + propertyId = PropertyId(request.manifest.propertyId), sourceRoots = request.sourceRoots, propertyEntryPointPaths = entryPointPaths, adapterRoot = workspace.adapterRoot.toString(), @@ -106,7 +112,7 @@ internal class FastCheckCoverageSession private constructor( ) } - return result.copy(coverage = artifact) + return artifact } private fun propertyEntryPointPaths(): Set { @@ -138,7 +144,7 @@ internal class FastCheckCoverageSession private constructor( command = listOf(nodeExecutable, converter.toString(), workspace.rawDirectory.toString()) + request.sourceRoots, request = "", - timeoutMillis = BRANCH_CONVERSION_TIMEOUT_MILLIS, + timeoutMillis = boundedTimeout(BRANCH_CONVERSION_TIMEOUT_MILLIS), reportedTimeoutMillis = BRANCH_CONVERSION_TIMEOUT_MILLIS, description = "TypeScript branch converter", ) @@ -193,6 +199,19 @@ internal class FastCheckCoverageSession private constructor( workspace.root.toFile().deleteRecursively() } + private fun boundedTimeout(limitMillis: Long): Long { + val remaining = remainingMillis?.invoke() ?: return limitMillis + if (remaining <= 0) { + throw PbtBackendException( + kind = BackendErrorKind.TIMEOUT, + code = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + message = "External witness deadline expired during coverage collection", + propertyId = request.manifest.propertyId, + ) + } + return minOf(limitMillis, remaining) + } + private fun canonicalizeExistingEntryPoint(candidate: Path): String = if (Files.exists(candidate)) candidate.toRealPath().toString() else candidate.toString() @@ -215,8 +234,9 @@ internal class FastCheckCoverageSession private constructor( nodeExecutable: String, adapterEntryPoint: Path, request: FastCheckExecutionRequest, + remainingMillis: (() -> Long)? = null, ): FastCheckCoverageSession { - val runtimeVersion = readSupportedNodeVersion(nodeExecutable, request) + val runtimeVersion = readSupportedNodeVersion(nodeExecutable, request, remainingMillis) val adapterRoot = adapterEntryPoint.parent?.parent?.parent ?: throw IllegalArgumentException("Adapter entry point has no runtime root: $adapterEntryPoint") val c8EntryPoint = adapterRoot.resolve("node_modules/c8/bin/c8.js") @@ -238,6 +258,7 @@ internal class FastCheckCoverageSession private constructor( request = request, runtimeVersion = runtimeVersion, workspace = workspace, + remainingMillis = remainingMillis, ) } @@ -264,7 +285,17 @@ internal class FastCheckCoverageSession private constructor( private fun readSupportedNodeVersion( nodeExecutable: String, request: FastCheckExecutionRequest, + remainingMillis: (() -> Long)?, ): String { + val remaining = remainingMillis?.invoke() ?: NODE_VERSION_TIMEOUT_MILLIS + if (remaining <= 0) { + failPreparation( + request = request, + code = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + message = "External witness deadline expired before the runtime probe", + kind = BackendErrorKind.TIMEOUT, + ) + } val transport = FastCheckProcessTransport( nodeExecutable = nodeExecutable, maxRequestBytes = 1, @@ -277,7 +308,7 @@ internal class FastCheckCoverageSession private constructor( transport.invoke( command = listOf(nodeExecutable, "--version"), request = "", - timeoutMillis = NODE_VERSION_TIMEOUT_MILLIS, + timeoutMillis = minOf(NODE_VERSION_TIMEOUT_MILLIS, remaining), reportedTimeoutMillis = NODE_VERSION_TIMEOUT_MILLIS, description = "Node.js version probe", ) diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt index 53246a08fc..65168e34f8 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt @@ -5,9 +5,13 @@ import kotlinx.serialization.Serializable import kotlinx.serialization.Transient import org.usvm.ts.pbt.backend.PropertyCoverageRequest import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.backend.WitnessNativeReplay +import org.usvm.ts.pbt.backend.WitnessReduction +import org.usvm.ts.pbt.backend.WitnessTarget import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.observation.PropertyObservationRequest +import org.usvm.ts.pbt.observation.PropertyObservationSource @Serializable internal data class FastCheckExecutionRequest( @@ -20,6 +24,7 @@ internal data class FastCheckExecutionRequest( val timeoutMillis: Long, val examples: List> = emptyList(), val observationRequest: PropertyObservationRequest? = null, + val witness: FastCheckWitnessOperation? = null, @Transient val coverageRequest: PropertyCoverageRequest? = null, ) @@ -28,9 +33,22 @@ internal data class FastCheckExecutionRequest( internal data class FastCheckExecutionWireResponse( val status: String, val result: PropertyRunResult? = null, + val witnessReplay: WitnessNativeReplay? = null, + val witnessReduction: WitnessReduction? = null, + val witnessPropertyId: String? = null, + val witnessTarget: WitnessTarget? = null, val diagnostics: List = emptyList(), ) +@Serializable +internal data class FastCheckWitnessOperation( + val mode: String, + val inputs: List, + val target: WitnessTarget, + val sources: List, + val expected: WitnessNativeReplay? = null, +) + /** Infrastructure categories that remain distinct from a falsified property result. */ @Serializable enum class BackendErrorKind { diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt index 5f71da5460..7024dc49df 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt @@ -51,15 +51,72 @@ internal class FastCheckProcessClient( } } + /** One external operation, using the same supervised transport and optional original-source collector. */ + fun witness( + request: FastCheckExecutionRequest, + remainingMillis: () -> Long, + ): FastCheckExecutionWireResponse { + val encodedRequest = encodeRequest(request) + val coverageSession = request.coverageRequest?.let { + FastCheckCoverageSession.prepare( + nodeExecutable = nodeExecutable, + adapterEntryPoint = adapterEntryPoint, + request = request, + remainingMillis = remainingMillis, + ) + } + + try { + val remaining = remainingMillis() + if (remaining <= 0) { + throw backendError( + kind = BackendErrorKind.TIMEOUT, + code = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + message = "External witness deadline expired", + request = request, + ) + } + + val output = invokeAdapter( + encodedRequest = encodedRequest, + request = request, + command = coverageSession?.adapterCommand ?: listOf(nodeExecutable, adapterEntryPoint.toString()), + timeoutMillis = remaining, + ) + validateProcessOutput(output, request) + val response = decodeResponse(output.stdout, request) + if (response.status == "error") throwNodeDiagnostic(response, request) + + val isReplayResponse = request.witness?.mode == "replay" && response.witnessReplay != null && + response.witnessReduction == null + val isReductionResponse = request.witness?.mode == "reduce" && response.witnessReduction != null && + response.witnessReplay == null + val validResponse = response.status == "ok" && response.result == null && + response.witnessPropertyId == request.manifest.propertyId && + response.witnessTarget == request.witness?.target && (isReplayResponse || isReductionResponse) + if (!validResponse) throw invalidResponse(message = "Invalid witness response", request = request) + + val replay = response.witnessReplay + return if (replay != null && coverageSession != null) { + response.copy(witnessReplay = replay.copy(coverage = coverageSession.readArtifact())) + } else { + response + } + } finally { + coverageSession?.close() + } + } + private fun invokeAdapter( encodedRequest: String, request: FastCheckExecutionRequest, command: List, + timeoutMillis: Long = saturatedAdd(request.timeoutMillis, transportGraceMillis), ): FastCheckProcessOutput = try { transport.invoke( command = command, request = encodedRequest, - timeoutMillis = saturatedAdd(request.timeoutMillis, transportGraceMillis), + timeoutMillis = timeoutMillis, reportedTimeoutMillis = request.timeoutMillis, description = "fast-check adapter", ) diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt new file mode 100644 index 0000000000..2b0ef5e294 --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt @@ -0,0 +1,396 @@ +package org.usvm.ts.pbt.fastcheck + +import kotlinx.serialization.decodeFromString +import org.usvm.ts.pbt.backend.ExternalWitnessCandidate +import org.usvm.ts.pbt.backend.PropertyCoverageRequest +import org.usvm.ts.pbt.backend.WitnessAdmission +import org.usvm.ts.pbt.backend.WitnessCoverageEdge +import org.usvm.ts.pbt.backend.WitnessEvidenceDelta +import org.usvm.ts.pbt.backend.WitnessNativeReplay +import org.usvm.ts.pbt.backend.WitnessOracleOutcome +import org.usvm.ts.pbt.backend.WitnessReduction +import org.usvm.ts.pbt.backend.WitnessReductionStatus +import org.usvm.ts.pbt.backend.WitnessReplayConfiguration +import org.usvm.ts.pbt.backend.WitnessReplayDeadline +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.backend.WitnessRole +import org.usvm.ts.pbt.backend.witnessManifestSha256 +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.model.JsConcreteValue +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.model.encodeToUtf8SafeString +import org.usvm.ts.pbt.validation.validatePropertyDefinition +import java.nio.file.Path + +/** Owns admission, repeatability, final validation and evidence publication; Node owns native shrinking. */ +internal class FastCheckWitnessCoordinator( + private val client: FastCheckProcessClient, + private val sourceRoots: List, +) { + fun confirm( + property: PropertyDefinition, + candidate: ExternalWitnessCandidate, + configuration: WitnessReplayConfiguration, + deadline: WitnessReplayDeadline, + ): WitnessEvidenceDelta { + val validation = validatePropertyDefinition(property) + if (!validation.isValid) { + return delta( + candidate = candidate, + status = WitnessReplayStatus.PROPERTY_ERROR, + diagnostic = validation.diagnostics.joinToString { diagnostic -> diagnostic.code }, + ) + } + val earlyStatus = validateCandidate(property, candidate) + if (earlyStatus != null) return delta(candidate = candidate, status = earlyStatus) + + val inputs = requireNotNull(candidate.inputs) + var firstReplay: WitnessNativeReplay? = null + try { + val original = replay(property, candidate, inputs, deadline) + firstReplay = original + val confirmation = replay(property, candidate, inputs, deadline) + if (!repeatable(original, confirmation)) { + return delta( + candidate = candidate, + status = WitnessReplayStatus.NONDETERMINISTIC, + original = original, + ) + } + } catch (error: PbtBackendException) { + return delta( + candidate = candidate, + status = error.replayStatus(), + original = firstReplay, + diagnostic = error.code, + ) + } + + val original = requireNotNull(firstReplay) + val status = classify(original, candidate) + if (!original.targetMatched || original.admission != WitnessAdmission.ADMITTED) { + return delta(candidate = candidate, status = status, original = original) + } + + var confirmedOriginal = original + var coverageDiagnostic: String? = null + val coverageRequest = configuration.coverageRequest + if (coverageRequest != null) { + try { + val covered = replay(property, candidate, inputs, deadline, coverageRequest) + if (!repeatable(original, covered)) { + return delta( + candidate = candidate, + status = WitnessReplayStatus.NONDETERMINISTIC, + original = original, + ) + } + confirmedOriginal = covered + } catch (error: PbtBackendException) { + coverageDiagnostic = error.code + } + } + + val reduction = reduce(property, candidate, confirmedOriginal, configuration, deadline) + val finalReduction = validateReduction(property, candidate, original, reduction, deadline) + + val additions = confirmedEdges(candidate, confirmedOriginal) - configuration.knownEdges + val refutations = if (candidate.target.role == WitnessRole.HYPOTHESIS) { + original.events.filter { event -> + event.binding == candidate.target.binding && event.guard && !event.holds + } + } else { + emptyList() + } + + return delta( + candidate = candidate, + status = status, + original = confirmedOriginal, + reduced = finalReduction.replay, + reduction = finalReduction.reduction, + edges = additions, + diagnostic = coverageDiagnostic, + ).copy(contextualRefutations = refutations) + } + + private fun validateReduction( + property: PropertyDefinition, + candidate: ExternalWitnessCandidate, + original: WitnessNativeReplay, + reduction: WitnessReduction, + deadline: WitnessReplayDeadline, + ): ValidatedReduction { + val inputs = reduction.inputs + if (reduction.status != WitnessReductionStatus.EXHAUSTED || inputs == null) { + return ValidatedReduction(reduction = reduction) + } + + if (!inDeclaredSupport(property, inputs)) { + return ValidatedReduction( + reduction = reduction.copy( + status = WitnessReductionStatus.FAILED, + inputs = null, + diagnostic = "Reduced input left declared support", + ), + ) + } + + return try { + val finalReplay = replay(property, candidate, inputs, deadline) + val finalConfirmation = replay(property, candidate, inputs, deadline) + val validFinal = repeatable(finalReplay, finalConfirmation) && sameTarget(finalReplay, original) + if (validFinal) { + ValidatedReduction( + reduction = reduction.copy(reducedEncodedBytes = encodedBytes(inputs)), + replay = finalReplay, + ) + } else { + ValidatedReduction( + reduction = reduction.copy( + status = WitnessReductionStatus.FAILED, + inputs = null, + diagnostic = "Final original oracle did not reproduce the same target", + ), + ) + } + } catch (error: PbtBackendException) { + ValidatedReduction( + reduction = reduction.copy( + status = if (error.kind == BackendErrorKind.TIMEOUT) { + WitnessReductionStatus.TIMEOUT + } else { + WitnessReductionStatus.FAILED + }, + inputs = null, + diagnostic = error.code, + ), + ) + } + } + + private fun validateCandidate( + property: PropertyDefinition, + candidate: ExternalWitnessCandidate, + ): WitnessReplayStatus? { + val sameRegistration = property.id == candidate.propertyId && + property.witnessManifestSha256() == candidate.manifestSha256 && property.toManifest() == candidate.manifest + if (!sameRegistration) return WitnessReplayStatus.SOURCE_MISMATCH + + val inputs = candidate.inputs ?: return WitnessReplayStatus.UNREPRESENTABLE_INPUT + val encodable = runCatching { + val encoded = PropertyManifestJson.json.encodeToUtf8SafeString(inputs) + PropertyManifestJson.json.decodeFromString>(encoded) + }.isSuccess + if (!encodable) return WitnessReplayStatus.UNREPRESENTABLE_INPUT + if (!inDeclaredSupport(property, inputs)) return WitnessReplayStatus.DOMAIN_REJECTED + + 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) } && + sourceModules.size == candidate.sources.size && requiredModules.all { module -> module in sourceModules } + if (!validSources) return WitnessReplayStatus.UNSUPPORTED_REPLAY + + val target = candidate.target + val binding = target.binding + val validCheck = target.role != WitnessRole.PROPERTY || if (binding == null) { + property.assertions.isEmpty() && target.id == property.predicate.exportName + } else { + binding.pointId == target.id && property.assertions.any { assertion -> assertion.id == target.id } + } + if (!validCheck) return WitnessReplayStatus.UNSUPPORTED_REPLAY + + return null + } + + private fun replay( + property: PropertyDefinition, + candidate: ExternalWitnessCandidate, + inputs: List, + deadline: WitnessReplayDeadline, + coverageRequest: PropertyCoverageRequest? = null, + ): WitnessNativeReplay { + val response = client.witness( + request = request( + property = property, + candidate = candidate, + operation = FastCheckWitnessOperation( + mode = "replay", + inputs = inputs, + target = candidate.target, + sources = candidate.sources, + ), + timeoutMillis = deadline.remainingMillis().coerceAtLeast(1), + coverageRequest = coverageRequest, + ), + remainingMillis = deadline::remainingMillis, + ) + + return requireNotNull(response.witnessReplay) + } + + private fun reduce( + property: PropertyDefinition, + candidate: ExternalWitnessCandidate, + original: WitnessNativeReplay, + configuration: WitnessReplayConfiguration, + deadline: WitnessReplayDeadline, + ): WitnessReduction { + val originalBytes = encodedBytes(requireNotNull(candidate.inputs)) + if (!configuration.shrink) { + return WitnessReduction(status = WitnessReductionStatus.DISABLED, originalEncodedBytes = originalBytes) + } + + val budget = deadline.remainingMillis() - configuration.validationReserveMillis + if (budget <= 0) { + return WitnessReduction(status = WitnessReductionStatus.TIMEOUT, originalEncodedBytes = originalBytes) + } + + val shrinkDeadline = WitnessReplayDeadline(timeoutMillis = budget) + return try { + val response = client.witness( + request = request( + property = property, + candidate = candidate, + operation = FastCheckWitnessOperation( + mode = "reduce", + inputs = requireNotNull(candidate.inputs), + target = candidate.target, + sources = candidate.sources, + expected = original.copy(coverage = null), + ), + timeoutMillis = budget, + ), + remainingMillis = { minOf(deadline.remainingMillis(), shrinkDeadline.remainingMillis()) }, + ) + requireNotNull(response.witnessReduction).copy(originalEncodedBytes = originalBytes) + } catch (error: PbtBackendException) { + WitnessReduction( + status = if (error.kind == BackendErrorKind.TIMEOUT) { + WitnessReductionStatus.TIMEOUT + } else { + WitnessReductionStatus.FAILED + }, + originalEncodedBytes = originalBytes, + diagnostic = error.code, + ) + } + } + + private fun request( + property: PropertyDefinition, + candidate: ExternalWitnessCandidate, + operation: FastCheckWitnessOperation, + timeoutMillis: Long, + coverageRequest: PropertyCoverageRequest? = null, + ): FastCheckExecutionRequest { + check(candidate.propertyId == property.id) + return FastCheckExecutionRequest( + manifest = property.toManifest(), + sourceRoots = sourceRoots.map(Path::toString), + numRuns = 1, + timeoutMillis = timeoutMillis, + witness = operation, + coverageRequest = coverageRequest, + ) + } + + private fun confirmedEdges( + candidate: ExternalWitnessCandidate, + original: WitnessNativeReplay, + ): Set { + val coverage = original.coverage ?: return emptySet() + val sourcesByPath = candidate.sources.flatMap { source -> + sourceRoots.map { root -> root.resolve(source.module).normalize().toString() to source } + }.toMap() + + return buildSet { + for (file in coverage.files) { + val source = sourcesByPath[file.path] ?: continue + val fileHasDiagnostic = coverage.diagnostics.any { diagnostic -> + diagnostic.path == null || diagnostic.path == file.path + } + if (fileHasDiagnostic) continue + + for (branch in file.branches) { + if (branch.type != "if" || branch.arms.size != 2) continue + + branch.arms.forEachIndexed { index, arm -> + if (arm.hits > 0) { + add(WitnessCoverageEdge(source = source, location = branch.location, outcome = index == 0)) + } + } + } + } + } + } + + private fun delta( + candidate: ExternalWitnessCandidate, + status: WitnessReplayStatus, + original: WitnessNativeReplay? = null, + reduced: WitnessNativeReplay? = null, + reduction: WitnessReduction = WitnessReduction(status = WitnessReductionStatus.NOT_ELIGIBLE), + edges: Set = emptySet(), + diagnostic: String? = null, + ) = WitnessEvidenceDelta( + candidate = candidate, + status = status, + originalReplay = original, + reducedReplay = reduced, + reduction = reduction, + confirmedEdgeAdditions = edges, + backendId = FastCheckBackend.FAST_CHECK_BACKEND_ID, + backendVersion = FastCheckRuntimeMetadata.fastCheckVersion, + diagnostic = diagnostic, + ) + + private companion object { + val SHA256_REGEX = Regex("[0-9a-f]{64}") + + fun inDeclaredSupport(property: PropertyDefinition, inputs: List): Boolean = + inputs.size == property.inputs.size && + property.inputs.zip(inputs).all { (input, value) -> value in input.domain } && + property.generator?.accepts(inputs) != false + + fun encodedBytes(inputs: List): Int = + PropertyManifestJson.json.encodeToUtf8SafeString(inputs).toByteArray(Charsets.UTF_8).size + + fun repeatable(first: WitnessNativeReplay, second: WitnessNativeReplay): Boolean = + first.diagnostic != "nondeterministic" && second.diagnostic != "nondeterministic" && + first.copy(coverage = null) == second.copy(coverage = null) + + fun sameTarget(actual: WitnessNativeReplay, expected: WitnessNativeReplay): Boolean = + actual.admission == WitnessAdmission.ADMITTED && actual.targetMatched && + actual.outcome == expected.outcome && actual.failure?.errorName == expected.failure?.errorName + + fun classify(replay: WitnessNativeReplay, candidate: ExternalWitnessCandidate): WitnessReplayStatus = when { + replay.outcome == WitnessOracleOutcome.ERROR -> WitnessReplayStatus.PROPERTY_ERROR + replay.admission == WitnessAdmission.DOMAIN_REJECTED -> WitnessReplayStatus.DOMAIN_REJECTED + replay.admission == WitnessAdmission.PRECONDITION_REJECTED -> WitnessReplayStatus.PRECONDITION_REJECTED + replay.diagnostic == "nondeterministic" -> WitnessReplayStatus.NONDETERMINISTIC + !replay.targetMatched && replay.outcome == WitnessOracleOutcome.HOLDS && + candidate.target.role == WitnessRole.PROPERTY -> WitnessReplayStatus.PROPERTY_HOLDS + !replay.targetMatched -> WitnessReplayStatus.TARGET_MISMATCH + replay.outcome == WitnessOracleOutcome.FALSE || replay.outcome == WitnessOracleOutcome.THREW -> + WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION + candidate.target.role == WitnessRole.HYPOTHESIS -> WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION + else -> WitnessReplayStatus.CONFIRMED_COVERAGE + } + + fun PbtBackendException.replayStatus(): WitnessReplayStatus = when { + kind == BackendErrorKind.TIMEOUT -> WitnessReplayStatus.TIMEOUT + code == "entrypoint.source-hash.mismatch" -> WitnessReplayStatus.SOURCE_MISMATCH + code.startsWith("js-value.") || code.startsWith("js-number.") -> WitnessReplayStatus.UNREPRESENTABLE_INPUT + else -> WitnessReplayStatus.REPLAY_ERROR + } + } +} + +private data class ValidatedReduction( + val reduction: WitnessReduction, + val replay: WitnessNativeReplay? = null, +) diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt new file mode 100644 index 0000000000..20d7fbb755 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt @@ -0,0 +1,447 @@ +package org.usvm.ts.pbt.fastcheck + +import kotlinx.serialization.decodeFromString +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.CoverageScope +import org.usvm.ts.pbt.backend.PropertyCoverageRequest +import org.usvm.ts.pbt.backend.WitnessBinding +import org.usvm.ts.pbt.backend.WitnessEvidenceDelta +import org.usvm.ts.pbt.backend.WitnessOracleOutcome +import org.usvm.ts.pbt.backend.WitnessReductionStatus +import org.usvm.ts.pbt.backend.WitnessReplayConfiguration +import org.usvm.ts.pbt.backend.WitnessReplayDeadline +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.backend.WitnessRole +import org.usvm.ts.pbt.backend.WitnessTarget +import org.usvm.ts.pbt.backend.captureWitness +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.ArrayIndexGenerator +import org.usvm.ts.pbt.model.ConstantDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyAssertion +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.PropertySourcePoint +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.model.encodeToUtf8SafeString +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.testResourcesRoot +import java.nio.file.Files +import java.security.MessageDigest +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class ExternalWitnessTest { + private val root = testResourcesRoot() + private val backend = FastCheckBackend(sourceRoots = listOf(root)) + private val configuration = WitnessReplayConfiguration(timeoutMillis = 15_000, validationReserveMillis = 3_000) + + @Test + fun `external witness shrinks and serializes original final inputs and backend provenance`() { + val property = property(predicate = "threshold") + val candidate = candidate(property = property) + + val result = backend.confirmWitness(property = property, candidate = candidate, configuration = configuration) + val json = PropertyManifestJson.json.encodeToUtf8SafeString(result) + val decoded = PropertyManifestJson.json.decodeFromString(json) + + assertEquals(result, decoded) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, result.status) + assertEquals(listOf(JsConcreteValue.number(80.0)), result.candidate.inputs) + assertEquals(listOf(JsConcreteValue.number(10.0)), result.reduction.inputs) + assertEquals(WitnessReductionStatus.EXHAUSTED, result.reduction.status) + assertEquals(WitnessOracleOutcome.FALSE, result.reducedReplay?.outcome) + assertTrue(result.reduction.acceptedShrinks > 0) + assertTrue(result.reduction.attempts > result.reduction.acceptedShrinks) + assertNotNull(result.reduction.reducedEncodedBytes) + assertEquals("fast-check", result.backendId) + assertEquals("4.9.0", result.backendVersion) + } + + @Test + fun `a different named failed check cannot replace the original check`() { + val property = property(predicate = "namedChecks").copy( + assertions = listOf(PropertyAssertion(id = "threshold-check", source = sourcePoint)), + ) + val target = WitnessTarget( + id = "threshold-check", + binding = binding(pointId = "threshold-check"), + ) + + val result = backend.confirmWitness( + property = property, + candidate = candidate(property = property, target = target), + configuration = configuration, + ) + + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, result.status) + assertEquals(listOf(JsConcreteValue.number(15.0)), result.reduction.inputs) + assertTrue(assertNotNull(result.reducedReplay).targetMatched) + } + + @Test + fun `guarded hypothesis refutation holds the original oracle and reduces the same contextual target`() { + val property = property(predicate = "hypothesis") + val target = hypothesisTarget + + val result = backend.confirmWitness( + property = property, + candidate = candidate(property = property, target = target), + configuration = configuration, + ) + + assertEquals(WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, result.status) + assertEquals(WitnessOracleOutcome.HOLDS, result.originalReplay?.outcome) + assertEquals(WitnessOracleOutcome.HOLDS, result.reducedReplay?.outcome) + assertEquals(listOf(JsConcreteValue.number(5.0)), result.reduction.inputs) + assertEquals(1, result.contextualRefutations.size) + assertEquals(target.binding, result.contextualRefutations.single().binding) + } + + @Test + fun `wrong context revision occurrence and inactive guard do not confirm hypotheses`() { + val cases = listOf( + MismatchCase(predicate = "differentContext", target = hypothesisTarget, value = 80.0), + MismatchCase( + predicate = "hypothesis", + target = hypothesisTarget.copy(binding = binding(pointId = "hypothesis").copy(revision = "v2")), + value = 80.0, + ), + MismatchCase(predicate = "repeatedHypothesis", target = hypothesisTarget, value = 80.0), + MismatchCase(predicate = "hypothesis", target = hypothesisTarget, value = 0.0), + ) + + for ((predicate, target, value) in cases) { + val property = property(predicate = predicate) + val result = backend.confirmWitness( + property = property, + candidate = candidate( + property = property, + target = target, + inputs = listOf(JsConcreteValue.number(value)) + ), + configuration = configuration, + ) + + assertEquals(WitnessReplayStatus.TARGET_MISMATCH, result.status) + assertTrue(result.contextualRefutations.isEmpty()) + assertTrue(result.confirmedEdgeAdditions.isEmpty()) + assertEquals(WitnessReductionStatus.NOT_ELIGIBLE, result.reduction.status) + } + } + + @Test + fun `passing rejected unrepresentable and erroneous candidates are not faults`() { + val property = property(predicate = "threshold") + val base = candidate(property = property) + val cases = listOf( + base.copy(inputs = listOf(JsConcreteValue.number(1.0))) to WitnessReplayStatus.PROPERTY_HOLDS, + base.copy(inputs = listOf(JsConcreteValue.number(101.0))) to WitnessReplayStatus.DOMAIN_REJECTED, + base.copy(inputs = null) to WitnessReplayStatus.UNREPRESENTABLE_INPUT, + base.copy(inputs = listOf(JsConcreteValue.String("wrong"))) to WitnessReplayStatus.DOMAIN_REJECTED, + ) + for ((candidate, status) in cases) { + val result = backend.confirmWitness( + property = property, + candidate = candidate, + configuration = configuration + ) + + assertEquals(status, result.status) + assertEquals(candidate, result.candidate) + assertNull(result.reduction.inputs) + assertTrue(result.confirmedEdgeAdditions.isEmpty()) + } + for ((precondition, status) in listOf( + "rejected" to WitnessReplayStatus.PRECONDITION_REJECTED, + "preconditionError" to WitnessReplayStatus.PROPERTY_ERROR, + )) { + val guarded = property.copy(precondition = TypeScriptEntryPoint(module = MODULE, exportName = precondition)) + val result = backend.confirmWitness( + property = guarded, + candidate = candidate(property = guarded), + configuration = configuration, + ) + + assertEquals(status, result.status) + } + } + + @Test + fun `predicate exception is a fault and nonboolean result is an error`() { + for ((predicate, status) in listOf( + "predicateError" to WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, + "contractError" to WitnessReplayStatus.PROPERTY_ERROR, + "nondeterministic" to WitnessReplayStatus.NONDETERMINISTIC, + )) { + val property = property(predicate = predicate) + val result = backend.confirmWitness( + property = property, + candidate = candidate(property = property), + configuration = configuration.copy(shrink = false), + ) + + assertEquals(status, result.status) + } + } + + @Test + fun `source and generator registration drift invalidate replay`() { + val property = property(predicate = "threshold") + val base = candidate(property = property) + val changedSource = base.copy( + sources = listOf(PropertyObservationSource(module = MODULE, sha256 = "0".repeat(64))) + ) + val changedProperty = property.copy( + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(max = 200))) + ) + + val sourceResult = backend.confirmWitness( + property = property, + candidate = changedSource, + configuration = configuration + ) + val registrationResult = backend.confirmWitness( + property = changedProperty, + candidate = base, + configuration = configuration + ) + + assertEquals(WitnessReplayStatus.SOURCE_MISMATCH, sourceResult.status) + assertEquals(WitnessReplayStatus.SOURCE_MISMATCH, registrationResult.status) + assertEquals(changedSource, sourceResult.candidate) + assertNull(sourceResult.reduction.inputs) + } + + @Test + fun `precondition admission is rechecked while shrinking`() { + val property = property(predicate = "threshold").copy( + precondition = TypeScriptEntryPoint(module = MODULE, exportName = "admitted"), + ) + + val result = backend.confirmWitness( + property = property, + candidate = candidate(property = property), + configuration = configuration + ) + + assertEquals(listOf(JsConcreteValue.number(20.0)), result.reduction.inputs) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, result.status) + } + + @Test + fun `mutating predicate inputs are isolated during replay and reduction`() { + val property = + property(predicate = "mutation", domains = listOf(ArrayDomain(element = IntegerDomain(min = 0, max = 100)))) + val inputs = + listOf(JsConcreteValue.Array(elements = listOf(80.0, 90.0, 100.0, 70.0).map(JsConcreteValue::number))) + + val result = backend.confirmWitness( + property = property, + candidate = candidate(property = property, inputs = inputs), + configuration = configuration, + ) + + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, result.status) + assertEquals(inputs, result.candidate.inputs) + assertEquals( + listOf(JsConcreteValue.Array(elements = List(3) { JsConcreteValue.number(0.0) })), + result.reduction.inputs + ) + } + + @Test + fun `special values and argument order survive native witness replay`() { + val inputs = listOf( + JsConcreteValue.number(-0.0), + JsConcreteValue.number(Double.NaN), + JsConcreteValue.String("\uD800"), + JsConcreteValue.Undefined, + JsConcreteValue.number(Double.POSITIVE_INFINITY), + ) + val property = + property(predicate = "specialValues", domains = inputs.map { value -> ConstantDomain(value = value) }) + + val result = backend.confirmWitness( + property = property, + candidate = candidate(property = property, inputs = inputs), + configuration = configuration, + ) + + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, result.status) + assertEquals(inputs, result.candidate.inputs) + assertEquals(inputs, result.reduction.inputs) + assertEquals(0, result.reduction.acceptedShrinks) + } + + @Test + fun `contextless dependent generator retains original confirmed witness`() { + val property = property( + predicate = "supportedIndex", + domains = listOf( + ArrayDomain(element = IntegerDomain(min = 0, max = 100), minLength = 1, maxLength = 3), + IntegerDomain(min = 0, max = 2), + ), + ).copy(generator = ArrayIndexGenerator(id = "index", arrayInputIndex = 0, indexInputIndex = 1)) + val inputs = listOf( + JsConcreteValue.Array(elements = listOf(JsConcreteValue.number(80.0), JsConcreteValue.number(90.0))), + JsConcreteValue.number(1.0), + ) + + val result = backend.confirmWitness( + property = property, + candidate = candidate(property = property, inputs = inputs), + configuration = configuration, + ) + + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, result.status) + assertEquals(WitnessReductionStatus.UNSUPPORTED, result.reduction.status) + assertEquals(inputs, result.candidate.inputs) + assertNull(result.reduction.inputs) + } + + @Test + fun `supervised reduction timeout retains original fault and shared expired deadline retains candidate`() { + val property = property(predicate = "slowShrink") + val candidate = candidate(property = property) + + val result = backend.confirmWitness( + property = property, + candidate = candidate, + configuration = configuration.copy(timeoutMillis = 3_000, validationReserveMillis = 2_000), + ) + val expired = WitnessReplayDeadline(timeoutMillis = 1) + Thread.sleep(5) + val timedOut = backend.confirmWitness( + property = property, + candidate = candidate, + configuration = configuration, + deadline = expired + ) + + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, result.status) + assertEquals(WitnessReductionStatus.TIMEOUT, result.reduction.status) + assertEquals(candidate, result.candidate) + assertNull(result.reduction.inputs) + assertEquals(WitnessReplayStatus.TIMEOUT, timedOut.status) + assertEquals(candidate, timedOut.candidate) + } + + @Test + fun `reducer error and failed fresh final replay preserve original confirmed inputs`() { + for (predicate in listOf("shrinkError", "requiresInitial")) { + val property = property(predicate = predicate) + val candidate = candidate(property = property) + + val result = backend.confirmWitness( + property = property, + candidate = candidate, + configuration = configuration, + ) + + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, result.status) + assertEquals(candidate, result.candidate) + assertEquals(WitnessReductionStatus.FAILED, result.reduction.status) + assertNull(result.reduction.inputs) + assertNull(result.reducedReplay) + } + } + + @Test + fun `symbolic false target is not confirmed by a different native exception`() { + val property = property(predicate = "predicateError") + val candidate = candidate( + property = property, + target = WitnessTarget(id = "predicateError", expectedOutcome = WitnessOracleOutcome.FALSE), + ) + + val result = backend.confirmWitness(property = property, candidate = candidate, configuration = configuration) + + assertEquals(WitnessReplayStatus.TARGET_MISMATCH, result.status) + assertEquals(WitnessOracleOutcome.THREW, result.originalReplay?.outcome) + assertEquals(WitnessReductionStatus.NOT_ELIGIBLE, result.reduction.status) + } + + @Test + fun `coverage witness contributes only confirmed exact edges and removes known additions`() { + val module = "properties/witness/CoverageWitness.ts" + val property = property( + predicate = "coverage" + ).copy(predicate = TypeScriptEntryPoint(module = module, exportName = "coverage")) + val candidate = candidate( + property = property, + target = WitnessTarget( + id = "positive-edge", + role = WitnessRole.COVERAGE, + binding = binding(pointId = "positive-edge") + ), + ) + val withCoverage = configuration.copy( + shrink = false, + coverageRequest = PropertyCoverageRequest(scopes = setOf(CoverageScope.PROPERTY_ENTRY_POINTS)), + ) + + val result = backend.confirmWitness(property = property, candidate = candidate, configuration = withCoverage) + val repeated = backend.confirmWitness( + property = property, + candidate = candidate, + configuration = withCoverage.copy(knownEdges = result.confirmedEdgeAdditions), + ) + + assertEquals(WitnessReplayStatus.CONFIRMED_COVERAGE, result.status) + assertEquals(WitnessOracleOutcome.HOLDS, result.originalReplay?.outcome) + assertEquals(1, result.confirmedEdgeAdditions.size, result.originalReplay?.coverage.toString()) + assertTrue(result.confirmedEdgeAdditions.single().outcome) + assertTrue(repeated.confirmedEdgeAdditions.isEmpty()) + } + + private fun property( + predicate: String, + domains: List = listOf(IntegerDomain(min = 0, max = 100)), + ) = PropertyDefinition( + id = PropertyId(value = "witness.$predicate"), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = predicate), + inputs = domains.mapIndexed { index, domain -> PropertyInput(name = "value$index", domain = domain) }, + ) + + private fun candidate( + property: PropertyDefinition, + target: WitnessTarget = WitnessTarget(id = property.predicate.exportName), + inputs: List? = listOf(JsConcreteValue.number(80.0)), + ) = property.captureWitness( + inputs = inputs, + target = target, + sources = listOf(source(module = property.predicate.module)), + provenance = "symbolic-fixture", + ) + + private fun source(module: String): PropertyObservationSource { + val bytes = Files.readAllBytes(root.resolve(module)) + val hash = MessageDigest.getInstance("SHA-256").digest(bytes).joinToString(separator = "") { byte -> + "%02x".format(byte.toInt() and 0xff) + } + return PropertyObservationSource(module = module, sha256 = hash) + } + + private fun binding(pointId: String) = WitnessBinding(pointId = pointId, contextId = "original", revision = "v1") + + private val hypothesisTarget = + WitnessTarget(id = "hypothesis", role = WitnessRole.HYPOTHESIS, binding = binding(pointId = "hypothesis")) + private val sourcePoint = PropertySourcePoint(module = MODULE, line = 1, column = 1) + + private data class MismatchCase( + val predicate: String, + val target: WitnessTarget, + val value: Double, + ) + + private companion object { + const val MODULE = "properties/witness/ExternalWitness.ts" + } +} diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt index 17978ced59..87ca3ca702 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt @@ -10,6 +10,10 @@ import org.usvm.ts.pbt.backend.ProjectionLevel import org.usvm.ts.pbt.backend.PropertyFailureKind import org.usvm.ts.pbt.backend.PropertyRunConfiguration import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.backend.WitnessOracleOutcome +import org.usvm.ts.pbt.backend.WitnessReplayConfiguration +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.backend.captureWitness import org.usvm.ts.pbt.fastcheck.BackendErrorKind import org.usvm.ts.pbt.fastcheck.FastCheckBackend import org.usvm.ts.pbt.fastcheck.PbtBackendException @@ -24,13 +28,46 @@ import org.usvm.ts.pbt.model.PropertyId import org.usvm.ts.pbt.model.PropertyInput import org.usvm.ts.pbt.model.TypeScriptEntryPoint import org.usvm.ts.pbt.model.contains +import org.usvm.ts.pbt.observation.PropertyObservationSource import org.usvm.ts.pbt.testResourcePath import org.usvm.ts.pbt.testResourcesRoot +import java.nio.file.Files +import java.security.MessageDigest import kotlin.test.assertEquals import kotlin.test.assertNotNull import kotlin.test.assertTrue class PropertyExecutionConformanceTest { + @Test + fun `resolved USVM candidate requires original oracle replay before becoming a fault`() { + val property = property(predicateExport = "falsePredicate") + val manifest = property.toManifest() + val symbolic = searcher.search( + manifest = manifest, + mapping = mapper.map(manifest), + concreteCapability = exactCapability, + ) + val bytes = Files.readAllBytes(fixtureDirectory.resolve(MODULE)) + val hash = MessageDigest.getInstance("SHA-256").digest(bytes).joinToString(separator = "") { byte -> + "%02x".format(byte.toInt() and 0xff) + } + val candidate = symbolic.captureWitness( + property = property, + sources = listOf(PropertyObservationSource(module = MODULE, sha256 = hash)), + ) + + val confirmed = backend.confirmWitness( + property = property, + candidate = candidate, + configuration = WitnessReplayConfiguration(timeoutMillis = 10_000), + ) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, symbolic.status) + assertEquals(symbolic.inputs, confirmed.candidate.inputs) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, confirmed.status) + assertEquals(WitnessOracleOutcome.FALSE, confirmed.reducedReplay?.outcome) + } + @Test fun `shared preconditions have the same concrete and search classification`() { val cases = listOf( diff --git a/usvm-ts-fast-check/src/test/resources/properties/witness/CoverageWitness.ts b/usvm-ts-fast-check/src/test/resources/properties/witness/CoverageWitness.ts new file mode 100644 index 0000000000..00489ba1cb --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/witness/CoverageWitness.ts @@ -0,0 +1,11 @@ +export function coverage(value: number): boolean { + const hook = (globalThis as Record)[Symbol.for('org.usvm.ts.pbt.witness')] as + ((point: string, context: string, revision: string, guard: boolean, holds: boolean) => boolean) | undefined; + + if (value >= 10) { + hook?.('positive-edge', 'original', 'v1', true, true); + return true; + } else { + return true; + } +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/witness/ExternalWitness.ts b/usvm-ts-fast-check/src/test/resources/properties/witness/ExternalWitness.ts new file mode 100644 index 0000000000..ed7360659b --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/witness/ExternalWitness.ts @@ -0,0 +1,80 @@ +type WitnessHook = (point: string, context: string, revision: string, guard: boolean, holds: boolean) => boolean; + +function observed(point: string, holds: boolean, guard = true, context = 'original'): boolean { + const hook = (globalThis as Record)[Symbol.for('org.usvm.ts.pbt.witness')] as WitnessHook | undefined; + return hook?.(point, context, 'v1', guard, holds) ?? holds; +} + +export function threshold(value: number): boolean { + return value < 10; +} + +export function namedChecks(value: number): boolean { + if (value < 10) { + return observed('other-check', false); + } + + return observed('threshold-check', value < 15); +} + +export function hypothesis(value: number): boolean { + observed('hypothesis', value < 5, value > 0); + return true; +} + +export function repeatedHypothesis(value: number): boolean { + observed('hypothesis', true); + observed('hypothesis', value < 5); + return true; +} + +export function differentContext(value: number): boolean { + observed('hypothesis', value < 5, true, 'different'); + return true; +} + +export function rejected(): boolean { return false; } +export function admitted(value: number): boolean { return value >= 20; } +export function preconditionError(): boolean { throw new Error('precondition'); } +export function predicateError(): boolean { throw new TypeError('original predicate'); } +export function contractError(): number { return 42; } +export function hangs(): boolean { while (true) { /* supervised timeout */ } } + +let flipped = false; +export function nondeterministic(): boolean { flipped = !flipped; return flipped; } + +export function mutation(values: number[]): boolean { + const originalLength = values.length; + values.pop(); + return originalLength < 3; +} + +export function specialValues(zero: number, nan: number, text: string, nil: undefined, infinity: number): boolean { + return !(Object.is(zero, -0) && Number.isNaN(nan) && text === '\ud800' && nil === undefined && infinity === Infinity); +} + +export function slowShrink(value: number): boolean { + if (value !== 80) { + while (true) { /* original still replayable; reduction is supervised */ } + } + + return false; +} + +export function supportedIndex(values: number[], index: number): boolean { + return values[index] < 10; +} + +export function shrinkError(value: number): boolean { + return value === 80 ? false : 42 as unknown as boolean; +} + +let initialSeen = false; +export function requiresInitial(value: number): boolean { + if (value === 80) { + initialSeen = true; + return false; + } + + return !initialSeen || value < 10; +} diff --git a/usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md b/usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md new file mode 100644 index 0000000000..103afe144e --- /dev/null +++ b/usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md @@ -0,0 +1,129 @@ +# External witness replay and reduction + +`ExternalWitnessBackend.confirmWitness` consumes an extracted input, executes the complete registered original +TypeScript precondition and predicate, and returns a serializable `WitnessEvidenceDelta`. It does not replace the +original oracle with an internal helper or a challenge predicate. `FastCheckBackend` implements this API using +its existing tagged codecs, invocation isolation, process supervisor, and source coverage collector. + +## Direct symbolic candidates + +```kotlin +val deadline = WitnessReplayDeadline(timeoutMillis = 30_000) +val symbolic = searcher.search( + manifest = property.toManifest(), + mapping = mapping, + concreteCapability = concreteCapability, +) +val candidate = symbolic.captureWitness( + property = property, + sources = selectedSourceHashes, +) +val evidence = backend.confirmWitness( + property = property, + candidate = candidate, + configuration = WitnessReplayConfiguration( + timeoutMillis = 30_000, + validationReserveMillis = 5_000, + ), + deadline = deadline, +) +val artifactJson = PropertyManifestJson.json.encodeToUtf8SafeString(evidence) +``` + +Capture requires a reached symbolic target; failed extraction produces an unrepresentable candidate. The original +candidate, reached target classification in provenance, complete manifest, manifest fingerprint, selected source +hashes, and ordered inputs remain in the artifact. A false symbolic target cannot be confirmed by a native +exception. The artifact also records original/final native outcomes, Node and FastCheck versions, adapter protocol, +accepted shrink steps, attempt counts, and encoded input sizes. Reproduction requires the same registration, +selected source files, source roots, and backend revision; it uses the saved inputs, not an arbitrary FastCheck +seed/path token. + +The manifest fingerprint covers input order, domains, declared joint generator, original precondition/predicate, +assertions, and registered source/build identity. Every original callback module must have a selected SHA-256 +source hash. Selected files are verified before import in every process. Hashes attest those files' exact bytes; +they do not attest unlisted transitive imports, package dependencies, or the registrant's build hash. Producers +must include all relevant local source/context revisions in the selected files and pin external dependencies in +their reproduction environment. + +## Named checks and guarded auxiliary targets + +For a registration without named assertions, an unbound property target identifies the original predicate export +as a single boolean/exception check. Registered named assertions cannot fall back to an unnamed predicate target. A named +check must be registered in `PropertyDefinition.assertions` and have an exact executable `WitnessBinding` whose +`pointId` equals that check ID. Auxiliary coverage/hypothesis targets always require a binding. A missing, +different, inactive, or differently numbered event cannot confirm that target. + +The original callback emits a passive event after evaluating the original guard and relation. For example: + +```typescript +type WitnessHook = ( + pointId: string, contextId: string, revision: string, guard: boolean, holds: boolean, +) => boolean; + +function recordRelation(guard: boolean, holds: boolean): boolean { + const hook = (globalThis as Record)[Symbol.for('org.usvm.ts.pbt.witness')] as + WitnessHook | undefined; + + return hook?.('result-bounded', 'public-entry/call-1/post', 'binding-v1', guard, holds) ?? holds; +} +``` + +Only events during the admitted original predicate count. Each invocation captures at most 256 events. Bindings +match point ID, context ID, binding revision, and zero-based occurrence exactly. Guard false is not refutation. +For a named original check, the complete oracle must also fail. A hypothesis-only refutation requires the complete +oracle to hold, and returns `CONFIRMED_HYPOTHESIS_REFUTATION`, not a property defect. If both the original oracle +and a matched hypothesis fail, the result retains the original violation and the contextual refutation separately. + +This is a concrete consumer contract for explicit executable bindings. It does not establish those bindings by +source-line coincidence, infer hypotheses, or generate EtsIR challenges. Automatic observation/hypothesis binding +and the accepted producer-to-replay integration remain the responsibility of #398. Manual runtime fixtures here +do not complete that issue or the full coupled hypothesis acceptance of #353/#405. + +## Reduction and failures + +Admission checks declared domains and joint support independently of shrinking capability, then executes the +original precondition. False preconditions reject; exceptions and nonboolean results are errors. Predicate false +and escaping predicate exceptions are original violations. Tagged special values, positional order, and the +existing isolated input-graph invocation contract apply to every attempt. The wire codec accepts value trees and +does not reconstruct aliases or cycles across separately encoded nodes. + +Replay repeats the original input within a process and in fresh supervised processes. Observed admission/outcome, +event, or failure changes report `NONDETERMINISTIC`. These finite checks do not prove universal determinism or +support persistent external/module state. + +For an eligible witness, FastCheck's arbitrary must accept `canShrinkWithoutContext`. An adapter replaces only +initial generation with the external input and delegates the complete shrink stream and subsequent contexts to +the original arbitrary. Dependent generators that require unavailable native context report `UNSUPPORTED`; no +general custom shrinker is substituted. #400/#402 own generator-choice/command extensions. + +The reduction predicate retains declared support, original precondition admission, the same named check or +guarded auxiliary binding, and the original oracle outcome/exception category. It repeats each attempted input. +After reduction, fresh processes recheck the complete original oracle and target again. Errors, drift, mismatches, +unsupported shrinking and timeouts preserve the original candidate and its confirmed outcome. Unvalidated partial +reductions are never published as final inputs. + +`EXHAUSTED` reports backend stream completion, not global minimality. Explicit examples, zero accepted shrinks, or +an unchanged encoded byte size are not minimality proofs. Counts measure attempts and accepted backend shrink +steps; byte sizes measure serialization size, not numeric magnitude. + +Replay, runtime probes, coverage conversion, and reduction consume the supplied monotonic deadline. Reduction +reserves final-validation time; synchronous/asynchronous hangs are stopped by the existing process supervisor. +Process teardown can take the supervisor's bounded shutdown grace after the execution budget expires. No fresh +full timeout is granted to the final replay. + +## Scheduler evidence + +The evidence delta contains the original admission/outcome and explicit terminal status even for unconfirmed +candidates. Only repeatable, admitted, target-matched native replay may contribute `confirmedEdgeAdditions` or +`contextualRefutations`. Rejected, mismatched, failed, unsupported and timed-out replay leaves goals intact. +Passing coverage/hypothesis evidence remains separate from original-property defects. + +Coverage replays use only the original candidate; shrink trials are not aggregated into its coverage. Edge +additions come from the existing exact native two-arm TypeScript `if` collector, carry source hashes and condition +ranges, exclude sources with collection diagnostics, and subtract the caller's already confirmed edges. This is +source coverage evidence, not automatic EtsIR edge mapping or a completed #481/#355 scheduler. + +Runtime tests in `ExternalWitnessTest`, `external-witness.test.ts`, and `PropertyExecutionConformanceTest` cover +actual external shrinking, named-check preservation, hypothesis-only evidence, context/guard mismatches, source +and registration drift, mutation isolation, special values, errors/timeouts, fresh final validation, source coverage, +and a resolved real USVM candidate passed to the original native oracle. diff --git a/usvm-ts-pbt/README.md b/usvm-ts-pbt/README.md index f8585fc773..bab278b2bd 100644 --- a/usvm-ts-pbt/README.md +++ b/usvm-ts-pbt/README.md @@ -147,6 +147,10 @@ throw `PbtBackendException`. Generation, replay, explicit examples, checking, and shrinking use the same invocation path and follow the [property execution contract](PROPERTY_EXECUTION_CONTRACT.md). +External symbolic candidates use `ExternalWitnessBackend.confirmWitness` to confirm the original oracle and +reduce the same target through native FastCheck shrinking. See the [external witness contract](EXTERNAL_WITNESS_REPLAY.md) +for admission/classification, guarded executable bindings, scheduler evidence, reproduction, and remaining #398 integration. + ## Per-property TypeScript coverage Coverage is a backend capability, not part of `PropertyDefinition` or `PropertyManifest`. diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt new file mode 100644 index 0000000000..8600ed1326 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt @@ -0,0 +1,186 @@ +package org.usvm.ts.pbt.backend + +import kotlinx.serialization.Serializable +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.observation.PropertyObservationSource + +/** Auxiliary witnesses are useful evidence even when the complete original oracle holds. */ +@Serializable +enum class WitnessRole { PROPERTY, COVERAGE, HYPOTHESIS } + +/** Exact executable hook binding supplied by a producer, never inferred from a source line. */ +@Serializable +data class WitnessBinding( + val pointId: String, + val contextId: String, + val revision: String, + val occurrence: Int = 0, +) { + init { + require(pointId.isNotBlank() && contextId.isNotBlank() && revision.isNotBlank()) + require(occurrence >= 0) + } +} + +/** An original named check or a guarded auxiliary target within the complete original predicate. */ +@Serializable +data class WitnessTarget( + val id: String, + val role: WitnessRole = WitnessRole.PROPERTY, + val binding: WitnessBinding? = null, + val expectedOutcome: WitnessOracleOutcome? = null, +) { + init { + require(id.isNotBlank()) + require(role == WitnessRole.PROPERTY || binding != null) + require( + expectedOutcome == null || expectedOutcome == WitnessOracleOutcome.FALSE || + expectedOutcome == WitnessOracleOutcome.THREW + ) + } +} + +/** Unconfirmed input and the exact registration/source revisions used to extract it. */ +@Serializable +data class ExternalWitnessCandidate( + val propertyId: PropertyId, + val target: WitnessTarget, + val inputs: List?, + val manifestSha256: String, + val manifest: PropertyManifest, + val sources: List, + val provenance: String, +) + +/** Concrete admission is separate from the original property outcome. */ +@Serializable +enum class WitnessAdmission { ADMITTED, DOMAIN_REJECTED, PRECONDITION_REJECTED, ERROR, UNKNOWN } + +/** Completion of the complete original predicate, including escaping assertion exceptions. */ +@Serializable +enum class WitnessOracleOutcome { HOLDS, FALSE, THREW, SKIPPED, ERROR, UNKNOWN } + +/** One guarded event produced during this original predicate invocation. */ +@Serializable +data class WitnessEvent( + val binding: WitnessBinding, + val guard: Boolean, + val holds: Boolean, +) + +/** A replay result is not a final fault until the coordinator confirms repeatability and target identity. */ +@Serializable +data class WitnessNativeReplay( + val admission: WitnessAdmission, + val outcome: WitnessOracleOutcome, + val targetMatched: Boolean, + val events: List = emptyList(), + val failure: PropertyFailureDetails? = null, + val diagnostic: String? = null, + val coverage: PropertyCoverageArtifact? = null, + val runtimeVersion: String? = null, +) + +/** Scheduler-visible classification; only confirmed original violations count as faults. */ +@Serializable +enum class WitnessReplayStatus { + CONFIRMED_PROPERTY_VIOLATION, + CONFIRMED_HYPOTHESIS_REFUTATION, + CONFIRMED_COVERAGE, + PROPERTY_HOLDS, + TARGET_MISMATCH, + DOMAIN_REJECTED, + PRECONDITION_REJECTED, + UNREPRESENTABLE_INPUT, + UNSUPPORTED_REPLAY, + SOURCE_MISMATCH, + NONDETERMINISTIC, + PROPERTY_ERROR, + REPLAY_ERROR, + TIMEOUT, +} + +/** Reduction failure never invalidates or replaces the original confirmed witness. */ +@Serializable +enum class WitnessReductionStatus { NOT_ELIGIBLE, DISABLED, UNSUPPORTED, EXHAUSTED, FAILED, TIMEOUT } + +/** EXHAUSTED means the backend stream was exhausted, not a global minimality proof. */ +@Serializable +data class WitnessReduction( + val status: WitnessReductionStatus, + val inputs: List? = null, + val attempts: Int = 0, + val acceptedShrinks: Int = 0, + val originalEncodedBytes: Int = 0, + val reducedEncodedBytes: Int? = null, + val diagnostic: String? = null, +) + +/** Source-qualified edge identity; only the exact native two-arm branch collector may produce it. */ +@Serializable +data class WitnessCoverageEdge( + val source: PropertyObservationSource, + val location: SourceRange, + val outcome: Boolean, +) + +/** Immutable evidence delta for the shared scheduler. Rejected replay never removes a coverage goal. */ +@Serializable +data class WitnessEvidenceDelta( + val candidate: ExternalWitnessCandidate, + val status: WitnessReplayStatus, + val originalReplay: WitnessNativeReplay? = null, + val reducedReplay: WitnessNativeReplay? = null, + val reduction: WitnessReduction = WitnessReduction(status = WitnessReductionStatus.NOT_ELIGIBLE), + val confirmedEdgeAdditions: Set = emptySet(), + val contextualRefutations: List = emptyList(), + val backendId: String, + val backendVersion: String, + val adapterProtocol: String = "external-witness-v1", + val diagnostic: String? = null, +) + +/** Backend-neutral external-candidate entry point; it does not launch a new symbolic search. */ +interface ExternalWitnessBackend { + fun confirmWitness( + property: org.usvm.ts.pbt.model.PropertyDefinition, + candidate: ExternalWitnessCandidate, + configuration: WitnessReplayConfiguration = WitnessReplayConfiguration(), + deadline: WitnessReplayDeadline = WitnessReplayDeadline(configuration.timeoutMillis), + ): WitnessEvidenceDelta +} + +/** Execution controls and the caller's already confirmed source-qualified edges. */ +data class WitnessReplayConfiguration( + val timeoutMillis: Long = 60_000L, + val validationReserveMillis: Long = 5_000L, + val shrink: Boolean = true, + val coverageRequest: PropertyCoverageRequest? = null, + val knownEdges: Set = emptySet(), +) { + init { + require(timeoutMillis in 1..PropertyRunConfiguration.MAX_TIMEOUT_MILLIS) + require(validationReserveMillis > 0) + } +} + +/** A monotonic budget that callers may create before search and share with replay/reduction. */ +class WitnessReplayDeadline(timeoutMillis: Long) { + private val startedAt = System.nanoTime() + private val budgetNanos = timeoutMillis * NANOS_PER_MILLISECOND + + init { + require(timeoutMillis in 1..PropertyRunConfiguration.MAX_TIMEOUT_MILLIS) + } + + fun remainingMillis(): Long { + val elapsedNanos = System.nanoTime() - startedAt + return ((budgetNanos - elapsedNanos) / NANOS_PER_MILLISECOND).coerceAtLeast(0) + } + + private companion object { + const val NANOS_PER_MILLISECOND = 1_000_000L + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/WitnessCandidateCapture.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/WitnessCandidateCapture.kt new file mode 100644 index 0000000000..fe7015326f --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/WitnessCandidateCapture.kt @@ -0,0 +1,60 @@ +package org.usvm.ts.pbt.backend + +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.encodeToUtf8SafeString +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.usvm.UsvmPropertySearchResult +import org.usvm.ts.pbt.usvm.UsvmPropertyViolationTarget +import java.security.MessageDigest + +/** Pins the complete registration, including ordered domains, generator, precondition, and original oracle. */ +fun PropertyDefinition.witnessManifestSha256(): String { + val bytes = PropertyManifestJson.json.encodeToUtf8SafeString(toManifest()).toByteArray(Charsets.UTF_8) + return MessageDigest.getInstance("SHA-256").digest(bytes).joinToString(separator = "") { byte -> + "%02x".format(byte.toInt() and BYTE_MASK) + } +} + +private const val BYTE_MASK = 0xff + +fun PropertyDefinition.captureWitness( + inputs: List?, + target: WitnessTarget, + sources: List, + provenance: String, +): ExternalWitnessCandidate = ExternalWitnessCandidate( + propertyId = id, + target = target, + inputs = inputs, + manifestSha256 = witnessManifestSha256(), + manifest = toManifest(), + sources = sources, + provenance = provenance, +) + +/** Failed extraction remains an unrepresentable candidate; symbolic reach alone never becomes a fault. */ +fun UsvmPropertySearchResult.captureWitness( + property: PropertyDefinition, + sources: List, +): ExternalWitnessCandidate { + require(propertyId == property.id) + requireNotNull(target) { "Capture requires a reached symbolic target" } + + return property.captureWitness( + inputs = inputs, + target = WitnessTarget( + id = property.predicate.exportName, + expectedOutcome = when (target) { + UsvmPropertyViolationTarget.PREDICATE_FALSE -> WitnessOracleOutcome.FALSE + UsvmPropertyViolationTarget.UNEXPECTED_EXCEPTION, + UsvmPropertyViolationTarget.ASSERTION_FAILURE, + -> WitnessOracleOutcome.THREW + }, + ), + sources = sources, + provenance = "usvm:$status:$target", + ) +} From e478aa87d11338304b268df14f1b864821897b71 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 23:13:46 +0300 Subject: [PATCH 2/4] [TS PBT] Return explicit outcomes for witness replay --- .../fast-check-adapter/src/diagnostics.ts | 1 + .../fast-check-adapter/src/entry-point.ts | 17 +- .../src/external-witness.ts | 60 +++++-- .../test/external-witness.test.ts | 35 +++- .../usvm/ts/pbt/FastCheckDiagnosticCode.kt | 1 + .../pbt/fastcheck/FastCheckCoverageSession.kt | 161 +++++++++++++----- .../pbt/fastcheck/FastCheckOperationResult.kt | 8 + .../pbt/fastcheck/FastCheckProcessClient.kt | 63 +++++-- .../fastcheck/FastCheckProcessTransport.kt | 89 +++++++--- .../fastcheck/FastCheckWitnessCoordinator.kt | 160 +++++++++++------ .../ts/pbt/fastcheck/WitnessInputEncoding.kt | 43 +++++ .../ts/pbt/fastcheck/ExternalWitnessTest.kt | 31 ++++ .../fastcheck/FastCheckWitnessTimeoutTest.kt | 145 ++++++++++++++++ .../properties/witness/ExternalWitness.ts | 13 ++ usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md | 3 + 15 files changed, 675 insertions(+), 155 deletions(-) create mode 100644 usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckOperationResult.kt create mode 100644 usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/WitnessInputEncoding.kt create mode 100644 usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessTimeoutTest.kt diff --git a/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts b/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts index fba52cc37a..c8b9a77d0f 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts +++ b/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'), diff --git a/usvm-ts-fast-check/fast-check-adapter/src/entry-point.ts b/usvm-ts-fast-check/fast-check-adapter/src/entry-point.ts index 1f02c51f6c..82a9319a5e 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/entry-point.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/entry-point.ts @@ -143,9 +143,8 @@ export async function verifySourceHash( expectedSha256: string, sourceRoots: string[], ): Promise { - 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 { + 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[], diff --git a/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts b/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts index 4c153b5fec..121d979f6e 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts @@ -2,7 +2,7 @@ import { AsyncLocalStorage } from 'node:async_hooks'; import { performance } from 'node:perf_hooks'; import fc from 'fast-check'; import { adapterDiagnostic } from './diagnostics.js'; -import { EntryPointInvocationError, loadEntryPoint, verifySourceHash, type LoadedEntryPoint } from './entry-point.js'; +import { EntryPointInvocationError, loadEntryPoint, sourceHashMatches, type LoadedEntryPoint } from './entry-point.js'; import { describePropertyFailure, invokePropertyOnce, 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'; @@ -30,8 +30,8 @@ export interface WitnessEvent { } export interface WitnessNativeReplay { - admission: 'ADMITTED' | 'DOMAIN_REJECTED' | 'PRECONDITION_REJECTED' | 'ERROR'; - outcome: 'HOLDS' | 'FALSE' | 'THREW' | 'SKIPPED' | 'ERROR'; + admission: 'ADMITTED' | 'DOMAIN_REJECTED' | 'PRECONDITION_REJECTED' | 'ERROR' | 'UNKNOWN'; + outcome: 'HOLDS' | 'FALSE' | 'THREW' | 'SKIPPED' | 'ERROR' | 'UNKNOWN'; targetMatched: boolean; events: WitnessEvent[]; failure?: FastCheckFailureDetails; @@ -63,7 +63,7 @@ export interface WitnessExecutionSuccess { witnessReduction?: WitnessReduction; } -interface WitnessContext { events: WitnessEvent[]; active: boolean; contractError?: ProtocolError } +interface WitnessContext { events: WitnessEvent[]; active: boolean; contractError?: string } const contexts = new AsyncLocalStorage(); /** A passive hook: evaluate the original guard/relation first; return its boolean without substituting an oracle. */ @@ -76,8 +76,9 @@ export function installWitnessHook(): void { 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) { - context.contractError = protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid or unbounded witness events', 'witness.events'); - throw context.contractError; + context.contractError = adapterDiagnostic.witnessEventsInvalid.code; + + return holds; } const occurrence = context.events.filter((event) => event.binding.pointId === pointId @@ -103,7 +104,20 @@ export async function executeWitness(value: unknown): Promise module !== undefined); @@ -150,19 +164,28 @@ export async function executeWitness(value: unknown): Promise { attempts += 1; try { if (!inWitnessSupport(request.manifest, input)) return true; const first = await replay(input); const second = await replay(input); - if (signature(first) !== signature(second)) throw new Error('Nondeterministic shrinking invocation'); - if (first.outcome === 'ERROR') throw new Error(first.diagnostic ?? 'Original oracle error during reduction'); + const nondeterministic = signature(first) !== signature(second); + if (nondeterministic) { + reductionDiagnostic ??= 'Nondeterministic shrinking invocation'; + + return true; + } + if (first.outcome === 'ERROR') { + reductionDiagnostic ??= first.diagnostic ?? 'Original oracle error during reduction'; + + return true; + } return !sameTarget(first, expected); } catch (error: unknown) { - reductionError ??= error; + reductionDiagnostic ??= describePropertyFailure(error).message; return true; } @@ -175,10 +198,10 @@ export async function executeWitness(value: unknown): Promise= request.timeoutMillis; - if (timedOut || reductionError !== undefined || details.counterexample === null) { + if (timedOut || reductionDiagnostic !== undefined || details.counterexample === null) { return { status: 'ok', ...identity, witnessReduction: { status: timedOut ? 'TIMEOUT' : 'FAILED', attempts, acceptedShrinks: details.numShrinks, - diagnostic: reductionError === undefined ? 'Reduction did not retain the target' : describePropertyFailure(reductionError).message, + diagnostic: reductionDiagnostic ?? 'Reduction did not retain the target', } }; } @@ -224,16 +247,21 @@ async function replayOnce( result.outcome = holds ? 'HOLDS' : 'FALSE'; } } catch (error: unknown) { - if (error instanceof EntryPointInvocationError && context.contractError === undefined) { + if (error instanceof EntryPointInvocationError) { result.outcome = 'THREW'; result.failure = { kind: 'property', ...describePropertyFailure(error.thrownValue) }; } else { result.admission = 'ERROR'; result.outcome = 'ERROR'; - result.diagnostic = context.contractError?.code - ?? (error instanceof ProtocolError ? error.code : describePropertyFailure(error).message); + result.diagnostic = error instanceof ProtocolError ? error.code : describePropertyFailure(error).message; } } + if (context.contractError !== undefined) { + result.admission = 'ERROR'; + result.outcome = 'ERROR'; + result.diagnostic = context.contractError; + } + 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'; diff --git a/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts index da7c9578df..644e2f9019 100644 --- a/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts +++ b/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts @@ -101,8 +101,12 @@ test('source drift and repeated outcome drift are retained explicitly', async () const changed = request('threshold'); changed.witness.sources[0]!.sha256 = '0'.repeat(64); - await assert.rejects(executeWitness(changed), (error) => error instanceof ProtocolError - && error.code === 'entrypoint.source-hash.mismatch'); + const stale = (await executeWitness(changed)).witnessReplay; + + assert.equal(stale?.admission, 'UNKNOWN'); + assert.equal(stale?.outcome, 'UNKNOWN'); + assert.equal(stale?.diagnostic, 'entrypoint.source-hash.mismatch'); + assert.equal(stale?.targetMatched, false); const replay = (await executeWitness(request('nondeterministic'))).witnessReplay; @@ -148,6 +152,33 @@ test('declared domain rejects values independently of shrinking capability', asy } }); +test('shrinking nondeterminism and oracle contract errors return explicit failed reductions', async () => { + const cases = [ + ['nondeterministicShrink', 'Nondeterministic shrinking invocation'], + ['shrinkError', 'entrypoint.result.invalid'], + ] as const; + + for (const [predicate, diagnostic] of cases) { + const base = request(predicate); + const original = (await executeWitness(base)).witnessReplay; + const result = (await executeWitness({ ...base, witness: { ...base.witness, mode: 'reduce', expected: original } })).witnessReduction; + + assert.equal(original?.outcome, 'FALSE'); + assert.equal(result?.status, 'FAILED'); + assert.equal(result?.diagnostic, diagnostic); + assert.equal(result?.inputs, undefined); + } +}); + +test('invalid witness events record an error without interrupting the complete original oracle', async () => { + const result = (await executeWitness(request('eventError'))).witnessReplay; + + assert.equal(result?.outcome, 'ERROR'); + assert.equal(result?.diagnostic, 'witness.events.invalid'); + assert.equal(result?.targetMatched, false); + assert.equal(result?.events.at(-1)?.binding.pointId, 'oracle-completed'); +}); + test('malformed witness operation and wrong symbolic failure kind cannot confirm a target', async () => { for (const witness of [null, [], {}, { ...request('threshold').witness, target: null }]) { await assert.rejects(executeWitness({ ...request('threshold'), witness }), ProtocolError); diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt index f23558924a..c57a625e88 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt @@ -44,4 +44,5 @@ internal object FastCheckDiagnosticCode { const val PROTOCOL_REQUEST_INVALID = "protocol.request.invalid" const val SOURCE_ROOT_INVALID = "source-root.invalid" + const val ENTRY_POINT_SOURCE_HASH_MISMATCH = "entrypoint.source-hash.mismatch" } diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt index 9755636050..a380011f32 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt @@ -62,14 +62,25 @@ internal class FastCheckCoverageSession private constructor( } fun attachTo(result: PropertyRunResult): PropertyRunResult { - return result.copy(coverage = readArtifact()) + check(remainingMillis == null) { "Ordinary property runs require an unbounded coverage session" } + val artifact = readArtifact() + check(artifact is FastCheckOperationResult.Completed) + + return result.copy(coverage = artifact.value) } - fun readArtifact(): PropertyCoverageArtifact { + fun readArtifact(): FastCheckOperationResult { + val remaining = remainingMillis?.invoke() + if (remaining != null && remaining <= 0) { + return FastCheckOperationResult.TimedOut( + message = "External witness deadline expired before reading coverage" + ) + } + val coverageRequest = requireNotNull(request.coverageRequest) val entryPointPaths = propertyEntryPointPaths() - val artifact = try { + return try { val context = IstanbulCoverageContext( backendId = FastCheckBackend.FAST_CHECK_BACKEND_ID, backendVersion = FastCheckRuntimeMetadata.fastCheckVersion, @@ -95,13 +106,22 @@ internal class FastCheckCoverageSession private constructor( ) val branchReport = if (finalArtifact.files.isEmpty()) { - RawBranchReport(files = emptyList(), diagnostics = emptyList()) + FastCheckOperationResult.Completed( + value = RawBranchReport(files = emptyList(), diagnostics = emptyList()) + ) } else { convertBranches() } - appendExactBranches( - artifact = finalArtifact.copy(diagnostics = diagnostics), - report = branchReport, + val branches = when (branchReport) { + is FastCheckOperationResult.Completed -> branchReport.value + is FastCheckOperationResult.TimedOut -> return branchReport + } + + FastCheckOperationResult.Completed( + value = appendExactBranches( + artifact = finalArtifact.copy(diagnostics = diagnostics), + report = branches, + ), ) } catch (error: CoverageArtifactException) { fail( @@ -111,8 +131,6 @@ internal class FastCheckCoverageSession private constructor( cause = error, ) } - - return artifact } private fun propertyEntryPointPaths(): Set { @@ -130,7 +148,14 @@ internal class FastCheckCoverageSession private constructor( return paths } - private fun convertBranches(): RawBranchReport { + private fun convertBranches(): FastCheckOperationResult { + val timeoutMillis = boundedTimeout(BRANCH_CONVERSION_TIMEOUT_MILLIS) + if (timeoutMillis <= 0) { + return FastCheckOperationResult.TimedOut( + message = "External witness deadline expired during coverage collection" + ) + } + val converter = workspace.adapterRoot.resolve("dist/src/coverage-branches.js") val transport = FastCheckProcessTransport( nodeExecutable = nodeExecutable, @@ -139,27 +164,43 @@ internal class FastCheckCoverageSession private constructor( maxStderrBytes = MAX_BRANCH_ERROR_BYTES, shutdownGraceMillis = BRANCH_SHUTDOWN_GRACE_MILLIS, ) - val output = try { - transport.invoke( + val outputResult = try { + transport.invokeWithResult( command = listOf(nodeExecutable, converter.toString(), workspace.rawDirectory.toString()) + request.sourceRoots, request = "", - timeoutMillis = boundedTimeout(BRANCH_CONVERSION_TIMEOUT_MILLIS), - reportedTimeoutMillis = BRANCH_CONVERSION_TIMEOUT_MILLIS, + timeoutMillis = timeoutMillis, + reportedTimeoutMillis = timeoutMillis, description = "TypeScript branch converter", ) } catch (error: FastCheckTransportException) { - return unsupportedBranches("Cannot convert TypeScript branches: ${error.message}") + return FastCheckOperationResult.Completed( + value = unsupportedBranches("Cannot convert TypeScript branches: ${error.message}"), + ) + } + val output = when (outputResult) { + is FastCheckOperationResult.Completed -> { + outputResult.value + } + is FastCheckOperationResult.TimedOut -> { + if (remainingMillis != null) return outputResult + + return FastCheckOperationResult.Completed(value = unsupportedBranches(outputResult.message)) + } } if (output.exitCode != 0) { - return unsupportedBranches("TypeScript branch conversion failed: ${output.stderr.trim()}") + return FastCheckOperationResult.Completed( + value = unsupportedBranches("TypeScript branch conversion failed: ${output.stderr.trim()}"), + ) } - return runCatching { + val report = runCatching { PropertyManifestJson.json.decodeFromString(output.stdout) }.getOrElse { error -> unsupportedBranches("Cannot read TypeScript branch coverage: ${error.message}") } + + return FastCheckOperationResult.Completed(value = report) } private fun appendExactBranches( @@ -201,15 +242,7 @@ internal class FastCheckCoverageSession private constructor( private fun boundedTimeout(limitMillis: Long): Long { val remaining = remainingMillis?.invoke() ?: return limitMillis - if (remaining <= 0) { - throw PbtBackendException( - kind = BackendErrorKind.TIMEOUT, - code = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, - message = "External witness deadline expired during coverage collection", - propertyId = request.manifest.propertyId, - ) - } - return minOf(limitMillis, remaining) + return minOf(limitMillis, remaining.coerceAtLeast(0)) } private fun canonicalizeExistingEntryPoint(candidate: Path): String = @@ -234,9 +267,54 @@ internal class FastCheckCoverageSession private constructor( nodeExecutable: String, adapterEntryPoint: Path, request: FastCheckExecutionRequest, - remainingMillis: (() -> Long)? = null, ): FastCheckCoverageSession { - val runtimeVersion = readSupportedNodeVersion(nodeExecutable, request, remainingMillis) + val version = readSupportedNodeVersion(nodeExecutable, request, timeoutMillis = NODE_VERSION_TIMEOUT_MILLIS) + val runtimeVersion = when (version) { + is FastCheckOperationResult.Completed -> version.value + is FastCheckOperationResult.TimedOut -> failPreparation( + request = request, + code = FastCheckDiagnosticCode.COVERAGE_RUNTIME_VERSION_UNAVAILABLE, + message = version.message, + ) + } + + return createSession(nodeExecutable, adapterEntryPoint, request, runtimeVersion, remainingMillis = null) + } + + fun prepareWithinBudget( + nodeExecutable: String, + adapterEntryPoint: Path, + request: FastCheckExecutionRequest, + remainingMillis: () -> Long, + ): FastCheckOperationResult { + val remaining = remainingMillis() + if (remaining <= 0) { + return FastCheckOperationResult.TimedOut( + message = "External witness deadline expired before the runtime probe" + ) + } + + val version = readSupportedNodeVersion( + nodeExecutable = nodeExecutable, + request = request, + timeoutMillis = minOf(NODE_VERSION_TIMEOUT_MILLIS, remaining), + ) + + return when (version) { + is FastCheckOperationResult.Completed -> FastCheckOperationResult.Completed( + value = createSession(nodeExecutable, adapterEntryPoint, request, version.value, remainingMillis), + ) + is FastCheckOperationResult.TimedOut -> version + } + } + + private fun createSession( + nodeExecutable: String, + adapterEntryPoint: Path, + request: FastCheckExecutionRequest, + runtimeVersion: String, + remainingMillis: (() -> Long)?, + ): FastCheckCoverageSession { val adapterRoot = adapterEntryPoint.parent?.parent?.parent ?: throw IllegalArgumentException("Adapter entry point has no runtime root: $adapterEntryPoint") val c8EntryPoint = adapterRoot.resolve("node_modules/c8/bin/c8.js") @@ -285,17 +363,8 @@ internal class FastCheckCoverageSession private constructor( private fun readSupportedNodeVersion( nodeExecutable: String, request: FastCheckExecutionRequest, - remainingMillis: (() -> Long)?, - ): String { - val remaining = remainingMillis?.invoke() ?: NODE_VERSION_TIMEOUT_MILLIS - if (remaining <= 0) { - failPreparation( - request = request, - code = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, - message = "External witness deadline expired before the runtime probe", - kind = BackendErrorKind.TIMEOUT, - ) - } + timeoutMillis: Long, + ): FastCheckOperationResult { val transport = FastCheckProcessTransport( nodeExecutable = nodeExecutable, maxRequestBytes = 1, @@ -304,12 +373,12 @@ internal class FastCheckCoverageSession private constructor( shutdownGraceMillis = VERSION_SHUTDOWN_GRACE_MILLIS, useProcessSupervisor = false, ) - val output = try { - transport.invoke( + val outputResult = try { + transport.invokeWithResult( command = listOf(nodeExecutable, "--version"), request = "", - timeoutMillis = minOf(NODE_VERSION_TIMEOUT_MILLIS, remaining), - reportedTimeoutMillis = NODE_VERSION_TIMEOUT_MILLIS, + timeoutMillis = timeoutMillis, + reportedTimeoutMillis = timeoutMillis, description = "Node.js version probe", ) } catch (error: FastCheckTransportException) { @@ -326,6 +395,10 @@ internal class FastCheckCoverageSession private constructor( cause = error, ) } + val output = when (outputResult) { + is FastCheckOperationResult.Completed -> outputResult.value + is FastCheckOperationResult.TimedOut -> return outputResult + } val version = output.stdout.trim() if (output.exitCode != 0 || version.isBlank()) { failPreparation( @@ -335,7 +408,7 @@ internal class FastCheckCoverageSession private constructor( ) } - return requireSupportedNodeVersion(version, request) + return FastCheckOperationResult.Completed(value = requireSupportedNodeVersion(version, request)) } private fun requireSupportedNodeVersion(version: String, request: FastCheckExecutionRequest): String { diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckOperationResult.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckOperationResult.kt new file mode 100644 index 0000000000..51d1baf36c --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckOperationResult.kt @@ -0,0 +1,8 @@ +package org.usvm.ts.pbt.fastcheck + +/** Expected budget exhaustion travels as data; backend and protocol failures retain their exception contracts. */ +internal sealed interface FastCheckOperationResult { + data class Completed(val value: T) : FastCheckOperationResult + + data class TimedOut(val message: String) : FastCheckOperationResult +} diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt index 7024dc49df..085aeef2be 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt @@ -55,34 +55,42 @@ internal class FastCheckProcessClient( fun witness( request: FastCheckExecutionRequest, remainingMillis: () -> Long, - ): FastCheckExecutionWireResponse { + ): FastCheckOperationResult { + val initialBudget = remainingMillis() + if (initialBudget <= 0) { + return FastCheckOperationResult.TimedOut(message = "External witness deadline expired") + } + val encodedRequest = encodeRequest(request) val coverageSession = request.coverageRequest?.let { - FastCheckCoverageSession.prepare( + val preparation = FastCheckCoverageSession.prepareWithinBudget( nodeExecutable = nodeExecutable, adapterEntryPoint = adapterEntryPoint, request = request, remainingMillis = remainingMillis, ) + when (preparation) { + is FastCheckOperationResult.Completed -> preparation.value + is FastCheckOperationResult.TimedOut -> return preparation + } } try { val remaining = remainingMillis() if (remaining <= 0) { - throw backendError( - kind = BackendErrorKind.TIMEOUT, - code = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, - message = "External witness deadline expired", - request = request, - ) + return FastCheckOperationResult.TimedOut(message = "External witness deadline expired") } - val output = invokeAdapter( + val outputResult = invokeWitnessAdapter( encodedRequest = encodedRequest, request = request, command = coverageSession?.adapterCommand ?: listOf(nodeExecutable, adapterEntryPoint.toString()), timeoutMillis = remaining, ) + val output = when (outputResult) { + is FastCheckOperationResult.Completed -> outputResult.value + is FastCheckOperationResult.TimedOut -> return outputResult + } validateProcessOutput(output, request) val response = decodeResponse(output.stdout, request) if (response.status == "error") throwNodeDiagnostic(response, request) @@ -97,16 +105,45 @@ internal class FastCheckProcessClient( if (!validResponse) throw invalidResponse(message = "Invalid witness response", request = request) val replay = response.witnessReplay - return if (replay != null && coverageSession != null) { - response.copy(witnessReplay = replay.copy(coverage = coverageSession.readArtifact())) - } else { - response + if (replay != null && coverageSession != null) { + val artifactResult = coverageSession.readArtifact() + return when (artifactResult) { + is FastCheckOperationResult.Completed -> FastCheckOperationResult.Completed( + value = response.copy(witnessReplay = replay.copy(coverage = artifactResult.value)), + ) + is FastCheckOperationResult.TimedOut -> artifactResult + } } + + return FastCheckOperationResult.Completed(value = response) } finally { coverageSession?.close() } } + private fun invokeWitnessAdapter( + encodedRequest: String, + request: FastCheckExecutionRequest, + command: List, + timeoutMillis: Long, + ): FastCheckOperationResult = try { + transport.invokeWithResult( + command = command, + request = encodedRequest, + timeoutMillis = timeoutMillis, + reportedTimeoutMillis = timeoutMillis, + description = "fast-check adapter", + ) + } catch (error: FastCheckTransportException) { + throw backendError( + kind = error.backendErrorKind(), + code = error.code, + message = error.message.orEmpty(), + request = request, + cause = error, + ) + } + private fun invokeAdapter( encodedRequest: String, request: FastCheckExecutionRequest, diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt index 72448b653f..ba4d7bfbc9 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt @@ -11,7 +11,6 @@ import java.util.concurrent.ExecutorService import java.util.concurrent.Executors import java.util.concurrent.Future import java.util.concurrent.TimeUnit -import java.util.concurrent.TimeoutException /** Completed output of one supervised request-response process. */ internal data class FastCheckProcessOutput( @@ -57,6 +56,31 @@ internal class FastCheckProcessTransport( reportedTimeoutMillis: Long, description: String, ): FastCheckProcessOutput { + val result = invokeWithResult( + command = command, + request = request, + timeoutMillis = timeoutMillis, + reportedTimeoutMillis = reportedTimeoutMillis, + description = description, + ) + + return when (result) { + is FastCheckOperationResult.Completed -> result.value + is FastCheckOperationResult.TimedOut -> fail( + code = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + message = result.message, + ) + } + } + + /** Uses the same supervisor and cleanup as [invoke], exposing timeout without exceptional unwinding. */ + fun invokeWithResult( + command: List, + request: String, + timeoutMillis: Long, + reportedTimeoutMillis: Long, + description: String, + ): FastCheckOperationResult { require(timeoutMillis > 0) { "Process timeout must be positive" } require(command.isNotEmpty()) { "Supervised command must not be empty" } requireRequestWithinLimit(request, description) @@ -67,26 +91,30 @@ internal class FastCheckProcessTransport( val tasks = startIoTasks(managedProcess.process, request, description, executor) try { - awaitProcess( + val processCompleted = awaitProcess( process = managedProcess.process, tasks = tasks.all, deadlineNanos = deadlineNanos, - reportedTimeoutMillis = reportedTimeoutMillis, description = description, ) - awaitIo( + if (!processCompleted) return timedOut(description, reportedTimeoutMillis) + + val ioCompleted = awaitIo( tasks = tasks, deadlineNanos = deadlineNanos, - reportedTimeoutMillis = reportedTimeoutMillis, description = description, ) + if (!ioCompleted) return timedOut(description, reportedTimeoutMillis) + val stdout = tasks.stdout.completedValue(description) val stderr = tasks.stderr.completedValue(description) - return FastCheckProcessOutput( - exitCode = managedProcess.process.exitValue(), - stdout = stdout, - stderr = stderr, + return FastCheckOperationResult.Completed( + value = FastCheckProcessOutput( + exitCode = managedProcess.process.exitValue(), + stdout = stdout, + stderr = stderr, + ), ) } finally { tasks.all.forEach { task -> task.cancel() } @@ -143,15 +171,14 @@ internal class FastCheckProcessTransport( process: Process, tasks: List>, deadlineNanos: Long, - reportedTimeoutMillis: Long, description: String, - ) { + ): Boolean { while (true) { tasks.forEach { task -> task.throwIfFailed(description) } val remainingMillis = remainingMillis(deadlineNanos) if (remainingMillis <= FORCED_TERMINATION_RESERVE_MILLIS) { - timeout(description, reportedTimeoutMillis) + return false } val completed = try { @@ -164,30 +191,41 @@ internal class FastCheckProcessTransport( cause = error, ) } - if (completed) return + if (completed) return true } } private fun awaitIo( tasks: ProcessIoTasks, deadlineNanos: Long, - reportedTimeoutMillis: Long, description: String, - ) { + ): Boolean { while (true) { tasks.all.forEach { task -> task.throwIfFailed(description) } - val pendingTask = tasks.all.firstOrNull { task -> !task.isDone } ?: break + val ioCompleted = tasks.all.all { task -> task.isDone } + if (ioCompleted) break val remainingMillis = remainingMillis(deadlineNanos) if (remainingMillis <= FORCED_TERMINATION_RESERVE_MILLIS) { - timeout(description, reportedTimeoutMillis) + return false } - pendingTask.await(minOf(remainingMillis, IO_POLL_MILLIS), description) + try { + Thread.sleep(minOf(remainingMillis, IO_POLL_MILLIS)) + } catch (error: InterruptedException) { + Thread.currentThread().interrupt() + fail( + code = FastCheckDiagnosticCode.BACKEND_PROCESS_INTERRUPTED, + message = "Interrupted while waiting for $description I/O", + cause = error, + ) + } } tasks.all.forEach { task -> task.completedValue(description) } + + return true } private fun startProcess( @@ -322,8 +360,7 @@ internal class FastCheckProcessTransport( runCatching { process.errorStream.close() } } - private fun timeout(description: String, reportedTimeoutMillis: Long): Nothing = fail( - code = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + private fun timedOut(description: String, reportedTimeoutMillis: Long) = FastCheckOperationResult.TimedOut( message = "$description exceeded the $reportedTimeoutMillis ms timeout", ) @@ -372,12 +409,14 @@ private data class ProcessIoTask( if (isDone) completedValue(description) } - fun completedValue(description: String): T = requireNotNull(await(waitMillis = 0, description)) + fun completedValue(description: String): T { + check(future.isDone) { "Cannot read the result of pending $operation" } + + return readCompletedValue(description) + } - fun await(waitMillis: Long, description: String): T? = try { - future.get(waitMillis, TimeUnit.MILLISECONDS) - } catch (_: TimeoutException) { - null + private fun readCompletedValue(description: String): T = try { + future.get() } catch (error: InterruptedException) { Thread.currentThread().interrupt() throw FastCheckTransportException( diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt index 2b0ef5e294..56a49dfbf3 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt @@ -1,6 +1,6 @@ package org.usvm.ts.pbt.fastcheck -import kotlinx.serialization.decodeFromString +import org.usvm.ts.pbt.FastCheckDiagnosticCode import org.usvm.ts.pbt.backend.ExternalWitnessCandidate import org.usvm.ts.pbt.backend.PropertyCoverageRequest import org.usvm.ts.pbt.backend.WitnessAdmission @@ -48,47 +48,40 @@ internal class FastCheckWitnessCoordinator( if (earlyStatus != null) return delta(candidate = candidate, status = earlyStatus) val inputs = requireNotNull(candidate.inputs) - var firstReplay: WitnessNativeReplay? = null - try { - val original = replay(property, candidate, inputs, deadline) - firstReplay = original - val confirmation = replay(property, candidate, inputs, deadline) - if (!repeatable(original, confirmation)) { - return delta( - candidate = candidate, - status = WitnessReplayStatus.NONDETERMINISTIC, - original = original, - ) - } - } catch (error: PbtBackendException) { - return delta( - candidate = candidate, - status = error.replayStatus(), - original = firstReplay, - diagnostic = error.code, - ) + val initial = verifyOriginal(property, candidate, inputs, deadline) + val replayConfirmed = when (initial.status) { + WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, + WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, + WitnessReplayStatus.CONFIRMED_COVERAGE, + -> true + else -> false } + if (!replayConfirmed) return initial - val original = requireNotNull(firstReplay) - val status = classify(original, candidate) - if (!original.targetMatched || original.admission != WitnessAdmission.ADMITTED) { - return delta(candidate = candidate, status = status, original = original) - } + val original = requireNotNull(initial.originalReplay) + val status = initial.status var confirmedOriginal = original var coverageDiagnostic: String? = null val coverageRequest = configuration.coverageRequest if (coverageRequest != null) { try { - val covered = replay(property, candidate, inputs, deadline, coverageRequest) - if (!repeatable(original, covered)) { + val coverageResult = replay(property, candidate, inputs, deadline, coverageRequest) + val covered = when (coverageResult) { + is FastCheckOperationResult.Completed -> coverageResult.value + is FastCheckOperationResult.TimedOut -> null + } + if (covered == null) { + coverageDiagnostic = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT + } else if (!repeatable(original, covered)) { return delta( candidate = candidate, status = WitnessReplayStatus.NONDETERMINISTIC, original = original, ) + } else { + confirmedOriginal = covered } - confirmedOriginal = covered } catch (error: PbtBackendException) { coverageDiagnostic = error.code } @@ -117,6 +110,52 @@ internal class FastCheckWitnessCoordinator( ).copy(contextualRefutations = refutations) } + private fun verifyOriginal( + property: PropertyDefinition, + candidate: ExternalWitnessCandidate, + inputs: List, + deadline: WitnessReplayDeadline, + ): WitnessEvidenceDelta { + var firstReplay: WitnessNativeReplay? = null + try { + val first = replay(property, candidate, inputs, deadline) + val original = when (first) { + is FastCheckOperationResult.Completed -> first.value + is FastCheckOperationResult.TimedOut -> return delta( + candidate = candidate, + status = WitnessReplayStatus.TIMEOUT, + diagnostic = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + ) + } + firstReplay = original + + val second = replay(property, candidate, inputs, deadline) + val confirmation = when (second) { + is FastCheckOperationResult.Completed -> second.value + is FastCheckOperationResult.TimedOut -> return delta( + candidate = candidate, + status = WitnessReplayStatus.TIMEOUT, + original = original, + diagnostic = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + ) + } + val status = if (repeatable(original, confirmation)) { + classify(original, candidate) + } else { + WitnessReplayStatus.NONDETERMINISTIC + } + + return delta(candidate = candidate, status = status, original = original) + } catch (error: PbtBackendException) { + return delta( + candidate = candidate, + status = error.replayStatus(), + original = firstReplay, + diagnostic = error.code, + ) + } + } + private fun validateReduction( property: PropertyDefinition, candidate: ExternalWitnessCandidate, @@ -140,8 +179,16 @@ internal class FastCheckWitnessCoordinator( } return try { - val finalReplay = replay(property, candidate, inputs, deadline) - val finalConfirmation = replay(property, candidate, inputs, deadline) + val first = replay(property, candidate, inputs, deadline) + val finalReplay = when (first) { + is FastCheckOperationResult.Completed -> first.value + is FastCheckOperationResult.TimedOut -> return reducedTimeout(reduction) + } + val second = replay(property, candidate, inputs, deadline) + val finalConfirmation = when (second) { + is FastCheckOperationResult.Completed -> second.value + is FastCheckOperationResult.TimedOut -> return reducedTimeout(reduction) + } val validFinal = repeatable(finalReplay, finalConfirmation) && sameTarget(finalReplay, original) if (validFinal) { ValidatedReduction( @@ -160,11 +207,7 @@ internal class FastCheckWitnessCoordinator( } catch (error: PbtBackendException) { ValidatedReduction( reduction = reduction.copy( - status = if (error.kind == BackendErrorKind.TIMEOUT) { - WitnessReductionStatus.TIMEOUT - } else { - WitnessReductionStatus.FAILED - }, + status = WitnessReductionStatus.FAILED, inputs = null, diagnostic = error.code, ), @@ -172,6 +215,14 @@ internal class FastCheckWitnessCoordinator( } } + private fun reducedTimeout(reduction: WitnessReduction): ValidatedReduction = ValidatedReduction( + reduction = reduction.copy( + status = WitnessReductionStatus.TIMEOUT, + inputs = null, + diagnostic = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + ), + ) + private fun validateCandidate( property: PropertyDefinition, candidate: ExternalWitnessCandidate, @@ -181,11 +232,7 @@ internal class FastCheckWitnessCoordinator( if (!sameRegistration) return WitnessReplayStatus.SOURCE_MISMATCH val inputs = candidate.inputs ?: return WitnessReplayStatus.UNREPRESENTABLE_INPUT - val encodable = runCatching { - val encoded = PropertyManifestJson.json.encodeToUtf8SafeString(inputs) - PropertyManifestJson.json.decodeFromString>(encoded) - }.isSuccess - if (!encodable) return WitnessReplayStatus.UNREPRESENTABLE_INPUT + if (!inputs.hasWitnessEncoding()) return WitnessReplayStatus.UNREPRESENTABLE_INPUT if (!inDeclaredSupport(property, inputs)) return WitnessReplayStatus.DOMAIN_REJECTED val sourceModules = candidate.sources.mapTo(hashSetOf()) { source -> source.module } @@ -212,8 +259,8 @@ internal class FastCheckWitnessCoordinator( inputs: List, deadline: WitnessReplayDeadline, coverageRequest: PropertyCoverageRequest? = null, - ): WitnessNativeReplay { - val response = client.witness( + ): FastCheckOperationResult { + val result = client.witness( request = request( property = property, candidate = candidate, @@ -229,7 +276,12 @@ internal class FastCheckWitnessCoordinator( remainingMillis = deadline::remainingMillis, ) - return requireNotNull(response.witnessReplay) + return when (result) { + is FastCheckOperationResult.Completed -> FastCheckOperationResult.Completed( + value = requireNotNull(result.value.witnessReplay), + ) + is FastCheckOperationResult.TimedOut -> result + } } private fun reduce( @@ -251,7 +303,7 @@ internal class FastCheckWitnessCoordinator( val shrinkDeadline = WitnessReplayDeadline(timeoutMillis = budget) return try { - val response = client.witness( + val result = client.witness( request = request( property = property, candidate = candidate, @@ -266,14 +318,18 @@ internal class FastCheckWitnessCoordinator( ), remainingMillis = { minOf(deadline.remainingMillis(), shrinkDeadline.remainingMillis()) }, ) - requireNotNull(response.witnessReduction).copy(originalEncodedBytes = originalBytes) + when (result) { + is FastCheckOperationResult.Completed -> requireNotNull(result.value.witnessReduction) + .copy(originalEncodedBytes = originalBytes) + is FastCheckOperationResult.TimedOut -> WitnessReduction( + status = WitnessReductionStatus.TIMEOUT, + originalEncodedBytes = originalBytes, + diagnostic = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + ) + } } catch (error: PbtBackendException) { WitnessReduction( - status = if (error.kind == BackendErrorKind.TIMEOUT) { - WitnessReductionStatus.TIMEOUT - } else { - WitnessReductionStatus.FAILED - }, + status = WitnessReductionStatus.FAILED, originalEncodedBytes = originalBytes, diagnostic = error.code, ) @@ -368,6 +424,8 @@ internal class FastCheckWitnessCoordinator( actual.outcome == expected.outcome && actual.failure?.errorName == expected.failure?.errorName fun classify(replay: WitnessNativeReplay, candidate: ExternalWitnessCandidate): WitnessReplayStatus = when { + replay.diagnostic == FastCheckDiagnosticCode.ENTRY_POINT_SOURCE_HASH_MISMATCH -> + WitnessReplayStatus.SOURCE_MISMATCH replay.outcome == WitnessOracleOutcome.ERROR -> WitnessReplayStatus.PROPERTY_ERROR replay.admission == WitnessAdmission.DOMAIN_REJECTED -> WitnessReplayStatus.DOMAIN_REJECTED replay.admission == WitnessAdmission.PRECONDITION_REJECTED -> WitnessReplayStatus.PRECONDITION_REJECTED @@ -382,8 +440,6 @@ internal class FastCheckWitnessCoordinator( } fun PbtBackendException.replayStatus(): WitnessReplayStatus = when { - kind == BackendErrorKind.TIMEOUT -> WitnessReplayStatus.TIMEOUT - code == "entrypoint.source-hash.mismatch" -> WitnessReplayStatus.SOURCE_MISMATCH code.startsWith("js-value.") || code.startsWith("js-number.") -> WitnessReplayStatus.UNREPRESENTABLE_INPUT else -> WitnessReplayStatus.REPLAY_ERROR } diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/WitnessInputEncoding.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/WitnessInputEncoding.kt new file mode 100644 index 0000000000..85d40be7e9 --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/WitnessInputEncoding.kt @@ -0,0 +1,43 @@ +package org.usvm.ts.pbt.fastcheck + +import org.usvm.ts.pbt.model.JsConcreteValue +import java.util.IdentityHashMap + +/** Validates the supported wire value tree without using serializer failures to select an admission outcome. */ +internal fun List.hasWitnessEncoding(): Boolean { + val pending = ArrayDeque() + val seen = IdentityHashMap() + pending.addAll(this) + + while (pending.isNotEmpty()) { + when (val value = pending.removeLast()) { + is JsConcreteValue.Number -> { + if (!value.number.hasValidEncoding()) return false + } + is JsConcreteValue.Array -> { + if (seen.put(value, true) != null) return false + + pending.addAll(value.elements) + } + + is JsConcreteValue.Object -> { + val hasUnsupportedFields = value.fields.keys.any { name -> name in UNSUPPORTED_OBJECT_FIELDS } + if (hasUnsupportedFields || seen.put(value, true) != null) return false + + pending.addAll(value.fields.values) + } + + JsConcreteValue.Null, + JsConcreteValue.Undefined, + is JsConcreteValue.Boolean, + is JsConcreteValue.String, + -> { + Unit + } + } + } + + return true +} + +private val UNSUPPORTED_OBJECT_FIELDS = hashSetOf("__proto__", "constructor", "prototype") diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt index 20d7fbb755..d0c05bbafe 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt @@ -20,6 +20,8 @@ import org.usvm.ts.pbt.model.ArrayIndexGenerator import org.usvm.ts.pbt.model.ConstantDomain import org.usvm.ts.pbt.model.IntegerDomain import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.JsNumber +import org.usvm.ts.pbt.model.JsNumberKind import org.usvm.ts.pbt.model.PropertyAssertion import org.usvm.ts.pbt.model.PropertyDefinition import org.usvm.ts.pbt.model.PropertyDomain @@ -35,6 +37,7 @@ import java.security.MessageDigest import kotlin.test.assertEquals import kotlin.test.assertNotNull import kotlin.test.assertNull +import kotlin.test.assertSame import kotlin.test.assertTrue class ExternalWitnessTest { @@ -353,6 +356,34 @@ class ExternalWitnessTest { } } + @Test + fun `invalid number encodings aliases and cycles are rejected before serialization`() { + val property = property(predicate = "threshold") + val shared = JsConcreteValue.Array(elements = listOf(JsConcreteValue.number(1.0))) + val cycleElements = mutableListOf() + val cycle = JsConcreteValue.Array(elements = cycleElements) + cycleElements.add(cycle) + val inputs = listOf( + listOf(JsConcreteValue.Number(number = JsNumber(value = JsNumberKind.FINITE, bits = "not-bits"))), + listOf(JsConcreteValue.Array(elements = listOf(shared, shared))), + listOf(cycle), + ) + + for (values in inputs) { + val candidate = candidate(property = property, inputs = values) + val result = backend.confirmWitness( + property = property, + candidate = candidate, + configuration = configuration + ) + + assertEquals(WitnessReplayStatus.UNREPRESENTABLE_INPUT, result.status) + assertSame(candidate, result.candidate) + assertNull(result.originalReplay) + assertNull(result.reduction.inputs) + } + } + @Test fun `symbolic false target is not confirmed by a different native exception`() { val property = property(predicate = "predicateError") diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessTimeoutTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessTimeoutTest.kt new file mode 100644 index 0000000000..34597aaf3a --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessTimeoutTest.kt @@ -0,0 +1,145 @@ +package org.usvm.ts.pbt.fastcheck + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.PropertyCoverageRequest +import org.usvm.ts.pbt.backend.WitnessTarget +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.testResourcesRoot +import java.nio.file.Files +import java.nio.file.Path +import kotlin.io.path.createTempDirectory +import kotlin.io.path.readText +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertIs +import kotlin.test.assertTrue + +class FastCheckWitnessTimeoutTest { + @Test + fun `expired replay budget returns timeout without starting a process`() { + val client = FastCheckProcessClient( + nodeExecutable = "definitely-not-a-node-executable", + adapterEntryPoint = Path.of("unused"), + ) + + val result = client.witness(request = request(), remainingMillis = { 0L }) + + assertIs(result) + } + + @Test + fun `expired runtime probe budget returns timeout without starting a process`() { + val result = FastCheckCoverageSession.prepareWithinBudget( + nodeExecutable = "definitely-not-a-node-executable", + adapterEntryPoint = Path.of("unused"), + request = request().copy(coverageRequest = PropertyCoverageRequest()), + remainingMillis = { 0L }, + ) + + assertIs(result) + } + + @Test + fun `budget expiry after runtime probe releases its coverage workspace`() { + val before = coverageWorkspaces() + var budgetReads = 0 + val client = FastCheckProcessClient(adapterEntryPoint = FastCheckRuntime.executionEntryPoint()) + + val result = client.witness( + request = request().copy(coverageRequest = PropertyCoverageRequest()), + remainingMillis = { + budgetReads += 1 + if (budgetReads <= 2) 5_000L else 0L + }, + ) + + assertIs(result) + assertEquals(3, budgetReads) + assertEquals(before, coverageWorkspaces()) + } + + @Test + fun `expired branch conversion budget returns timeout before reading its report`() { + var remaining = 5_000L + val preparation = FastCheckCoverageSession.prepareWithinBudget( + nodeExecutable = "node", + adapterEntryPoint = FastCheckRuntime.executionEntryPoint(), + request = request().copy(coverageRequest = PropertyCoverageRequest()), + remainingMillis = { remaining }, + ) + val session = assertIs>(preparation).value + remaining = 0L + + session.use { + val result = it.readArtifact() + + assertIs(result) + } + } + + @Test + fun `running witness timeout returns a result and terminates its process`() { + val directory = createTempDirectory(prefix = "witness-timeout-") + val adapter = directory.resolve("adapter.mjs") + val pidFile = directory.resolve("pid") + adapter.writeText( + """ + import { writeFileSync } from 'node:fs'; + writeFileSync(${jsString(pidFile.toString())}, String(process.pid)); + setInterval(() => {}, 1000); + """.trimIndent(), + ) + val client = FastCheckProcessClient(adapterEntryPoint = adapter) + + try { + val result = client.witness(request = request(), remainingMillis = { 500L }) + + assertIs(result) + assertTrue(Files.isRegularFile(pidFile), "The supervised adapter did not start") + val pid = pidFile.readText().toLong() + assertFalse(ProcessHandle.of(pid).map(ProcessHandle::isAlive).orElse(false)) + } finally { + directory.toFile().deleteRecursively() + } + } + + private fun request(): FastCheckExecutionRequest { + val module = "properties/witness/ExternalWitness.ts" + val property = PropertyDefinition( + id = PropertyId(value = "witness.timeout"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = 0, max = 100))), + predicate = TypeScriptEntryPoint(module = module, exportName = "threshold"), + ) + + return FastCheckExecutionRequest( + manifest = property.toManifest(), + sourceRoots = listOf(testResourcesRoot().toString()), + numRuns = 1, + timeoutMillis = 5_000, + witness = FastCheckWitnessOperation( + mode = "replay", + inputs = listOf(JsConcreteValue.number(80.0)), + target = WitnessTarget(id = "threshold"), + sources = listOf(PropertyObservationSource(module = module, sha256 = "0".repeat(64))), + ), + ) + } + + private fun coverageWorkspaces(): Set = Files.list( + Path.of(System.getProperty("java.io.tmpdir")) + ).use { files -> + files.iterator().asSequence() + .filter { path -> path.fileName.toString().startsWith("usvm-ts-fast-check-coverage-") } + .toHashSet() + } + + private fun jsString(value: String): String = "'${value.replace("\\", "\\\\").replace("'", "\\'")}'" +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/witness/ExternalWitness.ts b/usvm-ts-fast-check/src/test/resources/properties/witness/ExternalWitness.ts index ed7360659b..e16416c502 100644 --- a/usvm-ts-fast-check/src/test/resources/properties/witness/ExternalWitness.ts +++ b/usvm-ts-fast-check/src/test/resources/properties/witness/ExternalWitness.ts @@ -78,3 +78,16 @@ export function requiresInitial(value: number): boolean { return !initialSeen || value < 10; } + +export function nondeterministicShrink(value: number): boolean { + if (value === 80) return false; + + flipped = !flipped; + return flipped; +} + +export function eventError(): boolean { + const hook = (globalThis as Record)[Symbol.for('org.usvm.ts.pbt.witness')] as WitnessHook | undefined; + hook?.('', 'original', 'v1', true, false); + return observed('oracle-completed', true); +} diff --git a/usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md b/usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md index 103afe144e..80730c266a 100644 --- a/usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md +++ b/usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md @@ -108,6 +108,9 @@ steps; byte sizes measure serialization size, not numeric magnitude. Replay, runtime probes, coverage conversion, and reduction consume the supplied monotonic deadline. Reduction reserves final-validation time; synchronous/asynchronous hangs are stopped by the existing process supervisor. +Budget exhaustion and supervised timeouts return explicit results through the witness pipeline. Shrinking +nondeterminism, oracle contract errors, and invalid/bounded witness events are recorded as outcomes without +throwing exceptions to select the next step. Input wire eligibility is validated directly before serialization. Process teardown can take the supervisor's bounded shutdown grace after the execution budget expires. No fresh full timeout is granted to the final replay. From 24f5aa5e9882fe87b15dfa8fdf464f092a1d7bc4 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 00:26:46 +0300 Subject: [PATCH 3/4] [TS PBT] Preserve project resolution during witness replay --- .../src/external-witness.ts | 8 +++- .../usvm/ts/pbt/fastcheck/FastCheckBackend.kt | 6 ++- .../fastcheck/FastCheckWitnessCoordinator.kt | 2 + .../ts/pbt/fastcheck/ExternalWitnessTest.kt | 41 +++++++++++++++++++ .../properties/witness/aliases/Logic.ts | 7 ++++ .../witness/aliases/Precondition.ts | 5 +++ .../properties/witness/aliases/Predicate.ts | 5 +++ .../witness/aliases/witness.tsconfig.json | 8 ++++ 8 files changed, 79 insertions(+), 3 deletions(-) create mode 100644 usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Logic.ts create mode 100644 usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Precondition.ts create mode 100644 usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Predicate.ts create mode 100644 usvm-ts-fast-check/src/test/resources/properties/witness/aliases/witness.tsconfig.json diff --git a/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts b/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts index 121d979f6e..a3118d90a7 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts @@ -138,9 +138,13 @@ export async function executeWitness(value: unknown): Promise replayOnce(input, operation.target, predicate, precondition); if (operation.mode === 'replay') { diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt index b69c2d6e0c..ceb5ebe4f9 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt @@ -71,7 +71,11 @@ class FastCheckBackend( candidate: ExternalWitnessCandidate, configuration: WitnessReplayConfiguration, deadline: WitnessReplayDeadline, - ): WitnessEvidenceDelta = FastCheckWitnessCoordinator(client = client, sourceRoots = sourceRoots).confirm( + ): WitnessEvidenceDelta = FastCheckWitnessCoordinator( + client = client, + sourceRoots = sourceRoots, + tsconfig = tsconfig?.toRealPath()?.toString(), + ).confirm( property = property, candidate = candidate, configuration = configuration, diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt index 56a49dfbf3..35ea2ec9c7 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt @@ -29,6 +29,7 @@ import java.nio.file.Path internal class FastCheckWitnessCoordinator( private val client: FastCheckProcessClient, private val sourceRoots: List, + private val tsconfig: String? = null, ) { fun confirm( property: PropertyDefinition, @@ -347,6 +348,7 @@ internal class FastCheckWitnessCoordinator( return FastCheckExecutionRequest( manifest = property.toManifest(), sourceRoots = sourceRoots.map(Path::toString), + tsconfig = tsconfig, numRuns = 1, timeoutMillis = timeoutMillis, witness = operation, diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt index d0c05bbafe..4eab2021e7 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt @@ -67,6 +67,47 @@ class ExternalWitnessTest { assertEquals("4.9.0", result.backendVersion) } + @Test + fun `external replay preserves project aliases through admission and reduction`() { + val directory = "properties/witness/aliases" + val predicateModule = "$directory/Predicate.ts" + val preconditionModule = "$directory/Precondition.ts" + val property = property(predicate = "threshold").copy( + predicate = TypeScriptEntryPoint(module = predicateModule, exportName = "threshold"), + precondition = TypeScriptEntryPoint(module = preconditionModule, exportName = "admission"), + ) + val candidate = property.captureWitness( + inputs = listOf(JsConcreteValue.number(80.0)), + target = WitnessTarget(id = "threshold"), + sources = listOf( + source(module = predicateModule), + source(module = preconditionModule), + source(module = "$directory/Logic.ts"), + ), + provenance = "symbolic-fixture", + ) + val configuredBackend = FastCheckBackend( + sourceRoots = listOf(root), + tsconfig = root.resolve("$directory/witness.tsconfig.json"), + ) + val withCoverage = configuration.copy( + coverageRequest = PropertyCoverageRequest(scopes = setOf(CoverageScope.PROPERTY_ENTRY_POINTS)), + ) + + val result = configuredBackend.confirmWitness( + property = property, + candidate = candidate, + configuration = withCoverage, + ) + + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, result.status, result.diagnostic) + assertEquals(WitnessReductionStatus.EXHAUSTED, result.reduction.status) + assertEquals(listOf(JsConcreteValue.number(15.0)), result.reduction.inputs) + assertEquals(WitnessOracleOutcome.FALSE, result.originalReplay?.outcome) + assertEquals(WitnessOracleOutcome.FALSE, result.reducedReplay?.outcome) + assertNotNull(result.originalReplay?.coverage) + } + @Test fun `a different named failed check cannot replace the original check`() { val property = property(predicate = "namedChecks").copy( diff --git a/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Logic.ts b/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Logic.ts new file mode 100644 index 0000000000..9166a5bb52 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Logic.ts @@ -0,0 +1,7 @@ +export function holds(value: number): boolean { + return value < 10; +} + +export function admitted(value: number): boolean { + return value >= 15; +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Precondition.ts b/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Precondition.ts new file mode 100644 index 0000000000..1f470bbc3b --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Precondition.ts @@ -0,0 +1,5 @@ +import { admitted } from '@witness/logic'; + +export function admission(value: number): boolean { + return admitted(value); +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Predicate.ts b/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Predicate.ts new file mode 100644 index 0000000000..ba13030e8c --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/Predicate.ts @@ -0,0 +1,5 @@ +import { holds } from '@witness/logic'; + +export function threshold(value: number): boolean { + return holds(value); +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/witness.tsconfig.json b/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/witness.tsconfig.json new file mode 100644 index 0000000000..5c7268b16f --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/witness/aliases/witness.tsconfig.json @@ -0,0 +1,8 @@ +{ + "compilerOptions": { + "baseUrl": ".", + "paths": { + "@witness/logic": ["Logic.ts"] + } + } +} From 0715401d5d973479bc677072322925c47a501c77 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 01:21:16 +0300 Subject: [PATCH 4/4] Reserve graceful process shutdown within the total timeout --- .../fastcheck/FastCheckProcessTransport.kt | 14 ++- .../fastcheck/FastCheckWitnessTimeoutTest.kt | 92 ++++++++++++++++++- 2 files changed, 102 insertions(+), 4 deletions(-) diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt index ba4d7bfbc9..25f9029947 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt @@ -40,6 +40,12 @@ internal class FastCheckProcessTransport( private val shutdownGraceMillis: Long, private val useProcessSupervisor: Boolean = true, ) { + private val shutdownReserveMillis = if (useProcessSupervisor) { + shutdownGraceMillis + FORCED_TERMINATION_RESERVE_MILLIS + } else { + FORCED_TERMINATION_RESERVE_MILLIS + } + init { require(maxRequestBytes > 0) { "Maximum request size must be positive" } require(maxStdoutBytes > 0) { "Maximum stdout size must be positive" } @@ -85,6 +91,10 @@ internal class FastCheckProcessTransport( require(command.isNotEmpty()) { "Supervised command must not be empty" } requireRequestWithinLimit(request, description) + if (useProcessSupervisor && timeoutMillis <= shutdownReserveMillis) { + return timedOut(description, reportedTimeoutMillis) + } + val deadlineNanos = deadlineAfter(timeoutMillis) val managedProcess = startProcess(command, description) val executor = Executors.newFixedThreadPool(IO_TASK_COUNT) @@ -177,7 +187,7 @@ internal class FastCheckProcessTransport( tasks.forEach { task -> task.throwIfFailed(description) } val remainingMillis = remainingMillis(deadlineNanos) - if (remainingMillis <= FORCED_TERMINATION_RESERVE_MILLIS) { + if (remainingMillis <= shutdownReserveMillis) { return false } @@ -207,7 +217,7 @@ internal class FastCheckProcessTransport( if (ioCompleted) break val remainingMillis = remainingMillis(deadlineNanos) - if (remainingMillis <= FORCED_TERMINATION_RESERVE_MILLIS) { + if (remainingMillis <= shutdownReserveMillis) { return false } diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessTimeoutTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessTimeoutTest.kt index 34597aaf3a..64a66a185c 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessTimeoutTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessTimeoutTest.kt @@ -23,6 +23,18 @@ import kotlin.test.assertIs import kotlin.test.assertTrue class FastCheckWitnessTimeoutTest { + @Test + fun `short replay budget reserves shutdown before starting a supervised adapter`() { + val client = FastCheckProcessClient( + nodeExecutable = "definitely-not-a-node-executable", + adapterEntryPoint = Path.of("unused"), + ) + + val result = client.witness(request = request(), remainingMillis = { 250L }) + + assertIs(result) + } + @Test fun `expired replay budget returns timeout without starting a process`() { val client = FastCheckProcessClient( @@ -97,10 +109,15 @@ class FastCheckWitnessTimeoutTest { setInterval(() => {}, 1000); """.trimIndent(), ) - val client = FastCheckProcessClient(adapterEntryPoint = adapter) + val executionBudgetMillis = 500L + val shutdownGraceMillis = 250L + val client = FastCheckProcessClient(adapterEntryPoint = adapter, shutdownGraceMillis = shutdownGraceMillis) try { - val result = client.witness(request = request(), remainingMillis = { 500L }) + val result = client.witness( + request = request(), + remainingMillis = { executionBudgetMillis + shutdownGraceMillis }, + ) assertIs(result) assertTrue(Files.isRegularFile(pidFile), "The supervised adapter did not start") @@ -111,6 +128,77 @@ class FastCheckWitnessTimeoutTest { } } + @Test + fun `witness timeout lets its command complete cleanup within the existing shutdown grace`() { + val directory = createTempDirectory(prefix = "witness-timeout-cleanup-") + val adapter = directory.resolve("adapter.mjs") + val pidFile = directory.resolve("pid") + val cleanupFile = directory.resolve("cleaned") + adapter.writeText( + """ + import { writeFileSync } from 'node:fs'; + writeFileSync(${jsString(pidFile.toString())}, String(process.pid)); + process.on('SIGTERM', () => setTimeout(() => { + writeFileSync(${jsString(cleanupFile.toString())}, 'cleaned'); + process.exit(0); + }, 50)); + setInterval(() => {}, 1000); + """.trimIndent(), + ) + val client = FastCheckProcessClient(adapterEntryPoint = adapter, shutdownGraceMillis = 250) + + try { + val result = client.witness(request = request(), remainingMillis = { 1_000L }) + + assertIs(result) + assertTrue(Files.isRegularFile(pidFile), "The supervised adapter did not start") + assertTrue(Files.isRegularFile(cleanupFile), "Timeout skipped the configured graceful shutdown") + val pid = pidFile.readText().toLong() + assertFalse(ProcessHandle.of(pid).map(ProcessHandle::isAlive).orElse(false)) + } finally { + directory.toFile().deleteRecursively() + } + } + + @Test + fun `direct transport timeout still terminates and waits for its own process`() { + val directory = createTempDirectory(prefix = "direct-timeout-") + val adapter = directory.resolve("adapter.mjs") + val pidFile = directory.resolve("pid") + adapter.writeText( + """ + import { writeFileSync } from 'node:fs'; + writeFileSync(${jsString(pidFile.toString())}, String(process.pid)); + setInterval(() => {}, 1000); + """.trimIndent(), + ) + val transport = FastCheckProcessTransport( + nodeExecutable = "node", + maxRequestBytes = 1_024, + maxStdoutBytes = 1_024, + maxStderrBytes = 1_024, + shutdownGraceMillis = 250, + useProcessSupervisor = false, + ) + + try { + val result = transport.invokeWithResult( + command = listOf("node", adapter.toString()), + request = "{}", + timeoutMillis = 500, + reportedTimeoutMillis = 500, + description = "direct timeout adapter", + ) + + assertIs(result) + assertTrue(Files.isRegularFile(pidFile), "The direct adapter did not start") + val pid = pidFile.readText().toLong() + assertFalse(ProcessHandle.of(pid).map(ProcessHandle::isAlive).orElse(false)) + } finally { + directory.toFile().deleteRecursively() + } + } + private fun request(): FastCheckExecutionRequest { val module = "properties/witness/ExternalWitness.ts" val property = PropertyDefinition(