[TS PBT] Compose campaign artifacts and existing edge guidance

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt

@@ -330,13 +330,6 @@ class DslPropertyRunner(sourceRoots: List<Path>) {
         }.toList()
     }
 
-    private fun remainingBudget(deadline: WitnessReplayDeadline): Long {
-        val remaining = deadline.remainingMillis()
-        check(remaining > 0) { "Property execution deadline expired" }
-
-        return remaining
-    }
-
     private fun resolveModule(module: String, directory: Path): String {
         val modulePath = Path.of(module)
         val normalized = !modulePath.isAbsolute && '\\' !in module &&

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

@@ -1,9 +1,9 @@
 package org.usvm.ts.pbt.fastcheck
 
 import org.usvm.ts.pbt.FastCheckDiagnosticCode
+import org.usvm.ts.pbt.backend.CoverageDiagnostic
 import org.usvm.ts.pbt.backend.ExternalWitnessBackend
 import org.usvm.ts.pbt.backend.ExternalWitnessCandidate
-import org.usvm.ts.pbt.backend.CoverageDiagnostic
 import org.usvm.ts.pbt.backend.PropertyBasedTestingBackend
 import org.usvm.ts.pbt.backend.PropertyCoverageCapability
 import org.usvm.ts.pbt.backend.PropertyRunConfiguration

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/KotlinPropertyDslTest.kt

@@ -239,7 +239,7 @@ class KotlinPropertyDslTest {
         "elapsedMillis=$elapsedMillis, budgetMillis=$budgetMillis, " +
             "symbolicSkippedDueToDeadline=$symbolicSkippedDueToDeadline, symbolicStatus=${symbolic?.status}, " +
             "concreteStatus=${concrete?.status}, replayStatus=${symbolicReplay?.status}, " +
-            "replayFailure=${symbolicReplay?.failure}"
+            "replayFailure=${symbolicReplay?.originalReplay?.failure}"
 
     private fun addition(exportName: String): DslProperty = defineProperty(id = "calculator.$exportName") {
         val sum = function<(Double, Double) -> Double>(module = "calculator.ts", exportName = exportName)

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/PbtEdgeGuidanceTest.kt

@@ -119,7 +119,7 @@ class PbtEdgeGuidanceTest {
         assertTrue(trace.selections.isNotEmpty())
         assertTrue(trace.selections.all { it.goal == null && it.originalObjectiveTurn })
         assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, run.symbolic?.status)
-        assertEquals("original", run.symbolicReplay?.failure?.checkId)
+        assertEquals("original", run.symbolicReplay?.originalReplay?.failure?.checkId)
     }
 
     private fun positiveResult(exportName: String): DslProperty = defineProperty(id = "edge-guidance.$exportName") {

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/RuntimeLimitationDslTest.kt

@@ -3,6 +3,7 @@ package org.usvm.ts.pbt.dsl
 import org.junit.jupiter.api.Test
 import org.usvm.ts.pbt.backend.PropertyRunConfiguration
 import org.usvm.ts.pbt.backend.PropertyRunStatus
+import org.usvm.ts.pbt.backend.WitnessReplayStatus
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.testResourcesRoot
 import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus
@@ -44,7 +45,10 @@ class RuntimeLimitationDslTest {
     @Test
     fun `supported counterexample and its native replay survive an excluded path`() {
         val program = defineProperty(id = "runtime.mixed-counterexample") {
-            val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
+            val write = function<(Double) -> Double>(
+                module = "runtime-limitations.ts",
+                exportName = "supportedOrSparse",
+            )
             val index by int(min = 0, max = 2)
 
             check(name = "zero") { write(index) equalTo 0 }
@@ -56,15 +60,18 @@ class RuntimeLimitationDslTest {
         assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, symbolic.status)
         assertEquals(listOf(JsConcreteValue.number(0.0)), symbolic.inputs)
         assertTrue(symbolic.diagnostics.any { it.code == "usvm.runtime.array-index-growth" })
-        assertEquals(PropertyRunStatus.FAILURE, run.symbolicReplay?.status)
-        assertEquals("zero", run.symbolicReplay?.failure?.checkId)
+        assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, run.symbolicReplay?.status)
+        assertEquals("zero", run.symbolicReplay?.originalReplay?.failure?.checkId)
         assertFailsWith<DslPropertyAssertionError> { run.requireSuccess() }
     }
 
     @Test
     fun `supported successful paths do not hide excluded model paths`() {
         val program = defineProperty(id = "runtime.mixed-no-violation") {
-            val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
+            val write = function<(Double) -> Double>(
+                module = "runtime-limitations.ts",
+                exportName = "supportedOrSparse",
+            )
             val index by int(min = 0, max = 2)
 
             check(name = "positive") { write(index) greaterThan 0 }

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

@@ -1,5 +1,6 @@
 package org.usvm.ts.pbt.usvm
 
+import kotlinx.serialization.Serializable
 import org.usvm.ts.pbt.backend.PropertyCoverageArtifact
 import org.usvm.ts.pbt.backend.PropertyRunResult
 import org.usvm.ts.pbt.model.JsConcreteValue
@@ -11,6 +12,7 @@ data class UsvmCoverageFeedback(
 )
 
 /** Why a report can or cannot supply exact coverage goals for this property/source snapshot. */
+@Serializable
 enum class UsvmCoverageEvidenceStatus {
     ABSENT,
     STALE,
@@ -21,6 +23,7 @@ enum class UsvmCoverageEvidenceStatus {
 }
 
 /** Distinguishes a CFG edge from either of its endpoint statements. */
+@Serializable
 data class UsvmCoverageEdge(
     val method: String,
     val conditionIndex: Int,
@@ -29,6 +32,7 @@ data class UsvmCoverageEdge(
 )
 
 /** A real queue decision made during the original predicate analysis. */
+@Serializable
 data class UsvmEdgeSelection(
     val evidenceRevision: Int,
     val stateId: UInt,
@@ -41,6 +45,7 @@ data class UsvmEdgeSelection(
 )
 
 /** Concrete confirmation outcomes; none except CONFIRMED can add edges. */
+@Serializable
 enum class UsvmEdgeReplayStatus {
     CONFIRMED,
     EDGE_MISMATCH,
@@ -50,6 +55,7 @@ enum class UsvmEdgeReplayStatus {
 }
 
 /** A bounded exact-input native replay and its effect on the shared edge set. */
+@Serializable
 data class UsvmEdgeReplay(
     val inputs: List<JsConcreteValue>,
     val status: UsvmEdgeReplayStatus,
@@ -59,6 +65,7 @@ data class UsvmEdgeReplay(
 )
 
 /** Bounded history; symbolic reachability never updates [confirmedCovered]. */
+@Serializable
 data class UsvmEdgeGuidanceTrace(
     val evidenceStatus: UsvmCoverageEvidenceStatus,
     val initialCovered: Set<UsvmCoverageEdge>,

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

@@ -18,6 +18,7 @@ import org.usvm.ts.pbt.backend.PropertyRunStatus
 import org.usvm.ts.pbt.coverage.captureCoverageIdentity
 import org.usvm.ts.pbt.manifest.PropertyManifest
 import org.usvm.ts.pbt.mapping.EtsBranchArmTarget
+import org.usvm.ts.pbt.mapping.EtsCoverageMapping
 import org.usvm.ts.pbt.mapping.EtsMappingStatus
 import org.usvm.ts.pbt.mapping.PropertyEtsMapper
 import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact
@@ -54,57 +55,57 @@ internal class UsvmEdgeGuidance(
     private val initialGoals: Set<UsvmCoverageEdge>
 
     init {
-        val coverage = feedback.initialCoverage
-        evidenceStatus = evidenceStatus(coverage)
-        val usable = evidenceStatus == UsvmCoverageEvidenceStatus.EXACT ||
-            evidenceStatus == UsvmCoverageEvidenceStatus.PARTIAL
-        if (usable) {
-            val evidence = exactEdges(requireNotNull(coverage))
-            evidence.forEach { (edge, target, hits) ->
-                targets[edge] = target
-                if (hits > 0) covered += edge
-            }
+        val evidence = evaluateEvidence(feedback.initialCoverage)
+        evidenceStatus = evidence.status
+        evidence.edges.forEach { (edge, target, hits) ->
+            targets[edge] = target
+            if (hits > 0) covered += edge
         }
         initialCovered = covered.toSet()
         initialGoals = pendingGoals()
     }
 
-    private fun evidenceStatus(coverage: PropertyCoverageArtifact?): UsvmCoverageEvidenceStatus {
+    private fun evaluateEvidence(coverage: PropertyCoverageArtifact?): CoverageEvidence {
         if (!selectionSupported) {
             diagnostics += "Edge scheduling does not support state merging or selector loop bounds; " +
                 "original selection retained"
-            return UsvmCoverageEvidenceStatus.UNSUPPORTED
+            return CoverageEvidence(status = UsvmCoverageEvidenceStatus.UNSUPPORTED)
         }
-        if (coverage == null) return UsvmCoverageEvidenceStatus.ABSENT
+        if (coverage == null) return CoverageEvidence(status = UsvmCoverageEvidenceStatus.ABSENT)
         if (!coverage.provenance.request.admittedOnly || coverage.identity == null) {
-            return UsvmCoverageEvidenceStatus.UNSUPPORTED
+            return CoverageEvidence(status = UsvmCoverageEvidenceStatus.UNSUPPORTED)
         }
         val stale = coverage.identity != identity || coverage.propertyId.value != manifest.propertyId ||
             coverage.diagnostics.any { it.code == "coverage.source.stale" }
-        if (stale) return UsvmCoverageEvidenceStatus.STALE
-        if (coverage.admittedInvocations == null) return UsvmCoverageEvidenceStatus.UNSUPPORTED
-        if (coverage.admittedInvocations == 0) return UsvmCoverageEvidenceStatus.NO_ADMITTED_INPUTS
+        if (stale) return CoverageEvidence(status = UsvmCoverageEvidenceStatus.STALE)
+        if (coverage.admittedInvocations == null) {
+            return CoverageEvidence(status = UsvmCoverageEvidenceStatus.UNSUPPORTED)
+        }
+        if (coverage.admittedInvocations == 0) {
+            return CoverageEvidence(status = UsvmCoverageEvidenceStatus.NO_ADMITTED_INPUTS)
+        }
 
         val mapped = mapper().map(manifest, coverage).coverage
-        val exact = exactEdges(coverage)
+        val exact = exactEdges(mapped)
         val mappingDiagnostics = mapped.diagnostics + mapped.branches.flatMap { branch ->
             branch.mapping.diagnostics + branch.arms.flatMap { it.mapping.diagnostics }
         }
         diagnostics += mappingDiagnostics.map { "${it.code}: ${it.message}" }.distinct()
-        if (exact.isEmpty()) return UsvmCoverageEvidenceStatus.UNSUPPORTED
+        if (exact.isEmpty()) return CoverageEvidence(status = UsvmCoverageEvidenceStatus.UNSUPPORTED)
 
         val unknownBranches = mapped.branches.any { it.mapping.status != EtsMappingStatus.EXACT }
-        return if (unknownBranches || mapped.diagnostics.isNotEmpty()) {
+        val status = if (unknownBranches || mapped.diagnostics.isNotEmpty()) {
             UsvmCoverageEvidenceStatus.PARTIAL
         } else {
             UsvmCoverageEvidenceStatus.EXACT
         }
+        return CoverageEvidence(status = status, edges = exact)
     }
 
     private fun mapper() = PropertyEtsMapper(scene = scene, sourceRoots = roots)
 
-    private fun exactEdges(coverage: PropertyCoverageArtifact): List<ObservedEdge> {
-        return mapper().map(manifest, coverage).coverage.branches.flatMap { branch ->
+    private fun exactEdges(mapped: EtsCoverageMapping): List<ObservedEdge> {
+        return mapped.branches.flatMap { branch ->
             val sourcePath = branch.location?.path
             if (sourcePath !in identity.sourceSha256) return@flatMap emptyList()
 
@@ -191,7 +192,8 @@ internal class UsvmEdgeGuidance(
             return ReplayDecision(status = UsvmEdgeReplayStatus.REJECTED_OR_INCOMPATIBLE)
         }
 
-        val observed = exactEdges(requireNotNull(coverage))
+        val mapped = mapper().map(manifest, requireNotNull(coverage)).coverage
+        val observed = exactEdges(mapped)
         val confirmed = observed.filter { it.hits > 0 }.mapTo(hashSetOf()) { it.edge }
         if (!confirmed.containsAll(claimed)) return ReplayDecision(status = UsvmEdgeReplayStatus.EDGE_MISMATCH)
 
@@ -259,6 +261,11 @@ internal class UsvmEdgeGuidance(
         elapsedMillis = started.elapsedNow().inWholeMilliseconds,
     )
 
+    private data class CoverageEvidence(
+        val status: UsvmCoverageEvidenceStatus,
+        val edges: List<ObservedEdge> = emptyList(),
+    )
+
     private data class ObservedEdge(val edge: UsvmCoverageEdge, val target: EtsBranchArmTarget, val hits: Long)
     private data class GoalDistance(val goal: UsvmCoverageEdge, val distance: Int)
     private data class ReplayDecision(

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

@@ -103,7 +103,7 @@ class UsvmPropertySearcher(
             predicate = predicate,
             precondition = precondition,
             capability = capability,
-            deadlineReached = deadlineReached,
+            deadlineReached = deadlineReached ?: this.deadlineReached,
             guidance = guidance,
         ).copy(edgeGuidance = guidance?.snapshot())
     }