Preserve native PBT inputs at the generation deadline

usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts

@@ -79,6 +79,7 @@ export interface FastCheckExecutionRequest {
   replayPath?: string;
   numRuns: number;
   timeoutMillis: number;
+  generationTimeoutMillis?: number;
   examples: TaggedJsValue[][];
   observationRequest?: ObservationRequest;
   inputExportRequest?: InputExportRequest;
@@ -442,7 +443,7 @@ function buildParameters(
 
   const parameters: Parameters<[JsConcreteValue[]]> = {
     numRuns: request.numRuns,
-    interruptAfterTimeLimit: request.timeoutMillis,
+    interruptAfterTimeLimit: request.generationTimeoutMillis ?? request.timeoutMillis,
     markInterruptAsFailure: true,
     examples: decodedExamples,
   };
@@ -596,6 +597,13 @@ export function validateRequest(value: unknown): FastCheckExecutionRequest {
   if (request.tsconfig !== undefined && typeof request.tsconfig !== 'string') {
     throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'TypeScript config must be a path', 'tsconfig');
   }
+  const invalidGenerationTimeout = request.generationTimeoutMillis !== undefined
+    && (!Number.isInteger(request.generationTimeoutMillis) || (request.generationTimeoutMillis as number) < 1
+      || (request.generationTimeoutMillis as number) > (request.timeoutMillis as number));
+  if (invalidGenerationTimeout) {
+    throw protocolError(adapterDiagnostic.protocolRequestInvalid,
+      'Generation allowance must fit within the operation timeout', 'generationTimeoutMillis');
+  }
 
   if (request.seed !== undefined && !isSignedInt(request.seed)) {
     throw protocolError(
@@ -640,6 +648,7 @@ export function validateRequest(value: unknown): FastCheckExecutionRequest {
   if (request.tsconfig !== undefined) validated.tsconfig = request.tsconfig as string;
   if (request.seed !== undefined) validated.seed = request.seed as number;
   if (request.replayPath !== undefined) validated.replayPath = request.replayPath as string;
+  if (request.generationTimeoutMillis !== undefined) validated.generationTimeoutMillis = request.generationTimeoutMillis as number;
   if (request.admittedCoverage === true) validated.admittedCoverage = true;
   if (request.exactReplay === true) {
     if (request.numRuns !== 1 || examples.length !== 1 || request.replayPath !== undefined) {

usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts

@@ -10,10 +10,23 @@ import { installObservationHook, ObservationRecorder, type ObservationRequest }
 import { encodeJsValue, ProtocolError } from '../src/js-value.js';
 import {
   executeProperty,
+  validateRequest,
   type FastCheckExecutionRequest,
   type FastCheckRunResult,
 } from '../src/execute-property.js';
 
+test('private generation allowance must fit inside the operation timeout', () => {
+  const request = executionRequest('/unused', 'alwaysTrue');
+
+  for (const generationTimeoutMillis of [0, -1, 0.5, request.timeoutMillis + 1, Number.NaN]) {
+    assert.throws(() => validateRequest({ ...request, generationTimeoutMillis }), (error: unknown) =>
+      error instanceof ProtocolError && error.path === 'generationTimeoutMillis');
+  }
+
+  assert.equal(validateRequest({ ...request, generationTimeoutMillis: 1 }).generationTimeoutMillis, 1);
+  assert.equal(validateRequest(request).generationTimeoutMillis, undefined);
+});
+
 test('shrinking a named check does not switch to another violated check', async () => {
   await withPropertyModule(async (sourceRoot) => {
     await writeFile(path.join(sourceRoot, 'properties.ts'), `

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt

@@ -23,6 +23,7 @@ internal data class FastCheckExecutionRequest(
     val replayPath: String? = null,
     val numRuns: Int,
     val timeoutMillis: Long,
+    val generationTimeoutMillis: Long? = null,
     val examples: List<List<JsConcreteValue>> = emptyList(),
     val observationRequest: PropertyObservationRequest? = null,
     val inputExportRequest: PropertyInputExportRequest? = null,

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt

@@ -32,7 +32,6 @@ internal class FastCheckProcessClient(
         request: FastCheckExecutionRequest,
         remainingMillis: (() -> Long)? = null,
     ): PropertyRunResult {
-        val encodedRequest = encodeRequest(request)
         val coverageSession = request.coverageRequest?.let {
             if (remainingMillis == null) {
                 FastCheckCoverageSession.prepare(
@@ -59,8 +58,18 @@ internal class FastCheckProcessClient(
             val processBudget = remainingMillis?.invoke()?.coerceAtMost(phaseLimit) ?: phaseLimit
             if (processBudget <= 0) throw deadlineExpired(request, "Property campaign deadline expired")
 
+            // The existing transport grace must fit inside a caller-owned deadline, including startup and response I/O.
+            val generationRequest = if (remainingMillis == null) {
+                request
+            } else {
+                val generationBudgetMillis = (processBudget - transportGraceMillis).coerceAtLeast(minimumValue = 1)
+                request.copy(
+                    timeoutMillis = minOf(request.timeoutMillis, processBudget),
+                    generationTimeoutMillis = minOf(request.timeoutMillis, generationBudgetMillis),
+                )
+            }
             val output = invokeAdapter(
-                encodedRequest = encodedRequest,
+                encodedRequest = encodeRequest(generationRequest),
                 request = request,
                 command = coverageSession?.adapterCommand
                     ?: listOf(nodeExecutable, adapterEntryPoint.toString()),

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

@@ -3,6 +3,7 @@ package org.usvm.ts.pbt.campaign
 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.PropertyFailureKind
 import org.usvm.ts.pbt.backend.PropertyRunConfiguration
 import org.usvm.ts.pbt.backend.PropertyRunStatus
 import org.usvm.ts.pbt.backend.WitnessReductionStatus
@@ -117,9 +118,10 @@ class GuidedPropertyCampaignTest {
             pbtAllocationMillis = 1_000,
         )
 
-        assertNull(artifact.result.concrete)
+        val concrete = artifact.result.concrete
+        if (concrete != null) assertEquals(PropertyFailureKind.TIMEOUT, concrete.failure?.kind)
         assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, artifact.result.symbolic?.status)
-        assertTrue(artifact.result.diagnostic?.contains("PBT allocation expired") == true)
+        assertTrue(artifact.result.diagnostic?.startsWith("PBT allocation") == true)
         assertEquals(PropertyCampaignStop.COMPLETED, artifact.result.stop)
     }
 

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckGenerationDeadlineTest.kt

@@ -0,0 +1,56 @@
+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.PropertyFailureKind
+import org.usvm.ts.pbt.backend.PropertyInputExportRequest
+import org.usvm.ts.pbt.backend.PropertyRunConfiguration
+import org.usvm.ts.pbt.backend.WitnessReplayDeadline
+import org.usvm.ts.pbt.model.IntegerDomain
+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.security.MessageDigest
+import kotlin.test.assertEquals
+import kotlin.test.assertNotNull
+import kotlin.test.assertTrue
+
+class FastCheckGenerationDeadlineTest {
+    @Test
+    fun `budget-driven generation publishes retained native inputs before the transport deadline`() {
+        val root = testResourcesRoot()
+        val module = "properties/InputExportProperties.ts"
+        val hash = MessageDigest.getInstance("SHA-256").digest(Files.readAllBytes(root.resolve(module)))
+            .joinToString(separator = "") { "%02x".format(it.toInt() and 0xff) }
+        val property = PropertyDefinition(
+            id = PropertyId(value = "deadline.inputs"),
+            inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = -100, max = 100))),
+            predicate = TypeScriptEntryPoint(module = module, exportName = "holds"),
+        )
+        val configuration = PropertyRunConfiguration(
+            seed = 37,
+            numRuns = 1_000_000,
+            timeoutMillis = 5000,
+            coverageRequest = PropertyCoverageRequest(admittedOnly = true),
+            inputExportRequest = PropertyInputExportRequest(
+                sources = listOf(PropertyObservationSource(module = module, sha256 = hash)),
+            ),
+        )
+
+        val result = FastCheckBackend(sourceRoots = listOf(root)).run(
+            property = property,
+            configuration = configuration,
+            deadline = WitnessReplayDeadline(timeoutMillis = 5000),
+        )
+
+        val export = assertNotNull(result.inputExport)
+        assertEquals(PropertyFailureKind.TIMEOUT, result.failure?.kind)
+        assertTrue(export.records.size > 64)
+        assertEquals(result.numRuns + result.numSkips, export.records.size + export.droppedInvocations)
+        assertEquals(0, export.unsupportedInputs)
+    }
+}