[TS PBT] Select bounded scalar guidance and retain exclusion evidence

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

@@ -10,6 +10,7 @@ import org.usvm.ts.pbt.dsl.CompiledDslProperty
 import org.usvm.ts.pbt.dsl.DslNumericLocalCapture
 import org.usvm.ts.pbt.dsl.PropertyTypeScriptCompiler
 import org.usvm.ts.pbt.dsl.defineProperty
+import org.usvm.ts.pbt.dsl.equalTo
 import org.usvm.ts.pbt.dsl.invoke
 import org.usvm.ts.pbt.dsl.lessOrEqual
 import org.usvm.ts.pbt.fastcheck.FastCheckBackend
@@ -31,6 +32,7 @@ import java.nio.file.Path
 import java.security.MessageDigest
 import kotlin.test.assertEquals
 import kotlin.test.assertNotNull
+import kotlin.test.assertSame
 import kotlin.test.assertTrue
 
 class DslNumericLocalRelationTest {
@@ -246,6 +248,72 @@ class DslNumericLocalRelationTest {
         assertTrue(missing.targets.isEmpty())
     }
 
+    @Test
+    fun `native compiler observations keep a stronger equality and exclude the original order only`() {
+        val fixture = prepare()
+
+        val selected = selectScalarGuidance(fixture.inference, fixture.compiled)
+
+        assertSame(fixture.inference, selected.inference)
+        assertEquals(ScalarRelationTemplate.STRICT_EQUAL, selected.candidates.single().relation.template)
+        assertEquals(ScalarGuidanceRelevance.KNOWN_DSL_CHECK, selected.candidates.single().relevance)
+        assertEquals(ScalarRelationTemplate.LESS_OR_EQUAL, selected.excluded.single().relation.template)
+        assertEquals(ScalarGuidanceExclusionReason.ORIGINAL_CHECK, selected.excluded.single().reason)
+        assertEquals(ObservationBuildStatus.UNVERIFIED, selected.inference.buildStatus)
+    }
+
+    @Test
+    fun `an original equality excludes both equality and its weaker orders over the same captured operands`() {
+        val fixture = prepare(originalEquality = true)
+        val relations = fixture.inference.relations
+        val reversed = relations.map { relation ->
+            relation.copy(
+                pair = ScalarObservationPair(relation.pair.right, relation.pair.left),
+                evidence = relation.evidence.map { it.copy(left = it.right, right = it.left) },
+            )
+        }
+        val inference = fixture.inference.copy(relations = relations + reversed)
+
+        val selected = selectScalarGuidance(inference, fixture.compiled)
+
+        assertTrue(selected.candidates.isEmpty())
+        assertEquals(4, selected.excluded.size)
+        assertTrue(selected.excluded.all { it.reason == ScalarGuidanceExclusionReason.ORIGINAL_CHECK })
+        assertTrue(selected.excluded.all { it.relevance == ScalarGuidanceRelevance.KNOWN_DSL_CHECK })
+        assertEquals(inference.relations, selected.excluded.map { it.relation })
+    }
+
+    @Test
+    fun `forged retained program source or point metadata cannot establish original formula relevance`() {
+        val fixture = prepare()
+        val compiled = fixture.compiled
+        val capture = assertNotNull(compiled.numericLocalCapture)
+        val fake = capture.copy(result = capture.result.copy(operandId = "unrelated"))
+        val variants = listOf(
+            compiled.copy(numericLocalCapture = fake),
+            compiled.copy(typeScript = compiled.typeScript + "// changed source"),
+            compiled.copy(resolvedModules = emptyMap()),
+            compiled.copy(program = compiled.program.copy(checks = emptyList())),
+        )
+        for (changed in variants) {
+            val selected = selectScalarGuidance(fixture.inference, changed)
+
+            assertEquals(2, selected.candidates.size)
+            assertTrue(selected.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN })
+            assertTrue(selected.excluded.isEmpty())
+        }
+        val changedPoints = fixture.inference.relations.map { relation ->
+            relation.copy(pair = relation.pair.copy(left = relation.pair.left.copy(id = "other-result")))
+        }
+        val relabeled = selectScalarGuidance(fixture.inference.copy(relations = changedPoints), compiled)
+        assertTrue(relabeled.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN })
+        assertTrue(relabeled.excluded.isEmpty())
+
+        val staleSources = fixture.inference.sources.map { it.copy(sha256 = "0".repeat(n = 64)) }
+        val stale = selectScalarGuidance(fixture.inference.copy(sources = staleSources), compiled)
+        assertTrue(stale.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN })
+    }
+
     private fun ScalarRelation.changedResult(
         change: (PropertyPointEvent) -> PropertyPointEvent,
     ): ScalarRelation {
@@ -259,8 +327,8 @@ class DslNumericLocalRelationTest {
         return copy(evidence = changed)
     }
 
-    private fun prepare(): Fixture {
-        val compiled = compile()
+    private fun prepare(originalEquality: Boolean = false): Fixture {
+        val compiled = compile(originalEquality)
         val capture = assertNotNull(compiled.numericLocalCapture)
         val sources = capture.observationRequest().sources + source(module = "functions.ts")
         val request = capture.observationRequest().copy(sources = sources)
@@ -290,7 +358,7 @@ class DslNumericLocalRelationTest {
         return PropertyObservationSource(module, hash)
     }
 
-    private fun compile(): CompiledDslProperty {
+    private fun compile(originalEquality: Boolean): CompiledDslProperty {
         val source = """
             export function transform(input: number): number {
                 if (input === 417) return input - 1;
@@ -304,7 +372,9 @@ class DslNumericLocalRelationTest {
             val other by int(min = 0, max = 1000)
             val result by value(transform(input))
 
-            check(name = "bound") { result lessOrEqual input }
+            check(name = "bound") {
+                if (originalEquality) result equalTo input else result lessOrEqual input
+            }
             check(name = "other-input") { other lessOrEqual 1000 }
         }
         val compiled = PropertyTypeScriptCompiler().compile(

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCapture.kt

@@ -107,3 +107,18 @@ internal fun SelectedDslNumericLocalCapture.compileCapture(
 
     return CompiledDslNumericLocalCapture(binding, result, inputPoint)
 }
+
+internal fun CompiledDslProperty.isReproducibleCompilerOutput(): Boolean = try {
+    val capture = requireNotNull(numericLocalCapture)
+    val regenerated = PropertyTypeScriptCompiler().compile(
+        program,
+        generatedModule = definition.predicate.module,
+        resolveModule = { module -> requireNotNull(resolvedModules[module]) { "Unretained module: $module" } },
+        numericLocalCapture = DslNumericLocalCapture(capture.binding.localName, capture.result.assertionId),
+    )
+
+    definition == regenerated.definition && typeScript == regenerated.typeScript &&
+        numericLocalCapture == regenerated.numericLocalCapture
+} catch (_: IllegalArgumentException) {
+    false
+}

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

@@ -0,0 +1,127 @@
+package org.usvm.ts.pbt.inference
+
+import org.usvm.ts.pbt.dsl.CompiledDslProperty
+import org.usvm.ts.pbt.dsl.DslNumericLocalCapture
+import org.usvm.ts.pbt.dsl.PropertyExpressionTerm
+import org.usvm.ts.pbt.dsl.isReproducibleCompilerOutput
+import org.usvm.ts.pbt.dsl.selectNumericLocalCapture
+import org.usvm.ts.pbt.observation.ObservationPointKind
+
+/** KNOWN_DSL_CHECK identifies a direct original check, not a proved relation or executable body. */
+enum class ScalarGuidanceRelevance { KNOWN_DSL_CHECK, UNKNOWN }
+
+/** Selection decisions preserve each excluded relation and its original evidence. */
+enum class ScalarGuidanceExclusionReason {
+    NOT_SAMPLED,
+    DOMAIN_IMPLIED,
+    TAUTOLOGY,
+    DUPLICATE,
+    ORIGINAL_CHECK,
+    CANDIDATE_LIMIT,
+}
+
+/** An empirical candidate whose exact symbolic support still needs a consumer's binding checks. */
+data class ScalarGuidanceCandidate(val relation: ScalarRelation, val relevance: ScalarGuidanceRelevance)
+
+/** An unselected relation; exclusion never removes it from the original inference. */
+data class ScalarGuidanceExclusion(
+    val relation: ScalarRelation,
+    val reason: ScalarGuidanceExclusionReason,
+    val relevance: ScalarGuidanceRelevance,
+)
+
+/** Retains the complete original inference, including contradictory, insufficient and excluded evidence. */
+data class ScalarGuidanceSelection(
+    val inference: ScalarRelationInference,
+    val candidates: List<ScalarGuidanceCandidate>,
+    val excluded: List<ScalarGuidanceExclusion>,
+)
+
+/** One bounded selection before USVM. The campaign decides whether UNKNOWN relevance may guide its search. */
+fun selectScalarGuidance(
+    inference: ScalarRelationInference,
+    compiled: CompiledDslProperty? = null,
+    maxCandidates: Int = 16,
+): ScalarGuidanceSelection {
+    require(maxCandidates > 0) { "maxCandidates must be positive" }
+
+    val original = originalCheck(inference, compiled)
+    val candidates = mutableListOf<ScalarGuidanceCandidate>()
+    val excluded = mutableListOf<ScalarGuidanceExclusion>()
+    for (relation in inference.relations) {
+        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 restatesOriginal = known && original?.implies(relation) == true
+        val reason = when {
+            !sampled -> ScalarGuidanceExclusionReason.NOT_SAMPLED
+            restatesOriginal -> ScalarGuidanceExclusionReason.ORIGINAL_CHECK
+            duplicate -> ScalarGuidanceExclusionReason.DUPLICATE
+            candidates.size >= maxCandidates -> ScalarGuidanceExclusionReason.CANDIDATE_LIMIT
+            else -> null
+        }
+
+        if (reason == null) {
+            candidates += ScalarGuidanceCandidate(relation, relevance)
+        } else {
+            excluded += ScalarGuidanceExclusion(relation, reason, relevance)
+        }
+    }
+    for (relation in inference.domainImpliedRelations) {
+        val sameOriginalInput = relation.pair.left.kind == ObservationPointKind.ENTRY_ARGUMENT &&
+            relation.pair.right.kind == ObservationPointKind.ENTRY_ARGUMENT &&
+            relation.pair.left.inputIndex != null && relation.pair.left.inputIndex == relation.pair.right.inputIndex
+        val reason = if (sameOriginalInput) {
+            ScalarGuidanceExclusionReason.TAUTOLOGY
+        } else {
+            ScalarGuidanceExclusionReason.DOMAIN_IMPLIED
+        }
+        excluded += ScalarGuidanceExclusion(relation, reason, relevance = ScalarGuidanceRelevance.UNKNOWN)
+    }
+
+    return ScalarGuidanceSelection(inference, candidates, excluded)
+}
+
+private data class OriginalScalarCheck(val pair: ScalarObservationPair, val operator: String) {
+    fun contains(candidate: ScalarObservationPair): Boolean = candidate == pair ||
+        candidate.left == pair.right && candidate.right == pair.left
+
+    fun implies(relation: ScalarRelation): Boolean = operator == "===" ||
+        operator == "<=" && relation.template == ScalarRelationTemplate.LESS_OR_EQUAL && relation.pair == pair
+}
+
+private fun originalCheck(
+    inference: ScalarRelationInference,
+    compiled: CompiledDslProperty?,
+): OriginalScalarCheck? {
+    if (compiled == null) return null
+
+    val sameProperty = compiled.definition == inference.property && compiled.definition.id == inference.propertyId
+    if (!sameProperty) return null
+    if (!compiled.isReproducibleCompilerOutput()) return null
+
+    val capture = compiled.numericLocalCapture ?: return null
+    val source = inference.sources.singleOrNull { it.module == compiled.definition.predicate.module }
+    if (source?.sha256 != capture.binding.sourceSha256) return null
+
+    val request = DslNumericLocalCapture(capture.binding.localName, capture.result.assertionId)
+    val selected = compiled.program.selectNumericLocalCapture(request)
+    val comparison = selected.check.expression.term as PropertyExpressionTerm.Operation
+    val pair = if (selected.resultOperandIndex == 0) {
+        ScalarObservationPair(capture.result, capture.input)
+    } else {
+        ScalarObservationPair(capture.input, capture.result)
+    }
+
+    return OriginalScalarCheck(pair, comparison.operator)
+}
+
+private fun ScalarRelation.sameComparison(other: ScalarRelation): Boolean {
+    if (template != other.template) return false
+
+    val reversed = template == ScalarRelationTemplate.STRICT_EQUAL &&
+        pair.left == other.pair.right && pair.right == other.pair.left
+
+    return pair == other.pair || reversed
+}

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

@@ -5,8 +5,7 @@ import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsNumberType
 import org.usvm.ts.pbt.dsl.CompiledDslProperty
-import org.usvm.ts.pbt.dsl.DslNumericLocalCapture
-import org.usvm.ts.pbt.dsl.PropertyTypeScriptCompiler
+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
@@ -212,21 +211,6 @@ private fun CompiledDslProperty.matchesPinnedSources(
     false
 }
 
-private fun CompiledDslProperty.isReproducibleCompilerOutput(): Boolean = try {
-    val capture = requireNotNull(numericLocalCapture)
-    val regenerated = PropertyTypeScriptCompiler().compile(
-        program,
-        generatedModule = definition.predicate.module,
-        resolveModule = { module -> requireNotNull(resolvedModules[module]) { "Unretained module: $module" } },
-        numericLocalCapture = DslNumericLocalCapture(capture.binding.localName, capture.result.assertionId),
-    )
-
-    definition == regenerated.definition && typeScript == regenerated.typeScript &&
-        numericLocalCapture == regenerated.numericLocalCapture
-} catch (_: IllegalArgumentException) {
-    false
-}
-
 private fun EtsMethod.storesAt(
     point: PropertySourcePoint,
     localName: String,

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

@@ -47,6 +47,9 @@ class DomainImpliedScalarRelationTest {
         assertEquals(ScalarRelationStatus.REFUTED, result.relations.single().status)
         assertEquals(SOURCES, result.sources)
         assertEquals(property, result.property)
+        val selected = selectScalarGuidance(result)
+        val excludedOrder = selected.excluded.single { it.relation == implied }
+        assertEquals(ScalarGuidanceExclusionReason.DOMAIN_IMPLIED, excludedOrder.reason)
     }
 
     @Test
@@ -79,6 +82,29 @@ class DomainImpliedScalarRelationTest {
         assertTrue(result.domainImpliedRelations.all { it.status == ScalarRelationStatus.SAMPLED })
     }
 
+    @Test
+    fun `guidance reuses domain facts and keeps NaN capable reflexive comparisons as unknown candidates`() {
+        val pair = ScalarObservationPair(LEFT, RIGHT.copy(inputIndex = 0))
+        val samples = listOf(sample(id = 0, left = 0.0, right = 0.0), sample(id = 1, left = 1.0, right = 1.0))
+        val snapshots = samples.map { invocation ->
+            invocation.copy(points = listOf(invocation.points.first(), invocation.points.last().copy(inputIndex = 0)))
+        }
+        val integers = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 0, max = 1))
+        val numbers = property(NumberDomain(), IntegerDomain(min = 0, max = 1))
+        val tautologies = infer(integers, snapshots, pair)
+        val nanCapable = infer(numbers, snapshots, pair)
+
+        val excluded = selectScalarGuidance(tautologies)
+        val retained = selectScalarGuidance(nanCapable)
+
+        assertTrue(excluded.candidates.isEmpty())
+        assertEquals(tautologies.domainImpliedRelations, excluded.excluded.map { it.relation })
+        assertTrue(excluded.excluded.all { it.reason == ScalarGuidanceExclusionReason.TAUTOLOGY })
+        assertEquals(nanCapable.relations, retained.candidates.map { it.relation })
+        assertTrue(retained.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN })
+        assertTrue(retained.excluded.isEmpty())
+    }
+
     @Test
     fun `ordinary argument labels never establish input identity even when every sample matches`() {
         val left = LEFT.copy(kind = ObservationPointKind.ARGUMENT)