From 2bc2ee8d4c02c1afb65f5ccaf58513731c4172c7 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 21:10:25 +0300 Subject: [PATCH] [TS PBT] Replay native witness evidence for coverage feedback --- .../fast-check-adapter/src/execution-cli.ts | 2 +- .../src/external-witness.ts | 11 +- .../usvm/ts/pbt/fastcheck/FastCheckBackend.kt | 14 +++ .../fastcheck/FastCheckWitnessCoordinator.kt | 32 ++++++ .../fastcheck/UsvmEdgeFeedbackContractTest.kt | 106 +++++++++++++++++- .../usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt | 11 +- .../org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt | 49 +++++++- 7 files changed, 212 insertions(+), 13 deletions(-) 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 1ccf8bc0f9..aa21b484fb 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 @@ -27,7 +27,7 @@ try { try { if (inputError !== undefined) throw inputError; const isWitness = request !== null && typeof request === 'object' && 'witness' in request; - response = isWitness ? await executeWitness(request) : await executeProperty(request, coverage); + response = isWitness ? await executeWitness(request, coverage) : await executeProperty(request, coverage); } catch (error: unknown) { if (!(error instanceof ProtocolError)) throw 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 02f3c1edb0..754fc51dfe 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 @@ -7,6 +7,7 @@ import { describeNamedCheckFailure, describePropertyFailure, invokePropertyOnce, import { decodeJsValue, encodeJsValue, ProtocolError, protocolError, type JsConcreteValue, type TaggedJsValue } from './js-value.js'; import { buildPropertyArbitrary } from './property-arbitrary.js'; import { stringifyProtocolJson } from './protocol-json.js'; +import type { ExecutionCoverage } from './execution-coverage.js'; import { inWitnessSupport } from './witness-support.js'; export interface WitnessBinding { @@ -92,7 +93,7 @@ export function installWitnessHook(): void { } /** Uses the same invocation boundary, original entrypoints, codecs, and fast-check shrink stream as ordinary PBT. */ -export async function executeWitness(value: unknown): Promise { +export async function executeWitness(value: unknown, coverage?: ExecutionCoverage): 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 }; @@ -151,10 +152,11 @@ export async function executeWitness(value: unknown): Promise replayOnce(input, operation.target, predicate, precondition, diagnosticCheck); + const replay = (input: JsConcreteValue[], collect?: ExecutionCoverage) => + replayOnce(input, operation.target, predicate, precondition, diagnosticCheck, collect); if (operation.mode === 'replay') { - const first = await replay(values); + const first = await replay(values, coverage); const second = await replay(values); if (signature(first) !== signature(second)) first.diagnostic = 'nondeterministic'; @@ -242,6 +244,7 @@ class ExternalValueArbitrary extends fc.Arbitrary { async function replayOnce( values: JsConcreteValue[], target: WitnessTarget, predicate: LoadedEntryPoint, precondition: LoadedEntryPoint | undefined, diagnosticCheck: boolean, + coverage?: ExecutionCoverage, ): Promise { const context: WitnessContext = { events: [], active: false }; const result: WitnessNativeReplay = { @@ -249,7 +252,7 @@ async function replayOnce( }; try { const holds = await contexts.run(context, () => invokePropertyOnce( - values, predicate, precondition, undefined, 'replay', undefined, () => { context.active = true; }, + values, predicate, precondition, undefined, 'replay', coverage, () => { context.active = true; }, )); if (holds === null) { result.admission = 'PRECONDITION_REJECTED'; 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 001fa4187b..4c7b8ca121 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 @@ -6,9 +6,11 @@ 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.PropertyCoverageRequest 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.WitnessNativeReplay import org.usvm.ts.pbt.backend.WitnessReplayConfiguration import org.usvm.ts.pbt.backend.WitnessReplayDeadline import org.usvm.ts.pbt.coverage.captureCoverageIdentity @@ -114,6 +116,18 @@ class FastCheckBackend( deadline = deadline, ) + /** Native verification of a fixed candidate; this operation never starts PBT generation. */ + fun replayInput( + property: PropertyDefinition, + candidate: ExternalWitnessCandidate, + coverageRequest: PropertyCoverageRequest, + deadline: WitnessReplayDeadline, + ): WitnessNativeReplay = FastCheckWitnessCoordinator( + client = client, + sourceRoots = sourceRoots, + tsconfig = tsconfig?.toRealPath()?.toString(), + ).replayInput(property, candidate, coverageRequest, deadline) + internal fun confirmOriginalWitness( property: PropertyDefinition, candidate: ExternalWitnessCandidate, 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 6eca5ffd23..d22e536693 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 @@ -15,6 +15,7 @@ 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.coverage.captureCoverageIdentity import org.usvm.ts.pbt.manifest.PropertyManifestJson import org.usvm.ts.pbt.manifest.toManifest import org.usvm.ts.pbt.model.JsConcreteValue @@ -31,6 +32,36 @@ internal class FastCheckWitnessCoordinator( private val sourceRoots: List, private val tsconfig: String? = null, ) { + /** Replays one fixed input without invoking a random generator or reducing it. */ + fun replayInput( + property: PropertyDefinition, + candidate: ExternalWitnessCandidate, + coverageRequest: PropertyCoverageRequest, + deadline: WitnessReplayDeadline, + ): WitnessNativeReplay { + val earlyStatus = validateCandidate(property, candidate, allowOriginalCheck = true) + if (earlyStatus != null) return unavailableReplay(earlyStatus.name) + + val identity = captureCoverageIdentity(candidate.manifest, sourceRoots) + val result = replay(property, candidate, requireNotNull(candidate.inputs), deadline, coverageRequest) + val native = when (result) { + is FastCheckOperationResult.Completed -> result.value + is FastCheckOperationResult.TimedOut -> return unavailableReplay(result.message) + } + val coverage = native.coverage ?: return native + val unchanged = identity == captureCoverageIdentity(candidate.manifest, sourceRoots) + if (!unchanged) return native.copy(diagnostic = "coverage.source.stale") + + return native.copy(coverage = coverage.copy(identity = identity)) + } + + private fun unavailableReplay(diagnostic: String) = WitnessNativeReplay( + admission = WitnessAdmission.UNKNOWN, + outcome = WitnessOracleOutcome.UNKNOWN, + targetMatched = false, + diagnostic = diagnostic, + ) + /** Observes the complete oracle once before fixing the named target for confirmation and reduction. */ fun confirmOriginal( property: PropertyDefinition, @@ -425,6 +456,7 @@ internal class FastCheckWitnessCoordinator( timeoutMillis = timeoutMillis, witness = operation, coverageRequest = coverageRequest, + admittedCoverage = coverageRequest?.admittedOnly == true, ) } diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/UsvmEdgeFeedbackContractTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/UsvmEdgeFeedbackContractTest.kt index e2c211bd2e..3915333a4b 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/UsvmEdgeFeedbackContractTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/UsvmEdgeFeedbackContractTest.kt @@ -6,12 +6,18 @@ import org.jacodb.ets.utils.loadEtsProjectAutoConvert import org.junit.jupiter.api.Test import org.usvm.SolverType import org.usvm.UMachineOptions +import org.usvm.ts.pbt.FastCheckDiagnosticCode import org.usvm.ts.pbt.backend.ProjectionCapability import org.usvm.ts.pbt.backend.ProjectionLevel import org.usvm.ts.pbt.backend.PropertyCoverageArtifact import org.usvm.ts.pbt.backend.PropertyCoverageRequest import org.usvm.ts.pbt.backend.PropertyRunConfiguration import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.backend.WitnessNativeReplay +import org.usvm.ts.pbt.backend.WitnessReplayDeadline +import org.usvm.ts.pbt.backend.WitnessTarget +import org.usvm.ts.pbt.backend.captureWitness +import org.usvm.ts.pbt.campaign.campaignSourceSha256 import org.usvm.ts.pbt.manifest.toManifest import org.usvm.ts.pbt.mapping.PropertyEtsMapper import org.usvm.ts.pbt.model.IntegerDomain @@ -20,6 +26,7 @@ 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 org.usvm.ts.pbt.usvm.UsvmCoverageEvidenceStatus import org.usvm.ts.pbt.usvm.UsvmCoverageFeedback @@ -61,6 +68,98 @@ class UsvmEdgeFeedbackContractTest { assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, negativeSearch.status) } + @Test + fun `native single input evidence confirms new edges without invoking the legacy PBT callback`() { + val property = property() + val initial = backend.run(property, configuration) + val deadline = WitnessReplayDeadline(timeoutMillis = 30_000) + val sources = listOf("guidance-property.ts", "edge-guidance.ts").map { module -> + PropertyObservationSource(module = module, sha256 = campaignSourceSha256(roots.single().resolve(module))) + } + val nativeResults = mutableListOf() + + val result = search( + property, + initial.coverage, + nativeReplay = { inputs -> + val candidate = property.captureWitness( + inputs = inputs, + target = WitnessTarget(id = property.predicate.exportName), + sources = sources, + provenance = "native-coverage-test", + ) + backend.replayInput( + property = property, + candidate = candidate, + coverageRequest = requireNotNull(configuration.coverageRequest), + deadline = deadline, + ).also(nativeResults::add) + }, + replay = { error("Native feedback must never fall back to a PBT run") }, + ) + + val trace = assertNotNull(result.edgeGuidance) + assertTrue(nativeResults.isNotEmpty()) + assertTrue(nativeResults.all { it.coverage?.admittedInvocations == 1 }, nativeResults.toString()) + assertTrue(trace.replays.any { it.status == UsvmEdgeReplayStatus.CONFIRMED && it.additions.isNotEmpty() }) + assertTrue(trace.remainingGoals.isEmpty(), trace.toString()) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + } + + @Test + fun `a stale native source receipt is retained and cannot remove an edge goal`() { + val property = property() + val initial = backend.run(property, configuration) + val deadline = WitnessReplayDeadline(timeoutMillis = 30_000) + + val result = search( + property, + initial.coverage, + nativeReplay = { inputs -> + val candidate = property.captureWitness( + inputs = inputs, + target = WitnessTarget(id = property.predicate.exportName), + sources = listOf( + PropertyObservationSource(module = property.predicate.module, sha256 = "0".repeat(64)), + ), + provenance = "stale-native-source-test", + ) + backend.replayInput( + property = property, + candidate = candidate, + coverageRequest = requireNotNull(configuration.coverageRequest), + deadline = deadline, + ) + }, + replay = { error("A stale native receipt must not fall back to PBT") }, + ) + + val trace = assertNotNull(result.edgeGuidance) + assertEquals(trace.initialGoals, trace.remainingGoals) + assertTrue(trace.replays.all { it.status == UsvmEdgeReplayStatus.REJECTED_OR_INCOMPATIBLE }) + assertTrue(trace.diagnostics.any { it.contains(FastCheckDiagnosticCode.ENTRY_POINT_SOURCE_HASH_MISMATCH) }) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + } + + @Test + fun `an unavailable native operation never falls back to random generation`() { + val property = property() + val initial = backend.run(property, configuration) + + val result = search( + property, + initial.coverage, + nativeReplay = { throw IllegalStateException("native source mismatch") }, + replay = { error("Legacy callback must not be used after native failure") }, + ) + + val trace = assertNotNull(result.edgeGuidance) + assertEquals(trace.initialGoals, trace.remainingGoals) + assertTrue(trace.replays.all { it.status == UsvmEdgeReplayStatus.REPLAY_FAILED }) + assertTrue(trace.diagnostics.any { it.contains("native source mismatch") }) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + } + @Test fun `native replay cancellation propagates instead of becoming an ordinary replay failure`() { val property = property() @@ -199,6 +298,7 @@ class UsvmEdgeFeedbackContractTest { private fun search( property: PropertyDefinition, coverage: PropertyCoverageArtifact?, + nativeReplay: ((List) -> WitnessNativeReplay?)? = null, replay: (List) -> PropertyRunResult?, ): UsvmPropertySearchResult { val manifest = property.toManifest() @@ -210,7 +310,11 @@ class UsvmEdgeFeedbackContractTest { manifest = manifest, mapping = mapping, concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), - coverageFeedback = UsvmCoverageFeedback(initialCoverage = coverage, replay = replay), + coverageFeedback = UsvmCoverageFeedback( + initialCoverage = coverage, + nativeReplay = nativeReplay, + replay = replay, + ), ) } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt index c752cfb8a1..c51b72b642 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt @@ -3,13 +3,20 @@ package org.usvm.ts.pbt.usvm import kotlinx.serialization.Serializable import org.usvm.ts.pbt.backend.PropertyCoverageArtifact import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.backend.WitnessNativeReplay import org.usvm.ts.pbt.model.JsConcreteValue /** Concrete feedback for the original property analysis. A replay must execute exactly [inputs]. */ data class UsvmCoverageFeedback( val initialCoverage: PropertyCoverageArtifact?, - val replay: (inputs: List) -> PropertyRunResult?, -) + val nativeReplay: ((inputs: List) -> WitnessNativeReplay?)? = null, + val replay: (inputs: List) -> PropertyRunResult? = { null }, +) { + constructor( + initialCoverage: PropertyCoverageArtifact?, + replay: (inputs: List) -> PropertyRunResult?, + ) : this(initialCoverage = initialCoverage, nativeReplay = null, replay = replay) +} /** Why a report can or cannot supply exact coverage goals for this property/source snapshot. */ @Serializable diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt index 44723908a7..9ecfd8e9df 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt @@ -15,6 +15,9 @@ import org.usvm.ts.pbt.backend.PropertyCoverageArtifact import org.usvm.ts.pbt.backend.PropertyFailureKind import org.usvm.ts.pbt.backend.PropertyRunResult import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.backend.WitnessAdmission +import org.usvm.ts.pbt.backend.WitnessNativeReplay +import org.usvm.ts.pbt.backend.WitnessOracleOutcome import org.usvm.ts.pbt.coverage.captureCoverageIdentity import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.mapping.EtsBranchArmTarget @@ -161,11 +164,21 @@ internal class UsvmEdgeGuidance( claimed: Set, expectsViolation: Boolean, ): ReplayDecision = try { - val result = feedback.replay(inputs) - if (result == null) { - ReplayDecision(status = UsvmEdgeReplayStatus.NOT_RUN) + val nativeReplay = feedback.nativeReplay + if (nativeReplay != null) { + val result = nativeReplay(inputs) + if (result == null) { + ReplayDecision(status = UsvmEdgeReplayStatus.NOT_RUN) + } else { + confirmNativeReplay(result, claimed, expectsViolation) + } } else { - confirmReplay(result, inputs, claimed, expectsViolation) + val result = feedback.replay(inputs) + if (result == null) { + ReplayDecision(status = UsvmEdgeReplayStatus.NOT_RUN) + } else { + confirmReplay(result, inputs, claimed, expectsViolation) + } } } catch (error: InterruptedException) { Thread.currentThread().interrupt() @@ -192,7 +205,33 @@ internal class UsvmEdgeGuidance( return ReplayDecision(status = UsvmEdgeReplayStatus.REJECTED_OR_INCOMPATIBLE) } - val mapped = mapper().map(manifest, requireNotNull(coverage)).coverage + return confirmCoverage(requireNotNull(coverage), claimed) + } + + private fun confirmNativeReplay( + result: WitnessNativeReplay, + claimed: Set, + expectsViolation: Boolean, + ): ReplayDecision { + result.diagnostic?.let { diagnostics += "Native replay: $it" } + val coverage = result.coverage + val violated = result.outcome == WitnessOracleOutcome.FALSE || result.outcome == WitnessOracleOutcome.THREW + val completed = result.outcome == WitnessOracleOutcome.HOLDS || violated + val matchesOracle = result.admission == WitnessAdmission.ADMITTED && completed && + violated == expectsViolation && result.diagnostic == null + val compatible = coverage != null && isCompatible(coverage) + if (!matchesOracle || !compatible) { + return ReplayDecision(status = UsvmEdgeReplayStatus.REJECTED_OR_INCOMPATIBLE) + } + + return confirmCoverage(requireNotNull(coverage), claimed) + } + + private fun confirmCoverage( + coverage: PropertyCoverageArtifact, + claimed: Set, + ): ReplayDecision { + val mapped = mapper().map(manifest, coverage).coverage val observed = exactEdges(mapped) val confirmed = observed.filter { it.hits > 0 }.mapTo(hashSetOf()) { it.edge } if (!confirmed.containsAll(claimed)) return ReplayDecision(status = UsvmEdgeReplayStatus.EDGE_MISMATCH)