diff --git a/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts b/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts index 577628e6c3..c1717d479a 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts @@ -67,6 +67,7 @@ interface InvocationRecord { input: ObservationValue; admission: 'pending' | 'admitted' | 'rejected' | 'threw'; outcome: 'pending' | 'holds' | 'false' | 'threw' | 'skipped'; + pointsTruncated: boolean; points: Array & { pointId: string; occurrence: number; @@ -176,6 +177,7 @@ export class ObservationRecorder { admission: 'pending', outcome: 'pending', points: [], + pointsTruncated: false, }; this.artifact.invocations.push(record); if (this.reservedArtifactBytes() > this.request.maxBytes) { @@ -207,6 +209,7 @@ export class ObservationRecorder { // Adapter entry snapshots and compiler callbacks own these points; public hooks cannot replace them. if (point?.kind === 'entry-argument' || point?.compilerLocal !== undefined) return; if (point === undefined) { + record.pointsTruncated = true; this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints); return; @@ -217,6 +220,7 @@ export class ObservationRecorder { private capturePoint(record: InvocationRecord, point: ObservationPointRequest, value: unknown, unsupportedReason?: string): void { if (record.points.length >= this.request.maxPointsPerInvocation) { + record.pointsTruncated = true; this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints); return; @@ -235,8 +239,10 @@ export class ObservationRecorder { eventOrdinal: record.points.length, value: unsupportedReason === undefined ? this.snapshot(value) : { status: 'unsupported', reason: unsupportedReason }, }); + if (record.points.at(-1)?.value.status === 'truncated') record.pointsTruncated = true; if (this.reservedArtifactBytes() > this.request.maxBytes) { record.points.pop(); + record.pointsTruncated = true; this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints); } } diff --git a/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts index fcc206a589..8e84d89714 100644 --- a/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts +++ b/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts @@ -214,6 +214,7 @@ test('entry arguments are adapter snapshots before user code and cannot be repla assert.deepEqual(invocation.points.map((event) => event.occurrence), [0, 0]); assert.equal(recorder.result.buildStatus, 'unverified'); assert.equal(recorder.result.droppedPoints, 0); + assert.equal(invocation.pointsTruncated, false); }); test('observation limits report dropped invocations and points without changing returned values', () => { @@ -245,6 +246,7 @@ test('observation limits report dropped invocations and points without changing assert.equal(recorder.result.invocations[0]?.input.status, 'captured'); assert.equal(recorder.result.invocations[0]?.points[0]?.value.status, 'truncated'); assert.equal(recorder.result.droppedPoints, 1); + assert.equal(recorder.result.invocations[0]?.pointsTruncated, true); assert.equal(recorder.result.droppedInvocations, 1); }); @@ -398,6 +400,7 @@ test('the complete observation artifact stays within edge budgets after outcomes assert.equal(artifact.invocations[0]?.outcome, 'skipped'); assert.equal(artifact.droppedInvocations, 10); assert.ok(artifact.droppedPoints >= 10); + assert.equal(artifact.invocations[0]?.pointsTruncated, true); capturedPoints += artifact.invocations[0]?.points.length ?? 0; } diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyRelationCampaignTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyRelationCampaignTest.kt index 7947569f40..74e2c1dcee 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyRelationCampaignTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyRelationCampaignTest.kt @@ -15,6 +15,8 @@ import org.usvm.ts.pbt.dsl.lessOrEqual import org.usvm.ts.pbt.inference.ScalarGuidanceExclusionReason import org.usvm.ts.pbt.inference.ScalarGuidanceRelevance import org.usvm.ts.pbt.inference.ScalarObservationPair +import org.usvm.ts.pbt.inference.ScalarRelationLimitation +import org.usvm.ts.pbt.inference.ScalarRelationStatus import org.usvm.ts.pbt.inference.ScalarRelationTemplate import org.usvm.ts.pbt.model.IntegerDomain import org.usvm.ts.pbt.model.PropertyAssertion @@ -43,6 +45,44 @@ class PropertyRelationCampaignTest { private val configuration = PropertyRunConfiguration(seed = 42, numRuns = 8, timeoutMillis = 30_000) + @Test + fun `default one hundred PBT runs can challenge a relation from a bounded recorded sample`() { + val compiled = numericProperty(rareInput = 1_234_567_891, maximumInput = Int.MAX_VALUE) + + val artifact = run( + compiled, + PropertyRelationGuidance.numericLocal(compiled), + numRuns = PropertyRunConfiguration().numRuns, + ) + val file = root.resolve("bounded-campaign.json") + artifact.write(file) + val restored = PropertyCampaignArtifact.read(file) + + val concrete = assertNotNull(restored.result.concrete) + val observations = assertNotNull(concrete.observations) + val trace = assertNotNull(restored.result.relationGuidance) + assertEquals(100, concrete.numRuns) + assertTrue(observations.droppedInvocations > 0 || observations.droppedPoints > 0) + val selection = assertNotNull(trace.selection) + val equality = selection.inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + assertTrue(equality.evidence.size >= 2) + assertTrue(equality.evidence.all { it.holds }) + assertTrue(trace.attempts.isNotEmpty(), "Recorded relation: ${equality.status}, ${equality.limitations}") + val attempt = trace.attempts.single() + assertEquals(ScalarRelationStatus.SAMPLED, equality.status) + assertTrue(ScalarRelationLimitation.INCOMPLETE_CAPTURE in equality.limitations) + assertEquals(observations.droppedInvocations, selection.inference.droppedInvocations) + assertEquals(observations.droppedPoints, selection.inference.droppedPoints) + assertTrue(equality.evidence.all { it.invocation.pointsTruncated == false }) + assertEquals(UsvmRelationRefutationStatus.REFUTATION_REACHED, attempt.searchStatus) + assertEquals(WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, attempt.confirmation?.status) + assertEquals(WitnessOracleOutcome.HOLDS, attempt.confirmation?.originalReplay?.outcome) + assertEquals(ObservationBuildStatus.UNVERIFIED, assertNotNull(trace.selection).inference.buildStatus) + assertTrue(trace.originalAllocatedMillis >= trace.originalReserveMillis) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, restored.result.symbolic?.status) + assertFalse(restored.result.confirmedViolation) + } + @Test fun `one PBT snapshot challenges a sampled local equality and retains the unrestricted original search`() { val compiled = numericProperty() @@ -223,21 +263,26 @@ class PropertyRelationCampaignTest { relationGuidance = guidance, ) - private fun numericProperty(delta: String = "- 1", sparsePrefix: Boolean = false): CompiledDslProperty { + private fun numericProperty( + delta: String = "- 1", + sparsePrefix: Boolean = false, + rareInput: Int = 417, + maximumInput: Int = 1000, + ): CompiledDslProperty { val prefix = if (sparsePrefix) "const cache: number[] = []; cache[1001] = input;" else "" Files.writeString( root.resolve("functions.ts"), """ export function transform(input: number): number { $prefix - if (input === 417) return input $delta; + if (input === $rareInput) return input $delta; return input; } """.trimIndent() ) val program = defineProperty(id = "campaign.local-relation") { val transform = function<(Double) -> Double>(module = "functions.ts", exportName = "transform") - val input by int(min = 0, max = 1000) + val input by int(min = 0, max = maximumInput) val result by value(transform(input)) check(name = "bound") { result lessOrEqual input } diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt index 06242ca2d5..09c9256744 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt @@ -191,6 +191,21 @@ class EntryRelationRefutationTest { assertNull(refutation.inputs) } + @Test + fun `bounded native entry samples retain exact binding without bypassing original admission`() { + val inference = observe(predicate = "reflexive", precondition = "ordered", numRuns = 100) + val order = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + + val refutation = refute(inference, order) + + assertEquals(ScalarRelationStatus.SAMPLED, order.status) + assertTrue(ScalarRelationLimitation.INCOMPLETE_CAPTURE in order.limitations) + assertTrue(inference.droppedInvocations > 0) + assertEquals(EtsMappingStatus.EXACT, refutation.binding.status) + assertEquals(UsvmEntryRefutationStatus.PRECONDITION_REJECTED, refutation.status) + assertNull(refutation.inputs) + } + private fun refute(inference: ScalarRelationInference, relation: ScalarRelation): UsvmEntryRelationRefutation { val manifest = inference.property.toManifest() @@ -203,6 +218,7 @@ class EntryRelationRefutationTest { leftDomain: PropertyDomain = IntegerDomain(min = 0, max = 2), points: List = listOf(LEFT, RIGHT), seed: Int = 1, + numRuns: Int = 2, ): ScalarRelationInference { val property = PropertyDefinition( id = PropertyId("entry.auxiliary"), @@ -226,7 +242,7 @@ class EntryRelationRefutationTest { property, PropertyRunConfiguration( seed = seed, - numRuns = 2, + numRuns = numRuns, observationRequest = PropertyObservationRequest(points = points, sources = sources), ), ) 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 588c4e499c..35bd0b7604 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 @@ -18,6 +18,8 @@ import org.usvm.ts.pbt.observation.PropertyPointEvent * 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. + * Recording limits bound the sample, not the PBT executions: only complete recorded pairs supply + * evidence. Omission and truncation warnings remain visible without claiming agreement on lost executions. * * 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. @@ -85,6 +87,11 @@ private fun evaluatePair( limitations += ScalarRelationLimitation.INCOMPLETE_CAPTURE } + val unmarkedInvocation = observations.invocations.any { it.pointsTruncated == null } + val markedTruncation = observations.invocations.any { it.pointsTruncated == true } + val unattributedPointDrops = observations.droppedPoints > 0 && (unmarkedInvocation || !markedTruncation) + if (unattributedPointDrops) limitations += ScalarRelationLimitation.UNATTRIBUTED_POINT_DROPS + val matched = if (validPair && sourcesPresent) { invocations.mapNotNull { invocation -> numericPair(invocation, pair, limitations) } } else { @@ -119,7 +126,7 @@ private fun evaluatePair( val status = when { refuted -> ScalarRelationStatus.REFUTED matched.isEmpty() && unsupported -> ScalarRelationStatus.UNSUPPORTED - limitations.isNotEmpty() -> ScalarRelationStatus.INSUFFICIENT + limitations.any { !it.isSamplingWarning } -> ScalarRelationStatus.INSUFFICIENT else -> ScalarRelationStatus.SAMPLED } @@ -145,26 +152,39 @@ private fun numericPair( return null } + val truncated = invocation.pointsTruncated == true || invocation.input.status == ObservationValueStatus.TRUNCATED 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) { + 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) + val left = leftEvents.singleOrNull() + val right = rightEvents.singleOrNull() + val identitiesMatch = (left == null || left.matches(pair.left)) && (right == null || right.matches(pair.right)) if (!identitiesMatch) { limitations += ScalarRelationLimitation.POINT_IDENTITY_MISMATCH return null } - val numeric = left.isNumber() && right.isNumber() - if (!numeric) { + val malformedValues = listOfNotNull(left, right).any { event -> + !event.isNumber() && !(truncated && event.value.status == ObservationValueStatus.TRUNCATED) + } + if (malformedValues) { + limitations += ScalarRelationLimitation.UNSUPPORTED_VALUE + return null + } + if (truncated) { + limitations += ScalarRelationLimitation.TRUNCATED_INVOCATION + return null + } + if (left == null || right == null) { + limitations += ScalarRelationLimitation.MISSING_POINT + return null + } + val inputCaptured = invocation.input.status == ObservationValueStatus.CAPTURED && + invocation.input.value is JsConcreteValue.Array + if (!inputCaptured) { limitations += ScalarRelationLimitation.UNSUPPORTED_VALUE return null } 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 67218101c7..fcb05f7bb5 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 @@ -48,6 +48,8 @@ enum class ScalarRelationLimitation { CONSTANT_OBSERVED_PAIR, INVOCATION_LIMIT, INCOMPLETE_CAPTURE, + TRUNCATED_INVOCATION, + UNATTRIBUTED_POINT_DROPS, } /** Exact same-invocation point values, retaining origin, phase, input and event identities. */ @@ -86,3 +88,16 @@ data class ScalarRelationInference( /** Sampled entry relations already implied by declared numeric input support, retained for audit. */ val domainImpliedRelations: List = emptyList(), ) + +/** These warnings bound the observed sample; every other limitation blocks usable numeric support. */ +internal val ScalarRelationLimitation.isSamplingWarning: Boolean + get() = when (this) { + ScalarRelationLimitation.INVOCATION_LIMIT, + ScalarRelationLimitation.INCOMPLETE_CAPTURE, + ScalarRelationLimitation.TRUNCATED_INVOCATION, + -> true + else -> false + } + +internal fun ScalarRelation.hasSampledSupport(): Boolean = + status == ScalarRelationStatus.SAMPLED && limitations.all { it.isSamplingWarning } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt index 15acfcc9f3..59b6689edb 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt @@ -58,7 +58,7 @@ fun selectScalarGuidance( 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 sampled = relation.hasSampledSupport() val restatesOriginal = known && original?.implies(relation) == true val reason = when { !sampled -> ScalarGuidanceExclusionReason.NOT_SAMPLED diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/observation/PropertyObservation.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/observation/PropertyObservation.kt index 62d4febbf7..6f7121ebca 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/observation/PropertyObservation.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/observation/PropertyObservation.kt @@ -189,6 +189,8 @@ data class PropertyInvocationObservation( val admission: ObservationAdmission, val outcome: ObservationOutcome, val points: List, + /** Null for older producers; true means some point data was lost within this invocation. */ + val pointsTruncated: Boolean? = null, ) /** Optional artifact: unknown phase is not independent random evidence. */ diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt index 236f1158e0..74733906fc 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt @@ -8,7 +8,7 @@ import org.usvm.ts.pbt.dsl.CompiledDslProperty 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 +import org.usvm.ts.pbt.inference.hasSampledSupport import org.usvm.ts.pbt.inference.matches import org.usvm.ts.pbt.mapping.EtsEntryPointTarget import org.usvm.ts.pbt.mapping.EtsInputBinding @@ -58,8 +58,7 @@ fun bindDslNumericLocalRelation( message = "The retained program must reproduce the compiler output" ) } - val sampled = relation in inference.relations && relation.status == ScalarRelationStatus.SAMPLED && - relation.limitations.isEmpty() && relation.evidence.isNotEmpty() + val sampled = relation in inference.relations && relation.hasSampledSupport() && relation.evidence.isNotEmpty() if (!sampled) return unbound(reason = "not-sampled", message = "A complete sampled relation is required") val resultIsLeft = relation.pair.left == capture.result && relation.pair.right == capture.input diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationBinding.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationBinding.kt index 1d07374c01..1c6abaf170 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationBinding.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationBinding.kt @@ -6,8 +6,8 @@ import org.usvm.UBoolExpr import org.usvm.machine.state.TsState import org.usvm.ts.pbt.inference.ScalarRelation import org.usvm.ts.pbt.inference.ScalarRelationInference -import org.usvm.ts.pbt.inference.ScalarRelationStatus import org.usvm.ts.pbt.inference.ScalarRelationTemplate +import org.usvm.ts.pbt.inference.hasSampledSupport import org.usvm.ts.pbt.inference.matches import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.manifest.toManifest @@ -67,8 +67,7 @@ internal fun bindEntryRelation( return unsupported(reason = "property-mismatch", message = "Property definition or declared support changed") } - val sampled = relation in inference.relations && relation.status == ScalarRelationStatus.SAMPLED && - relation.limitations.isEmpty() + val sampled = relation in inference.relations && relation.hasSampledSupport() if (!sampled) { return unsupported(reason = "not-sampled", message = "A sampled relation from this inference is required") } 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 index 17818cd643..7e4f1400b3 100644 --- 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 @@ -223,12 +223,16 @@ class DomainImpliedScalarRelationTest { 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)) + val bounded = 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() }) + assertTrue(bounded.domainImpliedRelations.isNotEmpty()) + val warningsPreserved = bounded.domainImpliedRelations.all { + ScalarRelationLimitation.INCOMPLETE_CAPTURE in it.limitations + } + assertTrue(warningsPreserved) + assertTrue(listOf(refuted, insufficient).all { it.domainImpliedRelations.isEmpty() }) } @Test 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 index d74b74d517..6f03f2f7bf 100644 --- 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 @@ -1,6 +1,9 @@ package org.usvm.ts.pbt.inference +import kotlinx.serialization.json.JsonObject +import kotlinx.serialization.json.jsonObject import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.manifest.PropertyManifestJson import org.usvm.ts.pbt.model.IntegerDomain import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.JsNumber @@ -28,6 +31,7 @@ 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.assertNull import kotlin.test.assertSame import kotlin.test.assertTrue @@ -254,6 +258,97 @@ class InferScalarRelationsTest { assertTrue(droppedResult.relations.all { ScalarRelationLimitation.INCOMPLETE_CAPTURE in it.limitations }) } + @Test + fun `bounded sampling warnings preserve agreement only over complete retained invocations`() { + val samples = listOf( + invocation(id = 0, left = 0.0, right = 0.0), + invocation(id = 1, left = 1.0, right = 1.0), + invocation(id = 2, left = 2.0, right = 0.0), + ) + val observations = artifact(samples).copy(droppedInvocations = 97) + + val result = inferScalarRelations(PROPERTY, observations, listOf(PAIR), maxInvocations = 2) + val selected = selectScalarGuidance(result) + + assertEquals(2, selected.candidates.size) + assertTrue(result.relations.all { it.status == ScalarRelationStatus.SAMPLED }) + assertTrue(result.relations.all { it.evidence.map { evidence -> evidence.invocation } == samples.take(2) }) + assertTrue(result.relations.all { ScalarRelationLimitation.INVOCATION_LIMIT in it.limitations }) + assertTrue(result.relations.all { ScalarRelationLimitation.INCOMPLETE_CAPTURE in it.limitations }) + assertEquals(1, result.omittedInvocations) + assertEquals(97, result.droppedInvocations) + assertEquals(ObservationBuildStatus.UNVERIFIED, result.buildStatus) + assertEquals(samples, observations.invocations) + } + + @Test + fun `truncated invocations retain raw points but cannot supply either independent support or binding evidence`() { + val good = listOf(invocation(id = 0, left = 0.0, right = 0.0), invocation(id = 1, left = 1.0, right = 1.0)) + val partial = invocation(id = 2, left = 2.0, right = 2.0).copy(pointsTruncated = true) + val observations = artifact(good + partial).copy(droppedPoints = 1) + val partialPair = partial.copy(points = partial.points.take(1)) + + for (truncated in listOf(partial, partialPair)) { + val recorded = observations.copy(invocations = good + truncated) + val result = inferScalarRelations(PROPERTY, recorded, listOf(PAIR)) + + assertTrue(result.relations.all { it.status == ScalarRelationStatus.SAMPLED }) + assertTrue(result.relations.all { it.evidence.map { evidence -> evidence.invocation } == good }) + assertTrue(result.relations.all { ScalarRelationLimitation.TRUNCATED_INVOCATION in it.limitations }) + assertEquals(2, selectScalarGuidance(result).candidates.size) + assertEquals(1, result.droppedPoints) + assertEquals(good + truncated, recorded.invocations) + } + val oneGood = observations.copy(invocations = good.take(1) + partial) + val insufficient = inferScalarRelations(PROPERTY, oneGood, listOf(PAIR)) + assertTrue(insufficient.relations.all { it.status == ScalarRelationStatus.INSUFFICIENT }) + assertTrue(selectScalarGuidance(insufficient).candidates.isEmpty()) + } + + @Test + fun `older observation JSON keeps unknown point completeness while new receipts round trip their marker`() { + val sample = invocation(id = 0, left = 0.0, right = 0.0) + val json = PropertyManifestJson.json + val serializer = PropertyInvocationObservation.serializer() + val value = json.encodeToJsonElement(serializer, sample).jsonObject + val legacy = JsonObject(value - "pointsTruncated") + + val decoded = json.decodeFromJsonElement(serializer, legacy) + + assertNull(decoded.pointsTruncated) + for (marker in listOf(null, false, true)) { + val changed = sample.copy(pointsTruncated = marker) + val encoded = json.encodeToString(serializer, changed) + assertEquals(changed, json.decodeFromString(serializer, encoded)) + } + } + + @Test + fun `recording truncation does not excuse repeated mismatched nonnumeric nested or incomplete observations`() { + val good = listOf(invocation(id = 0, left = 0.0, right = 0.0), invocation(id = 1, left = 1.0, right = 1.0)) + val partial = invocation(id = 2, left = 2.0, right = 2.0).copy(pointsTruncated = true) + val first = partial.points.first() + val failures = listOf( + partial.copy(points = partial.points + first.copy(occurrence = 1)), + partial.copy(points = listOf(first.copy(inputIndex = 7), partial.points.last())), + partial.copy(points = listOf(first.copy(value = captured(JsConcreteValue.String("bad"))))), + partial.copy(parentInvocationId = 0), + partial.copy(outcome = ObservationOutcome.PENDING), + ) + for (invalid in failures) { + val observations = artifact(good + invalid).copy(droppedPoints = 1) + + val result = inferScalarRelations(PROPERTY, observations, listOf(PAIR)) + + assertTrue(result.relations.none { it.status == ScalarRelationStatus.SAMPLED }) + assertTrue(selectScalarGuidance(result).candidates.isEmpty()) + } + val legacy = artifact(good.map { it.copy(pointsTruncated = null) }).copy(droppedPoints = 1) + val result = inferScalarRelations(PROPERTY, legacy, listOf(PAIR)) + assertTrue(result.relations.all { ScalarRelationLimitation.UNATTRIBUTED_POINT_DROPS in it.limitations }) + assertTrue(selectScalarGuidance(result).candidates.isEmpty()) + } + @Test fun `selected source hashes are checked against property identity when declared`() { val sourceIdentity = PropertySourceIdentity( @@ -362,6 +457,7 @@ class InferScalarRelationsTest { admission = ObservationAdmission.ADMITTED, outcome = ObservationOutcome.HOLDS, points = listOf(event(LEFT, left, ordinal = 0), event(RIGHT, right, ordinal = 1)), + pointsTruncated = false, ) private fun event(point: PropertyObservationPoint, number: Double, ordinal: Int): PropertyPointEvent =