Repository navigation
[TS PBT] Execute Kotlin property definitions with fast-check #348
Description
Completed foundation and current continuation
The delivered fast-check execution/replay path and completed #384 contract are reused by #353 and #354. #396 adds per-run program values; #395 adapts user-authored properties/generators; #400 extends supported choice/context reuse. Executing an explicit example does not guarantee shrinking or neighborhood generation.
The original delivered scope below is historical context; new acceptance criteria are owned by the linked open issues.
Original delivered scope (historical)
Current follow-up
#384 is the priority correction for shared invocation semantics. It distinguishes a false precondition from a thrown/invalid precondition, preserves sample isolation, and reuses this backend's existing execution/replay/shrinking path. No new process protocol, custom shrinker or generic purity detector is required. This delivered issue remains closed; implementation corrections belong to #384.
Goal
Implement fast-check as the first concrete PBT backend for Kotlin property definitions.
Why
The Kotlin-first property model must be connected to a real concrete PBT lifecycle without making Node or fast-check the pipeline orchestrator.
Kotlin should select and validate a property, invoke the backend through a private one-shot protocol, and receive a structured result. The internal Node runtime should reconstruct fast-check arbitraries, import the declared TypeScript entry points, and keep fast-check authoritative for generation, execution, replay, and shrinking.
Scope
- Implement a
FastCheckBackendfor the common Kotlin PBT backend interface. - Load Kotlin property registries and reject duplicate property IDs.
- Serialize validated property definitions and run configuration into a private backend request.
- Launch and supervise the internal Node bridge from Kotlin.
- Reconstruct fast-check arbitraries from engine-neutral domain descriptors.
- Import TypeScript predicate and precondition module/export references.
- Support synchronous and asynchronous predicates.
- Execute properties through
fc.check. - Support:
- seed;
- replay path;
- number of runs;
- timeout;
- explicit examples.
- Produce a structured backend result containing:
- backend ID and version;
- property ID;
- success or failure status;
- seed and replay path;
- counterexample;
- run, skip, and shrink counts;
- failure details;
- execution time.
- Distinguish property failures, invalid backend requests, Node process failures, protocol errors, and timeouts.
- Provide a Kotlin command-line entry point for running one property or a property registry with the fast-check backend.
Source coverage, EtsIR integration, symbolic execution, and generic pipeline orchestration are outside this issue.
Definition of Done
- Kotlin selects and executes example property definitions through
FastCheckBackend. - Node is an internal backend runtime and never orchestrates USVM or the overall pipeline.
- Both synchronous and asynchronous TypeScript predicates are supported.
- A failing property produces a structured counterexample and shrink information.
- A failure can be reproduced using the reported seed and path.
- Explicit examples are executed through the same property definition.
- Duplicate IDs, invalid entry points, malformed protocol messages, and backend process failures produce actionable diagnostics.
- Reproduction uses the same property, configuration, fast-check version, seed and replay path. Timeouts and unsupported external/module state are reported; identical wall-clock-limited output is not promised.
- Focused tests cover successful, failing, asynchronous, replay, timeout, and invalid-property cases.
- The Kotlin API, internal protocol, CLI usage, and result format are documented.
- The implementation is delivered in a dedicated PR linked to this issue.
Activity
[-][TS PBT] Execute shared property definitions with fast-check[/-][+][TS PBT] Execute Kotlin property definitions with fast-check[/+]