[PBT] Infer bounded numeric relations from observations

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

@@ -0,0 +1,102 @@
+package org.usvm.ts.pbt.inference
+
+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.fastcheck.FastCheckBackend
+import org.usvm.ts.pbt.model.IntegerDomain
+import org.usvm.ts.pbt.model.PropertyAssertion
+import org.usvm.ts.pbt.model.PropertyDefinition
+import org.usvm.ts.pbt.model.PropertyId
+import org.usvm.ts.pbt.model.PropertyInput
+import org.usvm.ts.pbt.model.PropertyOperand
+import org.usvm.ts.pbt.model.PropertySourceIdentity
+import org.usvm.ts.pbt.model.PropertySourcePoint
+import org.usvm.ts.pbt.model.TypeScriptEntryPoint
+import org.usvm.ts.pbt.observation.ObservationBuildStatus
+import org.usvm.ts.pbt.observation.ObservationPointKind
+import org.usvm.ts.pbt.observation.PropertyObservationPoint
+import org.usvm.ts.pbt.observation.PropertyObservationRequest
+import org.usvm.ts.pbt.observation.PropertyObservationSource
+import org.usvm.ts.pbt.testResourcesRoot
+import java.nio.file.Files
+import java.security.MessageDigest
+import kotlin.test.assertEquals
+import kotlin.test.assertNotNull
+import kotlin.test.assertTrue
+
+class ScalarRelationCaptureTest {
+    @Test
+    fun `original FastCheck generation observations supply a numeric order hypothesis`() {
+        val source = testResourcesRoot().resolve(MODULE)
+        val hash = MessageDigest.getInstance("SHA-256")
+            .digest(Files.readAllBytes(source))
+            .joinToString(separator = "") { byte -> "%02x".format(byte) }
+        val callSite = PropertySourcePoint(module = MODULE, line = 3, column = 43)
+        val input = PropertyObservationPoint(
+            id = "input",
+            assertionId = "non-negative",
+            operandId = "input",
+            source = PropertySourcePoint(module = MODULE, line = 2, column = 11),
+            callSite = callSite,
+            kind = ObservationPointKind.ARGUMENT,
+            inputIndex = 0,
+        )
+        val result = PropertyObservationPoint(
+            id = "result",
+            assertionId = "non-negative",
+            operandId = "result",
+            source = PropertySourcePoint(module = MODULE, line = 3, column = 11),
+            callSite = callSite,
+            kind = ObservationPointKind.RETURN,
+        )
+        val property = PropertyDefinition(
+            id = PropertyId("test.magnitude"),
+            inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = -1, max = 0))),
+            predicate = TypeScriptEntryPoint(module = MODULE, exportName = "nonNegativeMagnitude"),
+            assertions = listOf(
+                PropertyAssertion(
+                    id = "non-negative",
+                    source = PropertySourcePoint(module = MODULE, line = 5, column = 5),
+                    testedCall = callSite,
+                    operands = listOf(
+                        PropertyOperand(id = input.operandId, source = input.source),
+                        PropertyOperand(id = result.operandId, source = result.source),
+                    ),
+                ),
+            ),
+            sourceIdentity = PropertySourceIdentity(
+                sourceSha256 = hash,
+                buildSha256 = hash,
+                buildScope = "direct TypeScript source; executable build unverified",
+            ),
+        )
+        val sources = listOf(PropertyObservationSource(module = MODULE, sha256 = hash))
+        val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot()))
+
+        val run = backend.run(
+            property,
+            PropertyRunConfiguration(
+                seed = 42,
+                numRuns = 16,
+                observationRequest = PropertyObservationRequest(points = listOf(input, result), sources = sources),
+            ),
+        )
+        val observations = assertNotNull(run.observations)
+        val inference = inferScalarRelations(property, observations, listOf(ScalarObservationPair(input, result)))
+        val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL }
+        val order = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL }
+
+        assertEquals(PropertyRunStatus.SUCCESS, run.status)
+        assertEquals(sources, inference.sources)
+        assertEquals(ObservationBuildStatus.UNVERIFIED, inference.buildStatus)
+        assertEquals(ScalarRelationStatus.REFUTED, equality.status)
+        assertEquals(ScalarRelationStatus.SAMPLED, order.status)
+        assertEquals(2, order.distinctGenerationInputs.size)
+        assertTrue(order.evidence.all { it.holds })
+    }
+
+    private companion object {
+        const val MODULE = "properties/inference/ScalarRelations.ts"
+    }
+}

usvm-ts-fast-check/src/test/resources/properties/inference/ScalarRelations.ts

@@ -0,0 +1,12 @@
+export function nonNegativeMagnitude(value: number): boolean {
+    const input = observePoint('input', value);
+    const result = observePoint('result', Math.abs(input));
+
+    return result >= 0;
+}
+
+function observePoint<T>(id: string, value: T): T {
+    const hook = (globalThis as Record<symbol, unknown>)[Symbol.for('org.usvm.ts.pbt.observe')];
+
+    return typeof hook === 'function' ? (hook as (pointId: string, value: T) => T)(id, value) : value;
+}

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

@@ -0,0 +1,214 @@
+package org.usvm.ts.pbt.inference
+
+import org.usvm.ts.pbt.model.JsConcreteValue
+import org.usvm.ts.pbt.model.PropertyDefinition
+import org.usvm.ts.pbt.observation.ObservationAdmission
+import org.usvm.ts.pbt.observation.ObservationOrigin
+import org.usvm.ts.pbt.observation.ObservationOutcome
+import org.usvm.ts.pbt.observation.ObservationPhase
+import org.usvm.ts.pbt.observation.ObservationValueStatus
+import org.usvm.ts.pbt.observation.PropertyInvocationObservation
+import org.usvm.ts.pbt.observation.PropertyObservationArtifact
+import org.usvm.ts.pbt.observation.PropertyObservationPoint
+import org.usvm.ts.pbt.observation.PropertyPointEvent
+
+/**
+ * Evaluates only explicitly selected assertion operand pairs, in selection order.
+ *
+ * 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.
+ *
+ * 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.
+ */
+fun inferScalarRelations(
+    property: PropertyDefinition,
+    observations: PropertyObservationArtifact,
+    pairs: List<ScalarObservationPair>,
+    maxPairs: Int = 16,
+    maxInvocations: Int = 64,
+): ScalarRelationInference {
+    require(maxPairs > 0) { "maxPairs must be positive" }
+    require(maxInvocations > 0) { "maxInvocations must be positive" }
+    require(property.id == observations.propertyId) { "Observation property does not match the selected property" }
+
+    val distinctPairs = pairs.distinct()
+    val selectedPairs = distinctPairs.take(maxPairs)
+    val invocations = observations.invocations.take(maxInvocations)
+    val omittedInvocations = observations.invocations.size - invocations.size
+    val relations = selectedPairs.flatMap { pair ->
+        evaluatePair(property, observations, pair, invocations, omittedInvocations)
+    }
+
+    return ScalarRelationInference(
+        propertyId = property.id,
+        runId = observations.runId,
+        sources = observations.verifiedSources,
+        buildStatus = observations.buildStatus,
+        relations = relations,
+        omittedPairs = distinctPairs.size - selectedPairs.size,
+        omittedInvocations = omittedInvocations,
+        droppedInvocations = observations.droppedInvocations,
+        droppedPoints = observations.droppedPoints,
+    )
+}
+
+private fun evaluatePair(
+    property: PropertyDefinition,
+    observations: PropertyObservationArtifact,
+    pair: ScalarObservationPair,
+    invocations: List<PropertyInvocationObservation>,
+    omittedInvocations: Int,
+): List<ScalarRelation> {
+    val limitations = linkedSetOf<ScalarRelationLimitation>()
+    val validPair = pair.isAssertionPair(property)
+    val verifiedModules = observations.verifiedSources.map { it.module }.toSet()
+    val selectedModules = setOf(pair.left.source.module, pair.right.source.module, pair.left.callSite.module)
+    val expectedSourceHash = property.sourceIdentity?.sourceSha256
+    val predicateSource = observations.verifiedSources.singleOrNull { it.module == property.predicate.module }
+    val propertySourceMatches = expectedSourceHash == null || predicateSource?.sha256 == expectedSourceHash
+    val sourcesPresent = verifiedModules.containsAll(selectedModules) && propertySourceMatches
+
+    if (!validPair) limitations += ScalarRelationLimitation.INVALID_PAIR
+    if (!sourcesPresent) limitations += ScalarRelationLimitation.SOURCE_MISMATCH
+    if (omittedInvocations > 0) limitations += ScalarRelationLimitation.INVOCATION_LIMIT
+    if (observations.droppedInvocations > 0 || observations.droppedPoints > 0) {
+        limitations += ScalarRelationLimitation.INCOMPLETE_CAPTURE
+    }
+
+    val matched = if (validPair && sourcesPresent) {
+        invocations.mapNotNull { invocation -> numericPair(invocation, pair, limitations) }
+    } else {
+        emptyList()
+    }
+    val generationEvidence = matched.filter { (invocation, _, _) -> invocation.isIndependentGeneration() }
+    val distinctInputs = generationEvidence.mapNotNull { (invocation, _, _) -> invocation.input.value }.toSet()
+    val distinctValues = generationEvidence.map { (_, left, right) ->
+        left.numericSupportValue() to right.numericSupportValue()
+    }.toSet()
+
+    if (distinctInputs.size < MINIMUM_DISTINCT_SUPPORT) {
+        limitations += ScalarRelationLimitation.INSUFFICIENT_DISTINCT_INPUTS
+    }
+    if (generationEvidence.isNotEmpty() && distinctValues.size < MINIMUM_DISTINCT_SUPPORT) {
+        limitations += ScalarRelationLimitation.CONSTANT_OBSERVED_PAIR
+    }
+
+    return ScalarRelationTemplate.entries.map { template ->
+        val evidence = matched.map { (invocation, left, right) ->
+            val leftNumber = (left.value.value as JsConcreteValue.Number).toDouble()
+            val rightNumber = (right.value.value as JsConcreteValue.Number).toDouble()
+            val holds = when (template) {
+                ScalarRelationTemplate.STRICT_EQUAL -> leftNumber == rightNumber
+                ScalarRelationTemplate.LESS_OR_EQUAL -> leftNumber <= rightNumber
+            }
+
+            ScalarRelationEvidence(invocation, left, right, holds)
+        }
+        val refuted = evidence.any { !it.holds }
+        val unsupported = limitations.any { it in UNSUPPORTED_LIMITATIONS }
+        val status = when {
+            refuted -> ScalarRelationStatus.REFUTED
+            matched.isEmpty() && unsupported -> ScalarRelationStatus.UNSUPPORTED
+            limitations.isNotEmpty() -> ScalarRelationStatus.INSUFFICIENT
+            else -> ScalarRelationStatus.SAMPLED
+        }
+
+        ScalarRelation(pair, template, status, evidence, distinctInputs, limitations.toSet())
+    }
+}
+
+private fun numericPair(
+    invocation: PropertyInvocationObservation,
+    pair: ScalarObservationPair,
+    limitations: MutableSet<ScalarRelationLimitation>,
+): Triple<PropertyInvocationObservation, PropertyPointEvent, PropertyPointEvent>? {
+    if (invocation.admission != ObservationAdmission.ADMITTED) return null
+
+    val complete = invocation.outcome in COMPLETE_OUTCOMES
+    if (!complete) {
+        limitations += ScalarRelationLimitation.INCOMPLETE_INVOCATION
+        return null
+    }
+    val supportedContext = invocation.parentInvocationId == null && invocation.callSite == pair.left.callSite
+    if (!supportedContext) {
+        limitations += ScalarRelationLimitation.UNSUPPORTED_CONTEXT
+        return null
+    }
+
+    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) {
+        limitations += ScalarRelationLimitation.REPEATED_POINT
+        return null
+    }
+
+    val left = leftEvents.single()
+    val right = rightEvents.single()
+    val identitiesMatch = left.matches(pair.left) && right.matches(pair.right)
+    if (!identitiesMatch) {
+        limitations += ScalarRelationLimitation.POINT_IDENTITY_MISMATCH
+        return null
+    }
+    val numeric = left.isNumber() && right.isNumber()
+    if (!numeric) {
+        limitations += ScalarRelationLimitation.UNSUPPORTED_VALUE
+        return null
+    }
+
+    return Triple(invocation, left, right)
+}
+
+private fun ScalarObservationPair.isAssertionPair(property: PropertyDefinition): Boolean {
+    if (left.id == right.id || left.operandId == right.operandId) return false
+    if (left.assertionId != right.assertionId || left.callSite != right.callSite) return false
+
+    val assertion = property.assertions.singleOrNull { it.id == left.assertionId } ?: return false
+    val leftOperand = assertion.operands.singleOrNull { it.id == left.operandId }
+    val rightOperand = assertion.operands.singleOrNull { it.id == right.operandId }
+
+    return assertion.testedCall == left.callSite &&
+        leftOperand?.source == left.source && rightOperand?.source == right.source
+}
+
+private fun PropertyPointEvent.matches(point: PropertyObservationPoint): Boolean =
+    assertionId == point.assertionId && operandId == point.operandId && source == point.source &&
+        callSite == point.callSite && kind == point.kind && inputIndex == point.inputIndex && occurrence == 0
+
+private fun PropertyPointEvent.isNumber(): Boolean {
+    val number = value.value as? JsConcreteValue.Number ?: return false
+
+    return value.status == ObservationValueStatus.CAPTURED && number.number.hasValidEncoding()
+}
+
+private fun PropertyPointEvent.numericSupportValue(): Double {
+    val number = (value.value as JsConcreteValue.Number).toDouble()
+
+    // Strict numeric equality treats both signed zeros as the same value.
+    return if (number == 0.0) 0.0 else number
+}
+
+private fun PropertyInvocationObservation.isIndependentGeneration(): Boolean =
+    origin == ObservationOrigin.FAST_CHECK && phase == ObservationPhase.GENERATION &&
+        input.status == ObservationValueStatus.CAPTURED && input.value != null
+
+private const val MINIMUM_DISTINCT_SUPPORT = 2
+private val COMPLETE_OUTCOMES = setOf(ObservationOutcome.HOLDS, ObservationOutcome.FALSE, ObservationOutcome.THREW)
+
+private val UNSUPPORTED_LIMITATIONS = setOf(
+    ScalarRelationLimitation.INVALID_PAIR,
+    ScalarRelationLimitation.SOURCE_MISMATCH,
+    ScalarRelationLimitation.MISSING_POINT,
+    ScalarRelationLimitation.REPEATED_POINT,
+    ScalarRelationLimitation.POINT_IDENTITY_MISMATCH,
+    ScalarRelationLimitation.UNSUPPORTED_VALUE,
+    ScalarRelationLimitation.UNSUPPORTED_CONTEXT,
+)