[TS PBT] Persist direct campaign results with existing evidence

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

@@ -0,0 +1,49 @@
+package org.usvm.ts.pbt.campaign
+
+import kotlinx.serialization.Serializable
+import kotlinx.serialization.decodeFromString
+import org.usvm.ts.pbt.backend.PropertyRunConfiguration
+import org.usvm.ts.pbt.backend.WitnessRole
+import org.usvm.ts.pbt.manifest.PropertyManifestJson
+import org.usvm.ts.pbt.model.PropertyDefinition
+import org.usvm.ts.pbt.model.encodeToUtf8SafeString
+import java.nio.file.Files
+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.
+ * Existing source and tool identities remain in the property and result provenance; absent identities stay unknown.
+ */
+@Serializable
+data class PropertyCampaignArtifact(
+    val property: PropertyDefinition,
+    val configuration: PropertyRunConfiguration,
+    val validationReserveMillis: Long,
+    val result: PropertyCampaignResult,
+    val targetRole: WitnessRole = WitnessRole.PROPERTY,
+) {
+    init {
+        val resultProperties = listOfNotNull(
+            result.propertyId,
+            result.concrete?.propertyId,
+            result.symbolic?.propertyId,
+            result.confirmation?.candidate?.propertyId,
+        )
+        val sameProperty = resultProperties.all { it == property.id }
+        require(sameProperty) { "Campaign evidence belongs to another property" }
+        require(validationReserveMillis > 0) { "Validation reserve must be positive" }
+        require(targetRole == WitnessRole.PROPERTY) { "Direct controls search the original property" }
+    }
+
+    /** Writes this completed snapshot; failure leaves the caller's artifact available for another destination. */
+    fun write(path: Path) {
+        val json = PropertyManifestJson.json.encodeToUtf8SafeString(this)
+        Files.writeString(path, json)
+    }
+
+    companion object {
+        fun read(path: Path): PropertyCampaignArtifact =
+            PropertyManifestJson.json.decodeFromString(Files.readString(path))
+    }
+}

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

@@ -1,5 +1,6 @@
 package org.usvm.ts.pbt.campaign
 
+import kotlinx.serialization.Serializable
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.EtsIrGenerationTimeoutException
 import org.jacodb.ets.utils.EtsIrProvider
@@ -38,14 +39,18 @@ import java.security.MessageDigest
 import java.util.concurrent.CancellationException
 import kotlin.time.Duration.Companion.milliseconds
 
+@Serializable
 enum class PropertyCampaignMode { PBT_ONLY, SYMBOLIC_ONLY, SEQUENTIAL }
 
+@Serializable
 enum class PropertyCampaignPhase { PREPARATION, PBT, SYMBOLIC, CONFIRMATION }
 
 /** COMPLETED describes orchestration; inspect the retained engine results for unsupported or incomplete work. */
+@Serializable
 enum class PropertyCampaignStop { COMPLETED, DEADLINE, EXECUTION_FAILURE }
 
 /** Only native violations count as confirmed; symbolic inputs remain candidates until replay succeeds. */
+@Serializable
 data class PropertyCampaignResult(
     val propertyId: PropertyId,
     val mode: PropertyCampaignMode,
@@ -69,6 +74,18 @@ class PropertyCampaignRunner(
     private val nodeExecutable: String = "node",
     private val machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES),
 ) {
+    /** Captures the requested direct controls and their actual result without repeating execution. */
+    fun runArtifact(
+        property: PropertyDefinition,
+        mode: PropertyCampaignMode,
+        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,