[TS PBT] Record scoped campaign metadata and observed Node versions

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

@@ -31,6 +31,8 @@ import {
   type ObservationRequest,
 } from './observe-property.js';
 
+const runtimeVersion = process.version;
+
 export interface PropertyManifestInput {
   name: string;
   domain: unknown;
@@ -98,6 +100,7 @@ export interface FastCheckRunResult {
   numShrinks: number;
   failure: FastCheckFailureDetails | null;
   executionTimeMillis: number;
+  runtimeVersion: string;
   observations?: ObservationArtifact;
 }
 
@@ -433,6 +436,7 @@ function toRunResult(
     numShrinks: details.numShrinks,
     failure,
     executionTimeMillis,
+    runtimeVersion,
   };
   if (observations !== undefined) result.observations = observations;
 

usvm-ts-fast-check/fast-check-adapter/test/execution-cli.test.ts

@@ -25,6 +25,7 @@ test('execution CLI emits one successful response document', async () => {
     assert.equal(invocation.stderr, '');
     assert.equal(invocation.stdout.trim().split('\n').length, 1);
     assert.equal(response.status, 'ok');
+    assert.equal((response.result as Record<string, unknown>).runtimeVersion, process.version);
     assert.equal('protocolVersion' in response, false);
   } finally {
     await rm(sourceRoot, { recursive: true, force: true });
@@ -48,6 +49,7 @@ test('execution CLI keeps one JSON response after a predicate adds inherited toJ
     await writeFile(sourceRoot + '/property.ts', `
 export function predicate(value: boolean) {
   Object.prototype.toJSON = () => { throw new Error('sentinel toJSON'); };
+  Object.defineProperty(process, 'version', { value: 'changed-by-property' });
   return value;
 }
 `);
@@ -58,6 +60,7 @@ export function predicate(value: boolean) {
     assert.equal(invocation.exitCode, 0);
     assert.equal(invocation.stdout.trim().split('\n').length, 1);
     assert.equal(response.status, 'ok');
+    assert.equal((response.result as Record<string, unknown>).runtimeVersion, process.version);
   } finally {
     await rm(sourceRoot, { recursive: true, force: true });
   }

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

@@ -12,7 +12,8 @@ import java.nio.file.Path
 
 /**
  * The declared property and direct-run controls with the results actually produced.
- * Constructor settings such as machine options, runtime paths and tsconfig are not attested here.
+ * Metadata records selected files and requested runtime settings, with an explicit limited source scope.
+ * Effective machine options and complete project/build identities are not attested here.
  * Existing source and tool identities remain in the property and result provenance; absent identities stay unknown.
  */
 @Serializable
@@ -22,6 +23,7 @@ data class PropertyCampaignArtifact(
     val validationReserveMillis: Long,
     val result: PropertyCampaignResult,
     val targetRole: WitnessRole = WitnessRole.PROPERTY,
+    val metadata: PropertyCampaignMetadata? = null,
 ) {
     init {
         val resultProperties = listOfNotNull(

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

@@ -0,0 +1,40 @@
+package org.usvm.ts.pbt.campaign
+
+import kotlinx.serialization.Serializable
+import org.usvm.ts.pbt.observation.PropertyObservationSource
+import java.nio.file.Files
+import java.nio.file.Path
+import java.security.MessageDigest
+
+/** Files read before engine work; imports, automatically discovered configuration and build outputs are excluded. */
+@Serializable
+enum class PropertyCampaignSourceScope {
+    PROPERTY_ENTRY_MODULES,
+}
+
+/** One explicitly supplied concrete-runtime configuration file, without its extended configuration closure. */
+@Serializable
+data class PropertyCampaignTsconfig(
+    val path: String,
+    val sha256: String,
+)
+
+/**
+ * Requested execution settings and the selected files observed before any engine work.
+ * This is not a full project/build identity: machine options, imports and effective tsconfig are not recorded.
+ * Observed Node versions belong to the actual concrete run and witness replay results.
+ */
+@Serializable
+data class PropertyCampaignMetadata(
+    val sourceRoot: String,
+    val requestedNodeCommand: String,
+    val sources: List<PropertyObservationSource>,
+    val explicitConcreteTsconfig: PropertyCampaignTsconfig? = null,
+    val sourceScope: PropertyCampaignSourceScope = PropertyCampaignSourceScope.PROPERTY_ENTRY_MODULES,
+)
+
+internal fun campaignSourceSha256(path: Path): String = MessageDigest.getInstance("SHA-256")
+    .digest(Files.readAllBytes(path))
+    .joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and BYTE_MASK) }
+
+private const val BYTE_MASK = 0xff

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

@@ -33,9 +33,7 @@ import org.usvm.ts.pbt.usvm.UsvmPropertySearcher
 import org.usvm.ts.pbt.validation.requireValid
 import org.usvm.ts.pbt.validation.validatePropertyDefinition
 import java.io.IOException
-import java.nio.file.Files
 import java.nio.file.Path
-import java.security.MessageDigest
 import java.util.concurrent.CancellationException
 import kotlin.time.Duration.Companion.milliseconds
 
@@ -81,22 +79,12 @@ class PropertyCampaignRunner(
         configuration: PropertyRunConfiguration = PropertyRunConfiguration(),
         validationReserveMillis: Long = DEFAULT_VALIDATION_RESERVE_MILLIS,
     ): PropertyCampaignArtifact {
-        val result = run(property, mode, configuration, validationReserveMillis)
-
-        return PropertyCampaignArtifact(property, configuration, validationReserveMillis, result)
-    }
-
-    fun run(
-        property: PropertyDefinition,
-        mode: PropertyCampaignMode,
-        configuration: PropertyRunConfiguration = PropertyRunConfiguration(),
-        validationReserveMillis: Long = DEFAULT_VALIDATION_RESERVE_MILLIS,
-    ): PropertyCampaignResult {
         require(validationReserveMillis > 0) { "Validation reserve must be positive" }
         val startedAt = System.nanoTime()
         val deadline = WitnessReplayDeadline(timeoutMillis = configuration.timeoutMillis)
         requireValid(validatePropertyDefinition(property))
 
+        var metadata: PropertyCampaignMetadata? = null
         var phase = PropertyCampaignPhase.PREPARATION
         var concrete: PropertyRunResult? = null
         var symbolic: UsvmPropertySearchResult? = null
@@ -105,39 +93,46 @@ class PropertyCampaignRunner(
         fun result(
             stop: PropertyCampaignStop = PropertyCampaignStop.COMPLETED,
             diagnostic: String? = null,
-        ) = PropertyCampaignResult(
-            propertyId = property.id,
-            mode = mode,
-            concrete = concrete,
-            symbolic = symbolic,
-            confirmation = confirmation,
-            stop = stop,
-            stoppedAt = phase.takeUnless { stop == PropertyCampaignStop.COMPLETED },
-            elapsedMillis = (System.nanoTime() - startedAt) / NANOS_PER_MILLISECOND,
-            diagnostic = diagnostic,
+        ) = PropertyCampaignArtifact(
+            property = property,
+            configuration = configuration,
+            validationReserveMillis = validationReserveMillis,
+            result = PropertyCampaignResult(
+                propertyId = property.id,
+                mode = mode,
+                concrete = concrete,
+                symbolic = symbolic,
+                confirmation = confirmation,
+                stop = stop,
+                stoppedAt = phase.takeUnless { stop == PropertyCampaignStop.COMPLETED },
+                elapsedMillis = (System.nanoTime() - startedAt) / NANOS_PER_MILLISECOND,
+                diagnostic = diagnostic,
+            ),
+            metadata = metadata,
         )
 
         try {
             val root = sourceRoot.toRealPath()
-            val roots = listOf(root)
-            val backend = FastCheckBackend(sourceRoots = roots, nodeExecutable = nodeExecutable, tsconfig = tsconfig)
+            if (deadline.remainingMillis() <= 0) return result(PropertyCampaignStop.DEADLINE)
+
+            metadata = captureMetadata(property = property, root = root)
+            if (deadline.remainingMillis() <= 0) return result(PropertyCampaignStop.DEADLINE)
+
+            val backend = FastCheckBackend(listOf(root), nodeExecutable = nodeExecutable, tsconfig = tsconfig)
             if (deadline.remainingMillis() <= 0) return result(PropertyCampaignStop.DEADLINE)
 
             if (mode != PropertyCampaignMode.SYMBOLIC_ONLY) {
                 phase = PropertyCampaignPhase.PBT
                 concrete = backend.run(property = property, configuration = configuration, deadline = deadline)
 
-                val coverageTimedOut = concrete.coverage?.diagnostics?.any { diagnostic ->
-                    diagnostic.code == FastCheckDiagnosticCode.COVERAGE_COLLECTION_TIMEOUT
-                } == true
+                val coverageTimedOut = coverageCollectionTimedOut(concrete)
                 if (coverageTimedOut || deadline.remainingMillis() <= 0) {
                     return result(
                         stop = PropertyCampaignStop.DEADLINE,
                         diagnostic = "Concrete result retained after the campaign or coverage collection timed out",
                     )
                 }
-                val concreteViolation = concrete.failure?.kind == PropertyFailureKind.PROPERTY
-                if (concreteViolation) return result()
+                if (concrete.failure?.kind == PropertyFailureKind.PROPERTY) return result()
                 if (concrete.failure?.kind == PropertyFailureKind.TIMEOUT) {
                     return result(PropertyCampaignStop.DEADLINE)
                 }
@@ -216,6 +211,32 @@ class PropertyCampaignRunner(
         }
     }
 
+    fun run(
+        property: PropertyDefinition,
+        mode: PropertyCampaignMode,
+        configuration: PropertyRunConfiguration = PropertyRunConfiguration(),
+        validationReserveMillis: Long = DEFAULT_VALIDATION_RESERVE_MILLIS,
+    ): PropertyCampaignResult = runArtifact(property, mode, configuration, validationReserveMillis).result
+
+    private fun captureMetadata(property: PropertyDefinition, root: Path): PropertyCampaignMetadata {
+        val explicitTsconfig = tsconfig?.toRealPath()
+        val configuration = explicitTsconfig?.let { path ->
+            PropertyCampaignTsconfig(path = path.toString(), sha256 = campaignSourceSha256(path))
+        }
+
+        return PropertyCampaignMetadata(
+            sourceRoot = root.toString(),
+            requestedNodeCommand = nodeExecutable,
+            sources = captureSources(property = property, root = root),
+            explicitConcreteTsconfig = configuration,
+        )
+    }
+
+    private fun coverageCollectionTimedOut(result: PropertyRunResult): Boolean =
+        result.coverage?.diagnostics?.any { diagnostic ->
+            diagnostic.code == FastCheckDiagnosticCode.COVERAGE_COLLECTION_TIMEOUT
+        } == true
+
     private fun loadScene(root: Path, timeoutMillis: Long): EtsScene {
         val directory = generateEtsIR(
             keepPartialOutputOnFailure = false,
@@ -267,17 +288,12 @@ class PropertyCampaignRunner(
             val path = root.resolve(module).toRealPath()
             require(path.startsWith(root)) { "Property module escapes its source root: $module" }
 
-            val hash = MessageDigest.getInstance("SHA-256")
-                .digest(Files.readAllBytes(path))
-                .joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and BYTE_MASK) }
-
-            PropertyObservationSource(module = module, sha256 = hash)
+            PropertyObservationSource(module = module, sha256 = campaignSourceSha256(path))
         }
     }
 
     private companion object {
         const val DEFAULT_VALIDATION_RESERVE_MILLIS = 5_000L
         const val NANOS_PER_MILLISECOND = 1_000_000L
-        const val BYTE_MASK = 0xff
     }
 }