From 983f99f5c69f5197fa3c5a30af41d575c75596f9 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 00:38:05 +0300 Subject: [PATCH] Infer bounded numeric relations from property observations --- .../inference/ScalarRelationCaptureTest.kt | 102 +++++ .../properties/inference/ScalarRelations.ts | 12 + .../ts/pbt/inference/InferScalarRelations.kt | 214 ++++++++++ .../usvm/ts/pbt/inference/ScalarRelation.kt | 76 ++++ .../pbt/inference/InferScalarRelationsTest.kt | 383 ++++++++++++++++++ 5 files changed, 787 insertions(+) create mode 100644 usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/ScalarRelationCaptureTest.kt create mode 100644 usvm-ts-fast-check/src/test/resources/properties/inference/ScalarRelations.ts create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/InferScalarRelationsTest.kt diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/ScalarRelationCaptureTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/ScalarRelationCaptureTest.kt new file mode 100644 index 0000000000..f43f7245ef --- /dev/null +++ b/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" + } +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/inference/ScalarRelations.ts b/usvm-ts-fast-check/src/test/resources/properties/inference/ScalarRelations.ts new file mode 100644 index 0000000000..a98ee3e085 --- /dev/null +++ b/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(id: string, value: T): T { + const hook = (globalThis as Record)[Symbol.for('org.usvm.ts.pbt.observe')]; + + return typeof hook === 'function' ? (hook as (pointId: string, value: T) => T)(id, value) : value; +} 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 new file mode 100644 index 0000000000..803a33ebba --- /dev/null +++ b/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, + 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, + omittedInvocations: Int, +): List { + val limitations = linkedSetOf() + 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, +): Triple? { + 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, +) 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 new file mode 100644 index 0000000000..ecb293afd5 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt @@ -0,0 +1,76 @@ +package org.usvm.ts.pbt.inference + +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.observation.ObservationBuildStatus +import org.usvm.ts.pbt.observation.PropertyInvocationObservation +import org.usvm.ts.pbt.observation.PropertyObservationPoint +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.observation.PropertyPointEvent + +/** An explicitly selected pair of assertion operands, each evaluated once per invocation. */ +data class ScalarObservationPair( + val left: PropertyObservationPoint, + val right: PropertyObservationPoint, +) + +/** Numeric JavaScript comparisons; no mathematical-real or coercing comparison is inferred. */ +enum class ScalarRelationTemplate { + STRICT_EQUAL, + LESS_OR_EQUAL, +} + +/** Sample agreement is empirical evidence, never an invariant or permission to prune a path. */ +enum class ScalarRelationStatus { + SAMPLED, + REFUTED, + INSUFFICIENT, + UNSUPPORTED, +} + +/** Reasons an invocation or selection cannot supply complete numeric evidence. */ +enum class ScalarRelationLimitation { + INVALID_PAIR, + SOURCE_MISMATCH, + MISSING_POINT, + REPEATED_POINT, + POINT_IDENTITY_MISMATCH, + UNSUPPORTED_VALUE, + UNSUPPORTED_CONTEXT, + INCOMPLETE_INVOCATION, + INSUFFICIENT_DISTINCT_INPUTS, + CONSTANT_OBSERVED_PAIR, + INVOCATION_LIMIT, + INCOMPLETE_CAPTURE, +} + +/** Exact same-invocation point values, retaining origin, phase, input and event identities. */ +data class ScalarRelationEvidence( + val invocation: PropertyInvocationObservation, + val left: PropertyPointEvent, + val right: PropertyPointEvent, + val holds: Boolean, +) + +/** Evaluation of one template for one selected pair, including every observed contradiction. */ +data class ScalarRelation( + val pair: ScalarObservationPair, + val template: ScalarRelationTemplate, + val status: ScalarRelationStatus, + val evidence: List, + val distinctGenerationInputs: Set, + val limitations: Set, +) + +/** Bounded, property-scoped results preserving selected-source and executable-build provenance. */ +data class ScalarRelationInference( + val propertyId: PropertyId, + val runId: String, + val sources: List, + val buildStatus: ObservationBuildStatus, + val relations: List, + val omittedPairs: Int, + val omittedInvocations: Int, + val droppedInvocations: Int, + val droppedPoints: Int, +) diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/InferScalarRelationsTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/InferScalarRelationsTest.kt new file mode 100644 index 0000000000..815a89dd56 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/InferScalarRelationsTest.kt @@ -0,0 +1,383 @@ +package org.usvm.ts.pbt.inference + +import org.junit.jupiter.api.Test +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.JsNumberKind +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.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.assertFailsWith +import kotlin.test.assertTrue + +class InferScalarRelationsTest { + @Test + fun `two and four value supports yield empirical relations without a large minimum`() { + for (supportSize in listOf(2, 4)) { + val samples = (0 until supportSize).map { index -> invocation(index, index.toDouble(), index.toDouble()) } + + val result = infer(samples) + + assertTrue(result.relations.all { it.status == ScalarRelationStatus.SAMPLED }) + assertEquals(supportSize, result.relations.first().distinctGenerationInputs.size) + assertEquals(ObservationBuildStatus.UNVERIFIED, result.buildStatus) + assertEquals(SOURCES, result.sources) + } + } + + @Test + fun `duplicate generation inputs and replay shrink solver samples do not manufacture support`() { + val sample = invocation(id = 0, left = 0.0, right = 0.0) + val samples = listOf( + sample, + sample.copy(invocationId = 1), + invocation(id = 2, left = 1.0, right = 1.0).copy(phase = ObservationPhase.REPLAY), + invocation(id = 3, left = 2.0, right = 2.0).copy(phase = ObservationPhase.SHRINK), + invocation(id = 4, left = 3.0, right = 3.0).copy(origin = ObservationOrigin.SOLVER), + invocation(id = 5, left = 4.0, right = 4.0).copy(phase = ObservationPhase.EXPLICIT), + invocation(id = 6, left = 5.0, right = 5.0).copy(phase = ObservationPhase.UNKNOWN), + ) + + val result = infer(samples).relations.first() + + assertEquals(ScalarRelationStatus.INSUFFICIENT, result.status) + assertEquals(1, result.distinctGenerationInputs.size) + assertEquals(7, result.evidence.size) + assertTrue(ScalarRelationLimitation.INSUFFICIENT_DISTINCT_INPUTS in result.limitations) + } + + @Test + fun `later correlated witnesses retain the refuted relation and exact evidence`() { + val original = listOf(invocation(id = 0, left = 0.0, right = 0.0), invocation(id = 1, left = 1.0, right = 1.0)) + + for (phase in listOf(ObservationPhase.REPLAY, ObservationPhase.SHRINK)) { + val witness = invocation(id = 2, left = 1.0, right = 0.0).copy(phase = phase) + val result = infer(original + witness) + + assertTrue(result.relations.all { it.status == ScalarRelationStatus.REFUTED }) + assertEquals(2, result.relations.first().distinctGenerationInputs.size) + val contradiction = result.relations.first().evidence.single { !it.holds } + assertEquals(witness, contradiction.invocation) + assertEquals(witness.points.first().eventOrdinal, contradiction.left.eventOrdinal) + } + + val solver = invocation(id = 3, left = 1.0, right = 0.0).copy(origin = ObservationOrigin.SOLVER) + assertTrue(infer(original + solver).relations.all { it.status == ScalarRelationStatus.REFUTED }) + } + + @Test + fun `rejected inputs neither support nor refute a relation`() { + val rejected = invocation(id = 2, left = 1.0, right = 0.0).copy(admission = ObservationAdmission.REJECTED) + val original = listOf(invocation(id = 0, left = 0.0, right = 0.0), invocation(id = 1, left = 1.0, right = 1.0)) + + val result = infer(original + rejected) + + assertTrue(result.relations.all { it.status == ScalarRelationStatus.SAMPLED }) + assertEquals(2, result.relations.first().evidence.size) + } + + @Test + fun `points from different invocations are never paired`() { + val leftOnly = invocation(id = 0, left = 0.0, right = 0.0).let { it.copy(points = it.points.take(1)) } + val rightOnly = invocation(id = 1, left = 1.0, right = 1.0).let { it.copy(points = it.points.drop(1)) } + + val result = infer(listOf(leftOnly, rightOnly)).relations.first() + + assertEquals(ScalarRelationStatus.UNSUPPORTED, result.status) + assertTrue(result.evidence.isEmpty()) + assertTrue(ScalarRelationLimitation.MISSING_POINT in result.limitations) + } + + @Test + fun `rare contexts keep independent evidence separate`() { + val first = invocation(id = 0, left = 0.0, right = 0.0) + val otherSite = CALL.copy(line = 100) + val elsewhere = invocation(id = 1, left = 1.0, right = 1.0).copy(callSite = otherSite) + val nested = invocation(id = 2, left = 2.0, right = 2.0).copy(parentInvocationId = 0) + + val result = infer(listOf(first, elsewhere, nested)).relations.first() + + assertEquals(ScalarRelationStatus.INSUFFICIENT, result.status) + assertEquals(1, result.distinctGenerationInputs.size) + assertTrue(ScalarRelationLimitation.UNSUPPORTED_CONTEXT in result.limitations) + } + + @Test + fun `changed assertion operand source callsite and repeated occurrence cannot supply evidence`() { + val sample = invocation(id = 0, left = 0.0, right = 0.0) + val left = sample.points.first() + val changed = listOf( + left.copy(assertionId = "another"), + left.copy(operandId = "another"), + left.copy(source = left.source.copy(line = 99)), + left.copy(callSite = CALL.copy(column = 99)), + left.copy(kind = ObservationPointKind.POST), + left.copy(inputIndex = 99), + left.copy(occurrence = 1), + ) + + for (event in changed) { + val result = infer(listOf(sample.copy(points = listOf(event, sample.points.last())))).relations.first() + + assertEquals(ScalarRelationStatus.UNSUPPORTED, result.status) + assertTrue(ScalarRelationLimitation.POINT_IDENTITY_MISMATCH in result.limitations) + } + + val repeated = sample.copy(points = sample.points + left.copy(occurrence = 1, eventOrdinal = 2)) + assertTrue(ScalarRelationLimitation.REPEATED_POINT in infer(listOf(repeated)).relations.first().limitations) + } + + @Test + fun `non numeric truncated and malformed numeric values remain unsupported`() { + val sample = invocation(id = 0, left = 0.0, right = 0.0) + val values = listOf( + captured(JsConcreteValue.Null), + captured(JsConcreteValue.Undefined), + captured(JsConcreteValue.String("0")), + captured(JsConcreteValue.Boolean(true)), + PropertyObservationValue(status = ObservationValueStatus.TRUNCATED, reason = "byte-budget"), + captured(JsConcreteValue.Number(JsNumber(value = JsNumberKind.FINITE, bits = "not-bits"))), + ) + + for (value in values) { + val points = listOf(sample.points.first().copy(value = value), sample.points.last()) + val result = infer(listOf(sample.copy(points = points))).relations.first() + + assertEquals(ScalarRelationStatus.UNSUPPORTED, result.status) + assertTrue(ScalarRelationLimitation.UNSUPPORTED_VALUE in result.limitations) + } + } + + @Test + fun `numeric equality and order preserve NaN infinities signed zero and binary64 rounding`() { + val cases = listOf( + Triple(Double.NaN, Double.NaN, false), + Triple(-0.0, 0.0, true), + Triple(Double.POSITIVE_INFINITY, Double.POSITIVE_INFINITY, true), + Triple(Double.NEGATIVE_INFINITY, Double.NEGATIVE_INFINITY, true), + Triple(9_007_199_254_740_992.0, 9_007_199_254_740_993.0, true), + ) + + for ((left, right, expected) in cases) { + val relations = infer(listOf(invocation(id = 0, left = left, right = right))).relations + + assertTrue(relations.all { it.evidence.single().holds == expected }) + } + + val ordered = infer(listOf(invocation(id = 0, left = Double.NEGATIVE_INFINITY, right = 0.0))).relations + assertEquals(false, ordered.first().evidence.single().holds) + assertEquals(true, ordered.last().evidence.single().holds) + } + + @Test + fun `constant observed pairs are not promoted by unrelated changing inputs`() { + val first = invocation(id = 0, left = 1.0, right = 1.0) + val second = invocation(id = 1, left = 1.0, right = 1.0).copy(input = captured(input(2.0))) + + val result = infer(listOf(first, second)).relations.first() + + assertEquals(2, result.distinctGenerationInputs.size) + assertEquals(ScalarRelationStatus.INSUFFICIENT, result.status) + assertTrue(ScalarRelationLimitation.CONSTANT_OBSERVED_PAIR in result.limitations) + } + + @Test + fun `self pairs unrelated points and missing source hashes stay unsupported`() { + val sample = invocation(id = 0, left = 0.0, right = 0.0) + val unrelated = RIGHT.copy(assertionId = "other") + val pairs = listOf(ScalarObservationPair(LEFT, LEFT), ScalarObservationPair(LEFT, unrelated)) + + val result = inferScalarRelations(PROPERTY, artifact(listOf(sample)), pairs) + + assertTrue(result.relations.all { ScalarRelationLimitation.INVALID_PAIR in it.limitations }) + val noSources = artifact(listOf(sample)).copy(verifiedSources = emptyList()) + val sourceResult = inferScalarRelations(PROPERTY, noSources, listOf(PAIR)).relations.first() + assertTrue(ScalarRelationLimitation.SOURCE_MISMATCH in sourceResult.limitations) + } + + @Test + fun `limits and deduplication are deterministic and preserve omitted evidence diagnostics`() { + val samples = (0..3).map { invocation(it, it.toDouble(), it.toDouble()) } + val observations = artifact(samples).copy(droppedInvocations = 2, droppedPoints = 3) + + val result = inferScalarRelations( + property = PROPERTY, + observations = observations, + pairs = listOf(PAIR, PAIR, ScalarObservationPair(RIGHT, LEFT)), + maxPairs = 1, + maxInvocations = 2, + ) + + assertEquals(2, result.relations.size) + assertEquals(1, result.omittedPairs) + assertEquals(2, result.omittedInvocations) + assertEquals(2, result.droppedInvocations) + assertEquals(3, result.droppedPoints) + assertTrue(result.relations.all { it.status == ScalarRelationStatus.INSUFFICIENT }) + assertTrue(result.relations.all { ScalarRelationLimitation.INVOCATION_LIMIT in it.limitations }) + } + + @Test + fun `empty pending and dropped capture report insufficient evidence`() { + val sample = invocation(id = 0, left = 0.0, right = 0.0) + val samples = listOf(sample, invocation(id = 1, left = 1.0, right = 1.0)) + val incomplete = artifact(samples).copy(droppedPoints = 1) + + val emptyResult = infer(emptyList()) + val pendingResult = infer(listOf(sample.copy(outcome = ObservationOutcome.PENDING))) + val droppedResult = inferScalarRelations(PROPERTY, incomplete, listOf(PAIR)) + + assertTrue(emptyResult.relations.all { it.status == ScalarRelationStatus.INSUFFICIENT }) + assertTrue(pendingResult.relations.all { it.status == ScalarRelationStatus.INSUFFICIENT }) + assertTrue(droppedResult.relations.all { it.status == ScalarRelationStatus.INSUFFICIENT }) + assertTrue(droppedResult.relations.all { ScalarRelationLimitation.INCOMPLETE_CAPTURE in it.limitations }) + } + + @Test + fun `selected source hashes are checked against property identity when declared`() { + val sourceIdentity = PropertySourceIdentity( + sourceSha256 = "b".repeat(64), + buildSha256 = "c".repeat(64), + buildScope = "test", + ) + val property = PROPERTY.copy(sourceIdentity = sourceIdentity) + val observations = artifact(listOf(invocation(id = 0, left = 0.0, right = 0.0))) + + val result = inferScalarRelations(property, observations, listOf(PAIR)) + + assertTrue(result.relations.all { it.status == ScalarRelationStatus.UNSUPPORTED }) + assertTrue(result.relations.all { ScalarRelationLimitation.SOURCE_MISMATCH in it.limitations }) + } + + @Test + fun `signed zeros alone do not count as numeric diversity`() { + val samples = listOf(invocation(id = 0, left = -0.0, right = -0.0), invocation(id = 1, left = 0.0, right = 0.0)) + + val result = infer(samples) + + assertTrue(result.relations.all { it.status == ScalarRelationStatus.INSUFFICIENT }) + assertTrue(result.relations.all { ScalarRelationLimitation.CONSTANT_OBSERVED_PAIR in it.limitations }) + assertEquals(2, result.relations.first().distinctGenerationInputs.size) + } + + @Test + fun `property identity and positive bounds are required`() { + val observations = artifact(emptyList()) + + assertFailsWith { + inferScalarRelations(PROPERTY, observations.copy(propertyId = PropertyId("other")), listOf(PAIR)) + } + assertFailsWith { + inferScalarRelations(PROPERTY, observations, listOf(PAIR), maxPairs = 0) + } + assertFailsWith { + inferScalarRelations(PROPERTY, observations, listOf(PAIR), maxInvocations = 0) + } + } + + private fun infer(samples: List): ScalarRelationInference = + inferScalarRelations(PROPERTY, artifact(samples), listOf(PAIR)) + + private fun invocation(id: Int, left: Double, right: Double): PropertyInvocationObservation = + PropertyInvocationObservation( + invocationId = id, + callSite = CALL, + origin = ObservationOrigin.FAST_CHECK, + phase = ObservationPhase.GENERATION, + input = captured(input(left)), + 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 artifact(samples: List): PropertyObservationArtifact = + PropertyObservationArtifact( + propertyId = PROPERTY.id, + runId = "sample-run", + verifiedSources = SOURCES, + buildStatus = ObservationBuildStatus.UNVERIFIED, + invocations = samples, + droppedInvocations = 0, + droppedPoints = 0, + captureTimeMillis = 0, + ) + + private fun input(number: Double): JsConcreteValue = JsConcreteValue.Array(listOf(JsConcreteValue.number(number))) + + private fun captured(value: JsConcreteValue): PropertyObservationValue = + PropertyObservationValue(status = ObservationValueStatus.CAPTURED, value = value) + + private companion object { + const val MODULE = "property.ts" + val CALL = PropertySourcePoint(module = MODULE, line = 1, column = 1) + val LEFT = PropertyObservationPoint( + id = "input", + assertionId = "check", + operandId = "input", + source = CALL, + callSite = CALL, + kind = ObservationPointKind.ARGUMENT, + inputIndex = 0, + ) + val RIGHT = PropertyObservationPoint( + id = "result", + assertionId = "check", + operandId = "result", + source = CALL.copy(column = 2), + callSite = CALL, + kind = ObservationPointKind.RETURN, + ) + val PAIR = ScalarObservationPair(LEFT, RIGHT) + val SOURCES = listOf(PropertyObservationSource(module = MODULE, sha256 = "a".repeat(64))) + val PROPERTY = PropertyDefinition( + id = PropertyId("test.numeric"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = 0, max = 3))), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = "check"), + 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), + ), + ), + ), + ) + } +}