[TS PBT] Execute Kotlin properties with fast-check by CaelmBleidd · Pull Request #375 · UnitTestBot/usvm

CaelmBleidd · 2026-08-23T14:25:47Z

Closes #348

Summary

keep property definitions, validation, registries, orchestration, and public results on the Kotlin side
use a thin packaged Node adapter to load TypeScript through tsx and delegate execution to fc.check
support seed and replay, explicit examples, shrinking, synchronous and asynchronous predicates/preconditions, and typed failures
exchange one versionless request and response with explicit diagnostic categories
supervise each property process with concurrent bounded I/O, a hard deadline, and forced termination when needed
document component dependencies and the complete execution flow in DESIGN.md

Verification

npm test in usvm-ts-pbt/fast-check-adapter — 36 tests
./gradlew :usvm-ts-pbt:check :usvm-ts-pbt:detekt :usvm-ts-pbt:installDist — 63 JVM tests, 0 detekt findings, distribution built

CaelmBleidd · 2026-08-24T12:52:53Z

+    const sourceRoot = sourceRoots[index];
+    if (sourceRoot === undefined || !path.isAbsolute(sourceRoot)) {
+      throw protocolError(
+        'source-root.invalid',


What are these strings? Do they occur randomly or the correponding matching exists somewhere? If it does, these lines should be places in some shared place with resources

Fixed. The adapter-owned identifiers are centralized in diagnostics.ts. Each descriptor carries both its stable code and explicit category, so call sites contain no raw diagnostic codes and Kotlin does not infer categories from prefixes.

CaelmBleidd · 2026-08-24T12:55:00Z

+}
+
+export interface PropertyManifestWire {
+  schemaVersion: number;


We discussed that there is no need in schemaVersion and protocolVersion since this files won't be saved anywhere and the latest version will be always the one

Removed schemaVersion and protocolVersion from the manifest and from both execution and projection request/response types. The private one-shot producer and consumer ship together, so there is no compatibility branch left.

CaelmBleidd · 2026-08-24T12:57:51Z

+  if (request.seed !== undefined && !isSignedInt(request.seed)) {
+    throw protocolError('protocol.seed.invalid', 'Seed must be a signed 32-bit integer', 'seed');
+  }
+  if (request.replayPath !== undefined &&


You must always extract such long and complicated conditions from the if condition

Fixed. The compound check is now named invalidReplayPath before the if statement.

CaelmBleidd · 2026-08-24T12:58:19Z

+
+function validateManifest(value: unknown): PropertyManifestWire {
+  const manifest = requireRecord(value, 'protocol.manifest.invalid', 'Manifest must be an object', 'manifest');
+  const valid = manifest.schemaVersion === 1


What is this? Why is it hardcoded with a particular version?

Removed this schema-version check together with the schemaVersion field.

CaelmBleidd · 2026-08-24T12:58:27Z

+    return { name: input.name, domain: input.domain };
+  });
+  const validated: PropertyManifestWire = {
+    schemaVersion: 1,


Removed the hardcoded schemaVersion from the reconstructed manifest.

CaelmBleidd · 2026-08-24T13:07:03Z

+}
+
+private const val MAX_RUNS = 10_000
+private const val MAX_TIMEOUT_MILLIS = 86_400_000L


Why? What is this number?

Removed the arbitrary one-day cap. The only upper bound now is Int.MAX_VALUE milliseconds, which matches the signed 32-bit delay supported by Node timers; that reason is documented in the configuration and design document.

CaelmBleidd · 2026-08-24T13:08:05Z

+
+    companion object {
+        private const val MAX_RUNS = 10_000
+        private const val MAX_TIMEOUT_MILLIS = 86_400_000L


Why? And it is the same constant as in another file. Looks suspicious, are they related?

Removed the duplicate backend constant. The CLI and backend now use PropertyRunConfiguration.MAX_TIMEOUT_MILLIS as the single Kotlin-side definition.

CaelmBleidd · 2026-08-24T13:11:05Z

+    }
+
+    private companion object {
+        const val PROCESS_IO_THREADS = 3


Isn't it too little?

Replaced the fixed three-thread pool with a cached executor. The client still submits exactly three independent tasks for stdin, stdout, and stderr, but scheduling no longer depends on a magic pool size.

CaelmBleidd · 2026-08-24T13:13:52Z

+    val value = validDoubleOrNull() ?: return false
+    val minimum = runCatching(domain.min::toDouble).getOrNull() ?: return false
+    val maximum = runCatching(domain.max::toDouble).getOrNull() ?: return false
+    return value in minimum..maximum


It is correct logic for numbers?

Verified and covered with focused tests for range boundaries, positive and negative zero, fractions, NaN, infinities, and invalid encodings. Membership deliberately matches the values the corresponding fast-check arbitrary can generate: fc.integer excludes negative zero, while NumberDomain preserves binary64 special values according to its bounds and allowNaN.

CaelmBleidd · 2026-08-24T13:14:13Z

+
+private fun JsConcreteValue.Number.validDoubleOrNull(): Double? = runCatching(::toDouble).getOrNull()
+
+private const val NEGATIVE_ZERO_BITS = "8000000000000000"


Can we not hardcode it and use some functions to extract it?

Fixed. Negative zero is now derived with Double.fromBits(Long.MIN_VALUE).toRawBits(), and values are checked through Double.toRawBits(); the hardcoded hexadecimal representation is gone.

CaelmBleidd added 2 commits August 23, 2026 15:21

[TS PBT] Execute Kotlin properties with fast-check

72d6c47

Format TypeScript logical blocks

4c6c965

CaelmBleidd commented Aug 24, 2026

View reviewed changes

CaelmBleidd added 2 commits August 24, 2026 16:15

Format Kotlin logical blocks

13f1723

[TS PBT] Simplify Kotlin Node contract

9d79c14


		private fun JsConcreteValue.Number.validDoubleOrNull(): Double? = runCatching(::toDouble).getOrNull()

		private const val NEGATIVE_ZERO_BITS = "8000000000000000"

Uh oh!

Conversation

CaelmBleidd commented Aug 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Verification

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

CaelmBleidd commented Aug 23, 2026 •

edited

Loading