From 4254b0987e1c5c4a23db894db1a1b27b24de8d75 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 10:51:14 +0300 Subject: [PATCH] Filter entry relations implied by declared numeric domains --- .../pbt/inference/EntryRelationSearchTest.kt | 11 +- .../inference/DomainImpliedScalarRelation.kt | 90 +++++ .../ts/pbt/inference/InferScalarRelations.kt | 10 +- .../usvm/ts/pbt/inference/ScalarRelation.kt | 2 + .../DomainImpliedScalarRelationTest.kt | 313 ++++++++++++++++++ 5 files changed, 419 insertions(+), 7 deletions(-) create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelation.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationSearchTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationSearchTest.kt index 2f6c5278c9..bb1a84150b 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationSearchTest.kt +++ b/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 diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelation.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelation.kt new file mode 100644 index 0000000000..e403866d39 --- /dev/null +++ b/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 +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt index b3a20ea138..91a3b3a03c 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt +++ b/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, ) } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt index c4bce5984b..d97b6763a5 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt +++ b/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 = emptyList(), ) diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt new file mode 100644 index 0000000000..47fefa6a5b --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt @@ -0,0 +1,313 @@ +package org.usvm.ts.pbt.inference + +import org.junit.jupiter.api.Test +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.JsNumber +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyAssertion +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyDomain +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.PropertySourcePoint +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.observation.ObservationAdmission +import org.usvm.ts.pbt.observation.ObservationBuildStatus +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.ObservationPointKind +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.PropertyObservationSource +import org.usvm.ts.pbt.observation.PropertyObservationValue +import org.usvm.ts.pbt.observation.PropertyPointEvent +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class DomainImpliedScalarRelationTest { + @Test + fun `separated inclusive integer domains remove only the already guaranteed order`() { + val property = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 2, max = 3)) + val samples = listOf(sample(id = 0, left = 0.0, right = 2.0), sample(id = 1, left = 1.0, right = 3.0)) + + val result = infer(property, samples) + + val implied = result.domainImpliedRelations.single() + assertEquals(ScalarRelationTemplate.LESS_OR_EQUAL, implied.template) + assertEquals(ScalarRelationStatus.SAMPLED, implied.status) + assertEquals(samples, implied.evidence.map { it.invocation }) + assertEquals(2, implied.distinctGenerationInputs.size) + assertEquals(ScalarRelationStatus.REFUTED, result.relations.single().status) + assertEquals(SOURCES, result.sources) + assertEquals(property, result.property) + } + + @Test + fun `touching interval endpoints imply order but overlapping intervals do not`() { + val samples = listOf(sample(id = 0, left = 0.0, right = 2.0), sample(id = 1, left = 1.0, right = 3.0)) + val touching = property(IntegerDomain(min = 0, max = 2), IntegerDomain(min = 2, max = 3)) + val overlapping = property(IntegerDomain(min = 0, max = 3), IntegerDomain(min = 2, max = 3)) + + val touchingResult = infer(touching, samples) + val overlappingResult = infer(overlapping, samples) + + assertEquals(1, touchingResult.domainImpliedRelations.size) + assertTrue(overlappingResult.domainImpliedRelations.isEmpty()) + assertEquals(ScalarRelationStatus.SAMPLED, overlappingResult.order().status) + } + + @Test + fun `same original numeric input makes both templates redundant when NaN is excluded`() { + val right = 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 aliasSamples = samples.map { invocation -> + invocation.copy(points = listOf(invocation.points.first(), invocation.points.last().copy(inputIndex = 0))) + } + val property = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 0, max = 1)) + + val result = infer(property, aliasSamples, pair = ScalarObservationPair(LEFT, right)) + + assertTrue(result.relations.isEmpty()) + assertEquals(ScalarRelationTemplate.entries.toSet(), result.domainImpliedRelations.map { it.template }.toSet()) + assertTrue(result.domainImpliedRelations.all { it.status == ScalarRelationStatus.SAMPLED }) + } + + @Test + fun `ordinary argument labels never establish input identity even when every sample matches`() { + val left = LEFT.copy(kind = ObservationPointKind.ARGUMENT) + val right = RIGHT.copy(kind = ObservationPointKind.ARGUMENT) + val samples = listOf(sample(id = 0, left = 0.0, right = 2.0), sample(id = 1, left = 1.0, right = 3.0)) + val ordinary = samples.map { invocation -> + invocation.copy(points = invocation.points.map { it.copy(kind = ObservationPointKind.ARGUMENT) }) + } + val property = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 2, max = 3)) + + val result = infer(property, ordinary, pair = ScalarObservationPair(left, right)) + + assertTrue(result.domainImpliedRelations.isEmpty()) + assertEquals(ScalarRelationStatus.SAMPLED, result.order().status) + } + + @Test + fun `changed snapshots invalid indices and observations outside domains are retained`() { + val first = sample(id = 0, left = 0.0, right = 2.0) + val second = sample(id = 1, left = 1.0, right = 3.0) + val property = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 2, max = 3)) + val differentInput = first.copy(input = captured(inputs(left = 1.0, right = 2.0))) + val snapshotResult = infer(property, listOf(differentInput, second)) + val outsideDomain = infer(property, listOf(first, sample(id = 1, left = 2.0, right = 3.0))) + val invalidPoint = LEFT.copy(inputIndex = 99) + val invalidSamples = listOf(first, second).map { invocation -> + invocation.copy(points = listOf(invocation.points.first().copy(inputIndex = 99), invocation.points.last())) + } + val invalidIndex = infer(property, invalidSamples, pair = ScalarObservationPair(invalidPoint, RIGHT)) + + for (result in listOf(snapshotResult, outsideDomain, invalidIndex)) { + assertTrue(result.domainImpliedRelations.isEmpty()) + assertEquals(ScalarRelationStatus.SAMPLED, result.order().status) + } + } + + @Test + fun `NaN enabled domains cannot guarantee either comparison`() { + val property = property(NumberDomain(), IntegerDomain(min = 2, max = 3)) + val samples = listOf(sample(id = 0, left = 0.0, right = 2.0), sample(id = 1, left = 1.0, right = 3.0)) + + val result = infer(property, samples) + + assertTrue(result.domainImpliedRelations.isEmpty()) + assertEquals(ScalarRelationStatus.SAMPLED, result.order().status) + } + + @Test + fun `NaN allowed on an aliased original input prevents reflexivity filtering`() { + val property = property(NumberDomain(), NumberDomain()) + val right = 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 aliases = samples.map { invocation -> + invocation.copy(points = listOf(invocation.points.first(), invocation.points.last().copy(inputIndex = 0))) + } + + val result = infer(property, aliases, pair = ScalarObservationPair(LEFT, right)) + + assertTrue(result.domainImpliedRelations.isEmpty()) + assertTrue(result.relations.all { it.status == ScalarRelationStatus.SAMPLED }) + } + + @Test + fun `binary64 bounds signed zero and infinities use numeric JavaScript ordering`() { + val negativeInfinity = Double.NEGATIVE_INFINITY + val positiveInfinity = Double.POSITIVE_INFINITY + val exactBoundary = 9_007_199_254_740_992.0 + val roundedBoundary = 9_007_199_254_740_993.0 + val cases = listOf( + property(numberDomain(min = -0.0, max = 0.0), numberDomain(min = 0.0, max = 1.0)) to listOf( + sample(id = 0, left = -0.0, right = 0.0), + sample(id = 1, left = 0.0, right = 1.0), + ), + property( + numberDomain(min = negativeInfinity, max = -1.0), + numberDomain(min = 0.0, max = positiveInfinity), + ) to listOf( + sample(id = 0, left = negativeInfinity, right = 0.0), + sample(id = 1, left = -1.0, right = positiveInfinity), + ), + property( + numberDomain(min = exactBoundary, max = roundedBoundary), + numberDomain(min = exactBoundary, max = positiveInfinity), + ) to listOf( + sample(id = 0, left = exactBoundary, right = exactBoundary), + sample(id = 1, left = exactBoundary, right = positiveInfinity), + ), + ) + + for ((property, samples) in cases) { + val result = infer(property, samples) + + assertEquals(ScalarRelationTemplate.LESS_OR_EQUAL, result.domainImpliedRelations.single().template) + } + } + + @Test + fun `numeric constants participate in ordering but optional and malformed supports do not`() { + val samples = listOf(sample(id = 0, left = 0.0, right = 0.0), sample(id = 1, left = 0.0, right = 1.0)) + val constant = ConstantDomain(JsConcreteValue.number(0.0)) + val right = IntegerDomain(min = 0, max = 1) + val numeric = property(constant, right) + val optional = property(OptionalDomain(constant), right) + val invalid = property(IntegerDomain(min = 1, max = 0), right) + + assertEquals(1, infer(numeric, samples).domainImpliedRelations.size) + assertTrue(infer(optional, samples).domainImpliedRelations.isEmpty()) + assertTrue(infer(invalid, samples).domainImpliedRelations.isEmpty()) + } + + @Test + fun `contradictions and insufficient or incomplete evidence never disappear into domain filtering`() { + val property = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 2, max = 3)) + val first = sample(id = 0, left = 0.0, right = 2.0) + val second = sample(id = 1, left = 1.0, right = 3.0) + 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)) + + 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() }) + } + + @Test + fun `unrepresented preconditions and original properties do not remove empirical relations`() { + val property = property(IntegerDomain(min = 0, max = 3), IntegerDomain(min = 0, max = 3)).copy( + precondition = TypeScriptEntryPoint(module = MODULE, exportName = "ordered"), + ) + val samples = listOf(sample(id = 0, left = 0.0, right = 0.0), sample(id = 1, left = 1.0, right = 1.0)) + + val result = infer(property, samples) + + assertTrue(result.domainImpliedRelations.isEmpty()) + assertTrue(result.relations.all { it.status == ScalarRelationStatus.SAMPLED }) + } + + private fun infer( + property: PropertyDefinition, + samples: List, + pair: ScalarObservationPair = PAIR, + ): ScalarRelationInference = inferScalarRelations(property, artifact(samples), listOf(pair)) + + private fun ScalarRelationInference.order(): ScalarRelation = + relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + + private fun property(left: PropertyDomain, right: PropertyDomain): PropertyDefinition = PropertyDefinition( + id = ID, + inputs = listOf(PropertyInput(name = "left", domain = left), PropertyInput(name = "right", domain = right)), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = "holds"), + assertions = listOf( + PropertyAssertion( + id = "check", + source = CALL, + testedCall = CALL, + operands = listOf( + PropertyOperand(id = LEFT.operandId, source = LEFT.source), + PropertyOperand(id = RIGHT.operandId, source = RIGHT.source), + ), + ), + ), + ) + + private fun sample(id: Int, left: Double, right: Double): PropertyInvocationObservation = + PropertyInvocationObservation( + invocationId = id, + callSite = CALL, + origin = ObservationOrigin.FAST_CHECK, + phase = ObservationPhase.GENERATION, + input = captured(inputs(left, right)), + admission = ObservationAdmission.ADMITTED, + outcome = ObservationOutcome.HOLDS, + points = listOf(event(LEFT, left, ordinal = 0), event(RIGHT, right, ordinal = 1)), + ) + + private fun event(point: PropertyObservationPoint, number: Double, ordinal: Int): PropertyPointEvent = + PropertyPointEvent( + pointId = point.id, + assertionId = point.assertionId, + operandId = point.operandId, + source = point.source, + callSite = point.callSite, + kind = point.kind, + inputIndex = point.inputIndex, + occurrence = 0, + eventOrdinal = ordinal, + value = captured(JsConcreteValue.number(number)), + ) + + private fun inputs(left: Double, right: Double): JsConcreteValue = + JsConcreteValue.Array(listOf(JsConcreteValue.number(left), JsConcreteValue.number(right))) + + private fun captured(value: JsConcreteValue): PropertyObservationValue = + PropertyObservationValue(status = ObservationValueStatus.CAPTURED, value = value) + + private fun artifact(samples: List) = PropertyObservationArtifact( + propertyId = ID, + runId = "domain-filter", + verifiedSources = SOURCES, + buildStatus = ObservationBuildStatus.UNVERIFIED, + invocations = samples, + droppedInvocations = 0, + droppedPoints = 0, + captureTimeMillis = 0, + ) + + private fun numberDomain(min: Double, max: Double) = NumberDomain( + min = JsNumber.fromDouble(min), + max = JsNumber.fromDouble(max), + allowNaN = false, + ) + + private companion object { + const val MODULE = "property.ts" + val ID = PropertyId("test.domain-filter") + val CALL = PropertySourcePoint(module = MODULE, line = 1, column = 1) + val LEFT = PropertyObservationPoint( + id = "left", + assertionId = "check", + operandId = "left", + source = CALL, + callSite = CALL, + kind = ObservationPointKind.ENTRY_ARGUMENT, + inputIndex = 0, + ) + val RIGHT = LEFT.copy(id = "right", operandId = "right", inputIndex = 1) + val PAIR = ScalarObservationPair(LEFT, RIGHT) + val SOURCES = listOf(PropertyObservationSource(module = MODULE, sha256 = "a".repeat(64))) + } +}