[TS PBT] Align property execution semantics

usvm-ts-pbt/DESIGN.md

@@ -10,6 +10,8 @@ API and CLI examples, see [README.md](README.md).
 - Per-property source coverage is an optional backend capability collected by Kotlin through an isolated c8 run.
 - A backend-neutral Kotlin mapping layer connects manifests and source coverage to EtsIR without changing the
   declarative property model.
+- One [property execution contract](PROPERTY_EXECUTION_CONTRACT.md) defines concrete, replay, projection, and
+  symbolic-search semantics.
 - The JSON exchange is one request and one response from the same packaged distribution; it has no persistence or
   compatibility negotiation.
 - Failures are typed without exposing runtime-dependent Node stack traces.
@@ -111,12 +113,11 @@ sequenceDiagram
     Backend-->>Caller: PropertyRunResult
 ```
 
-Input order is preserved from `PropertyDefinition.inputs` to the positional TypeScript arguments. If either the
-predicate or precondition is asynchronous, the adapter uses `fc.asyncProperty`; otherwise it uses `fc.property`.
-A false precondition becomes `fc.pre(false)`, leaving skip accounting to fast-check.
-Each callback receives its own recursive clone of the generated arguments. This keeps predicate and precondition
-mutations from changing fast-check's retained sample or leaking from one callback into the other during shrinking
-and replay, while preserving aliases and cycles within one invocation.
+The normative behavior is defined by the [property execution contract](PROPERTY_EXECUTION_CONTRACT.md).
+Mechanically, input order is preserved from `PropertyDefinition.inputs` to positional TypeScript arguments. If
+either entry point is asynchronous, the adapter uses `fc.asyncProperty`; otherwise it uses `fc.property`. A false
+precondition becomes `fc.pre(false)`, leaving skip accounting to fast-check. One `structuredClone` isolates each
+fast-check invocation; the precondition and predicate then receive that same clone in sequence.
 
 ## Results, errors, and timeouts
 
@@ -125,18 +126,19 @@ flowchart TD
     Check[Property execution] --> Held{Outcome}
     Held -->|held| Success[SUCCESS result]
     Held -->|falsified| Failure[FAILURE result with counterexample]
+    Held -->|discard budget exhausted| Discarded[FAILURE with PRECONDITION_EXHAUSTED]
     Held -->|fast-check timeout| TimeoutResult[FAILURE result with timeout details]
-    Held -->|typed adapter error| Diagnostic[Error response with explicit category]
+    Held -->|precondition or typed adapter error| Diagnostic[Error response with explicit category]
     Diagnostic --> Exception[PbtBackendException]
     Held -->|unexpected Node failure| Exit[Non-zero exit or invalid response]
     Exit --> Transport[PROCESS_FAILURE or PROTOCOL_ERROR]
     Held -->|hard JVM deadline| Kill[Terminate, then force-kill]
     Kill --> HardTimeout[TIMEOUT exception]
 ```
 
-Falsification and a timeout cleanly reported by fast-check are completed property results. Invalid input,
-entry-point failures, process failures, malformed responses, and the JVM hard timeout are infrastructure
-exceptions.
+Falsification, discard-budget exhaustion, and a timeout cleanly reported by fast-check are completed results with
+distinct failure kinds. Only falsification is a candidate property violation. Invalid input, entry-point contract
+failures, process failures, malformed responses, and the JVM hard timeout are infrastructure exceptions.
 
 Coverage collection failures use the separate `COVERAGE` infrastructure category. Stable diagnostics distinguish
 an unsupported backend or Node runtime, unavailable runtime version, missing collector, missing or malformed
@@ -281,6 +283,8 @@ classifier because `tsx` depends on a native esbuild package.
   fast-check: startup failure, non-zero exit, malformed output, explicit diagnostic categories, and hard timeout.
 - Backend integration tests execute real uncompiled TypeScript through the packaged adapter, including replay,
   shrinking, explicit examples, preconditions, async predicates, and timeouts.
+- Shared contract fixtures cover precondition admission, discard and errors; predicate violations and errors;
+  special values; aliases; mutation isolation; shrinking; and replay through observable outcomes.
 - Coverage golden tests assert literal TypeScript statement and branch outcomes for successful and falsified runs,
   cross-property isolation, scope and glob filtering, and source-map/report diagnostics.
 - Mapping golden tests load stable TypeScript fixtures through the native frontend and cover predicate,

usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md

@@ -0,0 +1,94 @@
+# Property execution contract
+
+This document is the normative contract shared by concrete execution, replay, shrinking, domain projection, and
+symbolic property search. Backend-specific documents may describe mechanics, but they must not redefine these
+semantics.
+
+## Inputs and one invocation
+
+Inputs follow the ordered Kotlin `PropertyDefinition.inputs` domains and the tagged `JsConcreteValue` encoding.
+Argument order is preserved. `undefined`, `null`, UTF-16 strings, NaN, both infinities, negative zero, and nested
+arrays retain their JavaScript meaning.
+
+Every predicate attempt receives an isolated input graph. Concrete generation, explicit examples, replay, and
+each shrinking attempt must not observe mutation left by another attempt. Aliases and cycles already present in
+one backend input graph are preserved inside that invocation. The tagged wire representation is a value tree and
+does not create reference identity between independently encoded nodes.
+
+When a property has a precondition, the precondition and predicate run sequentially over the same isolated graph.
+This matches symbolic execution, where both functions observe one state. A supported precondition is pure, so it
+does not change that graph.
+
+## Precondition
+
+A supported precondition is a pure boolean function of its inputs.
+
+| Completion            | Meaning                                                                           |
+| --------------------- | --------------------------------------------------------------------------------- |
+| `true`                | Admit the input and invoke the predicate.                                         |
+| `false`               | Discard the input without invoking the predicate.                                 |
+| Escaping exception    | Property-definition or execution error; never a discard or counterexample.        |
+| Non-boolean result    | Property-definition or execution error; never a discard or counterexample.        |
+| Unsupported execution | Report unsupported explicitly; do not substitute different execution semantics.   |
+
+If a concrete run exhausts fast-check's discard budget, it completes with
+`PropertyFailureKind.PRECONDITION_EXHAUSTED`. This is not a property violation and has no counterexample.
+
+Synchronous preconditions are the initial shared concrete and symbolic subset. Existing asynchronous concrete
+preconditions retain their JavaScript meaning; symbolic projection and search report them as unsupported.
+
+## Predicate
+
+A predicate returns a boolean.
+
+| Completion         | Meaning                                                                        |
+| ------------------ | ------------------------------------------------------------------------------ |
+| `true`             | The property holds for this invocation.                                        |
+| `false`            | Candidate property violation.                                                  |
+| Escaping exception | Candidate property violation, including an escaping assertion exception.       |
+| Non-boolean result | Property-definition or execution error; never a candidate property violation.  |
+
+An expected exception belongs inside the property: the predicate catches it, checks it, and returns a boolean.
+Asynchronous predicates remain available to the concrete backend and unsupported by symbolic execution until the
+symbolic engine can preserve their meaning.
+
+## Mutation and external state
+
+Predicate-local mutation of supported input values is allowed. The invocation boundary isolates it from other
+generated samples, explicit examples, replay, and shrinking while retaining aliases inside the current graph.
+
+Precondition purity is an author obligation. The initial contract does not include a purity analyzer, heap
+snapshotting, rollback of arbitrary side effects, mutable objects beyond the supported value model, or persistent
+external or module state. Properties that depend on those behaviors are outside the supported subset.
+
+## Projection and search classifications
+
+Projection is always relative to the complete declared Kotlin input domain:
+
+| Level         | Required interpretation                                                                                |
+| ------------- | ------------------------------------------------------------------------------------------------------ |
+| `EXACT`       | The projected values have exactly the declared domain semantics.                                       |
+| `APPROXIMATE` | Diagnostics state whether the projection over-approximates, under-approximates, or combines both.      |
+| `UNSUPPORTED` | The backend cannot preserve the declared semantics and must not silently execute a different property. |
+
+An over-approximation may produce candidates outside the declared domain; they require concrete validation. An
+under-approximation omits declared inputs, so an unsuccessful search cannot establish that the property holds.
+Every retained approximation must document its direction and limitation in a capability diagnostic.
+
+Only predicate `false` and escaping predicate exceptions are candidate violations. Timeout, unsupported
+execution, solver uncertainty, input-resolution failure, tool failure, and discard-budget exhaustion are neither
+violations nor proof that the property holds. A bounded search with no candidate reports only that no violation
+was reached within that search.
+
+## Implementation and regression points
+
+- `fast-check-adapter/src/execute-property.ts` applies this contract to generation, explicit examples, replay, and
+  shrinking through the existing fast-check invocation.
+- `fast-check-adapter/src/project-domain.ts` projects the declared Kotlin domains for concrete execution.
+- Downstream USVM projection and search implementations consume the same manifest and mapping artifacts and must
+  link to this contract when their dependent changes are integrated.
+- `src/test/resources/properties/contract/PropertyExecutionContract.ts` provides concrete regression coverage;
+  downstream symbolic integration extends the same fixture with symbolic assertions.
+
+Replay remains ordinary concrete execution with the reported seed and path. It does not introduce a separate
+property runner or alternate callback semantics.

usvm-ts-pbt/README.md

@@ -51,6 +51,9 @@ export function reverseTwicePreservesValues(values: number[]): boolean {
 `JsConcreteValue` is a lossless tagged representation used for examples and counterexamples. It preserves
 `undefined`, `null`, NaN, infinities, negative zero, and nested arrays.
 
+The normative behavior of inputs, preconditions, predicates, mutation isolation, projection, search, and replay is
+defined once in the [property execution contract](PROPERTY_EXECUTION_CONTRACT.md).
+
 ## Execute a property
 
 `FastCheckBackend` accepts TypeScript source roots and loads `.ts` entry points directly. User projects do not
@@ -75,12 +78,13 @@ The defaults are 100 successful runs and a 60-second timeout. Configuration also
 positional explicit examples. `PropertyRunResult` contains the property ID, status, actual seed, replay path,
 counterexample, run/skip/shrink counts, failure details, elapsed time, and optional per-property coverage.
 
-Predicate falsification and a timeout reported by fast-check are normal `FAILURE` results. Invalid input,
-entry-point, process, and transport failures throw `PbtBackendException`.
+Predicate falsification, discard-budget exhaustion, and a timeout reported by fast-check are completed `FAILURE`
+results with distinct `PropertyFailureKind` values. Only `PROPERTY` denotes a candidate violation;
+`PRECONDITION_EXHAUSTED` and `TIMEOUT` do not. Invalid input, entry-point contract, process, and transport failures
+throw `PbtBackendException`.
 
-Synchronous entry points must return a boolean directly. Asynchronous entry points must return an awaitable that
-resolves to a boolean. A false precondition is passed to fast-check as a skipped input. Generation, replay, explicit
-examples, checking, and shrinking retain fast-check semantics.
+Generation, replay, explicit examples, checking, and shrinking use the same invocation path and follow the
+[property execution contract](PROPERTY_EXECUTION_CONTRACT.md).
 
 ## Per-property TypeScript coverage
 

usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts

@@ -31,6 +31,7 @@ export const adapterDiagnostic = {
   domainKindUnknown: invalidRequest('domain.kind.unknown'),
   domainOptionalNil: invalidRequest('domain.optional.nil'),
   domainTupleEmpty: invalidRequest('domain.tuple.empty'),
+  domainConstantUnsupported: invalidRequest('domain.constant.unsupported'),
   domainNumberAllowNaNInvalid: invalidRequest('domain.number.allow-nan.invalid'),
   domainNumberBoundNaN: invalidRequest('domain.number.bound.nan'),
   domainNumberBounds: invalidRequest('domain.number.bounds'),
@@ -55,4 +56,5 @@ export const adapterDiagnostic = {
   entryPointModuleImportFailed: entryPoint('entrypoint.module.import-failed'),
   entryPointExecutionKindMismatch: entryPoint('entrypoint.execution-kind.mismatch'),
   entryPointResultInvalid: entryPoint('entrypoint.result.invalid'),
+  entryPointPreconditionThrew: entryPoint('entrypoint.precondition.threw'),
 } as const;

usvm-ts-pbt/fast-check-adapter/src/execute-property.ts

@@ -37,14 +37,15 @@ export interface FastCheckExecutionRequest {
   manifest: PropertyManifestWire;
   sourceRoots: string[];
   seed?: number;
+  /** Replay follows the same invocation contract as generation and shrinking. */
   replayPath?: string;
   numRuns: number;
   timeoutMillis: number;
   examples: TaggedJsValue[][];
 }
 
 export interface FastCheckFailureDetails {
-  kind: 'property' | 'timeout';
+  kind: 'property' | 'precondition-exhausted' | 'timeout';
   errorName: string;
   message: string;
 }
@@ -106,19 +107,63 @@ function buildProperty(
 
   if (asynchronous) {
     return fc.asyncProperty(arbitrary, async (values: JsConcreteValue[]): Promise<boolean> => {
-      if (precondition !== undefined && !(await precondition.invoke(cloneArguments(values)))) fc.pre(false);
+      const invocationValues = cloneArguments(values);
+      if (precondition !== undefined && !(await invokePrecondition(precondition, invocationValues))) fc.pre(false);
 
-      return await predicate.invoke(cloneArguments(values));
+      return await predicate.invoke(invocationValues);
     });
   }
 
   return fc.property(arbitrary, (values: JsConcreteValue[]): boolean => {
-    if (precondition !== undefined && !precondition.invoke(cloneArguments(values))) fc.pre(false);
+    const invocationValues = cloneArguments(values);
+    if (precondition !== undefined && !invokeSynchronousPrecondition(precondition, invocationValues)) fc.pre(false);
 
-    return predicate.invoke(cloneArguments(values)) as boolean;
+    return predicate.invoke(invocationValues) as boolean;
   });
 }
 
+async function invokePrecondition(
+  precondition: LoadedEntryPoint,
+  values: JsConcreteValue[],
+): Promise<boolean> {
+  try {
+    return await precondition.invoke(values);
+  } catch (error: unknown) {
+    throw classifyPreconditionError(error);
+  }
+}
+
+function invokeSynchronousPrecondition(
+  precondition: LoadedEntryPoint,
+  values: JsConcreteValue[],
+): boolean {
+  try {
+    return precondition.invoke(values) as boolean;
+  } catch (error: unknown) {
+    throw classifyPreconditionError(error);
+  }
+}
+
+function classifyPreconditionError(error: unknown): ProtocolError {
+  if (error instanceof ProtocolError) return error;
+
+  return protocolError(
+    adapterDiagnostic.entryPointPreconditionThrew,
+    `Property precondition threw ${describeThrownValue(error)}`,
+    'manifest.precondition',
+  );
+}
+
+function describeThrownValue(value: unknown): string {
+  if (value instanceof Error) {
+    const name = value.name || 'Error';
+
+    return value.message.length === 0 ? name : `${name}: ${value.message}`;
+  }
+
+  return `a non-Error value: ${String(value)}`;
+}
+
 async function checkProperty(
   property: fc.IProperty<[JsConcreteValue[]]> | fc.IAsyncProperty<[JsConcreteValue[]]>,
   parameters: Parameters<[JsConcreteValue[]]>,
@@ -139,28 +184,9 @@ async function checkProperty(
   }
 }
 
-/**
- * User callbacks must not mutate fast-check's sample, which it retains for shrinking and replay.
- * A shared clone map preserves aliases and cycles within one invocation while isolating separate invocations.
- */
+/** See [the contract](../../PROPERTY_EXECUTION_CONTRACT.md) for the invocation and isolation rules. */
 function cloneArguments(values: JsConcreteValue[]): JsConcreteValue[] {
-  return cloneArray(values, new Map());
-}
-
-function cloneArray(
-  value: JsConcreteValue[],
-  clones: Map<JsConcreteValue[], JsConcreteValue[]>,
-): JsConcreteValue[] {
-  const existing = clones.get(value);
-  if (existing !== undefined) return existing;
-
-  const clone: JsConcreteValue[] = [];
-  clones.set(value, clone);
-  for (const element of value) {
-    clone.push(Array.isArray(element) ? cloneArray(element, clones) : element);
-  }
-
-  return clone;
+  return structuredClone(values);
 }
 
 function buildParameters(request: FastCheckExecutionRequest): Parameters<[JsConcreteValue[]]> {
@@ -240,8 +266,8 @@ function failureDetails(details: RunDetails<[JsConcreteValue[]]>): FastCheckFail
 
   if (details.counterexample === null) {
     return {
-      kind: 'property',
-      errorName: 'PropertyFailure',
+      kind: 'precondition-exhausted',
+      errorName: 'PreconditionExhausted',
       message: 'Property could not satisfy its precondition within the skip limit',
     };
   }

usvm-ts-pbt/fast-check-adapter/src/project-domain.ts

@@ -21,6 +21,7 @@ export interface ProjectionCapability {
 
 type DomainRecord = Record<string, unknown>;
 
+/** See [the contract](../../PROPERTY_EXECUTION_CONTRACT.md) for projection fidelity requirements. */
 export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary<JsConcreteValue> {
   requireDomainObject(domain, path);
 
@@ -44,8 +45,19 @@ export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary<Js
         maxLength: domain.maxLength,
       }).map((units) => units.map((unit) => String.fromCharCode(unit)).join(''));
 
-    case 'constant':
-      return fc.constant(decodeJsValue(domain.value, `${path}.value`));
+    case 'constant': {
+      const value = decodeJsValue(domain.value, `${path}.value`);
+
+      if (Array.isArray(value)) {
+        throw protocolError(
+          adapterDiagnostic.domainConstantUnsupported,
+          'Constant domains support JavaScript primitives only',
+          path,
+        );
+      }
+
+      return fc.constant(value);
+    }
 
     case 'optional': {
       const nil = decodeJsValue(domain.nil, `${path}.nil`);