From 206929b29de19837f5370483085eec6ce55ecf50 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 01:05:04 +0300 Subject: [PATCH] Confirm and shrink named DSL witnesses through original companions --- .../src/execute-property.ts | 30 +- .../src/external-witness.ts | 29 +- .../fastcheck/FastCheckWitnessCoordinator.kt | 10 +- .../usvm/ts/pbt/dsl/DslExternalWitnessTest.kt | 261 ++++++++++++++++++ 4 files changed, 306 insertions(+), 24 deletions(-) create mode 100644 usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/DslExternalWitnessTest.kt 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 4af4985aae..c4f6a5d6c5 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 @@ -8,6 +8,7 @@ import { import { EntryPointInvocationError, isNamedCheckFailure, + type NamedCheckFailure, type ExecutionKind, loadEntryPoint, verifySourceHash, @@ -461,18 +462,7 @@ function failureDetails(details: RunDetails<[JsConcreteValue[]]>): FastCheckFail : details.errorInstance; if (isNamedCheckFailure(error)) { - const description = error.exception === undefined - ? describePropertyFailure(error) - : describePropertyFailure(error.exception.value); - return { - kind: 'property', - ...description, - checkId: error.checkId, - ...(error.exception === undefined ? { - actual: encodeJsValue(error.actual), - expected: encodeJsValue(error.expected), - } : {}), - }; + return describeNamedCheckFailure(error); } return { @@ -481,6 +471,22 @@ function failureDetails(details: RunDetails<[JsConcreteValue[]]>): FastCheckFail }; } +export function describeNamedCheckFailure(error: NamedCheckFailure): FastCheckFailureDetails { + const description = error.exception === undefined + ? describePropertyFailure(error) + : describePropertyFailure(error.exception.value); + + return { + kind: 'property', + ...description, + checkId: error.checkId, + ...(error.exception === undefined ? { + actual: encodeJsValue(error.actual), + expected: encodeJsValue(error.expected), + } : {}), + }; +} + export function describePropertyFailure(value: unknown): Pick { try { if (value instanceof Error) { diff --git a/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts b/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts index a3118d90a7..171d21cb77 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts @@ -2,8 +2,8 @@ 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 { EntryPointInvocationError, isNamedCheckFailure, loadEntryPoint, sourceHashMatches, type LoadedEntryPoint } from './entry-point.js'; +import { describeNamedCheckFailure, 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'; @@ -97,11 +97,13 @@ export async function executeWitness(value: unknown): Promise).witness, request.manifest.inputs.length); const identity = { witnessPropertyId: request.manifest.propertyId, witnessTarget: operation.target }; const target = operation.target; + const declaredCheck = request.manifest.assertions?.some((check) => check.id === target.id) === true; + const diagnosticCheck = request.manifest.predicate.checkResultExportName !== undefined && declaredCheck; 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)); + ? diagnosticCheck || (request.manifest.assertions?.length ?? 0) === 0 && target.id === request.manifest.predicate.exportName + : target.binding.pointId === target.id && declaredCheck); if (!validOriginalCheck) { - throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Original named check requires its executable binding', 'witness.target'); + throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Original named check requires a companion or executable binding', 'witness.target'); } for (const source of operation.sources) { const matches = await sourceHashMatches(source.module, source.sha256, request.sourceRoots); @@ -145,7 +147,7 @@ export async function executeWitness(value: unknown): Promise replayOnce(input, operation.target, predicate, precondition); + const replay = (input: JsConcreteValue[]) => replayOnce(input, operation.target, predicate, precondition, diagnosticCheck); if (operation.mode === 'replay') { const first = await replay(values); @@ -235,6 +237,7 @@ class ExternalValueArbitrary extends fc.Arbitrary { async function replayOnce( values: JsConcreteValue[], target: WitnessTarget, predicate: LoadedEntryPoint, precondition: LoadedEntryPoint | undefined, + diagnosticCheck: boolean, ): Promise { const context: WitnessContext = { events: [], active: false }; const result: WitnessNativeReplay = { @@ -251,7 +254,10 @@ async function replayOnce( result.outcome = holds ? 'HOLDS' : 'FALSE'; } } catch (error: unknown) { - if (error instanceof EntryPointInvocationError) { + if (isNamedCheckFailure(error)) { + result.outcome = error.exception === undefined ? 'FALSE' : 'THREW'; + result.failure = describeNamedCheckFailure(error); + } else if (error instanceof EntryPointInvocationError) { result.outcome = 'THREW'; result.failure = { kind: 'property', ...describePropertyFailure(error.thrownValue) }; } else { @@ -270,8 +276,11 @@ async function replayOnce( : context.events.find((entry) => sameBinding(entry.binding, target.binding as WitnessBinding)); const propertyFailed = result.outcome === 'FALSE' || result.outcome === 'THREW'; const guardedEvent = event !== undefined && event.guard; + const checkMatched = diagnosticCheck + ? result.failure?.checkId === target.id + : result.failure?.checkId === undefined || result.failure.checkId === target.id; result.targetMatched = result.admission === 'ADMITTED' && (target.role === 'PROPERTY' - ? propertyFailed && (target.expectedOutcome === undefined || target.expectedOutcome === result.outcome) + ? propertyFailed && checkMatched && (target.expectedOutcome === undefined || target.expectedOutcome === result.outcome) && (target.binding === undefined || (guardedEvent && !event.holds)) : guardedEvent && (target.role === 'COVERAGE' || !event.holds)); @@ -280,7 +289,9 @@ async function replayOnce( export function sameTarget(actual: WitnessNativeReplay, expected: WitnessNativeReplay): boolean { return actual.admission === 'ADMITTED' && actual.targetMatched && actual.outcome === expected.outcome - && actual.failure?.errorName === expected.failure?.errorName; + && actual.failure?.checkId === expected.failure?.checkId + && actual.failure?.errorName === expected.failure?.errorName + && actual.failure?.message === expected.failure?.message; } function sameBinding(left: WitnessBinding, right: WitnessBinding): boolean { diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt index 35ea2ec9c7..03b2c329c4 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt @@ -244,10 +244,12 @@ internal class FastCheckWitnessCoordinator( val target = candidate.target val binding = target.binding + val declaredCheck = property.assertions.any { assertion -> assertion.id == target.id } + val diagnosticCheck = property.predicate.checkResultExportName != null && declaredCheck val validCheck = target.role != WitnessRole.PROPERTY || if (binding == null) { - property.assertions.isEmpty() && target.id == property.predicate.exportName + diagnosticCheck || property.assertions.isEmpty() && target.id == property.predicate.exportName } else { - binding.pointId == target.id && property.assertions.any { assertion -> assertion.id == target.id } + binding.pointId == target.id && declaredCheck } if (!validCheck) return WitnessReplayStatus.UNSUPPORTED_REPLAY @@ -423,7 +425,9 @@ internal class FastCheckWitnessCoordinator( fun sameTarget(actual: WitnessNativeReplay, expected: WitnessNativeReplay): Boolean = actual.admission == WitnessAdmission.ADMITTED && actual.targetMatched && - actual.outcome == expected.outcome && actual.failure?.errorName == expected.failure?.errorName + actual.outcome == expected.outcome && actual.failure?.checkId == expected.failure?.checkId && + actual.failure?.errorName == expected.failure?.errorName && + actual.failure?.message == expected.failure?.message fun classify(replay: WitnessNativeReplay, candidate: ExternalWitnessCandidate): WitnessReplayStatus = when { replay.diagnostic == FastCheckDiagnosticCode.ENTRY_POINT_SOURCE_HASH_MISMATCH -> diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/DslExternalWitnessTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/DslExternalWitnessTest.kt new file mode 100644 index 0000000000..a2da049f0a --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/DslExternalWitnessTest.kt @@ -0,0 +1,261 @@ +package org.usvm.ts.pbt.dsl + +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.WitnessBinding +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.WitnessReplayStatus +import org.usvm.ts.pbt.backend.WitnessTarget +import org.usvm.ts.pbt.backend.captureWitness +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import org.usvm.ts.pbt.usvm.UsvmPropertySearcher +import java.nio.file.Files +import java.nio.file.Path +import java.security.MessageDigest +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class DslExternalWitnessTest { + @TempDir + lateinit var directory: Path + + private val configuration = WitnessReplayConfiguration(timeoutMillis = 15_000, validationReserveMillis = 3_000) + + @Test + fun `compiled DSL symbolic inputs confirm the explicitly selected original check`() { + val compiled = compile(threshold(includeEarlierCheck = false)) + val property = compiled.definition + val roots = listOf(directory) + val manifest = property.toManifest() + val scene = loadEtsProjectAutoConvert(directory, provider = EtsIrProvider.TS_FRONTEND) + val mapping = PropertyEtsMapper(scene = scene, sourceRoots = roots).map(manifest) + val searcher = UsvmPropertySearcher( + scene = scene, + machineOptions = UMachineOptions(solverType = SolverType.YICES, timeout = 10.seconds), + ) + + val symbolic = searcher.search( + manifest = manifest, + mapping = mapping, + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + ) + val candidate = property.captureWitness( + inputs = assertNotNull(symbolic.inputs), + target = WitnessTarget(id = "threshold", expectedOutcome = WitnessOracleOutcome.FALSE), + sources = sources(), + provenance = "usvm:${symbolic.status}:${symbolic.target}", + ) + val evidence = FastCheckBackend(sourceRoots = roots).confirmWitness( + property = property, + candidate = candidate, + configuration = configuration, + ) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, symbolic.status) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, evidence.status, evidence.diagnostic) + assertEquals(candidate, evidence.candidate) + assertEquals("threshold", evidence.originalReplay?.failure?.checkId) + assertEquals(WitnessOracleOutcome.FALSE, evidence.originalReplay?.outcome) + assertEquals("threshold", evidence.reducedReplay?.failure?.checkId) + assertEquals(WitnessReductionStatus.EXHAUSTED, evidence.reduction.status) + } + + @Test + fun `external DSL witness actually shrinks without switching to an earlier failed check`() { + val compiled = compile(threshold(includeEarlierCheck = true)) + + val evidence = confirm(compiled, value = 80.0) + + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, evidence.status, evidence.diagnostic) + assertEquals(inputs(value = 80.0), evidence.candidate.inputs) + assertEquals(inputs(value = 15.0), evidence.reduction.inputs) + assertEquals(WitnessReductionStatus.EXHAUSTED, evidence.reduction.status) + assertTrue(evidence.reduction.acceptedShrinks > 0) + assertEquals("threshold", evidence.originalReplay?.failure?.checkId) + assertEquals(JsConcreteValue.number(81.0), evidence.originalReplay?.failure?.actual) + assertEquals(JsConcreteValue.number(80.0), evidence.originalReplay?.failure?.expected) + assertEquals("threshold", evidence.reducedReplay?.failure?.checkId) + assertEquals(JsConcreteValue.number(16.0), evidence.reducedReplay?.failure?.actual) + assertEquals(JsConcreteValue.number(15.0), evidence.reducedReplay?.failure?.expected) + assertTrue(assertNotNull(evidence.reducedReplay).targetMatched) + } + + @Test + fun `wrong check domain and precondition do not confirm the selected DSL check`() { + val compiled = compile(threshold(includeEarlierCheck = true)) + val cases = listOf( + 5.0 to WitnessReplayStatus.TARGET_MISMATCH, + 0.0 to WitnessReplayStatus.PRECONDITION_REJECTED, + 101.0 to WitnessReplayStatus.DOMAIN_REJECTED, + ) + + for ((value, status) in cases) { + val evidence = confirm(compiled, value = value) + + assertEquals(status, evidence.status, "input=$value: ${evidence.diagnostic}") + assertEquals(WitnessReductionStatus.NOT_ELIGIBLE, evidence.reduction.status) + assertFalse(evidence.originalReplay?.targetMatched == true) + } + } + + @Test + fun `named exceptions remain distinct from false and preserve the original exception while shrinking`() { + val program = defineProperty(id = "witness.dsl-exception") { + val fail = function<(Double) -> Double>(module = "subject.ts", exportName = "fail") + val value by int(min = 0, max = 100) + + check(name = "threshold") { fail(value) lessThan 15 } + } + val compiled = compile(program) + + val wrongOutcome = confirm(compiled, value = 80.0) + val evidence = confirm(compiled, value = 80.0, outcome = WitnessOracleOutcome.THREW) + + assertEquals(WitnessReplayStatus.TARGET_MISMATCH, wrongOutcome.status) + assertEquals(WitnessOracleOutcome.THREW, wrongOutcome.originalReplay?.outcome) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, evidence.status, evidence.diagnostic) + assertEquals(inputs(value = 15.0), evidence.reduction.inputs) + assertTrue(evidence.reduction.acceptedShrinks > 0) + val failure = assertNotNull(evidence.reducedReplay?.failure) + assertEquals("threshold", failure.checkId) + assertEquals("TypeError", failure.errorName) + assertEquals("original exception", failure.message) + assertNull(failure.actual) + assertNull(failure.expected) + } + + @Test + fun `exception before a named check cannot impersonate that check`() { + val program = defineProperty(id = "witness.dsl-local-exception") { + val fail = function<(Double) -> Double>(module = "subject.ts", exportName = "fail") + val value by int(min = 0, max = 100) + val result by value(fail(value)) + + check(name = "threshold") { result lessThan 15 } + } + val compiled = compile(program) + + val evidence = confirm(compiled, value = 80.0, outcome = WitnessOracleOutcome.THREW) + + assertEquals(WitnessReplayStatus.TARGET_MISMATCH, evidence.status) + assertEquals(WitnessOracleOutcome.THREW, evidence.originalReplay?.outcome) + assertEquals("TypeError", evidence.originalReplay?.failure?.errorName) + assertNull(evidence.originalReplay?.failure?.checkId) + assertEquals(WitnessReductionStatus.NOT_ELIGIBLE, evidence.reduction.status) + } + + @Test + fun `named target without a diagnostic companion still requires an executable binding`() { + val compiled = compile(threshold(includeEarlierCheck = false)) + val property = compiled.definition.copy( + predicate = compiled.definition.predicate.copy(checkResultExportName = null), + ) + val withoutCompanion = compiled.copy(definition = property) + + val evidence = confirm(withoutCompanion, value = 80.0) + + assertEquals(WitnessReplayStatus.UNSUPPORTED_REPLAY, evidence.status) + assertNull(evidence.originalReplay) + } + + @Test + fun `diagnostic companion does not satisfy a contextual witness binding`() { + val compiled = compile(threshold(includeEarlierCheck = false)) + val candidate = compiled.definition.captureWitness( + inputs = inputs(value = 80.0), + target = WitnessTarget( + id = "threshold", + binding = WitnessBinding(pointId = "threshold", contextId = "selected-context", revision = "v1"), + ), + sources = sources(), + provenance = "contextual-fixture", + ) + + val evidence = FastCheckBackend(sourceRoots = listOf(directory)).confirmWitness( + property = compiled.definition, + candidate = candidate, + configuration = configuration, + ) + + assertEquals(WitnessReplayStatus.TARGET_MISMATCH, evidence.status) + assertEquals("threshold", evidence.originalReplay?.failure?.checkId) + assertFalse(assertNotNull(evidence.originalReplay).targetMatched) + } + + private fun threshold(includeEarlierCheck: Boolean): DslProperty = defineProperty(id = "witness.dsl-threshold") { + val threshold = function<(Double) -> Double>(module = "subject.ts", exportName = "threshold") + val value by int(min = 0, max = 100) + + assume { value greaterOrEqual 5 } + if (includeEarlierCheck) check(name = "earlier") { value greaterOrEqual 10 } + check(name = "threshold") { threshold(value) equalTo value } + } + + private fun compile(program: DslProperty): CompiledDslProperty { + Files.writeString(directory.resolve("subject.ts"), SUBJECT) + val compiled = PropertyTypeScriptCompiler().compile( + program = program, + generatedModule = GENERATED_MODULE, + resolveModule = { module -> "./$module" }, + ) + Files.writeString(directory.resolve(GENERATED_MODULE), compiled.typeScript) + + return compiled + } + + private fun confirm( + compiled: CompiledDslProperty, + value: Double, + outcome: WitnessOracleOutcome = WitnessOracleOutcome.FALSE, + ) = FastCheckBackend(sourceRoots = listOf(directory)).confirmWitness( + property = compiled.definition, + candidate = compiled.definition.captureWitness( + inputs = inputs(value), + target = WitnessTarget(id = "threshold", expectedOutcome = outcome), + sources = sources(), + provenance = "external-dsl-fixture", + ), + configuration = configuration, + ) + + private fun sources(): List = listOf(GENERATED_MODULE, "subject.ts").map { module -> + val bytes = Files.readAllBytes(directory.resolve(module)) + val hash = MessageDigest.getInstance("SHA-256").digest(bytes).joinToString(separator = "") { byte -> + "%02x".format(byte.toInt() and 0xff) + } + PropertyObservationSource(module = module, sha256 = hash) + } + + private fun inputs(value: Double): List = listOf(JsConcreteValue.number(value)) + + private companion object { + const val GENERATED_MODULE = "property.ts" + val SUBJECT = """ + export function threshold(value: number): number { + if (value < 15) return value; + return value + 1; + } + export function fail(value: number): number { + if (value < 15) throw new TypeError('different exception'); + throw new TypeError('original exception'); + } + """.trimIndent() + } +}