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/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/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..a3118d90a7 --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts @@ -0,0 +1,316 @@ +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, 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'; +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' | 'UNKNOWN'; + outcome: 'HOLDS' | 'FALSE' | 'THREW' | 'SKIPPED' | 'ERROR' | 'UNKNOWN'; + 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?: string } +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 = adapterDiagnostic.witnessEventsInvalid.code; + + return holds; + } + + 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) { + const matches = await sourceHashMatches(source.module, source.sha256, request.sourceRoots); + if (!matches) { + const diagnostic = adapterDiagnostic.entryPointSourceHashMismatch.code; + if (operation.mode === 'reduce') { + return { status: 'ok', ...identity, witnessReduction: { + status: 'FAILED', attempts: 0, acceptedShrinks: 0, diagnostic, + } }; + } + + return { status: 'ok', ...identity, witnessReplay: { + admission: 'UNKNOWN', outcome: 'UNKNOWN', targetMatched: false, events: [], + diagnostic, runtimeVersion: process.version, + } }; + } + } + 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', request.tsconfig, + ); + const precondition = request.manifest.precondition === undefined ? undefined + : await loadEntryPoint( + request.manifest.precondition, request.sourceRoots, 'manifest.precondition', request.tsconfig, + ); + 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 reductionDiagnostic: string | undefined; + 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); + 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) { + reductionDiagnostic ??= describePropertyFailure(error).message; + + 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 || reductionDiagnostic !== undefined || details.counterexample === null) { + return { status: 'ok', ...identity, witnessReduction: { + status: timedOut ? 'TIMEOUT' : 'FAILED', attempts, acceptedShrinks: details.numShrinks, + diagnostic: reductionDiagnostic ?? 'Reduction did not retain the target', + } }; + } + + 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) { + result.outcome = 'THREW'; + result.failure = { kind: 'property', ...describePropertyFailure(error.thrownValue) }; + } else { + result.admission = 'ERROR'; + result.outcome = 'ERROR'; + 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'; + 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..644e2f9019 --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts @@ -0,0 +1,192 @@ +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); + + 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; + + 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('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); + } + 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/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/FastCheckBackend.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt index 3fc53edcbf..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 @@ -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,22 @@ class FastCheckBackend( return client.check(request) } + override fun confirmWitness( + property: PropertyDefinition, + candidate: ExternalWitnessCandidate, + configuration: WitnessReplayConfiguration, + deadline: WitnessReplayDeadline, + ): WitnessEvidenceDelta = FastCheckWitnessCoordinator( + client = client, + sourceRoots = sourceRoots, + tsconfig = tsconfig?.toRealPath()?.toString(), + ).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..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 @@ -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,14 +62,29 @@ internal class FastCheckCoverageSession private constructor( } fun attachTo(result: PropertyRunResult): PropertyRunResult { + 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(): 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, - propertyId = result.propertyId, + propertyId = PropertyId(request.manifest.propertyId), sourceRoots = request.sourceRoots, propertyEntryPointPaths = entryPointPaths, adapterRoot = workspace.adapterRoot.toString(), @@ -89,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( @@ -105,8 +131,6 @@ internal class FastCheckCoverageSession private constructor( cause = error, ) } - - return result.copy(coverage = artifact) } private fun propertyEntryPointPaths(): Set { @@ -124,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, @@ -133,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 = 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( @@ -193,6 +240,11 @@ internal class FastCheckCoverageSession private constructor( workspace.root.toFile().deleteRecursively() } + private fun boundedTimeout(limitMillis: Long): Long { + val remaining = remainingMillis?.invoke() ?: return limitMillis + return minOf(limitMillis, remaining.coerceAtLeast(0)) + } + private fun canonicalizeExistingEntryPoint(candidate: Path): String = if (Files.exists(candidate)) candidate.toRealPath().toString() else candidate.toString() @@ -216,7 +268,53 @@ internal class FastCheckCoverageSession private constructor( adapterEntryPoint: Path, request: FastCheckExecutionRequest, ): FastCheckCoverageSession { - val runtimeVersion = readSupportedNodeVersion(nodeExecutable, request) + 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") @@ -238,6 +336,7 @@ internal class FastCheckCoverageSession private constructor( request = request, runtimeVersion = runtimeVersion, workspace = workspace, + remainingMillis = remainingMillis, ) } @@ -264,7 +363,8 @@ internal class FastCheckCoverageSession private constructor( private fun readSupportedNodeVersion( nodeExecutable: String, request: FastCheckExecutionRequest, - ): String { + timeoutMillis: Long, + ): FastCheckOperationResult { val transport = FastCheckProcessTransport( nodeExecutable = nodeExecutable, maxRequestBytes = 1, @@ -273,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 = NODE_VERSION_TIMEOUT_MILLIS, - reportedTimeoutMillis = NODE_VERSION_TIMEOUT_MILLIS, + timeoutMillis = timeoutMillis, + reportedTimeoutMillis = timeoutMillis, description = "Node.js version probe", ) } catch (error: FastCheckTransportException) { @@ -295,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( @@ -304,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/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/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 5f71da5460..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 @@ -51,15 +51,109 @@ internal class FastCheckProcessClient( } } + /** One external operation, using the same supervised transport and optional original-source collector. */ + fun witness( + request: FastCheckExecutionRequest, + remainingMillis: () -> Long, + ): FastCheckOperationResult { + val initialBudget = remainingMillis() + if (initialBudget <= 0) { + return FastCheckOperationResult.TimedOut(message = "External witness deadline expired") + } + + val encodedRequest = encodeRequest(request) + val coverageSession = request.coverageRequest?.let { + 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) { + return FastCheckOperationResult.TimedOut(message = "External witness deadline expired") + } + + 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) + + 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 + 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, 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/FastCheckProcessTransport.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt index 72448b653f..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 @@ -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( @@ -41,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" } @@ -57,36 +62,69 @@ 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) + if (useProcessSupervisor && timeoutMillis <= shutdownReserveMillis) { + return timedOut(description, reportedTimeoutMillis) + } + val deadlineNanos = deadlineAfter(timeoutMillis) val managedProcess = startProcess(command, description) val executor = Executors.newFixedThreadPool(IO_TASK_COUNT) 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 +181,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) + if (remainingMillis <= shutdownReserveMillis) { + return false } val completed = try { @@ -164,30 +201,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) + if (remainingMillis <= shutdownReserveMillis) { + 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 +370,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 +419,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 new file mode 100644 index 0000000000..35ea2ec9c7 --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt @@ -0,0 +1,454 @@ +package org.usvm.ts.pbt.fastcheck + +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 +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, + private val tsconfig: String? = null, +) { + 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) + 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(initial.originalReplay) + val status = initial.status + + var confirmedOriginal = original + var coverageDiagnostic: String? = null + val coverageRequest = configuration.coverageRequest + if (coverageRequest != null) { + try { + 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 + } + } 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 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, + 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 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( + 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 = WitnessReductionStatus.FAILED, + inputs = null, + diagnostic = error.code, + ), + ) + } + } + + 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, + ): 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 + if (!inputs.hasWitnessEncoding()) 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, + ): FastCheckOperationResult { + val result = 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 when (result) { + is FastCheckOperationResult.Completed -> FastCheckOperationResult.Completed( + value = requireNotNull(result.value.witnessReplay), + ) + is FastCheckOperationResult.TimedOut -> result + } + } + + 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 result = 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()) }, + ) + 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 = 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), + tsconfig = tsconfig, + 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.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 + 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 { + 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/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 new file mode 100644 index 0000000000..4eab2021e7 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/ExternalWitnessTest.kt @@ -0,0 +1,519 @@ +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.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 +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.assertSame +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 `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( + 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 `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") + 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/fastcheck/FastCheckWitnessTimeoutTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessTimeoutTest.kt new file mode 100644 index 0000000000..64a66a185c --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessTimeoutTest.kt @@ -0,0 +1,233 @@ +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 `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( + 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 executionBudgetMillis = 500L + val shutdownGraceMillis = 250L + val client = FastCheckProcessClient(adapterEntryPoint = adapter, shutdownGraceMillis = shutdownGraceMillis) + + try { + val result = client.witness( + request = request(), + remainingMillis = { executionBudgetMillis + shutdownGraceMillis }, + ) + + 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() + } + } + + @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( + 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/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..e16416c502 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/witness/ExternalWitness.ts @@ -0,0 +1,93 @@ +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; +} + +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-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"] + } + } +} diff --git a/usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md b/usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md new file mode 100644 index 0000000000..80730c266a --- /dev/null +++ b/usvm-ts-pbt/EXTERNAL_WITNESS_REPLAY.md @@ -0,0 +1,132 @@ +# 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. +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. + +## 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", + ) +}