diff --git a/usvm-ts-pbt/DESIGN.md b/usvm-ts-pbt/DESIGN.md index 0e40b6057..72ef50064 100644 --- a/usvm-ts-pbt/DESIGN.md +++ b/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,8 +126,9 @@ 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] @@ -134,9 +136,9 @@ flowchart TD 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, diff --git a/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md b/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md new file mode 100644 index 000000000..e91f20c26 --- /dev/null +++ b/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. diff --git a/usvm-ts-pbt/README.md b/usvm-ts-pbt/README.md index 5f01f441a..6219768fd 100644 --- a/usvm-ts-pbt/README.md +++ b/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 diff --git a/usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts b/usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts index e1ab704f4..145b2d57b 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts +++ b/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; diff --git a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts index 0b562d5cb..a11e5a39d 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts @@ -37,6 +37,7 @@ 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; @@ -44,7 +45,7 @@ export interface FastCheckExecutionRequest { } 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 => { - 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 { + 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[] { - 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', }; } diff --git a/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts b/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts index 391993901..1743ab083 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts @@ -21,6 +21,7 @@ export interface ProjectionCapability { type DomainRecord = Record; +/** See [the contract](../../PROPERTY_EXECUTION_CONTRACT.md) for projection fidelity requirements. */ export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary { requireDomainObject(domain, path); @@ -44,8 +45,19 @@ export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary 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`); diff --git a/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts b/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts index 58d11dc5d..c309c9f70 100644 --- a/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts +++ b/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts @@ -3,6 +3,7 @@ import { mkdtemp, mkdir, realpath, rm, symlink, writeFile } from 'node:fs/promis import { tmpdir } from 'node:os'; import path from 'node:path'; import test from 'node:test'; +import { fileURLToPath } from 'node:url'; import { ProtocolError } from '../src/js-value.js'; import { loadEntryPoint } from '../src/entry-point.js'; @@ -198,6 +199,22 @@ test('enforces declared execution kind and boolean results', async () => { }); }); +test('preserves aliases in one supported invocation graph', async () => { + const loaded = await loadEntryPoint( + { + module: CONTRACT_MODULE, + exportName: 'preservesNestedArrayAlias', + executionKind: 'sync', + }, + [CONTRACT_SOURCE_ROOT], + 'manifest.predicate', + ); + const sharedElement = [1]; + const aliasedValue = [sharedElement, sharedElement]; + + assert.equal(loaded.invoke([aliasedValue]), true); +}); + async function withWorkspace(block: (workspace: string) => Promise): Promise { const workspace = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-entry-point-'))); @@ -222,3 +239,6 @@ async function assertProtocolError( function isProtocolError(error: unknown, code: string): error is ProtocolError { return error instanceof ProtocolError && error.code === code; } + +const CONTRACT_SOURCE_ROOT = fileURLToPath(new URL('../../../src/test/resources/', import.meta.url)); +const CONTRACT_MODULE = 'properties/contract/PropertyExecutionContract.ts'; diff --git a/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts b/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts index 802922207..a9c179099 100644 --- a/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts +++ b/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts @@ -3,7 +3,8 @@ import { mkdtemp, mkdir, realpath, rm, writeFile } from 'node:fs/promises'; import { tmpdir } from 'node:os'; import path from 'node:path'; import test from 'node:test'; -import { encodeJsValue } from '../src/js-value.js'; +import { fileURLToPath } from 'node:url'; +import { encodeJsValue, ProtocolError } from '../src/js-value.js'; import { executeProperty, type FastCheckExecutionRequest, @@ -66,7 +67,7 @@ test('supports asynchronous predicates and preconditions', async () => { }); }); -test('reports exhausted preconditions as a property failure without a counterexample', async () => { +test('classifies exhausted preconditions separately from property violations', async () => { await withPropertyModule(async (sourceRoot) => { const request = executionRequest(sourceRoot, 'alwaysTrue', { precondition: { @@ -81,8 +82,8 @@ test('reports exhausted preconditions as a property failure without a counterexa assert.equal(response.result.status, 'failure'); assert.equal(response.result.counterexample, null); - assert.equal(response.result.failure?.kind, 'property'); - assert.equal(response.result.failure?.errorName, 'PropertyFailure'); + assert.equal(response.result.failure?.kind, 'precondition-exhausted'); + assert.equal(response.result.failure?.errorName, 'PreconditionExhausted'); assert.equal( response.result.failure?.message, 'Property could not satisfy its precondition within the skip limit', @@ -90,6 +91,111 @@ test('reports exhausted preconditions as a property failure without a counterexa }); }); +test('reports a throwing precondition as an execution error instead of a counterexample', async () => { + const request = contractExecutionRequest('alwaysTrue', { + preconditionExport: 'throwingPrecondition', + }); + + await assert.rejects( + executeProperty(request), + (error: unknown) => error instanceof ProtocolError + && error.code === 'entrypoint.precondition.threw' + && error.path === 'manifest.precondition' + && error.diagnosticMessage === 'Property precondition threw a non-Error value: precondition exploded', + ); +}); + +test('reports a non-boolean precondition as an entry-point contract error', async () => { + const request = contractExecutionRequest('alwaysTrue', { + preconditionExport: 'nonBooleanPrecondition', + }); + + await assert.rejects( + executeProperty(request), + (error: unknown) => error instanceof ProtocolError + && error.code === 'entrypoint.result.invalid' + && error.path === 'manifest.precondition.result', + ); +}); + +test('keeps false, throwing, and assertion predicates classified as property violations', async () => { + for (const predicateExport of ['falsePredicate', 'throwingPredicate', 'assertionPredicate']) { + const response = await executeProperty(contractExecutionRequest(predicateExport)); + + assert.equal(response.result.status, 'failure'); + assert.equal(response.result.failure?.kind, 'property'); + assert.ok(response.result.counterexample); + } +}); + +test('reports a non-boolean predicate as an entry-point contract error', async () => { + await assert.rejects( + executeProperty(contractExecutionRequest('nonBooleanPredicate')), + (error: unknown) => error instanceof ProtocolError + && error.code === 'entrypoint.result.invalid' + && error.path === 'manifest.predicate.result', + ); +}); + +test('preserves positional special values through one invocation', async () => { + const request = contractExecutionRequest('recognizesSpecialValues', { + inputDomains: [ + constantDomain(undefined), + constantDomain(null), + constantDomain(-0), + constantDomain(Number.NaN), + constantDomain(Number.POSITIVE_INFINITY), + constantDomain(Number.NEGATIVE_INFINITY), + ], + }); + + const response = await executeProperty(request); + + assert.equal(response.result.status, 'success'); +}); + +test('isolates predicate mutation between explicit examples and generated samples', async () => { + const request = contractExecutionRequest('isolatesPredicateMutation', { + inputDomains: [{ + kind: 'array', + element: { kind: 'integer', min: 1, max: 1 }, + minLength: 1, + maxLength: 1, + }], + }); + request.examples = [[encodeJsValue([1])]]; + request.numRuns = 2; + + const response = await executeProperty(request); + + assert.equal(response.result.status, 'success'); + assert.equal(response.result.numRuns, 2); +}); + +test('shrinks and replays the unmodified sample after predicate-local mutation', async () => { + const arrayDomain = { + kind: 'array', + element: { kind: 'integer', min: -10, max: 10 }, + minLength: 1, + maxLength: 3, + }; + const request = contractExecutionRequest('mutatesAndFails', { + inputDomains: [arrayDomain], + }); + + const first = await executeProperty(request); + const replay = await executeProperty({ + ...request, + replayPath: first.result.replayPath ?? undefined, + seed: first.result.seed, + }); + + assert.equal(first.result.status, 'failure'); + assert.ok(first.result.numShrinks > 0); + assert.notDeepEqual(first.result.counterexample, [encodeJsValue([999])]); + assert.deepEqual(replay.result.counterexample, first.result.counterexample); +}); + test('executes explicit examples through the same predicate', async () => { await withPropertyModule(async (sourceRoot) => { const request = executionRequest(sourceRoot, 'isNotSeven'); @@ -142,7 +248,17 @@ test('reports the original nested array when the predicate mutates its invocatio await withPropertyModule(async (sourceRoot) => { const originalValue = [[1]]; const request = executionRequest(sourceRoot, 'mutatesNestedArrayToObject', { - inputDomain: { kind: 'constant', value: encodeJsValue(originalValue) }, + inputDomain: { + kind: 'array', + element: { + kind: 'array', + element: { kind: 'integer', min: 1, max: 1 }, + minLength: 1, + maxLength: 1, + }, + minLength: 1, + maxLength: 1, + }, }); const response = await executeProperty(request); @@ -156,7 +272,12 @@ test('reports and replays the original array when the predicate creates a cycle' await withPropertyModule(async (sourceRoot) => { const originalValue = [1]; const request = executionRequest(sourceRoot, 'mutatesArrayToCycle', { - inputDomain: { kind: 'constant', value: encodeJsValue(originalValue) }, + inputDomain: { + kind: 'array', + element: { kind: 'integer', min: 1, max: 1 }, + minLength: 1, + maxLength: 1, + }, }); const first = await executeProperty(request); @@ -174,41 +295,6 @@ test('reports and replays the original array when the predicate creates a cycle' }); }); -test('isolates predicate input from recursive array mutation in the precondition', async () => { - await withPropertyModule(async (sourceRoot) => { - const request = executionRequest(sourceRoot, 'receivesOriginalNestedArray', { - precondition: { - module: 'properties.ts', - exportName: 'mutatesNestedArrayAndAccepts', - executionKind: 'sync', - }, - inputDomain: { kind: 'constant', value: encodeJsValue([[1]]) }, - }); - - const response = await executeProperty(request); - - assert.equal(response.result.status, 'success'); - }); -}); - -test('isolates asynchronous predicate input from recursive array mutation in the precondition', async () => { - await withPropertyModule(async (sourceRoot) => { - const request = executionRequest(sourceRoot, 'asyncReceivesOriginalNestedArray', { - predicateExecutionKind: 'async', - precondition: { - module: 'properties.ts', - exportName: 'asyncMutatesNestedArrayAndAccepts', - executionKind: 'async', - }, - inputDomain: { kind: 'constant', value: encodeJsValue([[1]]) }, - }); - - const response = await executeProperty(request); - - assert.equal(response.result.status, 'success'); - }); -}); - test('preserves non-Error thrown values including falsy primitives', async () => { await withPropertyModule(async (sourceRoot) => { const cases = ['boom', '', 0, false, null, undefined] as const; @@ -231,6 +317,7 @@ interface RequestOverrides { predicateExecutionKind?: 'sync' | 'async'; precondition?: FastCheckExecutionRequest['manifest']['precondition']; inputDomain?: unknown; + inputDomains?: unknown[]; } function executionRequest( @@ -238,12 +325,12 @@ function executionRequest( predicateExport: string, overrides: RequestOverrides = {}, ): FastCheckExecutionRequest { + const inputDomains = overrides.inputDomains ?? [ + overrides.inputDomain ?? { kind: 'integer', min: -10, max: 10 }, + ]; const manifest: FastCheckExecutionRequest['manifest'] = { propertyId: `example.${predicateExport}`, - inputs: [{ - name: 'value', - domain: overrides.inputDomain ?? { kind: 'integer', min: -10, max: 10 }, - }], + inputs: inputDomains.map((domain, index) => ({ name: `argument${index}`, domain })), predicate: { module: 'properties.ts', exportName: predicateExport, @@ -263,6 +350,36 @@ function executionRequest( }; } +interface ContractRequestOverrides { + preconditionExport?: string; + inputDomains?: unknown[]; +} + +function contractExecutionRequest( + predicateExport: string, + overrides: ContractRequestOverrides = {}, +): FastCheckExecutionRequest { + const requestOverrides: RequestOverrides = {}; + if (overrides.inputDomains !== undefined) requestOverrides.inputDomains = overrides.inputDomains; + + const request = executionRequest(CONTRACT_SOURCE_ROOT, predicateExport, requestOverrides); + request.manifest.predicate.module = CONTRACT_MODULE; + + if (overrides.preconditionExport !== undefined) { + request.manifest.precondition = { + module: CONTRACT_MODULE, + exportName: overrides.preconditionExport, + executionKind: 'sync', + }; + } + + return request; +} + +function constantDomain(value: unknown): unknown { + return { kind: 'constant', value: encodeJsValue(value) }; +} + async function withPropertyModule(block: (sourceRoot: string) => Promise): Promise { const workspace = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-execute-property-'))); const sourceRoot = path.join(workspace, 'src'); @@ -316,27 +433,10 @@ export function mutatesArrayToCycle(value: unknown[]): boolean { return false; } -export function mutatesNestedArrayAndAccepts(value: unknown[][]): boolean { - value[0]![0] = {}; - - return true; -} - -export function receivesOriginalNestedArray(value: unknown[][]): boolean { - return value[0]?.[0] === 1; -} - -export async function asyncMutatesNestedArrayAndAccepts(value: unknown[][]): Promise { - value[0]![0] = {}; - - return true; -} - -export async function asyncReceivesOriginalNestedArray(value: unknown[][]): Promise { - return value[0]?.[0] === 1; -} - export function throwsInput(value: unknown): never { throw value; } `.trimStart(); + +const CONTRACT_SOURCE_ROOT = fileURLToPath(new URL('../../../src/test/resources/', import.meta.url)); +const CONTRACT_MODULE = 'properties/contract/PropertyExecutionContract.ts'; diff --git a/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts b/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts index eb2a86f43..28d2c26c7 100644 --- a/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts +++ b/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts @@ -157,6 +157,29 @@ test('unknown domain kinds are rejected and reported as unsupported', () => { ); }); +test('constant domains reject composite values consistently with the Kotlin model', () => { + const domain = { + kind: 'constant', + value: { + kind: 'array', + elements: [{ kind: 'number', value: 'finite', bits: '3ff0000000000000' }], + }, + }; + + assert.throws(() => projectDomain(domain), /domain\.constant\.unsupported/); + assert.deepEqual( + projectionCapability(domain, 'inputs[0].domain'), + { + level: 'unsupported', + diagnostics: [{ + code: 'domain.constant.unsupported', + message: 'Constant domains support JavaScript primitives only', + path: 'inputs[0].domain', + }], + }, + ); +}); + function sample(domain: unknown, numRuns = 100): unknown[] { return fc.sample(projectDomain(domain), { seed: 42, numRuns }); } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt index d16949243..5772b997a 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt @@ -5,7 +5,7 @@ enum class ProjectionLevel { /** Every value produced by the backend has the declared Kotlin domain semantics. */ EXACT, - /** The backend can run the domain, but its values differ from the declared semantics. */ + /** The backend can run the domain, with diagnostics stating each over- or under-approximation. */ APPROXIMATE, /** The backend cannot project the domain. */ @@ -17,7 +17,7 @@ enum class PropertyCapabilityLevel { /** Both concrete and symbolic projections preserve the declared property semantics. */ EXACT, - /** Both projections are available, but at least one is approximate. */ + /** Both projections are available, but at least one has a documented directional approximation. */ APPROXIMATE, /** Concrete PBT execution is available, but symbolic execution is not. */ @@ -44,7 +44,7 @@ data class CapabilityDiagnostic( * Reports whether a property domain can be represented by an execution backend. * * @property level semantic fidelity of the projection - * @property diagnostics limitations that explain a non-exact [level] + * @property diagnostics limitations and directions that explain a non-exact [level] */ data class ProjectionCapability( val level: ProjectionLevel, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackend.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackend.kt index 4e666df08..94f433c8f 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackend.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackend.kt @@ -44,7 +44,7 @@ data class PropertyRunConfiguration( } } -/** Whether the predicate held for every value executed by the backend. */ +/** Completion status; inspect [PropertyFailureKind] before interpreting a failure as a property violation. */ @Serializable enum class PropertyRunStatus { @SerialName("success") @@ -57,9 +57,15 @@ enum class PropertyRunStatus { /** Stable classification of a completed property failure. */ @Serializable enum class PropertyFailureKind { + /** A predicate returned false or let an exception escape for one admitted input. */ @SerialName("property") PROPERTY, + /** No generated or explicit input was admitted before the backend skip limit was exhausted. */ + @SerialName("precondition-exhausted") + PRECONDITION_EXHAUSTED, + + /** The concrete backend reported its configured time limit; this is not a property violation. */ @SerialName("timeout") TIMEOUT, } @@ -107,7 +113,19 @@ data class PropertyRunResult( } PropertyRunStatus.FAILURE -> { - requireNotNull(failure) { "A failed run requires failure details" } + val failureDetails = requireNotNull(failure) { "A failed run requires failure details" } + + when (failureDetails.kind) { + PropertyFailureKind.PROPERTY -> { + requireNotNull(counterexample) { "A property violation requires a counterexample" } + } + + PropertyFailureKind.PRECONDITION_EXHAUSTED, + PropertyFailureKind.TIMEOUT, + -> require(counterexample == null) { + "A non-violation failure must not contain a counterexample" + } + } } } } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt index b9234fba9..01b548b25 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt @@ -22,10 +22,12 @@ value class PropertyId private constructor(val value: String) { /** * Backend-independent Kotlin definition of one property. * + * Invocation semantics are defined in `usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md`. + * * @property id stable identity of the property * @property inputs ordered domains matching positional TypeScript parameters - * @property predicate TypeScript function that must hold for generated inputs - * @property precondition optional TypeScript function that filters inputs before evaluation + * @property predicate boolean TypeScript function that must hold for admitted inputs + * @property precondition optional pure boolean TypeScript function that admits or discards inputs */ @Serializable data class PropertyDefinition( diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackendTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackendTest.kt index 1ea7658c3..fcd53c2dd 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackendTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackendTest.kt @@ -76,6 +76,35 @@ class PropertyBasedTestingBackendTest { } } + @Test + fun `property violation requires a counterexample`() { + assertFailsWith { + successfulResult().copy( + status = PropertyRunStatus.FAILURE, + failure = PropertyFailureDetails( + kind = PropertyFailureKind.PROPERTY, + errorName = "PropertyFailure", + message = "predicate returned false", + ), + ) + } + } + + @Test + fun `non-violation failure rejects a counterexample`() { + assertFailsWith { + successfulResult().copy( + status = PropertyRunStatus.FAILURE, + counterexample = listOf(JsConcreteValue.Boolean(false)), + failure = PropertyFailureDetails( + kind = PropertyFailureKind.PRECONDITION_EXHAUSTED, + errorName = "PreconditionExhausted", + message = "discard budget exhausted", + ), + ) + } + } + @Test fun `failure details preserve an empty thrown value message`() { val details = PropertyFailureDetails( diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt index 2d7addcfb..dc95a3f9a 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt @@ -357,7 +357,6 @@ class FastCheckProcessClientTest { } })) """.trimIndent(), - transportGraceMillis = 100, ) { client -> val result = client.check(validRequest.copy(timeoutMillis = 100)) diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt index 444dc50ce..0da8bd89f 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt @@ -203,7 +203,6 @@ class FastCheckProjectionClientTest { """.trimIndent(), transportLimits = transportLimits( maxStdoutBytes = 1_024, - wallClockTimeoutMillis = 250, shutdownGraceMillis = 500, ), ) { temporaryClient -> @@ -273,7 +272,6 @@ class FastCheckProjectionClientTest { process.exit(0) """.trimIndent(), transportLimits = transportLimits( - wallClockTimeoutMillis = 250, shutdownGraceMillis = 500, ), ) { temporaryClient -> diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt new file mode 100644 index 000000000..bddbe22c6 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt @@ -0,0 +1,246 @@ +package org.usvm.ts.pbt.fastcheck + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.PropertyFailureKind +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.ConstantDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcesRoot +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertNotEquals +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class PropertyExecutionContractTest { + private val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) + + @Test + fun `true precondition admits the input`() { + val result = backend.run( + property = property( + predicate = "alwaysTrue", + precondition = "truePrecondition", + ), + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + assertEquals(0, result.numSkips) + } + + @Test + fun `false precondition exhaustion is not a property violation`() { + val result = backend.run( + property = property( + predicate = "alwaysTrue", + precondition = "falsePrecondition", + ), + configuration = configuration.copy(numRuns = 1), + ) + + assertEquals(PropertyRunStatus.FAILURE, result.status) + assertEquals(PropertyFailureKind.PRECONDITION_EXHAUSTED, result.failure?.kind) + assertEquals("PreconditionExhausted", result.failure?.errorName) + assertNull(result.counterexample) + } + + @Test + fun `throwing and non-boolean preconditions are execution errors`() { + val cases = listOf( + ContractErrorCase( + exportName = "throwingPrecondition", + expectedCode = "entrypoint.precondition.threw", + expectedPath = "manifest.precondition", + ), + ContractErrorCase( + exportName = "nonBooleanPrecondition", + expectedCode = "entrypoint.result.invalid", + expectedPath = "manifest.precondition.result", + ), + ) + + cases.forEach { case -> + val error = assertFailsWith { + backend.run( + property = property( + predicate = "alwaysTrue", + precondition = case.exportName, + ), + configuration = configuration, + ) + } + + assertEquals(BackendErrorKind.ENTRY_POINT, error.kind) + assertEquals(case.expectedCode, error.code) + assertEquals(case.expectedPath, error.path) + } + } + + @Test + fun `false throwing and assertion predicates are property violations`() { + listOf("falsePredicate", "throwingPredicate", "assertionPredicate").forEach { predicate -> + val result = backend.run( + property = property(predicate = predicate), + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.FAILURE, result.status) + assertEquals(PropertyFailureKind.PROPERTY, result.failure?.kind) + assertNotNull(result.counterexample) + } + } + + @Test + fun `non-boolean predicate is an execution error`() { + val error = assertFailsWith { + backend.run( + property = property(predicate = "nonBooleanPredicate"), + configuration = configuration, + ) + } + + assertEquals(BackendErrorKind.ENTRY_POINT, error.kind) + assertEquals("entrypoint.result.invalid", error.code) + assertEquals("manifest.predicate.result", error.path) + } + + @Test + fun `a predicate may catch and classify an expected exception`() { + val result = backend.run( + property = property(predicate = "catchesExpectedException"), + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + } + + @Test + fun `special values retain their identity and argument order`() { + val domains = listOf( + ConstantDomain(value = JsConcreteValue.Undefined), + ConstantDomain(value = JsConcreteValue.Null), + ConstantDomain(value = JsConcreteValue.number(-0.0)), + ConstantDomain(value = JsConcreteValue.number(Double.NaN)), + ConstantDomain(value = JsConcreteValue.number(Double.POSITIVE_INFINITY)), + ConstantDomain(value = JsConcreteValue.number(Double.NEGATIVE_INFINITY)), + ) + + val result = backend.run( + property = property( + predicate = "recognizesSpecialValues", + domains = domains, + ), + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + } + + @Test + fun `predicate mutation is isolated between examples and generated samples`() { + val original = JsConcreteValue.Array( + elements = listOf(JsConcreteValue.number(1.0)), + ) + val domain = ArrayDomain( + element = IntegerDomain(min = 1, max = 1), + minLength = 1, + maxLength = 1, + ) + + val result = backend.run( + property = property( + predicate = "isolatesPredicateMutation", + domains = listOf(domain), + ), + configuration = configuration.copy( + numRuns = 2, + examples = listOf(listOf(original)), + ), + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + assertEquals(2, result.numRuns) + } + + @Test + fun `shrinking and replay retain the input before predicate mutation`() { + val domain = ArrayDomain( + element = IntegerDomain(min = -10, max = 10), + minLength = 1, + maxLength = 3, + ) + val definition = property( + predicate = "mutatesAndFails", + domains = listOf(domain), + ) + + val first = backend.run( + property = definition, + configuration = configuration, + ) + val counterexample = assertNotNull(first.counterexample) + val replayPath = assertNotNull(first.replayPath) + val replay = backend.run( + property = definition, + configuration = configuration.copy( + seed = first.seed, + replayPath = replayPath, + ), + ) + + assertEquals(PropertyRunStatus.FAILURE, first.status) + assertTrue(first.numShrinks > 0) + assertNotEquals( + JsConcreteValue.Array(elements = listOf(JsConcreteValue.number(999.0))), + counterexample.single(), + ) + assertEquals(counterexample, replay.counterexample) + } + + private fun property( + predicate: String, + precondition: String? = null, + domains: List = listOf(IntegerDomain(min = 0, max = 0)), + ): PropertyDefinition = PropertyDefinition( + id = PropertyId("contract.$predicate"), + inputs = domains.mapIndexed { index, domain -> + PropertyInput(name = "argument$index", domain = domain) + }, + predicate = TypeScriptEntryPoint( + module = MODULE, + exportName = predicate, + ), + precondition = precondition?.let { exportName -> + TypeScriptEntryPoint( + module = MODULE, + exportName = exportName, + ) + }, + ) + + private data class ContractErrorCase( + val exportName: String, + val expectedCode: String, + val expectedPath: String, + ) + + private companion object { + const val MODULE = "properties/contract/PropertyExecutionContract.ts" + + val configuration = PropertyRunConfiguration( + seed = 42, + numRuns = 5, + timeoutMillis = 1_000, + ) + } +} diff --git a/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts new file mode 100644 index 000000000..0f8e5ee7a --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts @@ -0,0 +1,76 @@ +export function alwaysTrue(_value: number): boolean { + return true; +} + +export function truePrecondition(_value: number): boolean { + return true; +} + +export function falsePrecondition(_value: number): boolean { + return false; +} + +export function throwingPrecondition(_value: number): boolean { + throw 'precondition exploded'; +} + +export function nonBooleanPrecondition(_value: number): number { + return 1; +} + +export function falsePredicate(_value: number): boolean { + return false; +} + +export function throwingPredicate(_value: number): boolean { + throw 'predicate exploded'; +} + +export function assertionPredicate(_value: number): boolean { + throw 'AssertionError: contract assertion'; +} + +export function nonBooleanPredicate(_value: number): number { + return 1; +} + +export function catchesExpectedException(_value: number): boolean { + try { + throw 'expected'; + } catch (error: unknown) { + return error === 'expected'; + } +} + +export function recognizesSpecialValues( + missing: undefined, + empty: null, + negativeZero: number, + notANumber: number, + positiveInfinity: number, + negativeInfinity: number, +): boolean { + return missing === undefined + && empty === null + && Object.is(negativeZero, -0) + && Number.isNaN(notANumber) + && positiveInfinity === Number.POSITIVE_INFINITY + && negativeInfinity === Number.NEGATIVE_INFINITY; +} + +export function preservesNestedArrayAlias(values: number[][]): boolean { + return values.length === 2 && values[0] === values[1]; +} + +export function isolatesPredicateMutation(value: number[]): boolean { + const pristine = value.length === 1 && value[0] === 1; + value[0] = 2; + + return pristine; +} + +export function mutatesAndFails(value: number[]): boolean { + value[0] = 999; + + return false; +}