[TS PBT] Design a Kotlin-first property abstraction for PBT engines and USVM

[CaelmBleidd]

Current execution contract

#384 defines the shared precondition, predicate, exception and isolation semantics used by the downstream pipeline. Reuse the existing property/domain/value model; no second abstraction or version-negotiation layer is required. The historical delivery below remains completed; follow-up corrections are tracked by #384.

Goal

Design and implement a Kotlin-first, engine-neutral abstraction for describing property inputs, primitive domains, preconditions, and predicates for concrete PBT backends and USVM.

Why

USVM participates in the hybrid pipeline independently of the selected concrete PBT engine. fast-check is the first backend, but it must not own the property model or orchestration.

Separate fast-check arbitraries, backend metadata, and symbolic domains would duplicate semantics and allow projections to diverge. At the same time, arbitrary runtime PBT objects and JavaScript closures cannot be serialized or analyzed reliably by USVM.

A Kotlin property model should provide one source of truth. Backend adapters project that model into their native generators, while USVM projects it into symbolic inputs and constraints. TypeScript predicate and precondition bodies remain explicit exported entry points used by both execution paths.

Scope

• Design a Kotlin property API describing:
  • stable property ID;
  • named and ordered input domains;
  • optional TypeScript precondition entry point;
  • TypeScript property predicate entry point.
• Define engine-neutral Kotlin domain types for:
  • boolean;
  • integer and bounded integer;
  • number and bounded number;
  • string;
  • constant;
  • optional value;
  • tuple;
  • array.
• Define a JSON-serializable PropertyManifest and tagged JsConcreteValue encoding for JavaScript values that are not represented faithfully by ordinary JSON.
• Encode concrete tuple and array samples recursively as JsConcreteValue.Array, while keeping ConstantDomain restricted to JavaScript primitives.
• Define a PBT backend projection contract that does not expose backend-native arbitrary types to the common model.
• Implement the initial fast-check domain projection through a private Kotlin-to-Node protocol that reconstructs real fast-check Arbitrary objects.
• Represent predicate and precondition entry points explicitly as TypeScript module/export references and execution kind.
• Report capability per backend projection as exact, approximate, or unsupported.
• Derive an explicit concrete-only property capability with diagnostic reasons when a concrete backend can execute a property but USVM cannot analyze it.
• Validate property IDs, input names, bounds, lengths, constants, entry points, and manifests.

Property discovery, campaign execution, source-to-EtsIR resolution, symbolic lowering, and pipeline orchestration are outside this issue.

Definition of Done

• A documented Kotlin-first property API is implemented.
• The common model has no dependency on fast-check or another backend-native generator type.
• Supported Kotlin domains are projected into real fast-check arbitraries by the initial adapter.
• The same Kotlin definitions produce a validated, engine-neutral PropertyManifest.
• No duplicate concrete and symbolic domain declarations are required.
• TypeScript predicate and precondition entry points are explicit and serializable.
• Capability is reported per backend, and unsupported symbolic constructs produce an explicit concrete-only capability with diagnostic reason.
• Unsupported custom domains are rejected or represented through an explicit backend-specific extension marked unsupported by other backends.
• Focused Kotlin and Node tests cover domain projection, protocol round trips, manifest serialization, recursive concrete values, validation, and capability aggregation.
• Example properties cover at least:
  • a two-input relational property;
  • a property with bounded inputs;
  • a property with a precondition;
  • an array property.
• The current supported subset, backend contract, and extension points are documented.
• The implementation is delivered in a dedicated PR linked to this issue.