[TS PBT] Use native witness results for coverage feedback

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;
 

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<WitnessExecutionSuccess> {
+export async function executeWitness(value: unknown, coverage?: ExecutionCoverage): Promise<WitnessExecutionSuccess> {
   const request = validateRequest(value);
   const operation = validateOperation((value as Record<string, unknown>).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<WitnessExecutionSu
     : await loadEntryPoint(
       request.manifest.precondition, request.sourceRoots, 'manifest.precondition', request.tsconfig,
     );
-  const replay = (input: JsConcreteValue[]) => 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,14 +244,15 @@ class ExternalValueArbitrary extends fc.Arbitrary<JsConcreteValue[]> {
 async function replayOnce(
   values: JsConcreteValue[], target: WitnessTarget, predicate: LoadedEntryPoint, precondition: LoadedEntryPoint | undefined,
   diagnosticCheck: boolean,
+  coverage?: ExecutionCoverage,
 ): Promise<WitnessNativeReplay> {
   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', undefined, () => { context.active = true; },
+      values, predicate, precondition, undefined, 'replay', coverage, () => { context.active = true; },
     ));
     if (holds === null) {
       result.admission = 'PRECONDITION_REJECTED';

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,

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<Path>,
     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,
         )
     }
 

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<WitnessNativeReplay>()
+
+        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<JsConcreteValue>) -> WitnessNativeReplay?)? = null,
         replay: (List<JsConcreteValue>) -> 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,
+            ),
         )
     }
 

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<JsConcreteValue>) -> PropertyRunResult?,
-)
+    val nativeReplay: ((inputs: List<JsConcreteValue>) -> WitnessNativeReplay?)? = null,
+    val replay: (inputs: List<JsConcreteValue>) -> PropertyRunResult? = { null },
+) {
+    constructor(
+        initialCoverage: PropertyCoverageArtifact?,
+        replay: (inputs: List<JsConcreteValue>) -> PropertyRunResult?,
+    ) : this(initialCoverage = initialCoverage, nativeReplay = null, replay = replay)
+}
 
 /** Why a report can or cannot supply exact coverage goals for this property/source snapshot. */
 @Serializable

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<UsvmCoverageEdge>,
         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<UsvmCoverageEdge>,
+        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<UsvmCoverageEdge>,
+    ): 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)