Allow explicitly larger compact input exports without changing default bounds

usvm-ts-fast-check/fast-check-adapter/src/input-export.ts

@@ -88,7 +88,7 @@ export function validateInputExportRequest(value: unknown, manifest: PropertyMan
     && Number.isInteger(request.maxInvocations) && (request.maxInvocations as number) >= 1
     && (request.maxInvocations as number) <= 100_000
     && Number.isInteger(request.maxBytes) && (request.maxBytes as number) >= 1024
-    && (request.maxBytes as number) <= 2 * 1024 * 1024
+    && (request.maxBytes as number) <= 64 * 1024 * 1024
     && Number.isInteger(request.maxArrayElements) && (request.maxArrayElements as number) >= 1
     && (request.maxArrayElements as number) <= 64 && Array.isArray(request.sources);
   if (!valid) throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid input export bounds', 'inputExportRequest');

usvm-ts-fast-check/fast-check-adapter/test/input-export.test.ts

@@ -6,6 +6,7 @@ import path from 'node:path';
 import test from 'node:test';
 import { executeProperty } from '../src/execute-property.js';
 import { ProtocolError } from '../src/js-value.js';
+import { validateInputExportRequest } from '../src/input-export.js';
 
 const source = `export async function delayed(value: number): Promise<boolean> {
   await new Promise(resolve => setTimeout(resolve, 100)); return true;
@@ -14,7 +15,7 @@ const source = `export async function delayed(value: number): Promise<boolean> {
 function request(sourceRoot: string) {
   return {
     manifest: { propertyId: 'input.late', inputs: [{ name: 'value', domain: { kind: 'integer', min: 0, max: 1 } }],
-      predicate: { module: 'properties.ts', exportName: 'delayed', executionKind: 'async' } },
+      predicate: { module: 'properties.ts', exportName: 'delayed', executionKind: 'async' as const } },
     sourceRoots: [sourceRoot], seed: 37, numRuns: 1, timeoutMillis: 10, examples: [],
     inputExportRequest: { sources: [{ module: 'properties.ts', sha256: createHash('sha256').update(source).digest('hex') }],
       maxInvocations: 100, maxBytes: 65_536, maxArrayElements: 16 },
@@ -41,7 +42,7 @@ test('a late asynchronous outcome cannot rewrite the already published input rec
 
 test('input export rejects invalid wire bounds and source identities before loading the property', async () => {
   const invalid = [
-    { ...request('/missing').inputExportRequest, maxBytes: 2 * 1024 * 1024 + 1 },
+    { ...request('/missing').inputExportRequest, maxBytes: 64 * 1024 * 1024 + 1 },
     { ...request('/missing').inputExportRequest, maxInvocations: 100_001 },
     { ...request('/missing').inputExportRequest, sources: [null] },
     { ...request('/missing').inputExportRequest, sources: [{ module: 'other.ts', sha256: '0'.repeat(64) }] },
@@ -51,3 +52,11 @@ test('input export rejects invalid wire bounds and source identities before load
       error => error instanceof ProtocolError && error.code === 'protocol.request.invalid');
   }
 });
+
+test('explicit large input export remains bounded without changing the ordinary byte allowance', () => {
+  const ordinary = request('/unused');
+  const large = { ...ordinary.inputExportRequest, maxBytes: 64 * 1024 * 1024 };
+
+  assert.equal(validateInputExportRequest(large, ordinary.manifest).maxBytes, 64 * 1024 * 1024);
+  assert.equal(validateInputExportRequest(ordinary.inputExportRequest, ordinary.manifest).maxBytes, 65_536);
+});

usvm-ts-fast-check/scripts/pbt_experiment.py

@@ -81,9 +81,9 @@ def validate_manifest(manifest):
         raise ValueError("PBT, runner validation and class replay allocations must fit the total budget")
     valid_limits = manifest["numRuns"] > 0 and 0 < manifest["pbtInputLimit"] <= 100_000 \
         and manifest["symbolicInputLimit"] > 0 and 1 <= manifest["maxArrayElements"] <= 64 \
-        and 1024 <= manifest["maxObservationBytes"] <= 2 * 1024 * 1024
+        and 1024 <= manifest["maxObservationBytes"] <= 64 * 1024 * 1024
     if not valid_limits:
-        raise ValueError("Frozen limits must fit the compact export's 100000-record/64-element/2MiB contract")
+        raise ValueError("Frozen limits must fit the compact export's 100000-record/64-element/64MiB contract")
     unique_cases = manifest["cases"] and len({case["id"] for case in manifest["cases"]}) == len(manifest["cases"])
     if not unique_cases:
         raise ValueError("The manifest must contain distinct case identities")

usvm-ts-fast-check/scripts/test_pbt_experiment.py

@@ -152,6 +152,18 @@ def test_functional_quota_and_early_success_are_not_full_budget_results(self):
         self.assertTrue(driver.full_budget_eligible(row))
 
 
+    def test_budget_driven_quota_is_independent_of_the_explicit_large_capture_limit(self):
+        manifest = driver.read_json(ROOT.parent / "experiments/two-phase-smoke/manifest.json")
+        manifest.update(comparisonKind="equal-budget", numRuns=1_000_000,
+                        pbtInputLimit=100_000, maxObservationBytes=64 * 1024 * 1024)
+
+        driver.validate_manifest(manifest)
+
+        manifest["maxObservationBytes"] += 1
+        with self.assertRaisesRegex(ValueError, "64MiB"):
+            driver.validate_manifest(manifest)
+
+
     def test_process_timeout_retains_raw_output_and_failure(self):
         process = driver.run_process(
             ["node", "-e", "process.stdout.write('started'); setInterval(() => {}, 1000)"], self.root, "slow", 0.2,

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

@@ -2,6 +2,7 @@ package org.usvm.ts.pbt.fastcheck
 
 import kotlinx.serialization.decodeFromString
 import org.usvm.ts.pbt.FastCheckDiagnosticCode
+import org.usvm.ts.pbt.backend.PropertyInputExportRequest
 import org.usvm.ts.pbt.backend.PropertyRunResult
 import org.usvm.ts.pbt.manifest.PropertyManifestJson
 import org.usvm.ts.pbt.model.JsConcreteValue
@@ -19,10 +20,22 @@ internal class FastCheckProcessClient(
     private val transportGraceMillis: Long = DEFAULT_TRANSPORT_GRACE_MILLIS,
     private val shutdownGraceMillis: Long = DEFAULT_SHUTDOWN_GRACE_MILLIS,
 ) {
-    private val transport = FastCheckProcessTransport(
+    private val defaultTransport = createTransport(maxStdoutBytes = MAX_STDOUT_BYTES)
+
+    private fun transport(request: FastCheckExecutionRequest): FastCheckProcessTransport {
+        val requestedBytes = request.inputExportRequest?.maxBytes ?: PropertyInputExportRequest.DEFAULT_MAX_BYTES
+        val additionalExportBytes = (requestedBytes - PropertyInputExportRequest.DEFAULT_MAX_BYTES)
+            .coerceAtLeast(minimumValue = 0)
+
+        if (additionalExportBytes == 0) return defaultTransport
+
+        return createTransport(maxStdoutBytes = MAX_STDOUT_BYTES + additionalExportBytes)
+    }
+
+    private fun createTransport(maxStdoutBytes: Int) = FastCheckProcessTransport(
         nodeExecutable = nodeExecutable,
         maxRequestBytes = MAX_REQUEST_BYTES,
-        maxStdoutBytes = MAX_STDOUT_BYTES,
+        maxStdoutBytes = maxStdoutBytes,
         maxStderrBytes = MAX_STDERR_BYTES,
         shutdownGraceMillis = shutdownGraceMillis,
     )
@@ -179,7 +192,7 @@ internal class FastCheckProcessClient(
         command: List<String>,
         timeoutMillis: Long,
     ): FastCheckOperationResult<FastCheckProcessOutput> = try {
-        transport.invokeWithResult(
+        transport(request).invokeWithResult(
             command = command,
             request = encodedRequest,
             timeoutMillis = timeoutMillis,
@@ -202,7 +215,7 @@ internal class FastCheckProcessClient(
         command: List<String>,
         timeoutMillis: Long = saturatedAdd(request.timeoutMillis, transportGraceMillis),
     ): FastCheckProcessOutput = try {
-        transport.invoke(
+        transport(request).invoke(
             command = command,
             request = encodedRequest,
             timeoutMillis = timeoutMillis,

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

@@ -68,7 +68,9 @@ class GuidedPropertyCampaignTest {
         val configuration = configuration.copy(
             examples = examples(1),
             inputExportRequest = PropertyInputExportRequest(
-                sources = listOf(PropertyObservationSource(module = MODULE, sha256 = campaignSourceSha256(root.resolve(MODULE)))),
+                sources = listOf(
+                    PropertyObservationSource(module = MODULE, sha256 = campaignSourceSha256(root.resolve(MODULE)))
+                ),
             ),
         )
 
@@ -79,10 +81,12 @@ class GuidedPropertyCampaignTest {
             pbtAllocationMillis = 15_000,
         )
 
-        assertEquals(1, artifact.result.concrete?.inputExport?.records?.size)
-        assertNull(artifact.result.concrete?.observations)
+        val concrete = assertNotNull(artifact.result.concrete)
+        assertEquals(1, concrete.inputExport?.records?.size)
+        assertNull(concrete.observations)
         assertNotNull(artifact.result.symbolic?.edgeGuidance)
-        assertTrue(assertNotNull(artifact.result.concrete?.coverage).provenance.request.admittedOnly)
+        val concreteCoverage = assertNotNull(concrete.coverage)
+        assertTrue(concreteCoverage.provenance.request.admittedOnly)
     }
 
     @Test

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

@@ -99,6 +99,45 @@ class FastCheckInputExportTest {
         assertEquals(text, firstInput.elements.single())
     }
 
+    @Test
+    fun `explicit large input export crosses the ordinary stdout limit without losing inputs`() {
+        val text = JsConcreteValue.String("x".repeat(n = 9000) + "\uD800")
+        val property = property(predicate = "textHolds", domain = ConstantDomain(value = text))
+        val requests = listOf(
+            PropertyInputExportRequest(sources = sources),
+            PropertyInputExportRequest(sources = sources, maxBytes = 8 * 1024 * 1024),
+        )
+
+        val results = requests.map { request ->
+            backend.run(
+                property,
+                configuration.copy(
+                    numRuns = 600,
+                    inputExportRequest = request,
+                    observationRequest = PropertyObservationRequest(points = emptyList(), sources = sources),
+                    coverageRequest = PropertyCoverageRequest(admittedOnly = true),
+                ),
+            )
+        }
+
+        val ordinary = assertNotNull(results[0].inputExport)
+        val large = assertNotNull(results[1].inputExport)
+        val encodedBytes = PropertyManifestJson.json.encodeToUtf8SafeString(large).toByteArray(Charsets.UTF_8).size
+        assertEquals(2 * 1024 * 1024, requests[0].maxBytes)
+        assertEquals(PropertyRunStatus.SUCCESS, results[1].status)
+        assertEquals(600, large.records.size)
+        assertTrue(encodedBytes > 4 * 1024 * 1024)
+        assertTrue(encodedBytes <= requests[1].maxBytes)
+        assertTrue(ordinary.droppedInvocations > 0)
+        assertEquals(0, large.droppedInvocations)
+        assertEquals(0, large.unsupportedInputs)
+        assertEquals(0, large.pendingInvocations)
+        assertNotNull(results[1].coverage)
+        assertNotNull(results[1].observations)
+        val firstInput = large.records.first().input.value as JsConcreteValue.Array
+        assertEquals(text, firstInput.elements.single())
+    }
+
     @Test
     fun `UTF16 and array inputs survive the actual process and artifact roundtrip`() {
         val values = JsConcreteValue.Array(listOf(JsConcreteValue.String("\uD800"), JsConcreteValue.String("\uDC00")))

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyInputExport.kt

@@ -13,14 +13,19 @@ import org.usvm.ts.pbt.observation.PropertyObservationValue
 data class PropertyInputExportRequest(
     val sources: List<PropertyObservationSource>,
     val maxInvocations: Int = 20_000,
-    val maxBytes: Int = MAX_INPUT_EXPORT_BYTES,
+    val maxBytes: Int = DEFAULT_MAX_BYTES,
     val maxArrayElements: Int = MAX_INPUT_EXPORT_ARRAY_ELEMENTS,
 ) {
     init {
         require(maxInvocations in 1..MAX_INPUT_EXPORT_INVOCATIONS)
-        require(maxBytes in MIN_INPUT_EXPORT_BYTES..MAX_INPUT_EXPORT_BYTES)
+        require(maxBytes in MIN_INPUT_EXPORT_BYTES..MAX_BYTES)
         require(maxArrayElements in 1..MAX_INPUT_EXPORT_ARRAY_ELEMENTS)
     }
+
+    companion object {
+        const val DEFAULT_MAX_BYTES: Int = 2 * 1024 * 1024
+        const val MAX_BYTES: Int = 64 * 1024 * 1024
+    }
 }
 
 /** The input snapshot precedes precondition and predicate mutations. */
@@ -50,6 +55,5 @@ data class PropertyInputExportArtifact(
 }
 
 internal const val MIN_INPUT_EXPORT_BYTES = 1024
-internal const val MAX_INPUT_EXPORT_BYTES = 2 * 1024 * 1024
 internal const val MAX_INPUT_EXPORT_INVOCATIONS = 100_000
 internal const val MAX_INPUT_EXPORT_ARRAY_ELEMENTS = 64