[TS PBT] Filter entry relations implied by declared numeric domains

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

@@ -105,21 +105,24 @@ class EntryRelationSearchTest {
     }
 
     @Test
-    fun `an infeasible focus is a scoped no-finding rather than an engine failure`() {
+    fun `domain implied entry order is retained for audit and cannot activate focused search`() {
         val property = property(
             exportName = "reflexive",
             leftDomain = IntegerDomain(min = 0, max = 1),
             rightDomain = IntegerDomain(min = 2, max = 3),
         )
         val inference = capture(property)
-        val order = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL }
+        val order = inference.domainImpliedRelations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL }
         val manifest = property.toManifest()
 
         val focused = searcher.searchFocusedOnEntryRelation(manifest, mapper.map(manifest), CONCRETE, inference, order)
 
         assertEquals(ScalarRelationStatus.SAMPLED, order.status)
-        assertEquals(EtsMappingStatus.EXACT, focused.binding.status)
-        assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, focused.search?.status)
+        assertEquals(2, order.distinctGenerationInputs.size)
+        assertTrue(order.evidence.all { it.holds })
+        assertTrue(inference.relations.none { it.template == ScalarRelationTemplate.LESS_OR_EQUAL })
+        assertEquals(EtsMappingStatus.UNSUPPORTED, focused.binding.status)
+        assertNull(focused.search)
     }
 
     @Test

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

@@ -0,0 +1,90 @@
+package org.usvm.ts.pbt.inference
+
+import org.usvm.ts.pbt.model.ConstantDomain
+import org.usvm.ts.pbt.model.IntegerDomain
+import org.usvm.ts.pbt.model.JsConcreteValue
+import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.PropertyDefinition
+import org.usvm.ts.pbt.model.PropertyDomain
+import org.usvm.ts.pbt.model.contains
+import org.usvm.ts.pbt.observation.ObservationPointKind
+
+/** Only adapter-owned entry points can turn declared input support into a fact about an observed value. */
+internal fun ScalarRelation.isDomainImplied(property: PropertyDefinition): Boolean {
+    if (status != ScalarRelationStatus.SAMPLED || evidence.isEmpty()) return false
+
+    val points = listOf(pair.left, pair.right)
+    val entryArguments = points.all { point -> point.kind == ObservationPointKind.ENTRY_ARGUMENT }
+    if (!entryArguments) return false
+
+    val leftIndex = pair.left.inputIndex ?: return false
+    val rightIndex = pair.right.inputIndex ?: return false
+    val leftDomain = property.inputs.getOrNull(leftIndex)?.domain ?: return false
+    val rightDomain = property.inputs.getOrNull(rightIndex)?.domain ?: return false
+    val leftBounds = leftDomain.numericBounds() ?: return false
+    val rightBounds = rightDomain.numericBounds() ?: return false
+    val snapshotsMatch = evidence.all { sample ->
+        val input = sample.invocation.input.value as? JsConcreteValue.Array
+        val left = sample.left.value.value
+        val right = sample.right.value.value
+
+        val identitiesMatch = sample.left.matches(pair.left) && sample.right.matches(pair.right)
+        val originalInputsMatch = left == input?.elements?.getOrNull(leftIndex) &&
+            right == input?.elements?.getOrNull(rightIndex)
+        val leftInDomain = left != null && left in leftDomain
+        val rightInDomain = right != null && right in rightDomain
+
+        identitiesMatch && originalInputsMatch && leftInDomain && rightInDomain
+    }
+    if (!snapshotsMatch) return false
+
+    if (leftIndex == rightIndex) return true
+
+    return when (template) {
+        ScalarRelationTemplate.STRICT_EQUAL -> {
+            leftBounds.minimum == leftBounds.maximum && rightBounds.minimum == rightBounds.maximum &&
+                leftBounds.minimum == rightBounds.minimum
+        }
+
+        ScalarRelationTemplate.LESS_OR_EQUAL -> leftBounds.maximum <= rightBounds.minimum
+    }
+}
+
+private data class NumericBounds(val minimum: Double, val maximum: Double)
+
+/** Bounds are useful only when every allowed value is a number and NaN is excluded. */
+private fun PropertyDomain.numericBounds(): NumericBounds? = when (this) {
+    is IntegerDomain -> {
+        val minimum = min.toDouble()
+        val maximum = max.toDouble()
+
+        if (min <= max) NumericBounds(minimum, maximum) else null
+    }
+
+    is NumberDomain -> {
+        val validEncoding = min.hasValidEncoding() && max.hasValidEncoding()
+        if (allowNaN || !validEncoding) {
+            null
+        } else {
+            val minimum = min.toDouble()
+            val maximum = max.toDouble()
+            val ordered = !minimum.isNaN() && !maximum.isNaN() && minimum <= maximum
+
+            if (ordered) NumericBounds(minimum, maximum) else null
+        }
+    }
+
+    is ConstantDomain -> {
+        val number = value as? JsConcreteValue.Number
+        val validEncoding = number?.number?.hasValidEncoding() == true
+        if (!validEncoding) {
+            null
+        } else {
+            val scalar = requireNotNull(number).toDouble()
+
+            if (scalar.isNaN()) null else NumericBounds(scalar, scalar)
+        }
+    }
+
+    else -> null
+}

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

@@ -22,8 +22,9 @@ import org.usvm.ts.pbt.observation.PropertyPointEvent
  * 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.
  *
- * This first slice does not inspect original formulas or declared support. A sampled relation
- * may repeat them; callers must not use this result as a trusted symbolic constraint.
+ * Sampled relations already implied by declared numeric input domains are separated only for
+ * adapter-owned entry arguments. Arbitrary point labels never establish original-input identity.
+ * Original formulas and preconditions are not inspected; retained relations remain empirical.
  */
 fun inferScalarRelations(
     property: PropertyDefinition,
@@ -44,17 +45,20 @@ fun inferScalarRelations(
         evaluatePair(property, observations, pair, invocations, omittedInvocations)
     }
 
+    val (domainImplied, retained) = relations.partition { relation -> relation.isDomainImplied(property) }
+
     return ScalarRelationInference(
         propertyId = property.id,
         runId = observations.runId,
         sources = observations.verifiedSources,
         buildStatus = observations.buildStatus,
-        relations = relations,
+        relations = retained,
         omittedPairs = distinctPairs.size - selectedPairs.size,
         omittedInvocations = omittedInvocations,
         droppedInvocations = observations.droppedInvocations,
         droppedPoints = observations.droppedPoints,
         property = property,
+        domainImpliedRelations = domainImplied,
     )
 }
 

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

@@ -75,4 +75,6 @@ data class ScalarRelationInference(
     val droppedInvocations: Int,
     val droppedPoints: Int,
     val property: PropertyDefinition,
+    /** Sampled entry relations already implied by declared numeric input support, retained for audit. */
+    val domainImpliedRelations: List<ScalarRelation> = emptyList(),
 )