Validate completed symbolic inputs during search

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunner.kt

@@ -29,6 +29,7 @@ import org.usvm.ts.pbt.model.PropertyDefinition
 import org.usvm.ts.pbt.model.PropertyId
 import org.usvm.ts.pbt.observation.PropertyObservationRequest
 import org.usvm.ts.pbt.observation.PropertyObservationSource
+import org.usvm.ts.pbt.usvm.UsvmCompletedInput
 import org.usvm.ts.pbt.usvm.UsvmCoverageFeedback
 import org.usvm.ts.pbt.usvm.UsvmPropertySearchResult
 import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus
@@ -226,6 +227,7 @@ class PropertyCampaignRunner(
                     null
                 },
                 completedInputLimit = completedInputLimit,
+                onCompletedInput = inputReplays?.let { it::captureForValidation },
             )
             if (symbolic == null) return result(PropertyCampaignStop.DEADLINE)
 
@@ -408,6 +410,7 @@ class PropertyCampaignRunner(
         validationReserveMillis: Long,
         feedback: UsvmCoverageFeedback?,
         completedInputLimit: Int,
+        onCompletedInput: ((UsvmCompletedInput) -> Unit)?,
     ): UsvmPropertySearchResult? {
         if (deadline.remainingMillis() <= validationReserveMillis) return null
 
@@ -430,6 +433,7 @@ class PropertyCampaignRunner(
             deadlineReached = { deadline.remainingMillis() <= validationReserveMillis },
             coverageFeedback = feedback,
             completedInputLimit = completedInputLimit,
+            onCompletedInput = onCompletedInput,
         )
     }
 

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplay.kt

@@ -78,6 +78,15 @@ internal class SymbolicInputReplayCollector(
     var timedOut: Boolean = false
         private set
 
+    fun captureForValidation(input: UsvmCompletedInput) {
+        // A fault must reach canonical confirmation before optional input coverage consumes its budget.
+        if (input.expectedOutcome != WitnessOracleOutcome.HOLDS) return
+        if (deadline.remainingMillis() <= validationReserveMillis) return
+
+        // The search cutoff already reserves validation time; do not subtract it from this operation again.
+        replay(input.inputs, reserveMillis = 0)
+    }
+
     fun replayForGuidance(inputs: List<JsConcreteValue>): WitnessNativeReplay? {
         val record = replay(inputs, reserveMillis = validationReserveMillis) ?: return null
         return if (record.completedWithinDeadline) {

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplayTest.kt

@@ -91,6 +91,7 @@ class SymbolicInputReplayTest {
         assertTrue(rawFaults.isNotEmpty(), artifact.toString())
         assertTrue(rawFaults.all { it.admittedCoverage == null })
         assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, artifact.result.confirmation?.status)
+        assertEquals(artifact.result.symbolic?.inputs, artifact.result.confirmation?.candidate?.inputs)
         val faultCoverage = assertNotNull(artifact.result.confirmation?.originalReplay?.coverage)
         assertTrue(faultCoverage.files.any { it.path.endsWith("CompletedSubject.ts") })
         assertTrue(artifact.result.confirmedViolation)
@@ -181,6 +182,122 @@ class SymbolicInputReplayTest {
         assertNotNull(collector.replays.single().admittedCoverage)
     }
 
+    @Test
+    fun `live validation uses the remaining deadline and is reused after the search reserve cutoff`() {
+        val log = directory.resolve("calls.txt")
+        val logLiteral = PropertyManifestJson.json.encodeToUtf8SafeString(log.toString())
+        writePredicate(
+            """
+            import { appendFileSync } from 'node:fs';
+            export function holds(value: number): boolean {
+                appendFileSync($logLiteral, String(value) + '\n');
+                const until = Date.now() + 750;
+                while (Date.now() < until) {}
+                return true;
+            }
+            """.trimIndent(),
+        )
+        val deadline = WitnessReplayDeadline(timeoutMillis = 8_000)
+        val collector = collector(deadline = deadline, validationReserveMillis = 7_000)
+        val input = completion(value = 1.0)
+
+        collector.captureForValidation(input)
+        val guidanceReplay = collector.replayForGuidance(input.inputs)
+        collector.collect(listOf(input, input))
+
+        assertTrue(deadline.remainingMillis() < 7_000)
+        assertEquals(listOf("1", "1"), Files.readAllLines(log))
+        assertEquals(WitnessOracleOutcome.HOLDS, guidanceReplay?.outcome)
+        assertEquals(1, collector.replays.size)
+        assertNotNull(collector.replays.single().admittedCoverage)
+        assertFalse(collector.timedOut)
+    }
+
+    @Test
+    fun `live validation leaves fault inputs to canonical confirmation and preserves grouped predictions`() {
+        val log = directory.resolve("calls.txt")
+        val logLiteral = PropertyManifestJson.json.encodeToUtf8SafeString(log.toString())
+        writePredicate(
+            """
+            import { appendFileSync } from 'node:fs';
+            export function holds(value: number): boolean {
+                appendFileSync($logLiteral, String(value) + '\n');
+                return true;
+            }
+            """.trimIndent(),
+        )
+        val collector = collector()
+        val healthy = completion(value = 1.0)
+        val fault = healthy.copy(expectedOutcome = WitnessOracleOutcome.FALSE)
+
+        collector.captureForValidation(fault)
+
+        assertFalse(Files.exists(log))
+
+        collector.captureForValidation(healthy)
+        collector.collect(listOf(healthy, fault))
+
+        assertEquals(listOf("1", "1"), Files.readAllLines(log))
+        val replay = collector.replays.single()
+        assertEquals(setOf(WitnessOracleOutcome.HOLDS, WitnessOracleOutcome.FALSE), replay.predictedOutcomes)
+        assertEquals("symbolic.native.oracle-mismatch", replay.replay.diagnostic)
+        assertNull(replay.admittedCoverage)
+    }
+
+    @Test
+    fun `a capture after the search cutoff remains available for final validation`() {
+        val log = directory.resolve("calls.txt")
+        val logLiteral = PropertyManifestJson.json.encodeToUtf8SafeString(log.toString())
+        writePredicate(
+            """
+            import { appendFileSync } from 'node:fs';
+            export function holds(value: number): boolean {
+                appendFileSync($logLiteral, String(value) + '\n');
+                return true;
+            }
+            """.trimIndent(),
+        )
+        val collector = collector(validationReserveMillis = 30_000)
+        val input = completion(value = 1.0)
+
+        collector.captureForValidation(input)
+
+        assertFalse(Files.exists(log))
+
+        collector.collect(listOf(input))
+
+        assertEquals(listOf("1", "1"), Files.readAllLines(log))
+        assertNotNull(collector.replays.single().admittedCoverage)
+    }
+
+    @Test
+    fun `live validation preserves unknown native receipts for final collection`() {
+        val log = directory.resolve("calls.txt")
+        val logLiteral = PropertyManifestJson.json.encodeToUtf8SafeString(log.toString())
+        writePredicate(
+            """
+            import { appendFileSync } from 'node:fs';
+            let calls = 0;
+            export function holds(value: number): boolean {
+                appendFileSync($logLiteral, String(value) + '\n');
+                return ++calls === 1;
+            }
+            """.trimIndent(),
+        )
+        val collector = collector()
+        val input = completion(value = 1.0)
+
+        collector.captureForValidation(input)
+        collector.collect(listOf(input))
+
+        val replay = collector.replays.single()
+        assertEquals(listOf("1", "1"), Files.readAllLines(log))
+        assertTrue(replay.replay.diagnostic?.contains("nondeterministic") == true)
+        assertEquals(setOf(WitnessOracleOutcome.HOLDS), replay.predictedOutcomes)
+        assertNull(replay.admittedCoverage)
+        assertNotNull(collector.diagnostic)
+    }
+
     @Test
     fun `source drift rejects native evidence without replacing its original snapshot`() {
         writePredicate("export function holds(value: number): boolean { return value === value; }")
@@ -234,6 +351,7 @@ class SymbolicInputReplayTest {
 
     private fun collector(
         deadline: WitnessReplayDeadline = WitnessReplayDeadline(timeoutMillis = 30_000),
+        validationReserveMillis: Long = 0,
     ): SymbolicInputReplayCollector {
         val property = property(exportName = "holds").copy(
             predicate = TypeScriptEntryPoint(module = "predicate.ts", exportName = "holds"),
@@ -251,7 +369,7 @@ class SymbolicInputReplayTest {
             sources = sources,
             coverageRequest = PropertyCoverageRequest(admittedOnly = true),
             deadline = deadline,
-            validationReserveMillis = 0,
+            validationReserveMillis = validationReserveMillis,
             limit = 8,
         )
     }

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt

@@ -62,6 +62,24 @@ class UsvmPropertySearcher(
         deadlineReached: (() -> Boolean)? = null,
         coverageFeedback: UsvmCoverageFeedback? = null,
         completedInputLimit: Int = 0,
+    ): UsvmPropertySearchResult = search(
+        manifest = manifest,
+        mapping = mapping,
+        concreteCapability = concreteCapability,
+        deadlineReached = deadlineReached,
+        coverageFeedback = coverageFeedback,
+        completedInputLimit = completedInputLimit,
+        onCompletedInput = null,
+    )
+
+    fun search(
+        manifest: PropertyManifest,
+        mapping: PropertyEtsMappingArtifact,
+        concreteCapability: ProjectionCapability,
+        deadlineReached: (() -> Boolean)?,
+        coverageFeedback: UsvmCoverageFeedback?,
+        completedInputLimit: Int,
+        onCompletedInput: ((UsvmCompletedInput) -> Unit)?,
     ): UsvmPropertySearchResult {
         require(completedInputLimit >= 0) { "Completed input limit must not be negative" }
         val capability = capabilityResolver.resolve(
@@ -111,6 +129,7 @@ class UsvmPropertySearcher(
             deadlineReached = deadlineReached ?: this.deadlineReached,
             guidance = guidance,
             completedInputLimit = completedInputLimit,
+            onCompletedInput = onCompletedInput,
         ).copy(edgeGuidance = guidance?.snapshot())
     }
 
@@ -122,6 +141,7 @@ class UsvmPropertySearcher(
         deadlineReached: (() -> Boolean)?,
         guidance: UsvmEdgeGuidance?,
         completedInputLimit: Int,
+        onCompletedInput: ((UsvmCompletedInput) -> Unit)?,
     ): UsvmPropertySearchResult {
         lateinit var projection: UsvmDeclaredDomainProjection
         val completedInputs = linkedSetOf<UsvmCompletedInput>()
@@ -149,8 +169,9 @@ class UsvmPropertySearcher(
                 }
                 if (inputs != null) {
                     if (capture) {
-                        val expected = completedOutcome(violation)
-                        completedInputs += UsvmCompletedInput(inputs = inputs, expectedOutcome = expected)
+                        val input = UsvmCompletedInput(inputs = inputs, expectedOutcome = completedOutcome(violation))
+                        val added = completedInputs.add(input)
+                        if (added) onCompletedInput?.invoke(input)
                     }
                     guidance?.confirm(replayState, inputs, expectsViolation = violation != null)
                 }

usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt

@@ -10,6 +10,7 @@ import org.usvm.UMachineOptions
 import org.usvm.machine.TsOptions
 import org.usvm.ts.pbt.backend.ProjectionCapability
 import org.usvm.ts.pbt.backend.ProjectionLevel
+import org.usvm.ts.pbt.backend.WitnessOracleOutcome
 import org.usvm.ts.pbt.manifest.PropertyManifest
 import org.usvm.ts.pbt.mapping.PropertyEtsMapper
 import org.usvm.ts.pbt.model.ArrayDomain
@@ -355,6 +356,52 @@ class UsvmPropertySearcherTest {
         assertNull(result.inputs)
     }
 
+    @Test
+    fun `completed input validation can exhaust the caller budget before another path runs`() {
+        val manifest = manifest(predicateExport = "branchingValidProperty")
+        val captured = mutableListOf<UsvmCompletedInput>()
+        var deadlineReached = false
+
+        val result = searcher.search(
+            manifest = manifest,
+            mapping = mapper.map(manifest),
+            concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT),
+            deadlineReached = { deadlineReached },
+            coverageFeedback = null,
+            completedInputLimit = 8,
+            onCompletedInput = { input ->
+                captured += input
+                deadlineReached = true
+            },
+        )
+
+        assertEquals(UsvmPropertySearchStatus.TIMEOUT, result.status)
+        assertEquals(1, captured.size)
+        assertEquals(captured, result.completedInputs)
+        assertEquals(WitnessOracleOutcome.HOLDS, captured.single().expectedOutcome)
+        assertEquals(0, result.omittedCompletedInputs)
+    }
+
+    @Test
+    fun `disabled completed input capture never invokes validation`() {
+        val manifest = manifest(predicateExport = "branchingValidProperty")
+        val captured = mutableListOf<UsvmCompletedInput>()
+
+        val result = searcher.search(
+            manifest = manifest,
+            mapping = mapper.map(manifest),
+            concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT),
+            deadlineReached = null,
+            coverageFeedback = null,
+            completedInputLimit = 0,
+            onCompletedInput = { captured += it },
+        )
+
+        assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status)
+        assertTrue(captured.isEmpty())
+        assertTrue(result.completedInputs.isEmpty())
+    }
+
     private fun search(manifest: PropertyManifest): UsvmPropertySearchResult = searcher.search(
         manifest = manifest,
         mapping = mapper.map(manifest),

usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts

@@ -2,6 +2,12 @@ export function validProperty(value: number): boolean {
   return value === value;
 }
 
+export function branchingValidProperty(value: number): boolean {
+  if (value < 0) return true;
+
+  return value === value;
+}
+
 export function violatedProperty(value: number): boolean {
   return value !== 2;
 }