[TS PBT] Keep complete bounded samples usable for relation guidance

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

@@ -67,6 +67,7 @@ interface InvocationRecord {
   input: ObservationValue;
   admission: 'pending' | 'admitted' | 'rejected' | 'threw';
   outcome: 'pending' | 'holds' | 'false' | 'threw' | 'skipped';
+  pointsTruncated: boolean;
   points: Array<Omit<ObservationPointRequest, 'id'> & {
     pointId: string;
     occurrence: number;
@@ -176,6 +177,7 @@ export class ObservationRecorder {
       admission: 'pending',
       outcome: 'pending',
       points: [],
+      pointsTruncated: false,
     };
     this.artifact.invocations.push(record);
     if (this.reservedArtifactBytes() > this.request.maxBytes) {
@@ -207,6 +209,7 @@ export class ObservationRecorder {
     // Adapter entry snapshots and compiler callbacks own these points; public hooks cannot replace them.
     if (point?.kind === 'entry-argument' || point?.compilerLocal !== undefined) return;
     if (point === undefined) {
+      record.pointsTruncated = true;
       this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints);
 
       return;
@@ -217,6 +220,7 @@ export class ObservationRecorder {
 
   private capturePoint(record: InvocationRecord, point: ObservationPointRequest, value: unknown, unsupportedReason?: string): void {
     if (record.points.length >= this.request.maxPointsPerInvocation) {
+      record.pointsTruncated = true;
       this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints);
 
       return;
@@ -235,8 +239,10 @@ export class ObservationRecorder {
       eventOrdinal: record.points.length,
       value: unsupportedReason === undefined ? this.snapshot(value) : { status: 'unsupported', reason: unsupportedReason },
     });
+    if (record.points.at(-1)?.value.status === 'truncated') record.pointsTruncated = true;
     if (this.reservedArtifactBytes() > this.request.maxBytes) {
       record.points.pop();
+      record.pointsTruncated = true;
       this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints);
     }
   }

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

@@ -214,6 +214,7 @@ test('entry arguments are adapter snapshots before user code and cannot be repla
   assert.deepEqual(invocation.points.map((event) => event.occurrence), [0, 0]);
   assert.equal(recorder.result.buildStatus, 'unverified');
   assert.equal(recorder.result.droppedPoints, 0);
+  assert.equal(invocation.pointsTruncated, false);
 });
 
 test('observation limits report dropped invocations and points without changing returned values', () => {
@@ -245,6 +246,7 @@ test('observation limits report dropped invocations and points without changing
   assert.equal(recorder.result.invocations[0]?.input.status, 'captured');
   assert.equal(recorder.result.invocations[0]?.points[0]?.value.status, 'truncated');
   assert.equal(recorder.result.droppedPoints, 1);
+  assert.equal(recorder.result.invocations[0]?.pointsTruncated, true);
   assert.equal(recorder.result.droppedInvocations, 1);
 });
 
@@ -398,6 +400,7 @@ test('the complete observation artifact stays within edge budgets after outcomes
     assert.equal(artifact.invocations[0]?.outcome, 'skipped');
     assert.equal(artifact.droppedInvocations, 10);
     assert.ok(artifact.droppedPoints >= 10);
+    assert.equal(artifact.invocations[0]?.pointsTruncated, true);
     capturedPoints += artifact.invocations[0]?.points.length ?? 0;
   }
 

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

@@ -15,6 +15,8 @@ import org.usvm.ts.pbt.dsl.lessOrEqual
 import org.usvm.ts.pbt.inference.ScalarGuidanceExclusionReason
 import org.usvm.ts.pbt.inference.ScalarGuidanceRelevance
 import org.usvm.ts.pbt.inference.ScalarObservationPair
+import org.usvm.ts.pbt.inference.ScalarRelationLimitation
+import org.usvm.ts.pbt.inference.ScalarRelationStatus
 import org.usvm.ts.pbt.inference.ScalarRelationTemplate
 import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.PropertyAssertion
@@ -43,6 +45,44 @@ class PropertyRelationCampaignTest {
 
     private val configuration = PropertyRunConfiguration(seed = 42, numRuns = 8, timeoutMillis = 30_000)
 
+    @Test
+    fun `default one hundred PBT runs can challenge a relation from a bounded recorded sample`() {
+        val compiled = numericProperty(rareInput = 1_234_567_891, maximumInput = Int.MAX_VALUE)
+
+        val artifact = run(
+            compiled,
+            PropertyRelationGuidance.numericLocal(compiled),
+            numRuns = PropertyRunConfiguration().numRuns,
+        )
+        val file = root.resolve("bounded-campaign.json")
+        artifact.write(file)
+        val restored = PropertyCampaignArtifact.read(file)
+
+        val concrete = assertNotNull(restored.result.concrete)
+        val observations = assertNotNull(concrete.observations)
+        val trace = assertNotNull(restored.result.relationGuidance)
+        assertEquals(100, concrete.numRuns)
+        assertTrue(observations.droppedInvocations > 0 || observations.droppedPoints > 0)
+        val selection = assertNotNull(trace.selection)
+        val equality = selection.inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL }
+        assertTrue(equality.evidence.size >= 2)
+        assertTrue(equality.evidence.all { it.holds })
+        assertTrue(trace.attempts.isNotEmpty(), "Recorded relation: ${equality.status}, ${equality.limitations}")
+        val attempt = trace.attempts.single()
+        assertEquals(ScalarRelationStatus.SAMPLED, equality.status)
+        assertTrue(ScalarRelationLimitation.INCOMPLETE_CAPTURE in equality.limitations)
+        assertEquals(observations.droppedInvocations, selection.inference.droppedInvocations)
+        assertEquals(observations.droppedPoints, selection.inference.droppedPoints)
+        assertTrue(equality.evidence.all { it.invocation.pointsTruncated == false })
+        assertEquals(UsvmRelationRefutationStatus.REFUTATION_REACHED, attempt.searchStatus)
+        assertEquals(WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, attempt.confirmation?.status)
+        assertEquals(WitnessOracleOutcome.HOLDS, attempt.confirmation?.originalReplay?.outcome)
+        assertEquals(ObservationBuildStatus.UNVERIFIED, assertNotNull(trace.selection).inference.buildStatus)
+        assertTrue(trace.originalAllocatedMillis >= trace.originalReserveMillis)
+        assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, restored.result.symbolic?.status)
+        assertFalse(restored.result.confirmedViolation)
+    }
+
     @Test
     fun `one PBT snapshot challenges a sampled local equality and retains the unrestricted original search`() {
         val compiled = numericProperty()
@@ -223,21 +263,26 @@ class PropertyRelationCampaignTest {
         relationGuidance = guidance,
     )
 
-    private fun numericProperty(delta: String = "- 1", sparsePrefix: Boolean = false): CompiledDslProperty {
+    private fun numericProperty(
+        delta: String = "- 1",
+        sparsePrefix: Boolean = false,
+        rareInput: Int = 417,
+        maximumInput: Int = 1000,
+    ): CompiledDslProperty {
         val prefix = if (sparsePrefix) "const cache: number[] = []; cache[1001] = input;" else ""
         Files.writeString(
             root.resolve("functions.ts"),
             """
             export function transform(input: number): number {
                 $prefix
-                if (input === 417) return input $delta;
+                if (input === $rareInput) return input $delta;
                 return input;
             }
             """.trimIndent()
         )
         val program = defineProperty(id = "campaign.local-relation") {
             val transform = function<(Double) -> Double>(module = "functions.ts", exportName = "transform")
-            val input by int(min = 0, max = 1000)
+            val input by int(min = 0, max = maximumInput)
             val result by value(transform(input))
 
             check(name = "bound") { result lessOrEqual input }

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt

@@ -191,6 +191,21 @@ class EntryRelationRefutationTest {
         assertNull(refutation.inputs)
     }
 
+    @Test
+    fun `bounded native entry samples retain exact binding without bypassing original admission`() {
+        val inference = observe(predicate = "reflexive", precondition = "ordered", numRuns = 100)
+        val order = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL }
+
+        val refutation = refute(inference, order)
+
+        assertEquals(ScalarRelationStatus.SAMPLED, order.status)
+        assertTrue(ScalarRelationLimitation.INCOMPLETE_CAPTURE in order.limitations)
+        assertTrue(inference.droppedInvocations > 0)
+        assertEquals(EtsMappingStatus.EXACT, refutation.binding.status)
+        assertEquals(UsvmEntryRefutationStatus.PRECONDITION_REJECTED, refutation.status)
+        assertNull(refutation.inputs)
+    }
+
     private fun refute(inference: ScalarRelationInference, relation: ScalarRelation): UsvmEntryRelationRefutation {
         val manifest = inference.property.toManifest()
 
@@ -203,6 +218,7 @@ class EntryRelationRefutationTest {
         leftDomain: PropertyDomain = IntegerDomain(min = 0, max = 2),
         points: List<PropertyObservationPoint> = listOf(LEFT, RIGHT),
         seed: Int = 1,
+        numRuns: Int = 2,
     ): ScalarRelationInference {
         val property = PropertyDefinition(
             id = PropertyId("entry.auxiliary"),
@@ -226,7 +242,7 @@ class EntryRelationRefutationTest {
             property,
             PropertyRunConfiguration(
                 seed = seed,
-                numRuns = 2,
+                numRuns = numRuns,
                 observationRequest = PropertyObservationRequest(points = points, sources = sources),
             ),
         )

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt

@@ -18,6 +18,8 @@ import org.usvm.ts.pbt.observation.PropertyPointEvent
  * At least two distinct original admitted generation inputs and two observed value pairs are
  * required for sample agreement. Replay, shrinking and solver evidence can refute a relation,
  * but cannot increase independent support. Repeated points and nested contexts are unsupported.
+ * Recording limits bound the sample, not the PBT executions: only complete recorded pairs supply
+ * evidence. Omission and truncation warnings remain visible without claiming agreement on lost executions.
  *
  * Only selected module hashes are available for provenance; a declared predicate source hash
  * is checked when present. Executable build status is carried through without promotion.
@@ -85,6 +87,11 @@ private fun evaluatePair(
         limitations += ScalarRelationLimitation.INCOMPLETE_CAPTURE
     }
 
+    val unmarkedInvocation = observations.invocations.any { it.pointsTruncated == null }
+    val markedTruncation = observations.invocations.any { it.pointsTruncated == true }
+    val unattributedPointDrops = observations.droppedPoints > 0 && (unmarkedInvocation || !markedTruncation)
+    if (unattributedPointDrops) limitations += ScalarRelationLimitation.UNATTRIBUTED_POINT_DROPS
+
     val matched = if (validPair && sourcesPresent) {
         invocations.mapNotNull { invocation -> numericPair(invocation, pair, limitations) }
     } else {
@@ -119,7 +126,7 @@ private fun evaluatePair(
         val status = when {
             refuted -> ScalarRelationStatus.REFUTED
             matched.isEmpty() && unsupported -> ScalarRelationStatus.UNSUPPORTED
-            limitations.isNotEmpty() -> ScalarRelationStatus.INSUFFICIENT
+            limitations.any { !it.isSamplingWarning } -> ScalarRelationStatus.INSUFFICIENT
             else -> ScalarRelationStatus.SAMPLED
         }
 
@@ -145,26 +152,39 @@ private fun numericPair(
         return null
     }
 
+    val truncated = invocation.pointsTruncated == true || invocation.input.status == ObservationValueStatus.TRUNCATED
     val leftEvents = invocation.points.filter { it.pointId == pair.left.id }
     val rightEvents = invocation.points.filter { it.pointId == pair.right.id }
-    if (leftEvents.isEmpty() || rightEvents.isEmpty()) {
-        limitations += ScalarRelationLimitation.MISSING_POINT
-        return null
-    }
-    if (leftEvents.size != 1 || rightEvents.size != 1) {
+    if (leftEvents.size > 1 || rightEvents.size > 1) {
         limitations += ScalarRelationLimitation.REPEATED_POINT
         return null
     }
 
-    val left = leftEvents.single()
-    val right = rightEvents.single()
-    val identitiesMatch = left.matches(pair.left) && right.matches(pair.right)
+    val left = leftEvents.singleOrNull()
+    val right = rightEvents.singleOrNull()
+    val identitiesMatch = (left == null || left.matches(pair.left)) && (right == null || right.matches(pair.right))
     if (!identitiesMatch) {
         limitations += ScalarRelationLimitation.POINT_IDENTITY_MISMATCH
         return null
     }
-    val numeric = left.isNumber() && right.isNumber()
-    if (!numeric) {
+    val malformedValues = listOfNotNull(left, right).any { event ->
+        !event.isNumber() && !(truncated && event.value.status == ObservationValueStatus.TRUNCATED)
+    }
+    if (malformedValues) {
+        limitations += ScalarRelationLimitation.UNSUPPORTED_VALUE
+        return null
+    }
+    if (truncated) {
+        limitations += ScalarRelationLimitation.TRUNCATED_INVOCATION
+        return null
+    }
+    if (left == null || right == null) {
+        limitations += ScalarRelationLimitation.MISSING_POINT
+        return null
+    }
+    val inputCaptured = invocation.input.status == ObservationValueStatus.CAPTURED &&
+        invocation.input.value is JsConcreteValue.Array
+    if (!inputCaptured) {
         limitations += ScalarRelationLimitation.UNSUPPORTED_VALUE
         return null
     }

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt

@@ -48,6 +48,8 @@ enum class ScalarRelationLimitation {
     CONSTANT_OBSERVED_PAIR,
     INVOCATION_LIMIT,
     INCOMPLETE_CAPTURE,
+    TRUNCATED_INVOCATION,
+    UNATTRIBUTED_POINT_DROPS,
 }
 
 /** Exact same-invocation point values, retaining origin, phase, input and event identities. */
@@ -86,3 +88,16 @@ data class ScalarRelationInference(
     /** Sampled entry relations already implied by declared numeric input support, retained for audit. */
     val domainImpliedRelations: List<ScalarRelation> = emptyList(),
 )
+
+/** These warnings bound the observed sample; every other limitation blocks usable numeric support. */
+internal val ScalarRelationLimitation.isSamplingWarning: Boolean
+    get() = when (this) {
+        ScalarRelationLimitation.INVOCATION_LIMIT,
+        ScalarRelationLimitation.INCOMPLETE_CAPTURE,
+        ScalarRelationLimitation.TRUNCATED_INVOCATION,
+        -> true
+        else -> false
+    }
+
+internal fun ScalarRelation.hasSampledSupport(): Boolean =
+    status == ScalarRelationStatus.SAMPLED && limitations.all { it.isSamplingWarning }

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt

@@ -58,7 +58,7 @@ fun selectScalarGuidance(
         val known = original?.contains(relation.pair) == true
         val relevance = if (known) ScalarGuidanceRelevance.KNOWN_DSL_CHECK else ScalarGuidanceRelevance.UNKNOWN
         val duplicate = candidates.any { candidate -> candidate.relation.sameComparison(relation) }
-        val sampled = relation.status == ScalarRelationStatus.SAMPLED && relation.limitations.isEmpty()
+        val sampled = relation.hasSampledSupport()
         val restatesOriginal = known && original?.implies(relation) == true
         val reason = when {
             !sampled -> ScalarGuidanceExclusionReason.NOT_SAMPLED

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/observation/PropertyObservation.kt

@@ -189,6 +189,8 @@ data class PropertyInvocationObservation(
     val admission: ObservationAdmission,
     val outcome: ObservationOutcome,
     val points: List<PropertyPointEvent>,
+    /** Null for older producers; true means some point data was lost within this invocation. */
+    val pointsTruncated: Boolean? = null,
 )
 
 /** Optional artifact: unknown phase is not independent random evidence. */

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

@@ -8,7 +8,7 @@ import org.usvm.ts.pbt.dsl.CompiledDslProperty
 import org.usvm.ts.pbt.dsl.isReproducibleCompilerOutput
 import org.usvm.ts.pbt.inference.ScalarRelation
 import org.usvm.ts.pbt.inference.ScalarRelationInference
-import org.usvm.ts.pbt.inference.ScalarRelationStatus
+import org.usvm.ts.pbt.inference.hasSampledSupport
 import org.usvm.ts.pbt.inference.matches
 import org.usvm.ts.pbt.mapping.EtsEntryPointTarget
 import org.usvm.ts.pbt.mapping.EtsInputBinding
@@ -58,8 +58,7 @@ fun bindDslNumericLocalRelation(
             message = "The retained program must reproduce the compiler output"
         )
     }
-    val sampled = relation in inference.relations && relation.status == ScalarRelationStatus.SAMPLED &&
-        relation.limitations.isEmpty() && relation.evidence.isNotEmpty()
+    val sampled = relation in inference.relations && relation.hasSampledSupport() && relation.evidence.isNotEmpty()
     if (!sampled) return unbound(reason = "not-sampled", message = "A complete sampled relation is required")
 
     val resultIsLeft = relation.pair.left == capture.result && relation.pair.right == capture.input

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

@@ -6,8 +6,8 @@ import org.usvm.UBoolExpr
 import org.usvm.machine.state.TsState
 import org.usvm.ts.pbt.inference.ScalarRelation
 import org.usvm.ts.pbt.inference.ScalarRelationInference
-import org.usvm.ts.pbt.inference.ScalarRelationStatus
 import org.usvm.ts.pbt.inference.ScalarRelationTemplate
+import org.usvm.ts.pbt.inference.hasSampledSupport
 import org.usvm.ts.pbt.inference.matches
 import org.usvm.ts.pbt.manifest.PropertyManifest
 import org.usvm.ts.pbt.manifest.toManifest
@@ -67,8 +67,7 @@ internal fun bindEntryRelation(
         return unsupported(reason = "property-mismatch", message = "Property definition or declared support changed")
     }
 
-    val sampled = relation in inference.relations && relation.status == ScalarRelationStatus.SAMPLED &&
-        relation.limitations.isEmpty()
+    val sampled = relation in inference.relations && relation.hasSampledSupport()
     if (!sampled) {
         return unsupported(reason = "not-sampled", message = "A sampled relation from this inference is required")
     }

usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt

@@ -223,12 +223,16 @@ class DomainImpliedScalarRelationTest {
         val refuted = infer(property, listOf(first, second, sample(id = 2, left = 3.0, right = 2.0)))
         val insufficient = infer(property, listOf(first))
         val dropped = artifact(listOf(first, second)).copy(droppedInvocations = 1)
-        val incomplete = inferScalarRelations(property, dropped, listOf(PAIR))
+        val bounded = inferScalarRelations(property, dropped, listOf(PAIR))
 
         assertEquals(ScalarRelationStatus.REFUTED, refuted.order().status)
         assertEquals(ScalarRelationStatus.INSUFFICIENT, insufficient.order().status)
-        assertEquals(ScalarRelationStatus.INSUFFICIENT, incomplete.order().status)
-        assertTrue(listOf(refuted, insufficient, incomplete).all { it.domainImpliedRelations.isEmpty() })
+        assertTrue(bounded.domainImpliedRelations.isNotEmpty())
+        val warningsPreserved = bounded.domainImpliedRelations.all {
+            ScalarRelationLimitation.INCOMPLETE_CAPTURE in it.limitations
+        }
+        assertTrue(warningsPreserved)
+        assertTrue(listOf(refuted, insufficient).all { it.domainImpliedRelations.isEmpty() })
     }
 
     @Test