From d51dbeeb8b2868d5df0cbba66dad0a009e10c2cc Mon Sep 17 00:00:00 2001 From: Kyle Mathews Date: Wed, 11 Nov 2026 13:01:30 -0700 Subject: [PATCH 1/4] feat(oracles): shardable units for generated sources, with ORACLE_UNIT replay A generated source registers each part of its campaigns as its own test: `fixed seed N: ` and `fixed seed N: generated` for each fixed seed, `random seed: ` and `random seed: generated` for the random campaign, and one `determinism: ` test per compared history. The units of a seed run exactly the histories the campaign ran; each decides its own first failure, shrinks within its own timeout, and prints its own reach line. A unit that fails or times out prints no reach line. The random units share one seed per property (maintainer decision, 2026-11-11, Q2). `${prefix}_UNIT` names the random unit a path replay runs and requires `${prefix}_PROPERTY` (Q3). A path replay of a generated source without UNIT, or with a UNIT that names no random unit, fails at registration (Q4). Every failing unit prints a replay command that names its unit, and a failing fixed-seed unit prints a `-t` rerun of itself. Duplicate constructed or fixed names, and a constructed history named `generated`, fail to load. The framework self-oracle gains the `units` and `replay-config` laws, unit names, a custom prefix, a drawn replay environment, a second fixed seed, and names that extend each other. Co-authored-by: Isaac --- .changeset/shardable-units.md | 11 + packages/oracles/src/oracle-config.ts | 5 +- packages/oracles/src/oracle-environment.ts | 21 +- packages/oracles/src/oracle-property.ts | 418 +++-- .../oracle-property-self-oracle-fixture.ts | 32 +- .../tests/oracle-property-self-oracle.test.ts | 1523 ++++++++++++++--- 6 files changed, 1637 insertions(+), 373 deletions(-) create mode 100644 .changeset/shardable-units.md diff --git a/.changeset/shardable-units.md b/.changeset/shardable-units.md new file mode 100644 index 0000000..1b037ab --- /dev/null +++ b/.changeset/shardable-units.md @@ -0,0 +1,11 @@ +--- +'@tanstack/oracles': patch +--- + +A generated source now registers each part of a campaign as its own test, so a runner can shard a long campaign across jobs. For each fixed seed N, `oracleProperty` registers `fixed seed N: ` for each constructed history and `fixed seed N: generated` for the generated histories. The random campaign registers `random seed: ` and `random seed: generated` in the same way. The determinism test becomes one test per history: `determinism: fixed history: `, `determinism: constructed history: `, and `determinism: generated 0` to `2`. The units of a seed run exactly the histories that the campaign ran. Each unit decides its own first failure, shrinks within its own timeout, and prints its own reach line, ` reach {...}`. A campaign's reach is the sum of its units' lines. A unit that fails or times out prints no reach line. An enumerated source keeps its one `determinism` test. + +Test names change. A `-t "fixed seed"` filter still selects the fixed-seed units, and `-t "random seed"` the random units. A filter that names the old `determinism` test of a generated source now selects all its determinism units. The random units of a property share one seed, which the first random unit that runs selects and logs in the one `ORACLE_SEED` line. + +A path replay now names its unit in the new `${prefix}_UNIT` variable, such as `ORACLE_UNIT='random seed: generated'`. `UNIT` requires `PROPERTY`. During a path replay, only the random unit of that name runs. A path replay of a generated source without `UNIT` fails when the property registers, with "`ORACLE_PATH` of a generated source requires `ORACLE_UNIT`". A `UNIT` that names no random unit of the replayed property also fails its registration. A failing unit prints its replay command, with the seed, the path, the property, the unit, and its `-t` pattern, under the configured prefix. A failing fixed-seed unit also prints `Rerun: -t '...'`, which reruns it. The retired-variable message names `${prefix}_UNIT`. + +A generated source fails to load when two of its tests would share a name: a constructed history named `generated`, two constructed histories of one name, or two fixed histories of one name. diff --git a/packages/oracles/src/oracle-config.ts b/packages/oracles/src/oracle-config.ts index 4f8b655..3da5a16 100644 --- a/packages/oracles/src/oracle-config.ts +++ b/packages/oracles/src/oracle-config.ts @@ -30,7 +30,7 @@ export type { OracleRoute } from './oracle-route.js' export interface OracleConfigurationOptions { /** * The prefix of every oracle environment variable: `${envPrefix}_SEED`, - * `${envPrefix}_PATH`, `${envPrefix}_PROPERTY`, + * `${envPrefix}_PATH`, `${envPrefix}_PROPERTY`, `${envPrefix}_UNIT`, * `${envPrefix}_RUNS_MULTIPLIER`, `${envPrefix}_CALIBRATION`, * `${envPrefix}_REPLAY_WITNESS`, and `${envPrefix}_REPLAY_WITNESS_MODE`. A project with its own prefix keeps its * variable names by passing it here. @@ -132,7 +132,7 @@ export function assertRegisteredOracleProperty(property: string): void { export function readOracleRunConfig( environment?: OracleEnvironment, ): Readonly { - const { multiplier, campaignSeed, replayPath, replayProperty } = + const { multiplier, campaignSeed, replayPath, replayProperty, replayUnit } = environment === undefined ? replayConfig() : readRunConfig(environment, oracleSettings()) @@ -141,6 +141,7 @@ export function readOracleRunConfig( campaignSeed, replayPath, replayProperty, + replayUnit, // A seed the process's replay environment selected is declared fixed, // so options built from this configuration name it `fixed seed`. ...(environment === undefined && campaignSeed !== undefined diff --git a/packages/oracles/src/oracle-environment.ts b/packages/oracles/src/oracle-environment.ts index 9ead0b9..4718419 100644 --- a/packages/oracles/src/oracle-environment.ts +++ b/packages/oracles/src/oracle-environment.ts @@ -63,6 +63,11 @@ export type OracleReplayConfig = { campaignSeed: number | undefined replayPath: string | undefined replayProperty: string | undefined + /** + * The random unit a path replay runs, such as `random seed: generated`; + * every other test of the property stands aside. + */ + replayUnit?: string | undefined } // The replay environment under the current configuration: read by @@ -101,6 +106,7 @@ export function changesReadSelection(next: RunConfig): boolean { read.campaignSeed !== next.campaignSeed || read.replayPath !== next.replayPath || read.replayProperty !== next.replayProperty || + read.replayUnit !== next.replayUnit || read.calibration !== next.calibration ) } @@ -122,6 +128,7 @@ export function readRunConfig( const seedName = name(`SEED`) const pathName = name(`PATH`) const propertyName = name(`PROPERTY`) + const unitName = name(`UNIT`) const multiplierName = name(`RUNS_MULTIPLIER`) const retired = within.retired.filter( (variable) => environment[variable] !== undefined, @@ -129,8 +136,8 @@ export function readRunConfig( if (retired.length > 0) { throw new Error( `Retired oracle replay variables are set: ${retired.join(`, `)}. ` + - `Use ${seedName}, ${pathName}, and ` + - `${propertyName} to select a replay, and ` + + `Use ${seedName}, ${pathName}, ${propertyName}, and ` + + `${unitName} to select a replay, and ` + `${multiplierName} to scale run counts.`, ) } @@ -150,6 +157,13 @@ export function readRunConfig( const seedValue = environment[seedName] const replayPath = environment[pathName] const replayProperty = environment[propertyName] + const replayUnit = environment[unitName] + // The unit is checked after every other variable, so their order stays. + const unitNeedsProperty = () => { + if (replayUnit !== undefined) { + throw new Error(`${unitName} requires ${propertyName}`) + } + } if (seedValue === undefined) { if (replayPath !== undefined) { throw new Error(`${pathName} requires ${seedName}`) @@ -157,6 +171,7 @@ export function readRunConfig( if (replayProperty !== undefined) { throw new Error(`${propertyName} requires ${pathName}`) } + unitNeedsProperty() return { multiplier, calibration, @@ -176,6 +191,7 @@ export function readRunConfig( if (replayProperty !== undefined) { throw new Error(`${propertyName} requires ${pathName}`) } + unitNeedsProperty() return { multiplier, calibration, @@ -206,5 +222,6 @@ export function readRunConfig( campaignSeed, replayPath, replayProperty, + replayUnit, } } diff --git a/packages/oracles/src/oracle-property.ts b/packages/oracles/src/oracle-property.ts index 4efc1df..93699f0 100644 --- a/packages/oracles/src/oracle-property.ts +++ b/packages/oracles/src/oracle-property.ts @@ -77,15 +77,52 @@ * so the gap report can tell an output the check does not compare from one * that never changed. * - * A generated source runs one test per fixed seed and one random test, with - * the same arbitrary, check, and budget (ORC-007). The random test reads the - * replay variables through `oraclePropertyOptions`, and every test stands - * aside during another property's path replay. + * A generated source runs one campaign per fixed seed and one random + * campaign, with the same arbitrary, check, and budget (ORC-007), and every + * test stands aside during another property's path replay. + * + * - **Units** (maintainer decision, 2026-11-11, option D). A generated source + * registers each part of a campaign as its own test, so a runner can shard + * them. For each fixed seed N, it registers `fixed seed N: ` for each + * constructed history, which runs only that history, built from seed N + + * its index, as a fast-check example with no generated runs; and then + * `fixed seed N: generated`, which runs the campaign's generated histories: + * the same seed and the same `oracleRuns(runs)`, with no examples. + * fast-check draws its generated histories independently of its examples, + * so the units of seed N run exactly the histories that the campaign ran. + * The random campaign registers `random seed: ` and `random seed: + * generated` in the same way. Its units share one seed per registration: + * the first random unit that runs selects it through + * `oraclePropertyOptions`, which reads the replay variables and logs the one + * `ORACLE_SEED` line (maintainer decision, 2026-11-11, Q2). Each unit keeps + * its campaign's route, decides its own first failure, shrinks on its own + * within its own timeout, and prints its own reach line, ` reach + * {...}`; a campaign's reach is the sum of its units' lines. A constructed + * history named `generated`, or two constructed or two fixed histories of one + * name, would give two tests one name, so the property fails to load. + * - **Unit replay** (maintainer decisions, 2026-11-11, Q3 and Q4). A path + * indexes one unit's stream, so a path replay names its unit in + * `${prefix}_UNIT`, such as `random seed: generated`, which requires + * `${prefix}_PROPERTY`. During a path replay of a property, only its random + * unit of that name runs, and every other test stands aside. A path replay + * of a generated source without `UNIT` fails when the property registers, + * with "`${prefix}_PATH` of a generated source requires `${prefix}_UNIT`", + * and so does a `UNIT` that names no random unit of the replayed property, + * an enumerated property's included; these come after every other load + * error of the property. A failing unit prints its replay command, `Replay: + * ${prefix}_SEED=... ${prefix}_PATH=... ${prefix}_PROPERTY=... ${prefix}_UNIT=... + * vitest run -t '...'`, which names the random unit of its own name: a + * fixed-seed unit's replay runs that random unit with the fixed seed, which + * draws the same stream. Run with the project's test command in place of + * `vitest run`, it runs only that unit and reproduces the counterexample. A + * failing random unit's violation prints the same command as its rerun + * line, and a failing fixed-seed unit prints `Rerun: -t '...'`, which reruns + * it, shrinking included. * * - **Reach** names the states a history entered. By default the driver * reports them with `observe("reach", state)`. A state that only the model * can name, such as "a failure while the seed is active", comes from - * `reached(history, trace, expected)` instead. Each campaign prints how many + * `reached(history, trace, expected)` instead. Each unit prints how many * histories entered each declared state, including none (ORC-015). An * enumerated source runs every history, so its required states need no * constructed history (maintainer decision, 2026-11-10): its `reach` test, @@ -128,7 +165,7 @@ * driver must await the work it starts. * - A **constructed history** is built from a generated history so that it * reaches states that the laws need, and it names those declared states. - * Every campaign runs every constructed history once as an example, and a + * Every campaign runs every constructed history once, in its own unit, and a * constructed history that does not enter a named state fails. Only * constructed histories make reach required: a state that random histories * reach is measured, never gated. So every state in `states` must be named @@ -174,10 +211,14 @@ * start. A required difference that the empty difference holds, the empty * text or a pattern that matches the empty string, fails registration, and * a difference that is not text fails the calibration. - * - **Determinism.** A `determinism` test runs some histories twice and - * requires the same trace: every fixed and constructed history of a generated - * source and three generated histories, or up to eight evenly spaced - * enumerated histories. Two runs are compared by their observations' data + * - **Determinism.** The determinism tests run some histories twice and + * require the same trace. A generated source registers one test + * `determinism: ` for each history it compares: every fixed + * history (`determinism: fixed history: `), every constructed history + * built from the first fixed seed (`determinism: constructed history: + * `), and three generated histories (`determinism: generated 0` to + * `2`). An enumerated source registers one `determinism` test over up to + * eight evenly spaced enumerated histories. Two runs are compared by their observations' data * encodings, so `-0` and `0`, key order, and Map and Set order count, as a * check that iterates them can see. A trace * that differs between runs of one history breaks replay, shrinking, and the gap @@ -190,10 +231,10 @@ * the reported counterexample still shows the first failure (ORC-010). * Within one history a driver error decides first, then a law violation, * then a constructed history that missed its state. - * - **Shrinking ends in time.** A campaign starts no shrink run once half its + * - **Shrinking ends in time.** A unit starts no shrink run once half its * test's `timeout` has passed. A shrink it does not run counts as passing, * so fast-check ends its search and reports the smallest failure it found, - * with the first failure's law. A campaign whose first failure is judged in + * with the first failure's law. A unit whose first failure is judged in * time, and whose runs each take less than half its timeout, so reports that * law and a replayable counterexample before its timeout, however long * shrinking would take; that counterexample can be larger than the smallest @@ -234,7 +275,8 @@ import { oracleRuns, withOracleFixedHistories, } from './oracle-config.js' -import { oracleEnvName } from './oracle-environment.js' +import { oracleEnvName, replayConfig } from './oracle-environment.js' +import { recordOracleReplay } from './oracle-replay-witness.js' import { oracleFixedSeed, oracleRoute, oracleRouteOf } from './oracle-route.js' import type { OracleRoute } from './oracle-route.js' @@ -621,7 +663,7 @@ export interface OraclePropertyOptions { predict?: (plan: TPlan) => Readonly> /** * Each registered test's limit in milliseconds; 120 seconds by default, and - * none at 0 or less. A campaign stops shrinking at half of it. + * none at 0 or less. Each unit of a campaign stops shrinking at half of it. */ timeout?: number /** @@ -783,6 +825,37 @@ export function oracleProperty( const timeoutOf = (options: { timeout?: number }) => options.timeout ?? 120_000 +/** Whether no path replay is selected, or the selected one names this unit. */ +const replaySelects = (unit: string) => + replayConfig().replayPath === undefined || replayConfig().replayUnit === unit + +/** + * During a path replay of this property, the replay's unit must name one of + * its random units: a path indexes one unit's stream, so a replay without a + * unit, or with another, would run an unrelated history or nothing at all. + */ +function assertReplayUnit(id: string, randomUnits: ReadonlyArray) { + const { replayPath, replayProperty, replayUnit } = replayConfig() + if (replayPath === undefined || replayProperty !== id) return + const unitName = oracleEnvName(`UNIT`) + const units = randomUnits.map((unit) => JSON.stringify(unit)).join(`, `) + if (randomUnits.length === 0) { + if (replayUnit !== undefined) + throw new Error( + `${id}: ${unitName} names "${replayUnit}", but an enumerated source has no random units to replay.`, + ) + return + } + if (replayUnit === undefined) + throw new Error( + `${id}: ${oracleEnvName(`PATH`)} of a generated source requires ${unitName}, the random unit whose path it replays: one of ${units}. A failing unit's replay line prints it.`, + ) + if (!randomUnits.includes(replayUnit)) + throw new Error( + `${id}: ${unitName} names "${replayUnit}", which is no random unit of this property; its random units are ${units}.`, + ) +} + /** The declared states, when the source declares any. */ const declaredOf = (source: { states?: ReadonlyArray @@ -887,14 +960,16 @@ function enumeratedTests( process.stdout.write(`${id} enumerated reach ${countsText(counts)}\n`) }, } - return [ + const tests = [ ...historyTests, ...(declared ? [reachTest] : []), ...calibrationTests(options, () => named), - determinismTest(options, () => + determinismTest(options, `determinism`, () => named.filter((_, index) => index % spacing === 0), ), ] + assertReplayUnit(id, []) + return tests } // The running history's trace, and where in it a controlled clock passed its @@ -1356,10 +1431,11 @@ function reportText(value: unknown): string { function determinismTest( options: BoundOptions, + testName: string, histories: () => ReadonlyArray<{ name: string; history: THistory }>, ): PropertyTest { return { - name: `determinism`, + name: testName, route: `calibration`, replays: [], run: async () => { @@ -1786,10 +1862,12 @@ function rerunOf(task: NamedTask): string { for (let at: NamedTask | undefined = task; at; at = at.suite) names.unshift(at.name) const escape = (text: string) => text.replace(/[.*+?^${}()|[\]\\]/g, `\\$&`) - const pattern = `^${names.map(escape).join(`(?: | > )`)}$` - return `-t '${pattern.replace(/'/g, `'\\''`)}'` + return `-t ${shellQuoted(`^${names.map(escape).join(`(?: | > )`)}$`)}` } +/** Text in a POSIX shell's single quotes. */ +const shellQuoted = (text: string) => `'${text.replace(/'/g, `'\\''`)}'` + /** * A fixed or constructed history whose arbitrary's `canShrinkWithoutContext` * is false, so fast-check could not shrink it. fast-check 4 answers false @@ -1850,8 +1928,27 @@ function generatedTests( `${id}: constructed history "${construction.name}" names undeclared states ${undeclared.join(`, `)}.`, ) } + // Each unit and determinism test is named by its history, so two tests + // would share a name. + const twice = (names: ReadonlyArray) => + names.find((name, at) => names.indexOf(name) !== at) + const constructedNames = constructions.map(({ name }) => name) + if (constructedNames.includes(`generated`)) + throw new Error( + `${id}: constructed history "generated" has the name of a campaign's generated unit, so two tests would share a name. Rename the constructed history.`, + ) + const constructedTwice = twice(constructedNames) + if (constructedTwice !== undefined) + throw new Error( + `${id}: two constructed histories are named "${constructedTwice}", so two tests would share a name. Give each constructed history its own name.`, + ) + const fixedTwice = twice((source.fixed ?? []).map(({ name }) => name)) + if (fixedTwice !== undefined) + throw new Error( + `${id}: two fixed histories are named "${fixedTwice}", so two tests would share a name. Give each fixed history its own name.`, + ) - // Each campaign gets a fresh predicate: its first failure fixes the kind + // Each unit gets a fresh predicate: its first failure fixes the kind // that shrinking must keep, a setup error, a constructed history that missed // its state, or one law. A // smaller history that fails some other way counts as passing. It counts @@ -1862,6 +1959,7 @@ function generatedTests( constructionOf: Map>, counts: Map, shrinkUntil: number, + rerun: string, ) => { let firstKind: string | undefined const keeps = (kind: string) => (firstKind ??= kind) === kind @@ -1898,42 +1996,32 @@ function generatedTests( ) } if (!keeps(`law:${lawOf(verdict)}`)) return - throw failure( - options, - verdict, - history, - `${oracleEnvName(`PROPERTY`)}=${id} with the seed and path that fast-check reports`, - ) + throw failure(options, verdict, history, rerun) } } - // Each campaign runs every constructed history, built from histories its own - // seed draws. - // fast-check passes example inputs by reference, which identifies them. - // At registration, an error from sampling or building names its - // constructed history: it would otherwise fail the file's load unnamed. - const examplesFor = (seed: number, registering = false) => { - const constructionOf = new Map>() - const examples = constructions.map((construction, index) => { - let history: THistory - try { - const [generated] = fc.sample(source.arbitrary, { - seed: seed + index, - numRuns: 1, - }) - history = construction.build(generated!) - } catch (error) { - if (!registering) throw error - throw new Error( - `oracleProperty ${id}: constructed history "${construction.name}" threw while it was built for registration: ${error instanceof Error ? error.message : reportText(error)}`, - { cause: error }, - ) - } - if (!source.arbitrary.canShrinkWithoutContext(history)) - throw untakeable(id, `constructed history "${construction.name}" built`) - constructionOf.set(history, construction) - return [history] as [THistory] - }) - return { examples, constructionOf } + // Constructed history `index`, built from the history its campaign's seed + // draws at seed + index. At registration, an error from sampling or + // building names its constructed history: it would otherwise fail the + // file's load unnamed. + const constructedAt = (seed: number, index: number, registering = false) => { + const construction = constructions[index]! + let history: THistory + try { + const [generated] = fc.sample(source.arbitrary, { + seed: seed + index, + numRuns: 1, + }) + history = construction.build(generated!) + } catch (error) { + if (!registering) throw error + throw new Error( + `oracleProperty ${id}: constructed history "${construction.name}" threw while it was built for registration: ${error instanceof Error ? error.message : reportText(error)}`, + { cause: error }, + ) + } + if (!source.arbitrary.canShrinkWithoutContext(history)) + throw untakeable(id, `constructed history "${construction.name}" built`) + return history } // Registration checks every fixed history, then the constructed histories // built from the first fixed seed (or seed 0 when there is none), so a @@ -1941,24 +2029,57 @@ function generatedTests( for (const [index, fixed] of (source.fixed ?? []).entries()) if (!source.arbitrary.canShrinkWithoutContext(fixed.history)) throw untakeable(id, `fixed history ${index} ("${fixed.name}") is`) - examplesFor(source.fixedSeeds[0] ?? 0, true) + const firstSeed = source.fixedSeeds[0] ?? 0 + for (const index of constructions.keys()) + constructedAt(firstSeed, index, true) - // A campaign reports its reach counts after it passes; a failing campaign - // reports its counterexample instead. - const runCampaign = async ( - name: string, + // A campaign's units: one per constructed history, then `generated`. + const unitNames = [...constructedNames, `generated`] + /** + * Runs one unit of a campaign whose parameters are `base`. A constructed + * unit runs its one history, built from the campaign's seed, as an + * example with no generated runs; the `generated` unit runs the + * campaign's generated runs, with no examples, so fast-check draws the + * same histories that the whole campaign drew. A unit reports its reach + * counts after it passes, and its rerun and replay commands when it fails. + */ + const runUnit = async ( + task: NamedTask, + signal: AbortSignal, + unit: string, seed: number, - parameters: ( - examples: Array<[THistory]>, - ) => NonNullable[1]>, + base: NonNullable[1]> & { + numRuns: number + path?: string + }, + random: boolean, ) => { // Vitest's clock for the test is already running. const started = performance.now() - const { examples, constructionOf } = examplesFor(seed) + const index = constructedNames.indexOf(unit) + const constructionOf = new Map>() + // fast-check reports a run's details itself; the replay witness is + // recorded from them below. + const { reporter: _reporter, asyncReporter: _asyncReporter, ...rest } = base + let run: typeof rest = rest + if (index >= 0) { + const history = constructedAt(seed, index) + // fast-check passes example inputs by reference, which identifies them. + constructionOf.set(history, constructions[index]!) + run = withOracleFixedHistories( + run.path === undefined ? { ...run, numRuns: 0 } : run, + [[history]], + ) + } + oracleRoute(oracleRouteOf(run)) const counts = new Map( [...(declared ?? [])].map((state) => [state, 0]), ) - const run = parameters(examples) + // A random unit's replay runs itself; a fixed-seed unit's replay runs the + // random unit of its name with the fixed seed, which draws the same + // stream. + const replayed = { name: `random seed: ${unit}`, suite: task.suite } + const rerun = random ? replayPlaceholder : rerunOf(task) // A path replay shrinks no further than the counterexample it replays. // Vitest reads a timeout of 0 or less as none, which sets no budget. const timeout = timeoutOf(options) @@ -1968,47 +2089,84 @@ function generatedTests( : timeout > 0 ? started + timeout / 2 : Infinity - await fc.assert( + const details = await fc.check( fc.asyncProperty( arbitrary, - predicateFor(constructionOf, counts, shrinkUntil), + predicateFor(constructionOf, counts, shrinkUntil, rerun), ), run, ) + recordOracleReplay(id, details) + if (details.failed) { + const report = await fc.asyncDefaultReportMessage(details) + const path = details.counterexamplePath + const replay = + path === null + ? undefined + : `${oracleEnvName(`SEED`)}=${details.seed} ${oracleEnvName(`PATH`)}=${path} ${oracleEnvName(`PROPERTY`)}=${shellQuoted(id)} ${oracleEnvName(`UNIT`)}=${shellQuoted(replayed.name)} vitest run ${rerunOf(replayed)}` + // A random unit's violation names its replay as its rerun. + const cause: unknown = details.errorInstance + if (replay !== undefined && random && cause instanceof OracleViolation) + cause.message = cause.message.replace( + `Rerun: ${replayPlaceholder}`, + // A function, so the command's `$'` is not a replacement pattern. + () => `Rerun: ${replay}`, + ) + throw new Error( + [ + report, + ...(random ? [] : [`Rerun: ${rerun}`]), + ...(replay === undefined ? [] : [`Replay: ${replay}`]), + ].join(`\n`), + { cause }, + ) + } // Vitest hides console output from a passing test; stdout reaches the log. - process.stdout.write(`${id} ${name} reach ${countsText(counts)}\n`) + // A unit that passes after its test timed out did not pass this run, so a + // sum of the units' lines never counts it. + if (!signal.aborted) + process.stdout.write(`${id} ${task.name} reach ${countsText(counts)}\n`) } - const fixedCampaigns = source.fixedSeeds.map((seed): PropertyTest => ({ - name: `fixed seed ${seed}`, - route: `fixed seed`, - replays: [], - run: () => { - const parameters = oracleFixedSeed(seed, { - numRuns: oracleRuns(source.runs), - }) - oracleRoute(oracleRouteOf(parameters)) - return runCampaign(`fixed seed ${seed}`, seed, (examples) => - withOracleFixedHistories(parameters, examples), - ) - }, - })) - // The random campaign picks its seed itself, so a replay of that seed - // rebuilds the same constructed histories, which the replay path counts. - const randomCampaign: PropertyTest = { - name: `random seed`, + const fixedUnits = source.fixedSeeds.flatMap((seed) => + unitNames.map((unit): PropertyTest => ({ + name: `fixed seed ${seed}: ${unit}`, + route: `fixed seed`, + replays: [], + run: (task, signal) => + runUnit( + task, + signal, + unit, + seed, + oracleFixedSeed(seed, { numRuns: oracleRuns(source.runs) }), + false, + ), + })), + ) + // The random units share one seed per registration: the first random unit + // that runs selects and logs it, and a replay reads that log line. A + // replay of that seed rebuilds the same constructed histories, which the + // replay path counts. + let randomParameters: ReturnType | undefined + const randomUnits = unitNames.map((unit): PropertyTest => ({ + name: `random seed: ${unit}`, route: `random seed`, - replays: [id], - run: () => { - // One call selects and logs the seed; a replay reads that log line. - const parameters = oraclePropertyOptions(source.runs, id) + // During a path replay, only the unit the replay names runs. + replays: replaySelects(`random seed: ${unit}`) ? [id] : [], + run: (task, signal) => { + randomParameters ??= oraclePropertyOptions(source.runs, id) // A path replay runs one recorded history, a seed from the replay - // environment reseeds the campaign, and a drawn seed is random. - oracleRoute(oracleRouteOf(parameters)) - return runCampaign(`random seed`, parameters.seed!, (examples) => - withOracleFixedHistories(parameters, examples), + // environment reseeds the units, and a drawn seed is random. + return runUnit( + task, + signal, + unit, + randomParameters.seed!, + randomParameters, + true, ) }, - } + })) const fixedTests = (source.fixed ?? []).map((fixed): PropertyTest => ({ name: `fixed history: ${fixed.name}`, route: `fixed history`, @@ -2028,48 +2186,62 @@ function generatedTests( })) // Fixed histories and the constructed histories of the first fixed seed (or // seed 0), so these checks are reproducible. Registration built them once to - // check them; they are built again when a test runs, like a - // campaign's. - const namedHistories = () => { - const { examples, constructionOf } = examplesFor(source.fixedSeeds[0] ?? 0) - return [ - ...(source.fixed ?? []).map(({ name, history }) => ({ - name: `fixed history: ${name}`, - history, - })), - ...examples.map(([history]) => ({ - name: `constructed history: ${constructionOf.get(history)!.name}`, - history, - })), - ] - } + // check them; they are built again when a test runs, like a unit's. Each + // is built only when its test asks for it. + const namedHistories = () => [ + ...(source.fixed ?? []).map(({ name, history }) => ({ + name: `fixed history: ${name}`, + history: () => history, + })), + ...constructions.map(({ name }, index) => ({ + name: `constructed history: ${name}`, + history: () => constructedAt(firstSeed, index), + })), + ] // Determinism also covers three generated histories, so a property whose // driver varies is caught even without fixed or constructed histories. - const determinism = determinismTest(options, () => [ + // Each history is its own test. + const sampled = () => + fc.sample(source.arbitrary, { seed: firstSeed, numRuns: 3 }) + const determinism = [ ...namedHistories(), - ...fc - .sample(source.arbitrary, { seed: source.fixedSeeds[0] ?? 0, numRuns: 3 }) - .map((history, index) => ({ name: `generated ${index}`, history })), - ]) + ...[0, 1, 2].map((index) => ({ + name: `generated ${index}`, + history: () => sampled()[index]!, + })), + ].map(({ name, history }) => + determinismTest(options, `determinism: ${name}`, () => [ + { name, history: history() }, + ]), + ) // A calibration also tries a fixed sample of generated histories. const calibrations = calibrationTests(options, () => [ - ...namedHistories(), + ...namedHistories().map(({ name, history }) => ({ + name, + history: history(), + })), ...fc - .sample(source.arbitrary, { - seed: source.fixedSeeds[0] ?? 0, - numRuns: 100, - }) + .sample(source.arbitrary, { seed: firstSeed, numRuns: 100 }) .map((history, index) => ({ name: `sample ${index}`, history })), ]) - return [ - ...fixedCampaigns, - randomCampaign, + const tests = [ + ...fixedUnits, + ...randomUnits, ...fixedTests, ...calibrations, - determinism, + ...determinism, ] + assertReplayUnit( + id, + randomUnits.map(({ name }) => name), + ) + return tests } +// A random unit's violation is thrown before fast-check knows its path, so +// its rerun line is completed once the unit fails. +const replayPlaceholder = `the replay command of this unit's failure` + // A collect-only run (ORACLE_MANIFEST set) records each registration, so the // committed manifest can be generated without running any history. function recordRegistration( diff --git a/packages/oracles/tests/oracle-property-self-oracle-fixture.ts b/packages/oracles/tests/oracle-property-self-oracle-fixture.ts index 6c0578f..7a34ebd 100644 --- a/packages/oracles/tests/oracle-property-self-oracle-fixture.ts +++ b/packages/oracles/tests/oracle-property-self-oracle-fixture.ts @@ -23,7 +23,8 @@ * driver's `observe("reach", state)`. A `slow` spec's driver takes about * 300 ms per history, so a small `timeout` fails every test that runs one. * A `slowShrink` spec's driver takes about 2 s on a history that holds a 4, - * but only while a campaign (`fixed seed` or `random seed`) runs it, and no + * but only while a campaign or one of its units (`fixed seed N: ` or + * `random seed: `) runs it, and no * time elsewhere, so only shrinking is slow. Every history that holds a 4 * fails, so a campaign runs at most one slow history before its first * failure. Under its 5 s timeout, the shrink of `[4,2,2]` (`[4,2]`, then @@ -150,10 +151,28 @@ export const syntheticIds = [ `self-oracle.synthetic-3`, ] as const +// A child run that draws its seed draws it through Math.random, which is a +// fixed-seed generator here (mulberry32), so it draws the same seeds in +// every run of a file and the self-oracle's own determinism test can compare +// the traces. Each draw is still the framework's own: the replay environment +// declares no seed. +let randomState = 20251111 +Math.random = () => { + randomState = (randomState + 0x6d2b79f5) | 0 + let mixed = Math.imul(randomState ^ (randomState >>> 15), 1 | randomState) + mixed = (mixed + Math.imul(mixed ^ (mixed >>> 7), 61 | mixed)) ^ mixed + return ((mixed ^ (mixed >>> 14)) >>> 0) / 4294967296 +} + // Every fixture and self-test property must be registered; `self-oracle.unregistered` -// is not, so a spec that names it fails to load. +// is not, so a spec that names it fails to load. A child run names the +// environment prefix in SELF_ORACLE_PREFIX, so a suite can run under a custom +// `envPrefix`; `SELF_ORACLE_RETIRED` is a retired replay variable. A +// malformed replay environment fails here, so every spec file fails to load. configureOracles({ + envPrefix: process.env.SELF_ORACLE_PREFIX ?? `ORACLE`, registry: [...syntheticIds, `self-oracle.framework`], + retiredVariables: [`SELF_ORACLE_RETIRED`], }) export type SyntheticHistory = ReadonlyArray @@ -203,6 +222,8 @@ export type SyntheticSpec = { source: | { kind: `generated`; runs: number; seed: number } | { kind: `enumerated`; histories: ReadonlyArray } + /** A second fixed seed, ten times the first, whose text the first's extends. */ + secondSeed?: boolean /** Required states; each must be entered by a constructed history. */ states: ReadonlyArray constructed: ReadonlyArray<{ @@ -685,7 +706,7 @@ function syntheticDriver(spec: SyntheticSpec, mutant?: `first` | `last`) { if ( spec.slowShrink && history.includes(4) && - / > (?:fixed seed -?\d+|random seed)$/.test( + / > (?:fixed seed -?\d+|random seed)(?:: .*)?$/.test( expect.getState().currentTestName ?? ``, ) ) @@ -1032,7 +1053,10 @@ export function syntheticProperty(spec: SyntheticSpec): void { .filter((state) => !spec.states.includes(state)) .map(declare), runs: spec.source.runs, - fixedSeeds: [spec.source.seed], + fixedSeeds: [ + spec.source.seed, + ...(spec.secondSeed ? [spec.source.seed * 10] : []), + ], constructed: spec.constructed.map(({ name, prefix, enters }, at) => ({ name, enters, diff --git a/packages/oracles/tests/oracle-property-self-oracle.test.ts b/packages/oracles/tests/oracle-property-self-oracle.test.ts index c836d9f..b89f22f 100644 --- a/packages/oracles/tests/oracle-property-self-oracle.test.ts +++ b/packages/oracles/tests/oracle-property-self-oracle.test.ts @@ -7,9 +7,14 @@ * process, and compares what Vitest reports with what an independent model * predicts. The laws, each judged per test or per probe: * - * - `registration`: a property registers its campaigns, fixed histories, calibrations, and - * determinism test, and an enumerated property without a `label` gives - * distinct histories distinct test names, or fails to load when its id is not a registered + * - `registration`: a property registers its campaigns' units, fixed histories, calibrations, and + * determinism tests, exactly: for each fixed seed N, `fixed seed N: ` for each constructed + * history and then `fixed seed N: generated`; `random seed: ` for each constructed history + * and then `random seed: generated`; `fixed history: ` for each fixed history; one test per + * calibration; and, for a generated source, `determinism: fixed history: `, + * `determinism: constructed history: `, and `determinism: generated 0` to `2`. An + * enumerated source keeps one `determinism` test. An enumerated property without a `label` gives + * distinct histories distinct test names. A property fails to load when its id is not a registered * oracle property, a required state has no constructed history, a constructed history names an * undeclared state, a fixed or constructed history is one the arbitrary cannot take back (law * `membership`), or `owns` is not a non-empty literal list of strings (the gap report reads it @@ -19,7 +24,18 @@ * fails with its first error alone. This precedence is analyst-chosen (2026-11-10): no contract * text or maintainer decision orders these errors. The source kind decides which checks reach the * histories, so fixing the shape can remove a data error, and fixing the data error first can be - * wasted work. + * wasted work. A generated source also fails to load when two of its tests would share a name: a + * constructed history named `generated`, two constructed histories of one name, or two fixed + * histories of one name (maintainer decision, 2026-11-11, option D). These come after its state + * checks and before law `membership`, in that order (analyst-chosen, 2026-11-11). + * - `units` (maintainer decision, 2026-11-11, option D): a campaign's units run exactly the + * histories that the campaign ran, each in its own test. The constructed unit of history k, for + * seed S, runs one history: the construction built from the arbitrary's sample at seed S + k. + * The `generated` unit runs the stream that `fc.sample` draws from the property's arbitrary, with + * its constructed weighting, at seed S, for the property's `runs`. The model draws these with + * fast-check itself, never through the framework. A unit that fails ran that stream up to its + * first failure, then its shrinks. The random units of a property run the one seed it logged: the + * seed of the replay environment in a seeded run, and a drawn seed in a seedless run. * - `verdict`: a test fails with a violation of law L exactly when its first * failing history violates L, whatever values the history holds (a bigint, * a Map, NaN, or -0 too). Within one history a driver error decides @@ -28,8 +44,9 @@ * accept any prefix of a trace: one that throws on a trace a driver error or * a clock spin cut short fails the history with an `OracleModelError` that * names the model (maintainer decision, 2026-11-08). - * - `shrink`: a campaign's reported failure keeps the kind and law of its first - * failure, and its counterexample still has them. + * - `shrink`: a unit's reported failure keeps the kind and law of its own first + * failure, and its counterexample still has them. Each unit decides its own first + * failure: a failure in one unit does not change another unit's outcome. * - `shrink budget`: a campaign whose first failure is judged in time reports * that failure's kind and law, with a counterexample that replays, before * its timeout, however long shrinking would take: it starts no shrink run @@ -54,8 +71,10 @@ * the load with an error that names the property and the constructed history and carries the * build's error as its cause; constructed histories are built and checked in order. * - `reach`: a fixed or constructed history that does not enter a state it names fails, and - * a passing campaign reports how many of its histories entered each declared - * state, whether the property names reach itself or the driver records it. An enumerated + * each passing unit reports how many of its histories entered each declared + * state, whether the property names reach itself or the driver records it. A unit that + * fails or times out prints no reach line, so the sum of a campaign's unit lines counts + * only passing units. An enumerated * source that declares `states` or `measured` registers a `reach` test after its histories: * it fails when no enumerated history entered a required state, and otherwise reports how * many entered each declared state. A history counts when it was judged, passing or @@ -84,8 +103,10 @@ * matches the empty string, fails the property's load, naming the * calibration. A check that gives a difference that is not text, where a * calibration requires one, fails that calibration naming it and the law. - * - `determinism`: the determinism test runs every fixed and constructed history - * and three generated ones, and fails for a driver whose trace changes, + * - `determinism`: a generated source's determinism units run every fixed and + * constructed history and three generated ones, each unit its one history + * twice (an enumerated source's one test runs its spaced histories), and fail + * for a driver whose trace changes, * compared by their data encoding: `-0` is not `0`, and key order and * Map and Set order count, which a check that iterates them can see. * - `agreement`: for a probe-bound state, a history whose `predict` says it @@ -112,10 +133,29 @@ * even when it comes right after the spin. * A model that throws on the trace cut at the spin is a model error, as * above. - * - `timeout`: a property's `timeout` limits every test it registers. - * - `replay`: replaying a failing campaign's seed and path runs only that - * property's random campaign, starts from the counterexample itself, and - * reproduces it. + * - `timeout`: a property's `timeout` limits every test it registers, each unit + * on its own. + * - `replay`: a failing campaign unit prints a replay command: the seed, the + * path, the property, and `${prefix}_UNIT` naming the random unit of the same + * name (`random seed: `), under the configured prefix, then that unit's + * `-t` pattern (maintainer decisions, 2026-11-11, Q3 and Q4). A failing random + * unit's violation prints the same command as its rerun line. Run as printed, + * the command runs only that random unit, starts from the counterexample + * itself, and reproduces it; every other test stands aside. + * - `replay-config`: the replay environment is read in a fixed order of + * errors: a retired variable (whose message names `${prefix}_UNIT` beside the + * seed, path, and property), then `PATH requires SEED`, `PROPERTY requires + * PATH`, a seed that is not an integer, an empty or malformed path, `PATH + * requires PROPERTY`, and an unregistered property; `${prefix}_UNIT requires + * ${prefix}_PROPERTY` comes after all of them (maintainer decision, + * 2026-11-11, Q3). A malformed environment fails every spec file's load with + * its first error. In a path replay of a generated source, `PATH` without + * `UNIT` fails that property's load with "`${prefix}_PATH` of a generated + * source requires `${prefix}_UNIT`" (Q4), and a `UNIT` that names no random + * unit of the replayed property fails its load, an enumerated property's + * included. A `UNIT` that names a random unit runs only that unit, from the + * path, and every other test stands aside. These replay errors come after + * every declaration error of the property (analyst-chosen, 2026-11-11). * - `data`: observations and enumerated histories are a closed data domain * (maintainer decision, 2026-11-08): primitives (with -0, NaN, the * infinities, bigints, and undefined), dense arrays, plain objects with @@ -128,19 +168,23 @@ * message, not its stack). * - `rerun`: a violation's printed rerun command, pasted into a POSIX shell, * runs exactly that test, also when its name holds a shell's special - * characters and when the property sits inside another suite. + * characters and when the property sits inside another suite. A failing + * fixed-seed unit prints `Rerun: -t` with its own pattern, which runs only + * that unit, also beside a unit whose name extends its name. * - `route`: each history runs under the route, in the one vocabulary of - * `oracle-route.ts`, of the campaign that runs it: a fixed-seed campaign - * `fixed seed`; the random campaign `random seed`, or `fixed seed` when a + * `oracle-route.ts`, of the campaign that runs it, each unit keeping its + * campaign's route: a fixed-seed unit + * `fixed seed`; a random unit `random seed`, or `fixed seed` when a * seed-only replay reseeds it (as the main child runs here do; a seedless * child run, without `ORACLE_SEED`, shows `random seed`), or `fixed * history` in a path replay; a fixed history `fixed history`; an enumerated * history `case`; calibrations, probe calibrations, and the determinism test - * `calibration` (TanStack/oracles#1 coordinator decisions, 2026-11-08: a + * `calibration`, and so do the determinism units (TanStack/oracles#1 coordinator decisions, 2026-11-08: a * route describes the campaign that runs, in one vocabulary). - * - `seed-log`: a random campaign logs exactly one `ORACLE_SEED` line for its - * property, the seed it runs, and no other test logs one; a replay tool - * reads that line. + * - `seed-log`: a property logs exactly one `ORACLE_SEED` line, in its first + * random unit, and no other test logs one; every random unit runs that seed + * (maintainer decision, 2026-11-11, Q2: one seed per property per process). A + * replay tool reads that line. * * Authority: the contract in the header of `oracle-property.ts`, including * its state probes (user decision of 2026-11-04 adopting differential reach); the @@ -151,8 +195,13 @@ * fails at registration, naming the history and the fix; and the oracle rubric's replay * (ORC-007), calibration (ORC-006), and declared-reach (ORC-015) rules; the * maintainer decision of 2026-11-11 (F27) that a calibration can require its - * violation's difference; and the maintainer decision of 2026-11-11 (F31) that - * a law violation is reported before the timeout, however slow shrinking would be. + * violation's difference; the maintainer decision of 2026-11-11 (F31) that + * a law violation is reported before the timeout, however slow shrinking would be; + * and the maintainer decisions of 2026-11-11 on shardable units (option D of + * the e2e speed plan, with Q2: one seed per property per process, Q3: a + * `${prefix}_UNIT` variable that requires `${prefix}_PROPERTY`, and Q4: a path + * replay of a generated source without `UNIT` fails at registration, and + * every replay line names its unit). * * Limits: synthetic properties with histories of one to three integers, held * as an array, a bigint-tagged object, or a Map, one or two per run. An @@ -184,6 +233,12 @@ * machine's speed, so a seed-only rerun can report another one; a path replay reports the same. * A driver that leaves fake timers installed that fake `performance` freezes the deadline; no * history leaves them. + * The units law reads only the prefix of a failing unit's log up to its first failure, and + * no unit of a slow spec, whose driver runs on after its test timed out. A replay environment is + * drawn with path `0` and the first spec's property only, and its unit is the first random unit + * of that spec or a missing one. A custom prefix applies to every spec of a suite. Only one fixed + * unit's `-t` rerun is probed per property, and only the determinism of a generated source is + * split into units. * A calibration's required difference is drawn only as four texts and * four patterns, including the empty ones, judged against the difference a wrong answer * reports, `item k is 3`, where k is the first item or a `driver-last` candidate's last item. A @@ -210,6 +265,7 @@ import { syntheticArbitrary, syntheticIds, } from './oracle-property-self-oracle-fixture.js' +import type { Verdict } from '../src/index.js' import type { CalibrationDifference, OddKind, @@ -257,6 +313,17 @@ type Draft = { statesMode: `exact` | `extra` | `missing` constructed: Array<{ prefix: SyntheticHistory; enters: Array }> fixed: Array<{ history: SyntheticHistory; enters: Array | null }> + /** + * How the constructed histories are named: by index; with names that + * extend each other (`c`, `c.1`), which a `-t` pattern without its `$` + * anchor cannot tell apart; with the first named `generated`; or all with + * one name. The last two break registration. + */ + constructedNames: `indexed` | `prefixed` | `generated` | `duplicate` + /** `duplicate` gives every fixed history one name, which breaks registration. */ + fixedNames: `indexed` | `duplicate` + /** A second fixed seed, ten times the first, whose text the first's extends. */ + secondSeed: boolean /** * How a generated source's arbitrary maps its histories: not at all (only * a form maps, with an unmapper), through a `.map` with an unmapper, or @@ -318,8 +385,25 @@ type Draft = { strictModel: boolean } // `seedless`: one more child run, without `ORACLE_SEED`, records the routes -// of each random campaign as an ordinary run draws its seed. -type Suite = { drafts: Array; seedless: boolean } +// of each random unit as an ordinary run draws its seed, and the seed it logged. +// `prefix`: every spec of the suite runs under this environment prefix. +// `environment`: one more child run under a drawn replay environment (law +// `replay-config`), whose path is `0` and whose property is the first spec's. +type Suite = { + drafts: Array + seedless: boolean + prefix: Prefix + environment: ReplayEnvironment | null +} +type Prefix = `ORACLE` | `SYNTH_ORACLE` +type ReplayEnvironment = { + retired: boolean + seed: `absent` | `valid` | `invalid` + path: `absent` | `valid` | `empty` | `malformed` + property: `absent` | `first` | `empty` | `unregistered` + /** The first random unit of the first spec, or a unit no spec has. */ + unit: `absent` | `named` | `missing` +} // Outside the synthetic language: an item 5, or four items. const outside = fc.oneof( @@ -371,6 +455,24 @@ const draft: fc.Arbitrary = fc.record({ }), { maxLength: 2 }, ), + // Names that extend each other are common; names that break registration + // are rare. + constructedNames: fc.oneof( + { arbitrary: fc.constant(`indexed` as const), weight: 6 }, + { arbitrary: fc.constant(`prefixed` as const), weight: 3 }, + { + arbitrary: fc.constantFrom(`generated` as const, `duplicate` as const), + weight: 1, + }, + ), + fixedNames: fc.oneof( + { arbitrary: fc.constant(`indexed` as const), weight: 9 }, + { arbitrary: fc.constant(`duplicate` as const), weight: 1 }, + ), + secondSeed: fc.oneof( + { arbitrary: fc.constant(false), weight: 4 }, + { arbitrary: fc.constant(true), weight: 1 }, + ), // Rare: a `.map` with or without an unmapper, which decides whether the // arbitrary can take a fixed or constructed history back. arbitraryMap: fc.oneof( @@ -606,12 +708,49 @@ const draft: fc.Arbitrary = fc.record({ { weight: 1, arbitrary: fc.constant(true) }, ), }) +const replayEnvironment: fc.Arbitrary = fc.record({ + retired: fc.oneof( + { weight: 5, arbitrary: fc.constant(false) }, + { weight: 1, arbitrary: fc.constant(true) }, + ), + seed: fc.constantFrom( + `absent` as const, + `valid` as const, + `invalid` as const, + ), + path: fc.constantFrom( + `absent` as const, + `valid` as const, + `empty` as const, + `malformed` as const, + ), + property: fc.constantFrom( + `absent` as const, + `first` as const, + `empty` as const, + `unregistered` as const, + ), + unit: fc.constantFrom( + `absent` as const, + `named` as const, + `missing` as const, + ), +}) const suite: fc.Arbitrary = fc.record({ drafts: fc.array(draft, { minLength: 1, maxLength: 2 }), seedless: fc.oneof( { weight: 5, arbitrary: fc.constant(false) }, { weight: 1, arbitrary: fc.constant(true) }, ), + prefix: fc.oneof( + { weight: 4, arbitrary: fc.constant(`ORACLE` as const) }, + { weight: 1, arbitrary: fc.constant(`SYNTH_ORACLE` as const) }, + ), + // Rare: one more child run under a replay environment. + environment: fc.oneof( + { weight: 4, arbitrary: fc.constant(null) }, + { weight: 1, arbitrary: replayEnvironment }, + ), }) // --------------------------------------------------------------------------- @@ -624,16 +763,35 @@ const suite: fc.Arbitrary = fc.record({ // constructed history that names an undeclared state). An enumerated draft has no // constructed or fixed histories. -type Plan = { specs: Array; seedless: boolean } +type Plan = { + specs: Array + seedless: boolean + prefix: Prefix + environment: ReplayEnvironment | null +} -function resolveSuite({ drafts, seedless }: Suite): Plan { +// A constructed history's name under the draft's naming. +const constructedName = (names: Draft[`constructedNames`], at: number) => + names === `prefixed` + ? at === 0 + ? `c` + : `c.${at}` + : names === `generated` && at === 0 + ? `generated` + : names === `duplicate` + ? `constructed` + : `constructed-${at}` + +function resolveSuite({ drafts, seedless, prefix, environment }: Suite): Plan { return { seedless, + prefix, + environment, specs: drafts.map((d, index) => { const generated = d.source.kind === `generated` const constructed = generated ? d.constructed.map((construction, at) => ({ - name: `constructed-${at}`, + name: constructedName(d.constructedNames, at), ...construction, })) : [] @@ -652,9 +810,10 @@ function resolveSuite({ drafts, seedless }: Suite): Plan { source: d.source, states, constructed, + ...(generated && d.secondSeed ? { secondSeed: true } : {}), fixed: generated ? d.fixed.map((fixedHistory, at) => ({ - name: `fixed-${at}`, + name: d.fixedNames === `duplicate` ? `fixed` : `fixed-${at}`, history: fixedHistory.history, ...(fixedHistory.enters ? { enters: fixedHistory.enters } : {}), })) @@ -1036,7 +1195,9 @@ const forcedCalibrationNames = (spec: SyntheticSpec) => // framework; the model learns that name from the log, which records the name // of the test that ran each history. const frameworkTest = (name: string) => - name === `determinism` || name === `reach` || name.startsWith(`calibration:`) + name.startsWith(`determinism`) || + name === `reach` || + name.startsWith(`calibration:`) function enumeratedName( spec: SyntheticSpec, history: SyntheticHistory, @@ -1067,14 +1228,93 @@ const calibrationCandidates = ( return [ ...spec.fixed.map(({ history }) => history), ...spec.constructed.map(({ prefix }, at) => - [ - ...prefix, - ...fc.sample(syntheticArbitrary, { seed: seed + at, numRuns: 1 })[0]!, - ].slice(0, 3), + constructedAt(prefix, seed + at), ), ...fc.sample(syntheticArbitrary, { seed, numRuns: 100 }), ] } + +// Model law `units`. A synthetic constructed history is its prefix followed by +// a generated history, cut to three items; the generated history is the +// arbitrary's sample at the seed it is built from. +const constructedAt = (prefix: SyntheticHistory, seed: number) => + [...prefix, ...fc.sample(syntheticArbitrary, { seed, numRuns: 1 })[0]!].slice( + 0, + 3, + ) +// The seed every seeded child run gives the random units (`${prefix}_SEED`). +const childSeed = 20251103 +const fixedSeedsOf = (spec: SyntheticSpec): Array => + spec.source.kind === `generated` + ? [spec.source.seed, ...(spec.secondSeed ? [spec.source.seed * 10] : [])] + : [] +// A campaign's units, in order: one per constructed history, then `generated`. +const unitNames = (spec: SyntheticSpec) => [ + ...spec.constructed.map(({ name }) => name), + `generated`, +] +const fixedUnit = (seed: number, name: string) => `fixed seed ${seed}: ${name}` +const randomUnit = (name: string) => `random seed: ${name}` +// The unit a campaign test runs: its seed (undefined for a random unit) and +// its name within the campaign. +const unitOf = (test: string): { seed?: number; name: string } | undefined => { + const fixed = /^fixed seed (-?\d+): (.*)$/.exec(test) + if (fixed) return { seed: Number(fixed[1]), name: fixed[2]! } + const random = /^random seed: (.*)$/.exec(test) + return random ? { name: random[1]! } : undefined +} +// The histories a unit draws at `seed`, in order: a constructed unit its one +// construction, built from seed + its index; the `generated` unit the stream +// that fast-check samples from the property's arbitrary with its constructed +// weighting (each constructed history weighs 1, and the language weighs their +// count) for `runs` draws. Drawn with fast-check itself, never the framework. +function unitStream( + spec: SyntheticSpec, + seed: number, + name: string, +): Array { + if (spec.source.kind !== `generated`) return [] + const at = spec.constructed.findIndex( + (construction) => construction.name === name, + ) + if (at >= 0) return [constructedAt(spec.constructed[at]!.prefix, seed + at)] + const weighted = + spec.constructed.length === 0 + ? syntheticArbitrary + : fc.oneof( + { arbitrary: syntheticArbitrary, weight: spec.constructed.length }, + ...spec.constructed.map(({ prefix }) => ({ + arbitrary: syntheticArbitrary.map((items) => + [...prefix, ...items].slice(0, 3), + ), + weight: 1, + })), + ) + return fc.sample(weighted, { seed, numRuns: spec.source.runs }) +} +// The history each determinism unit runs twice: a generated source's fixed +// histories, its constructed histories built from the first fixed seed, and +// three samples at that seed. +function determinismUnits(spec: SyntheticSpec): Map { + const [seed] = fixedSeedsOf(spec) + if (seed === undefined) return new Map() + return new Map([ + ...spec.fixed.map( + ({ name, history }) => + [`determinism: fixed history: ${name}`, history] as const, + ), + ...spec.constructed.map( + ({ name, prefix }, at) => + [ + `determinism: constructed history: ${name}`, + constructedAt(prefix, seed + at), + ] as const, + ), + ...fc + .sample(syntheticArbitrary, { seed, numRuns: 3 }) + .map((history, k) => [`determinism: generated ${k}`, history] as const), + ]) +} // What a required difference holds, stated apart from the fixture's values: // text by containment, a pattern by a match anywhere. The empty ones never // register. @@ -1098,8 +1338,7 @@ const mutatedDifference = ( ) => `item ${kind === `driver-last` ? history.length - 1 : 0} is 3` const emptyDifference = (difference: CalibrationDifference | undefined) => difference === `empty text` || difference === `empty pattern` -const isCampaign = (name: string) => - name.startsWith(`fixed seed`) || name === `random seed` +const isCampaign = (name: string) => unitOf(name) !== undefined // Model law for an enumerated source's declared states: every history runs, // so each required state must be entered by at least one of them, and the @@ -1220,6 +1459,8 @@ type SpecExpectation = /** A label that names a framework test. */ reservedLabel?: boolean dataError?: boolean + /** Two tests would share a name. */ + nameError?: boolean /** Which history failed law `membership`. */ membership?: `fixed` | `constructed` /** Whether that history is in the language, so only a `.map` without an unmapper failed it. */ @@ -1228,13 +1469,16 @@ type SpecExpectation = | { loads: true tests: Map - /** Histories a passing determinism test must run, each twice. */ - determinismRuns?: number - /** For each passing campaign, the histories entering each state. */ + /** The history each determinism unit must run, twice. */ + determinism: Map + /** The histories each campaign unit draws in this run (law `units`). */ + streams: Map> + /** For each passing unit, the histories entering each state. */ reach: Map> - /** Campaigns owed a replay probe, and the test owed a rerun probe. */ + /** Units owed a replay probe, and the tests owed a rerun probe. */ replays: Array rerun?: string + unitRerun?: string } function predictSpec( @@ -1313,6 +1557,21 @@ function predictSpec( [...entered].some((state) => !declared.has(state)) ) return { loads: false } + // Every unit and determinism test is named by its history, so two + // histories of one name, or a constructed history named like the + // generated unit, would give two tests one name. + const twice = (names: Array) => + names.find((name, at) => names.indexOf(name) !== at) + const constructedNames = spec.constructed.map(({ name }) => name) + const nameError = constructedNames.includes(`generated`) + ? `${spec.id}: constructed history "generated" has the name of a campaign's generated unit` + : twice(constructedNames) !== undefined + ? `${spec.id}: two constructed histories are named "${twice(constructedNames)}"` + : twice(spec.fixed.map(({ name }) => name)) !== undefined + ? `${spec.id}: two fixed histories are named "${twice(spec.fixed.map(({ name }) => name))}"` + : undefined + if (nameError) + return { loads: false, loadError: nameError, nameError: true } // A fixed or constructed history that the arbitrary cannot take back // fails the load (law `membership`), fixed histories first, naming the // property, the history, and the fix. @@ -1358,14 +1617,30 @@ function predictSpec( loadError: `${spec.id}: calibration "${empty.name}" requires difference`, emptyDifference: true, } + // Each campaign unit's histories in this run: a fixed seed's units at that + // seed, and the random units at the child run's seed. + const streams = new Map>([ + ...fixedSeedsOf(spec).flatMap((seed) => + unitNames(spec).map( + (name) => + [fixedUnit(seed, name), unitStream(spec, seed, name)] as const, + ), + ), + ...(generated + ? unitNames(spec).map( + (name) => + [randomUnit(name), unitStream(spec, childSeed, name)] as const, + ) + : []), + ]) + const determinismOf = determinismUnits(spec) const names = spec.source.kind === `enumerated` ? spec.source.histories.map((history) => enumeratedName(spec, history, logged), ) : [ - `fixed seed ${spec.source.seed}`, - `random seed`, + ...streams.keys(), ...spec.fixed.map( (fixedHistory) => `fixed history: ${fixedHistory.name}`, ), @@ -1375,8 +1650,9 @@ function predictSpec( ...(declaredOf(spec) ? [`reach`] : []), ...spec.calibrations.map(({ name }) => `calibration: ${name}`), ...forcedCalibrationNames(spec), - `determinism`, + ...(generated ? determinismOf.keys() : [`determinism`]), ] + const loaded = { determinism: determinismOf, streams } // A slow driver outlives the 100 ms limit in every test that runs a // history, and every test runs at least one. // A driver that observes a value outside the data domain fails every @@ -1395,17 +1671,25 @@ function predictSpec( return { loads: true, tests, + ...loaded, reach: new Map(outcome.kind === `pass` ? [[`enumerated`, counts]] : []), replays: [], } } if (data) { for (const name of all) tests.set(name, data) + const failing = names.filter(isCampaign) return { loads: true, tests, + ...loaded, reach: new Map(), - replays: names.filter(isCampaign), + replays: failing, + ...(failing.find((name) => unitOf(name)?.seed !== undefined) + ? { + unitRerun: failing.find((name) => unitOf(name)?.seed !== undefined), + } + : {}), } } if (spec.slow) { @@ -1417,7 +1701,7 @@ function predictSpec( `reach`, enumeratedReach(spec, spec.source.histories, () => false).outcome, ) - return { loads: true, tests, reach: new Map(), replays: [] } + return { loads: true, tests, ...loaded, reach: new Map(), replays: [] } } // A calibration needs a candidate whose clean trace passes; it skips the // others (maintainer decision, 2026-11-03). Every history has an item, so @@ -1454,8 +1738,9 @@ function predictSpec( // A generated property's determinism test also runs three generated // histories (maintainer decision, 2026-11-03), so a nondeterministic driver // fails it even without fixed or constructed histories. - const determinism = (): Outcome => { - const histories = ran(`determinism`).filter((_, at) => at % 2 === 0) + const determinism = ( + histories = ran(`determinism`).filter((_, at) => at % 2 === 0), + ): Outcome => { // An unbound probe that enters on every other run changes only the probe // records a run keeps, which the determinism test also compares. const varies = @@ -1474,16 +1759,19 @@ function predictSpec( if (throwsIn(history)) return { kind: `setup` } if (varies) return { kind: `determinism` } } - if (varies && generated) return { kind: `determinism` } return { kind: `pass` } } // A driver error decides a history first, then a law violation, then a // constructed history that misses a state it names (maintainer decision, - // 2026-11-03). A campaign runs its constructed histories first, in order. + // 2026-11-03). Each unit decides its own first failure, over the stream it + // draws (law `units`): a constructed unit's one history, or the generated + // unit's stream. const campaign = (test: string): Outcome => { - for (const [at, history] of ran(test).entries()) { + const construction = spec.constructed.find( + ({ name }) => name === unitOf(test)!.name, + ) + for (const history of streams.get(test)!) { const { cause: _shrinkable, ...verdict } = judged(spec, history) - const construction = spec.constructed[at] // Without a budget, a constructed history's failure shrinks to the // end. No smaller history is a constructed one, so a missed state // keeps the constructed history itself. @@ -1522,8 +1810,7 @@ function predictSpec( ).outcome, ) } else { - tests.set(names[0]!, campaign(names[0]!)) - tests.set(`random seed`, campaign(`random seed`)) + for (const unit of streams.keys()) tests.set(unit, campaign(unit)) for (const fixedHistory of spec.fixed) { const verdict = judged(spec, fixedHistory.history) tests.set( @@ -1554,7 +1841,10 @@ function predictSpec( : { kind: `calibration-none` }, ) } - tests.set(`determinism`, determinism()) + if (generated) + for (const [name, history] of determinismOf) + tests.set(name, determinism([history])) + else tests.set(`determinism`, determinism()) // A passing campaign counts, for every declared and measured state, the // histories it ran that entered it. const reach = new Map>() @@ -1569,20 +1859,23 @@ function predictSpec( judgedKind(verdictOf(history, spec)), ).counts, ) - for (const name of names.filter(isCampaign)) + // Each passing unit prints its reach: the histories of its stream that + // entered each state. + for (const [name, histories] of streams) if (tests.get(name)!.kind === `pass`) reach.set( name, Object.fromEntries( allStates.map((state) => [ state, - ran(name).filter((history) => + histories.filter((history) => reachedOf(spec, history).includes(state), ).length, ]), ), ) - // A campaign that fails inside fast-check reports a seed and path to replay. + // A unit that fails inside fast-check reports a seed and path to replay, + // and a fixed-seed unit a `-t` pattern to rerun. const replays = names.filter( (name) => isCampaign(name) && @@ -1597,15 +1890,15 @@ function predictSpec( const rerun = names.find( (name) => !isCampaign(name) && tests.get(name)!.kind === `violation`, ) + const unitRerun = replays.find((name) => unitOf(name)?.seed !== undefined) return { loads: true, tests, + ...loaded, reach, replays, ...(rerun ? { rerun } : {}), - ...(generated - ? { determinismRuns: spec.fixed.length + spec.constructed.length + 3 } - : {}), + ...(unitRerun ? { unitRerun } : {}), } } @@ -1622,8 +1915,8 @@ function suiteModel( // A late spec calls its probe again, unawaited, after every run of a history // holding a 0, also when its driver threw, and each such call throws: one // unhandled error per run the log records. A slow spec's driver runs on -// after its test timed out, so its calls may land after the run ended; they -// count at most once each. +// after its test timed out, so its calls may land after the run ended, and +// the driver records no log for it: its calls are not bounded above. const lateCalls = (plan: Plan, logged: ReadonlyArray) => { let min = 0 let max = 0 @@ -1632,22 +1925,23 @@ const lateCalls = (plan: Plan, logged: ReadonlyArray) => { const calls = logged.filter( (entry) => entry.id === spec.id && entry.history.includes(0), ).length - max += calls + max += spec.slow ? Infinity : calls if (!spec.slow) min += calls } return { min, max } } -// The route of the campaign each test runs. Every child run sets a -// seed-only replay (ORACLE_SEED), which reseeds the random campaign; a path -// replay of it runs one recorded history. +// The route of the campaign each test runs; a unit keeps its campaign's. Every +// child run sets a seed-only replay (`${prefix}_SEED`), which reseeds the +// random units; a path replay of one runs one recorded history. function owedRoute(name: string, replay = false): string { - if (name.startsWith(`fixed seed`)) return `fixed seed` - if (name === `random seed`) return replay ? `fixed history` : `fixed seed` + const unit = unitOf(name) + if (unit?.seed !== undefined) return `fixed seed` + if (unit) return replay ? `fixed history` : `fixed seed` if (name.startsWith(`fixed history:`)) return `fixed history` if ( name.startsWith(`calibration:`) || - name === `determinism` || + name.startsWith(`determinism`) || name === `reach` ) return `calibration` @@ -1731,6 +2025,21 @@ const frameworkStates = [ `enumerated-timed-out-not-rerun`, `enumerated-shape-error`, `reserved-label-error`, + `unit-split-verdict`, + `unit-name-load-error`, + `second-fixed-seed`, + `unit-replay-constructed`, + `unit-replay-generated`, + `unit-replay-custom-prefix`, + `unit-rerun`, + `unit-rerun-beside-extension`, + `seedless-units-drawn`, + `replay-environment-error`, + `unit-requires-property`, + `retired-names-unit`, + `replay-without-unit-error`, + `replay-unit-missing-error`, + `replay-unit-selected`, ] as const function frameworkReach( @@ -1751,6 +2060,7 @@ function frameworkReach( if (owed.buildError) reached.add(`constructed-build-load-error`) if (owed.emptyDifference) reached.add(`calibration-empty-difference-error`) + if (owed.nameError) reached.add(`unit-name-load-error`) if (owed.membership === `fixed`) reached.add(`fixed-membership-failure`) if (owed.membership === `constructed`) reached.add(`constructed-membership-failure`) @@ -1763,6 +2073,22 @@ function frameworkReach( } continue } + if (spec.secondSeed) reached.add(`second-fixed-seed`) + // A constructed unit and the generated unit of one seed that fail under + // different laws: each unit decided its own first failure. + for (const seed of fixedSeedsOf(spec)) { + const laws = unitNames(spec).map( + (unit) => owed.tests.get(fixedUnit(seed, unit))?.law, + ) + const generatedLaw = laws.at(-1) + if ( + generatedLaw !== undefined && + laws + .slice(0, -1) + .some((law) => law !== undefined && law !== generatedLaw) + ) + reached.add(`unit-split-verdict`) + } const named = spec.fixed.length + spec.constructed.length > 0 if (spec.arbitraryMap?.unmapper === true && named) reached.add(`unmapper-history-loads`) @@ -1811,7 +2137,8 @@ function frameworkReach( name.startsWith(`fixed history:`) ) reached.add(`uncut-spin-model-error`) - if (name === `random seed`) reached.add(`random-campaign`) + if (isCampaign(name) && unitOf(name)!.seed === undefined) + reached.add(`random-campaign`) if (outcome.kind === `determinism`) reached.add(`determinism-caught`) if (outcome.law === agreementLaw) reached.add(`agreement-violation`) if (outcome.law === `bounded clock`) reached.add(`clock-violation`) @@ -1936,7 +2263,7 @@ function frameworkReach( spec.probe === `late` && logged.some( ({ test, history }) => - test === `${spec.id} > determinism` && + test.startsWith(`${spec.id} > determinism`) && history.includes(0) && history.includes(6), ) @@ -1951,6 +2278,30 @@ function frameworkReach( if (checkpoint === `rerun` && spec?.nested) reached.add(`nested-rerun`) if (checkpoint === `replay` && (probe.routes?.length ?? 0) > 0) reached.add(`replayed-route`) + if (checkpoint === `replay` && probe.failure) { + reached.add( + unitOf(probe.target)?.name === `generated` + ? `unit-replay-generated` + : `unit-replay-constructed`, + ) + if (plan.prefix !== `ORACLE`) reached.add(`unit-replay-custom-prefix`) + } + if (checkpoint === `rerun` && spec && isCampaign(probe.target)) { + reached.add(`unit-rerun`) + // A sibling unit whose name extends the target's, which a pattern + // without its `$` anchor would also select. + if ( + expected.get(spec.id)!.loads && + [ + ...( + expected.get(spec.id) as { tests: Map } + ).tests.keys(), + ].some( + (other) => other !== probe.target && other.startsWith(probe.target), + ) + ) + reached.add(`unit-rerun-beside-extension`) + } } // A history whose probe is reached without entering the state passes the // agreement wherever the model predicts no entry, so the state is reached. @@ -1980,13 +2331,46 @@ function frameworkReach( if (trace.some(({ checkpoint }) => checkpoint === `replay`)) reached.add(`replay-probe`) const seedless = trace.find(({ checkpoint }) => checkpoint === `seedless`) + ?.value as SeedlessRun | undefined + if (seedless && Object.values(seedless).some(({ routes }) => routes.length)) + reached.add(`seedless-route`) if ( seedless && - Object.values(seedless.value as Record>).some( - (routes) => routes.length > 0, + plan.specs.some( + (spec) => + !spec.slow && Object.keys(seedless[spec.id]?.ran ?? {}).length > 0, ) ) - reached.add(`seedless-route`) + reached.add(`seedless-units-drawn`) + // Law `replay-config`: the environment's first error, or the selection a + // path replay of the first spec makes. + const under = trace.find(({ checkpoint }) => checkpoint === `environment`) + ?.value as EnvironmentRun | undefined + if (plan.environment && under) { + const error = environmentError(plan) + if (error) reached.add(`replay-environment-error`) + if (error?.includes(`_UNIT requires`)) reached.add(`unit-requires-property`) + if (error?.startsWith(`Retired`)) reached.add(`retired-names-unit`) + const [first] = plan.specs + const errors = under.files[first!.id]?.loadErrors ?? [] + if ( + !error && + errors.some((message) => + message.includes(`of a generated source requires`), + ) + ) + reached.add(`replay-without-unit-error`) + if (!error && errors.some((message) => message.includes(`_UNIT names "`))) + reached.add(`replay-unit-missing-error`) + if ( + !error && + plan.environment.path === `valid` && + (under.files[first!.id]?.tests ?? []).some( + (test) => test.state !== `skipped` && isCampaign(test.name), + ) + ) + reached.add(`replay-unit-selected`) + } if (trace.some(({ checkpoint }) => checkpoint === `rerun`)) reached.add(`rerun-probe`) return reached @@ -2001,11 +2385,15 @@ function frameworkReach( // records each file's load errors, each test's state and failure (with the // cause fast-check attaches), each passing campaign's printed reach counts, and // the synthetic driver's log. Then it probes: -// - replay: for every failing campaign with a reported seed and path, Vitest runs -// all the files again with that replay selected and its own log, which -// shows the history the replay started from; -// - rerun: for each property's first failure that printed a rerun command, -// Vitest runs that file with the command's `-t` pattern; +// - replay: for every failing campaign unit that printed a replay command, +// /bin/sh runs that command as printed, with this child's Vitest in place +// of `vitest run`, over all the files and with its own log, which shows the +// history the replay started from; +// - rerun: for each property's first history test that printed a rerun +// command, and its first fixed-seed unit that did, Vitest runs that file +// with the command's `-t` pattern; +// - environment: for a suite that draws a replay environment, Vitest runs +// all the files once under it; // - reach alone: for each loaded enumerated source that declares states, // Vitest runs that file with a `-t` pattern that selects only its reach // test. @@ -2040,7 +2428,12 @@ type Failure = { counterexample?: string seed?: number path?: string + /** The `-t` part of a rerun command, from the violation or from the unit's failure. */ rerun?: string + /** A violation's whole rerun line, as printed. */ + violationRerun?: string + /** A campaign unit's replay command, as printed. */ + replay?: string /** Whether a law's failure prints the history's items. */ showsHistory?: boolean /** Whether a model error quotes this machine's paths. */ @@ -2071,18 +2464,43 @@ type SuiteRun = { } type ProbeRun = { id: string - /** The probed test: a campaign for replay, a fixed or enumerated history for rerun. */ + /** The failing test whose command ran: a campaign unit for replay, a unit or a history for rerun. */ target: string original: Failure + /** For a replay: the printed command's variables, by name. */ + variables?: Record + /** The test the command must run: the random unit of the target's name for a replay. */ + probed: string /** Each test's state in the probe run, by property id and name. */ states: Array<[string, string, string]> /** The probed test's failure in the probe run. */ failure?: Failure - /** Histories the replayed random campaign ran, in order. */ + /** Histories the replayed random unit ran, in order. */ ran?: Array /** The routes those histories ran under. */ routes?: Array } +/** A seedless child run, per property: its random units' routes, its logged seeds, and what each unit ran. */ +type SeedlessRun = Record< + string, + { + routes: Array + seeds: Array + ran: Record> + } +> +/** The run under a drawn replay environment. */ +type EnvironmentRun = { + files: Record< + string, + { + loaded: boolean + loadErrors: Array + tests: Array<{ name: string; state: string; failure?: Failure }> + } + > + log: Array +} /** A reach test run alone, under a `-t` pattern that selects only it. */ type ReachAlone = { @@ -2114,8 +2532,17 @@ function classify(error: ReportedError | undefined): Failure { const seed = /seed: (-?\d+)/.exec(outer)?.[1] const path = /path: "([\d:]+)"/.exec(outer)?.[1] const counterexample = /Counterexample: (.*)/.exec(outer)?.[1] - // The rerun command as printed, to be pasted into a shell. - const rerun = /^Rerun: (-t .*)$/m.exec(text)?.[1] + // The rerun command as printed, to be pasted into a shell: the violation's, + // or, for a campaign unit's failure, the one its message prints. + const rerun = + /^Rerun: (-t .*)$/m.exec(text)?.[1] ?? /^Rerun: (-t .*)$/m.exec(outer)?.[1] + const violationRerun = + inner.name === `OracleViolation` + ? /^Rerun: (.*)$/m.exec(text)?.[1] + : undefined + const replay = outer.startsWith(`Property failed`) + ? /^Replay: (.*)$/m.exec(outer)?.[1] + : undefined const history = /^History: (.*)$/m.exec(text)?.[1] const law = /\(law: ([^)]+)\)/.exec(text)?.[1] const checkpoint = /violated at checkpoint "([^"]+)"/.exec(text)?.[1] @@ -2192,6 +2619,8 @@ function classify(error: ReportedError | undefined): Failure { ...(path !== undefined ? { path } : {}), ...(counterexample !== undefined ? { counterexample } : {}), ...(rerun !== undefined ? { rerun } : {}), + ...(violationRerun !== undefined ? { violationRerun } : {}), + ...(replay !== undefined ? { replay } : {}), // Only whether it shows the items: a report may print machine paths. ...(history !== undefined ? { @@ -2210,18 +2639,34 @@ const shellWord = (word: string) => `'${word.replace(/'/g, `'\\''`)}'` function runVitest( directory: string, files: Array, - env: Record, - // Shell text appended to the command, which then runs in /bin/sh, as a - // pasted rerun command does. - shellTail?: string, - // Without a seed, the random campaigns draw theirs, as in an ordinary run. - seeded = true, + { + env = {}, + shellHead, + shellTail, + seeded = true, + prefix, + }: { + env?: Record + // Shell text before the command (variable assignments) and after it (a + // `-t` pattern), which then runs in /bin/sh, as a pasted command does. + shellHead?: string + shellTail?: string + // Without a seed, the random units draw theirs, as in an ordinary run. + seeded?: boolean + // The environment prefix every spec of the suite configures. + prefix: Prefix + }, ): Report { const report = join(directory, `report-${runCount++}.json`) - // The child reads the default `ORACLE` variables, so none of the parent's - // oracle variables may leak into it. + // The child reads the suite's oracle variables, so none of the parent's + // oracle variables, under either prefix, may leak into it. const childEnv = Object.fromEntries( - Object.entries(process.env).filter(([key]) => !key.startsWith(`ORACLE_`)), + Object.entries(process.env).filter( + ([key]) => + !key.startsWith(`ORACLE_`) && + !key.startsWith(`SYNTH_ORACLE_`) && + !key.startsWith(`SELF_ORACLE_`), + ), ) const argv = [ vitest, @@ -2235,19 +2680,21 @@ function runVitest( `--dir=${directory}`, ...files, ] + const shell = shellTail !== undefined || shellHead !== undefined const run = spawnSync( - shellTail === undefined ? process.execPath : `/bin/sh`, - shellTail === undefined - ? argv - : [ + shell ? `/bin/sh` : process.execPath, + shell + ? [ `-c`, - `${[process.execPath, ...argv].map(shellWord).join(` `)} ${shellTail}`, - ], + `${shellHead ?? ``} ${[process.execPath, ...argv].map(shellWord).join(` `)} ${shellTail ?? ``}`, + ] + : argv, { cwd: packageDirectory, env: { ...childEnv, - ...(seeded ? { ORACLE_SEED: `20251103` } : {}), + SELF_ORACLE_PREFIX: prefix, + ...(seeded ? { [`${prefix}_SEED`]: String(childSeed) } : {}), ...env, SELF_ORACLE_REPORT: report, }, @@ -2274,6 +2721,16 @@ const unnested = (name: string) => name.startsWith(`${outerSuite} > `) ? name.slice(outerSuite.length + 3) : name const short = (id: string, name: string) => unnested(name).replace(`${id} > `, ``) +// A slow spec's driver runs on after its test timed out and logs under +// whichever test runs then, which the machine's speed decides, so the driver +// records no log entry of a slow spec; the model judges none. +const settledLog = (plan: Plan, log: Array) => + log.filter( + ({ id }) => !plan.specs.some((spec) => spec.slow && spec.id === id), + ) +// Each property's entries in the order its file ran them. The child runs +// spec files in parallel, so entries of two files interleave differently +// from run to run; a stable sort by id keeps each file's own order. const readLog = (log: string): Array => existsSync(log) ? readFileSync(log, `utf8`) @@ -2284,6 +2741,7 @@ const readLog = (log: string): Array => const entry = JSON.parse(line) as LogEntry return { ...entry, test: unnested(entry.test) } }) + .sort((a, b) => (a.id < b.id ? -1 : a.id > b.id ? 1 : 0)) : [] // The items of a counterexample that fast-check printed, in any form: the // first bracketed list of integers, where the lossy form's `Number.NaN` is a @@ -2310,6 +2768,75 @@ const statesIn = (report: Report, plan: Plan, files: Array) => ), ) +// The variables a printed replay command sets, by name: each `NAME=value` +// word before `vitest run`, a value single-quoted as a POSIX shell quotes it. +const replayParts = ( + command: string, +): + | { head: string; tail: string; variables: Record } + | undefined => { + const split = /^(.*?) vitest run (.*)$/.exec(command) + if (!split) return undefined + const variables: Record = {} + for (const [, name, value] of split[1]!.matchAll( + /([A-Z_]+)=('(?:[^']|'\\'')*'|\S*)/g, + )) + variables[name!] = value!.startsWith(`'`) + ? value!.slice(1, -1).replace(/'\\''/g, `'`) + : value! + return { head: split[1]!, tail: split[2]!, variables } +} + +// The `ORACLE_SEED` lines a test logged for a property, by seed. +const seedLogsOf = (test: ReportedTest, id: string) => + test.console + .split(`\n`) + .filter((line) => + line.startsWith(`ORACLE_SEED {"property":${JSON.stringify(id)},`), + ) + .map( + (line) => + (JSON.parse(line.slice(`ORACLE_SEED `.length)) as { seed: number }) + .seed, + ) + +// The variables of a drawn replay environment, under the suite's prefix. +function environmentOf(plan: Plan): Record { + const drawn = plan.environment! + const name = (setting: string) => `${plan.prefix}_${setting}` + const [first] = plan.specs + const values: Record = { + SELF_ORACLE_RETIRED: drawn.retired ? `1` : undefined, + [name(`SEED`)]: { absent: undefined, valid: `5`, invalid: `x` }[drawn.seed], + [name(`PATH`)]: { + absent: undefined, + valid: `0`, + empty: ``, + malformed: `a`, + }[drawn.path], + [name(`PROPERTY`)]: { + absent: undefined, + first: first!.id, + empty: ``, + unregistered: `self-oracle.unregistered`, + }[drawn.property], + [name(`UNIT`)]: { + absent: undefined, + named: randomUnit( + first!.source.kind === `generated` + ? unitNames(first!)[0]! + : `generated`, + ), + missing: randomUnit(`missing`), + }[drawn.unit], + } + return Object.fromEntries( + Object.entries(values).filter( + (entry): entry is [string, string] => entry[1] !== undefined, + ), + ) +} + async function driveSuite( plan: Plan, observe: (checkpoint: string, value: unknown) => void, @@ -2318,6 +2845,7 @@ async function driveSuite( packageDirectory, `.self-oracle-${process.pid}-${runCount++}`, ) + const { prefix } = plan mkdirSync(directory, { recursive: true }) try { const log = join(directory, `log.jsonl`) @@ -2329,21 +2857,21 @@ async function driveSuite( ) return file }) - const report = runVitest(directory, files, { SELF_ORACLE_LOG: log }) + const report = runVitest(directory, files, { + env: { SELF_ORACLE_LOG: log }, + prefix, + }) const run: SuiteRun = { files: {}, - log: readLog(log), + log: settledLog(plan, readLog(log)), unhandled: report.unhandled.map((error) => error.message ?? ``), } for (const [index, spec] of plan.specs.entries()) { const reported = report.files.find((file) => file.file === files[index]) - // A passing campaign prints ` reach {...}`. + // A passing unit prints ` reach {...}`. const reach: Record> = {} for (const line of report.stdout.split(`\n`)) { - const match = - /^(\S+) (fixed seed -?\d+|random seed|enumerated) reach (\{.*\})$/.exec( - line, - ) + const match = /^(\S+) (.+) reach (\{.*\})$/.exec(line) if (match?.[1] === spec.id) reach[match[2]!] = JSON.parse(match[3]!) as Record } @@ -2361,21 +2889,7 @@ async function driveSuite( ...(test.state === `failed` ? { failure: classify(test.errors[0]) } : {}), - seedLogs: test.console - .split(`\n`) - .filter((line) => - line.startsWith( - `ORACLE_SEED {"property":${JSON.stringify(spec.id)},`, - ), - ) - .map( - (line) => - ( - JSON.parse(line.slice(`ORACLE_SEED `.length)) as { - seed: number - } - ).seed, - ), + seedLogs: seedLogsOf(test, spec.id), })), reach, } @@ -2383,55 +2897,78 @@ async function driveSuite( observe(`run`, run) if (plan.seedless) { const seedlessLog = join(directory, `seedless-${runCount}.jsonl`) - runVitest( - directory, - files, - { SELF_ORACLE_LOG: seedlessLog }, - undefined, - false, - ) + const seedless = runVitest(directory, files, { + env: { SELF_ORACLE_LOG: seedlessLog }, + seeded: false, + prefix, + }) const logged = readLog(seedlessLog) - // The routes each random campaign ran under: the same whatever seed it - // drew, so this observation repeats. + const settled = new Set(settledLog(plan, logged)) + // Per property: the routes its random units ran under, the same + // whatever seed it drew; the seed it logged; and what each random unit + // ran, which that seed decides (none for a slow spec). observe( `seedless`, Object.fromEntries( - plan.specs.map((spec) => [ - spec.id, - [ - ...new Set( - logged - .filter((entry) => entry.test === `${spec.id} > random seed`) - .map((entry) => entry.route), - ), - ].sort(), - ]), - ), + plan.specs.map((spec, index) => { + const random = logged.filter( + (entry) => + entry.id === spec.id && + unitOf(entry.test.slice(spec.id.length + 3))?.seed === + undefined && + isCampaign(entry.test.slice(spec.id.length + 3)), + ) + const ran: Record> = {} + for (const entry of random.filter((kept) => settled.has(kept))) + (ran[entry.test.slice(spec.id.length + 3)] ??= []).push( + entry.history, + ) + return [ + spec.id, + { + routes: [...new Set(random.map((entry) => entry.route))].sort(), + seeds: ( + seedless.files.find((file) => file.file === files[index]) + ?.tests ?? [] + ).flatMap((test) => seedLogsOf(test, spec.id)), + ran, + }, + ] + }), + ) satisfies SeedlessRun, ) } for (const spec of plan.specs) { - for (const campaign of run.files[spec.id]!.tests) { - if (!isCampaign(campaign.name) || campaign.failure?.path === undefined) - continue + // replay: each failing unit's printed replay command, run as printed. + for (const unit of run.files[spec.id]!.tests) { + const command = unit.failure?.replay + if (!isCampaign(unit.name) || command === undefined) continue + const parts = replayParts(command) + const probed = randomUnit(unitOf(unit.name)!.name) const replayLog = join(directory, `replay-${runCount}.jsonl`) - const replay = runVitest(directory, files, { - ORACLE_SEED: String(campaign.failure.seed), - ORACLE_PATH: campaign.failure.path, - ORACLE_PROPERTY: spec.id, - SELF_ORACLE_LOG: replayLog, - }) + const replay = parts + ? runVitest(directory, files, { + env: { SELF_ORACLE_LOG: replayLog }, + shellHead: parts.head, + shellTail: parts.tail, + seeded: false, + prefix, + }) + : undefined const index = plan.specs.indexOf(spec) - const random = replay.files + const random = replay?.files .find((file) => file.file === files[index]) - ?.tests.find((test) => test.name.endsWith(`random seed`)) + ?.tests.find((test) => short(spec.id, test.name) === probed) const replayed = readLog(replayLog).filter( - (entry) => entry.test === `${spec.id} > random seed`, + (entry) => entry.test === `${spec.id} > ${probed}`, ) observe(`replay`, { id: spec.id, - target: campaign.name, - original: campaign.failure, - states: statesIn(replay, plan, files), + target: unit.name, + original: unit.failure!, + variables: parts?.variables ?? {}, + probed, + states: replay ? statesIn(replay, plan, files) : [], ...(random?.state === `failed` ? { failure: classify(random.errors[0]) } : {}), @@ -2439,25 +2976,72 @@ async function driveSuite( routes: replayed.map((entry) => entry.route), } satisfies ProbeRun) } - const target = run.files[spec.id]!.tests.find( - (test) => test.failure?.rerun !== undefined, - ) - if (!target) continue - const index = plan.specs.indexOf(spec) - const rerun = runVitest( - directory, - [files[index]!], - {}, - target.failure!.rerun, - ) - const ran = rerun.files[0]?.tests.find((test) => test.state === `failed`) - observe(`rerun`, { - id: spec.id, - target: target.name, - original: target.failure!, - states: statesIn(rerun, plan, files), - ...(ran ? { failure: classify(ran.errors[0]) } : {}), - } satisfies ProbeRun) + // rerun: the first history test and the first fixed-seed unit that + // printed a `-t` pattern. + const targets = [ + run.files[spec.id]!.tests.find( + (test) => !isCampaign(test.name) && test.failure?.rerun !== undefined, + ), + run.files[spec.id]!.tests.find( + (test) => + unitOf(test.name)?.seed !== undefined && + test.failure?.rerun !== undefined, + ), + ] + for (const target of targets) { + if (!target) continue + const index = plan.specs.indexOf(spec) + const rerun = runVitest(directory, [files[index]!], { + shellTail: target.failure!.rerun, + prefix, + }) + const ran = rerun.files[0]?.tests.find( + (test) => test.state === `failed`, + ) + observe(`rerun`, { + id: spec.id, + target: target.name, + original: target.failure!, + probed: target.name, + states: statesIn(rerun, plan, files), + ...(ran ? { failure: classify(ran.errors[0]) } : {}), + } satisfies ProbeRun) + } + } + // environment: every file once under the drawn replay environment. + if (plan.environment) { + const environmentLog = join(directory, `environment-${runCount}.jsonl`) + const under = runVitest(directory, files, { + env: { ...environmentOf(plan), SELF_ORACLE_LOG: environmentLog }, + seeded: false, + prefix, + }) + observe(`environment`, { + files: Object.fromEntries( + plan.specs.map((spec, index) => { + const reported = under.files.find( + (file) => file.file === files[index], + ) + return [ + spec.id, + { + loaded: reported !== undefined && reported.errors.length === 0, + loadErrors: (reported?.errors ?? []).map( + (error) => error.message ?? ``, + ), + tests: (reported?.tests ?? []).map((test) => ({ + name: short(spec.id, test.name), + state: test.state, + ...(test.state === `failed` + ? { failure: classify(test.errors[0]) } + : {}), + })), + }, + ] + }), + ), + log: settledLog(plan, readLog(environmentLog)), + } satisfies EnvironmentRun) } // reach: for each loaded enumerated source that declares states, Vitest // runs that file again with a `-t` pattern that selects only its reach @@ -2469,12 +3053,10 @@ async function driveSuite( const escape = (text: string) => text.replace(/[.*+?^${}()|[\]\\]/g, `\\$&`) const pattern = `^${[...(spec.nested ? [outerSuite] : []), spec.id, `reach`].map(escape).join(`(?: | > )`)}$` - const alone = runVitest( - directory, - [files[index]!], - {}, - `-t ${shellWord(pattern)}`, - ) + const alone = runVitest(directory, [files[index]!], { + shellTail: `-t ${shellWord(pattern)}`, + prefix, + }) const test = alone.files[0]?.tests.find( (candidate) => short(spec.id, candidate.name) === `reach`, ) @@ -2506,17 +3088,21 @@ async function driveSuite( // // For each property: it loads exactly when the model says so; it registers // exactly the owed tests; each test passes, or fails with the owed kind, law, -// and cause; a campaign's counterexample still violates the owed law; a passing -// determinism test ran every history it owes; and each passing campaign printed -// the owed reach counts. Then the probes: the replays and reruns the model -// owes all happened; in each, every other test stood aside; the probed test -// failed again the same way; and a replay started from the counterexample -// itself, as a direct replay must, and reported the same one. +// and cause; a unit's counterexample still violates the owed law; each unit +// ran the stream the model draws (law `units`); a passing determinism unit +// ran its history twice; and each passing unit printed the owed reach counts. +// Then the probes: the replays and reruns the model owes all happened; a +// replay command names the seed, path, property, and unit under the suite's +// prefix; in each, every other test stood aside; the probed test failed again +// the same way; and a replay started from the counterexample itself, as a +// direct replay must, and reported the same one. Last, the seedless run's +// random units ran the seed they logged, and a run under a drawn replay +// environment failed or selected as law `replay-config` owes. const lawOfTest = (name: string) => name.startsWith(`calibration:`) ? `calibration` - : name === `determinism` + : name.startsWith(`determinism`) ? `determinism` : name === `reach` ? `reach` @@ -2534,6 +3120,60 @@ const lawOfKind = (kind: string, name: string) => ? `reach` : lawOfTest(name) +// Whether a unit's history fails it: a data error, a failing verdict, or, in +// a constructed unit, a state its construction names and does not enter. +const failsUnit = ( + spec: SyntheticSpec, + unit: string, + history: SyntheticHistory, +) => { + const construction = spec.constructed.find( + ({ name }) => name === unitOf(unit)?.name, + ) + return ( + dataOutcome(spec) !== undefined || + judged(spec, history).kind !== `pass` || + (construction !== undefined && !reaches(spec, history, construction.enters)) + ) +} +// A unit's log, compared with its stream: all of it when the unit passes, +// and up to its first failure when it fails, after which it shrinks. +const streamPrefix = ( + spec: SyntheticSpec, + unit: string, + stream: ReadonlyArray, +) => { + const first = stream.findIndex((history) => failsUnit(spec, unit, history)) + return first < 0 ? stream : stream.slice(0, first + 1) +} + +// Model law `replay-config`: the first error of the drawn replay +// environment, in the order the law states, or none. +function environmentError(plan: Plan): string | undefined { + const drawn = plan.environment! + const name = (setting: string) => `${plan.prefix}_${setting}` + if (drawn.retired) + return `Retired oracle replay variables are set: SELF_ORACLE_RETIRED. Use ${name(`SEED`)}, ${name(`PATH`)}, ${name(`PROPERTY`)}, and ${name(`UNIT`)} to select a replay, and ${name(`RUNS_MULTIPLIER`)} to scale run counts.` + // An empty property is still set. + const property = drawn.property !== `absent` + const unit = drawn.unit !== `absent` + if (drawn.seed === `absent` && drawn.path !== `absent`) + return `${name(`PATH`)} requires ${name(`SEED`)}` + if (drawn.seed !== `invalid` && drawn.path === `absent`) { + if (property) return `${name(`PROPERTY`)} requires ${name(`PATH`)}` + return unit ? `${name(`UNIT`)} requires ${name(`PROPERTY`)}` : undefined + } + if (drawn.seed === `invalid`) return `${name(`SEED`)} must be an integer` + if (drawn.path === `empty`) return `${name(`PATH`)} must be non-empty` + if (drawn.path === `malformed`) + return `${name(`PATH`)} must contain colon-separated nonnegative integers` + if (!property || drawn.property === `empty`) + return `${name(`PATH`)} requires ${name(`PROPERTY`)}` + if (drawn.property === `unregistered`) + return `unknown oracle property: self-oracle.unregistered` + return undefined +} + function checkSuite( plan: Plan, trace: ReadonlyArray<{ checkpoint: string; value: unknown }>, @@ -2550,6 +3190,7 @@ function checkSuite( checkpoint, probe: value as ProbeRun, })) + const name = (setting: string) => `${plan.prefix}_${setting}` for (const spec of plan.specs) { const owed = expected.get(spec.id)! const seen = run.files[spec.id]! @@ -2558,7 +3199,7 @@ function checkSuite( if (seen.loaded) return violation( `run`, - `${spec.id} loaded, but its id is unregistered, a required state has no constructed history, a constructed history names an undeclared state, a fixed or constructed history is one the arbitrary cannot take back, \`owns\` is not a non-empty literal list of strings, or a history is not data`, + `${spec.id} loaded, but its id is unregistered, a required state has no constructed history, a constructed history names an undeclared state, two of its tests would share a name, a fixed or constructed history is one the arbitrary cannot take back, \`owns\` is not a non-empty literal list of strings, or a history is not data`, law, ) const owedText = [owed.loadError, owed.loadFix].filter( @@ -2576,7 +3217,7 @@ function checkSuite( return violation( `run`, `${spec.id} failed to load with ${JSON.stringify(seen.loadErrors)}, owed ${JSON.stringify(owedText)}`, - owed.membership ? law : `data`, + owed.membership || owed.nameError ? law : `data`, { actual: seen.loadErrors, expected: owedText }, ) continue @@ -2601,6 +3242,13 @@ function checkSuite( `registration`, { actual: seenNames, expected: names }, ) + // The property's one logged seed, which its first random unit logs. + const firstRandom = + spec.source.kind === `generated` + ? randomUnit(unitNames(spec)[0]!) + : undefined + const loggedSeed = seen.tests.find((test) => test.name === firstRandom) + ?.seedLogs[0] for (const test of seen.tests) { const outcome = owed.tests.get(test.name)! const failure = test.failure @@ -2619,7 +3267,7 @@ function checkSuite( return violation( `run`, `${spec.id} "${test.name}" ${test.state} as ${JSON.stringify(failure ?? null)}, owed ${JSON.stringify(outcome)}`, - // A campaign that owes a failure and times out shrank too long. + // A unit that owes a failure and times out shrank too long. isCampaign(test.name) && observedKind === `timeout` && ![`pass`, `timeout`].includes(outcome.kind) @@ -2649,9 +3297,9 @@ function checkSuite( `${spec.id} "${test.name}" printed a History line that does not show the history`, `verdict`, ) - // A random campaign selects its seed once and logs that selection once; - // a failing campaign's reported seed is the logged one. - const owedSeedLogs = test.name === `random seed` ? 1 : 0 + // A property selects its seed once, in its first random unit, and + // logs that selection once; every random unit runs it. + const owedSeedLogs = test.name === firstRandom ? 1 : 0 if (test.seedLogs.length !== owedSeedLogs) return violation( `run`, @@ -2661,29 +3309,62 @@ function checkSuite( ) if ( failure?.seed !== undefined && - test.name === `random seed` && - test.seedLogs[0] !== failure.seed + unitOf(test.name) !== undefined && + unitOf(test.name)!.seed === undefined && + loggedSeed !== failure.seed ) return violation( `run`, - `${spec.id} "${test.name}" logged seed ${test.seedLogs[0]} but ran seed ${failure.seed}`, + `${spec.id} "${test.name}" ran seed ${failure.seed}, but the property logged seed ${loggedSeed}`, `seed-log`, - { actual: failure.seed, expected: test.seedLogs[0] }, + { actual: failure.seed, expected: loggedSeed }, ) - if ( - test.name === `determinism` && - test.state === `passed` && - owed.determinismRuns !== undefined - ) { - const runs = run.log.filter( - (entry) => - entry.id === spec.id && entry.test === `${spec.id} > determinism`, - ).length - if (runs !== 2 * owed.determinismRuns) + // A failing unit prints its replay command; a failing fixed-seed unit + // also prints its own `-t` pattern; a failing random unit's violation + // prints the replay command as its rerun line. + const unit = unitOf(test.name) + if (unit && failure?.seed !== undefined) { + if (failure.replay === undefined) + return violation( + `run`, + `${spec.id} "${test.name}" failed with seed ${failure.seed} and printed no replay command`, + `replay`, + ) + if (unit.seed !== undefined && failure.rerun === undefined) + return violation( + `run`, + `${spec.id} "${test.name}" failed and printed no \`-t\` rerun of itself`, + `rerun`, + ) + const owedLine = + unit.seed === undefined ? failure.replay : failure.rerun + if ( + failure.violationRerun !== undefined && + failure.violationRerun !== owedLine + ) + return violation( + `run`, + `${spec.id} "${test.name}" printed the rerun line ${JSON.stringify(failure.violationRerun)} in its violation, owed ${JSON.stringify(owedLine)}`, + unit.seed === undefined ? `replay` : `rerun`, + { actual: failure.violationRerun, expected: owedLine }, + ) + } + // A passing determinism unit ran its one history twice. + const twice = owed.determinism.get(test.name) + if (twice && test.state === `passed`) { + const runs = run.log + .filter( + (entry) => + entry.id === spec.id && + entry.test === `${spec.id} > ${test.name}`, + ) + .map((entry) => entry.history) + if (JSON.stringify(runs) !== JSON.stringify([twice, twice])) return violation( `run`, - `${spec.id} determinism ran ${runs / 2} histories, owed ${owed.determinismRuns}`, + `${spec.id} "${test.name}" ran ${JSON.stringify(runs)}, owed ${JSON.stringify(twice)} twice`, `determinism`, + { actual: runs, expected: [twice, twice] }, ) } // Without a timeout, a campaign shrinks without a budget. @@ -2710,6 +3391,24 @@ function checkSuite( ) } } + // Law `units`: each unit ran the stream the model draws, up to its + // first failure. A slow spec's driver runs on after its test timed out, + // so its log names other tests. + if (!spec.slow) + for (const [unit, stream] of owed.streams) { + const owedRun = streamPrefix(spec, unit, stream) + const ran = run.log + .filter((entry) => entry.test === `${spec.id} > ${unit}`) + .map((entry) => entry.history) + .slice(0, owedRun.length) + if (JSON.stringify(ran) !== JSON.stringify(owedRun)) + return violation( + `run`, + `${spec.id} "${unit}" ran ${JSON.stringify(ran)}, owed ${JSON.stringify(owedRun)}`, + `units`, + { actual: ran, expected: owedRun }, + ) + } for (const [campaign, counts] of owed.reach) if (JSON.stringify(seen.reach[campaign]) !== JSON.stringify(counts)) return violation( @@ -2718,6 +3417,18 @@ function checkSuite( `reach`, { actual: seen.reach[campaign], expected: counts }, ) + // Only a test that passes in time prints reach: a merge of the units' + // lines must not count a unit that failed or timed out. + const unowed = Object.keys(seen.reach).filter( + (test) => !owed.reach.has(test), + ) + if (unowed.length > 0) + return violation( + `run`, + `${spec.id} printed reach for ${JSON.stringify(unowed)}, which passed no test in time`, + `reach`, + { actual: unowed, expected: [] }, + ) for (const campaign of owed.replays) if ( !probes.some( @@ -2732,37 +3443,67 @@ function checkSuite( `${spec.id} "${campaign}" failed but was never replayed`, `replay`, ) - if ( - owed.rerun && - !probes.some( - ({ checkpoint, probe }) => - checkpoint === `rerun` && probe.id === spec.id, - ) - ) - return violation( - `rerun`, - `${spec.id} "${owed.rerun}" printed no rerun command`, - `rerun`, + for (const [owedRerun, unitTarget] of [ + [owed.rerun, false], + [owed.unitRerun, true], + ] as const) + if ( + owedRerun && + !probes.some( + ({ checkpoint, probe }) => + checkpoint === `rerun` && + probe.id === spec.id && + isCampaign(probe.target) === unitTarget, + ) ) + return violation( + `rerun`, + `${spec.id} "${owedRerun}" printed no rerun command`, + `rerun`, + ) } - // In a run without a seed, every history of a random campaign runs under - // `random seed`, and a loaded campaign runs at least one. A slow campaign - // times out, but its first history starts before it does. + // In a run without a seed, every history of a random unit runs under + // `random seed`, and a loaded property runs at least one. A slow unit + // times out, but its first history starts before it does. The property + // logged one seed, and each random unit ran the stream of that seed. const seedless = trace.find(({ checkpoint }) => checkpoint === `seedless`) - ?.value as Record> | undefined + ?.value as SeedlessRun | undefined if (seedless) for (const spec of plan.specs) { - const owedRoutes = + const generated = expected.get(spec.id)!.loads && spec.source.kind === `generated` - ? [`random seed`] - : [] - if (JSON.stringify(seedless[spec.id]) !== JSON.stringify(owedRoutes)) + const owedRoutes = generated ? [`random seed`] : [] + const { routes, seeds, ran } = seedless[spec.id]! + if (JSON.stringify(routes) !== JSON.stringify(owedRoutes)) return violation( `seedless`, - `${spec.id}: an ordinary run's random campaign ran under ${JSON.stringify(seedless[spec.id])}, owed ${JSON.stringify(owedRoutes)}`, + `${spec.id}: an ordinary run's random units ran under ${JSON.stringify(routes)}, owed ${JSON.stringify(owedRoutes)}`, `route`, - { actual: seedless[spec.id], expected: owedRoutes }, + { actual: routes, expected: owedRoutes }, ) + if (seeds.length !== (generated ? 1 : 0)) + return violation( + `seedless`, + `${spec.id}: an ordinary run logged ${seeds.length} ORACLE_SEED lines, owed ${generated ? 1 : 0}`, + `seed-log`, + { actual: seeds, expected: generated ? 1 : 0 }, + ) + if (!generated || spec.slow) continue + for (const unit of unitNames(spec).map(randomUnit)) { + const owedRun = streamPrefix( + spec, + unit, + unitStream(spec, seeds[0]!, unitOf(unit)!.name), + ) + const logged = (ran[unit] ?? []).slice(0, owedRun.length) + if (JSON.stringify(logged) !== JSON.stringify(owedRun)) + return violation( + `seedless`, + `${spec.id} "${unit}" ran ${JSON.stringify(logged)} in an ordinary run that logged seed ${seeds[0]}, owed ${JSON.stringify(owedRun)}`, + `units`, + { actual: logged, expected: owedRun }, + ) + } } // In a full run, every history's test starts, so the reach test runs // none of them again: it reuses what their tests recorded. @@ -2824,20 +3565,39 @@ function checkSuite( for (const spec of plan.specs) { if (!expected.get(spec.id)!.loads || spec.slow) continue for (const entry of run.log.filter(({ id }) => id === spec.id)) { - const name = entry.test.slice(spec.id.length + 3) - if (entry.route !== owedRoute(name)) + const test = entry.test.slice(spec.id.length + 3) + if (entry.route !== owedRoute(test)) return violation( `run`, - `${spec.id} "${name}" ran ${JSON.stringify(entry.history)} under route ${JSON.stringify(entry.route)}, owed ${JSON.stringify(owedRoute(name))}`, + `${spec.id} "${test}" ran ${JSON.stringify(entry.history)} under route ${JSON.stringify(entry.route)}, owed ${JSON.stringify(owedRoute(test))}`, `route`, - { actual: entry.route, expected: owedRoute(name) }, + { actual: entry.route, expected: owedRoute(test) }, ) } } for (const { checkpoint, probe } of probes) { - const probed = checkpoint === `replay` ? `random seed` : probe.target + if (checkpoint === `replay`) { + // The printed command names the seed, the path, the property, and the + // random unit of the target's name, under the suite's prefix. + const owedVariables = { + [name(`SEED`)]: String(probe.original.seed), + [name(`PATH`)]: probe.original.path, + [name(`PROPERTY`)]: probe.id, + [name(`UNIT`)]: probe.probed, + } + const printed = Object.fromEntries( + Object.keys(owedVariables).map((key) => [key, probe.variables?.[key]]), + ) + if (JSON.stringify(printed) !== JSON.stringify(owedVariables)) + return violation( + checkpoint, + `${probe.id} "${probe.target}" printed a replay command with ${JSON.stringify(probe.variables)}, owed ${JSON.stringify(owedVariables)}`, + `replay`, + { actual: printed, expected: owedVariables }, + ) + } const others = probe.states.filter( - ([id, name]) => !(id === probe.id && name === probed), + ([id, test]) => !(id === probe.id && test === probe.probed), ) if (others.some(([, , state]) => state !== `skipped`)) return violation( @@ -2848,7 +3608,7 @@ function checkSuite( if (!probe.failure) return violation( checkpoint, - `${probe.id} ${checkpoint} of "${probe.target}": "${probed}" did not fail again`, + `${probe.id} ${checkpoint} of "${probe.target}": "${probe.probed}" did not fail again`, checkpoint, ) if ( @@ -2861,7 +3621,7 @@ function checkSuite( checkpoint, ) if (checkpoint !== `replay`) continue - const replayRoute = owedRoute(`random seed`, true) + const replayRoute = owedRoute(probe.probed, true) if (probe.routes?.some((route) => route !== replayRoute)) return violation( checkpoint, @@ -2888,7 +3648,104 @@ function checkSuite( `replay`, ) } - return pass + return checkEnvironment(plan, trace, expected) ?? pass +} + +// Law `replay-config`: under a malformed replay environment every file fails +// to load with its first error. Otherwise, in a path replay of the first +// spec's property, a generated source without `UNIT`, or with a `UNIT` that +// names none of its random units, fails to load, and so does an enumerated +// source with a `UNIT`; a `UNIT` that names a random unit runs only that +// unit, the history at path `0` of its stream at seed 5. Every other spec +// stands aside. Without a path, every spec loads as it does in the main run. +function checkEnvironment( + plan: Plan, + trace: ReadonlyArray<{ checkpoint: string; value: unknown }>, + expected: ReturnType, +): Verdict | undefined { + const under = trace.find(({ checkpoint }) => checkpoint === `environment`) + ?.value as EnvironmentRun | undefined + if (!plan.environment || !under) return undefined + const name = (setting: string) => `${plan.prefix}_${setting}` + const failed = (text: string) => + violation(`environment`, text, `replay-config`) + const error = environmentError(plan) + const drawn = plan.environment + const replays = drawn.path === `valid` && error === undefined + const unit = environmentOf(plan)[name(`UNIT`)] + for (const [index, spec] of plan.specs.entries()) { + const owed = expected.get(spec.id)! + const seen = under.files[spec.id]! + const selected = replays && index === 0 && !spec.unregistered + // The text of the replay error the selected spec's registration owes. + const replayError = !selected + ? undefined + : spec.source.kind === `enumerated` + ? unit === undefined + ? undefined + : `${spec.id}: ${name(`UNIT`)} names "${unit}"` + : unit === undefined + ? `${spec.id}: ${name(`PATH`)} of a generated source requires ${name(`UNIT`)}` + : unitNames(spec).map(randomUnit).includes(unit) + ? undefined + : `${spec.id}: ${name(`UNIT`)} names "${unit}"` + const owedError = + error ?? (owed.loads ? replayError : (owed.loadError ?? undefined)) + const owedLoads = error === undefined && owed.loads && !replayError + if (seen.loaded !== owedLoads) + return failed( + `${spec.id} ${seen.loaded ? `loaded` : `failed to load with ${JSON.stringify(seen.loadErrors)}`} under ${JSON.stringify(environmentOf(plan))}, owed ${owedLoads ? `a load` : JSON.stringify(owedError ?? `a load error`)}`, + ) + if ( + !seen.loaded && + owedError !== undefined && + !seen.loadErrors.some((message) => message.includes(owedError)) + ) + return failed( + `${spec.id} failed to load with ${JSON.stringify(seen.loadErrors)} under ${JSON.stringify(environmentOf(plan))}, owed ${JSON.stringify(owedError)}`, + ) + if (!seen.loaded || !replays) continue + // A path replay: only the selected unit runs, if any. + const running = seen.tests.filter((test) => test.state !== `skipped`) + const owedRunning = selected && unit !== undefined ? [unit] : [] + if ( + JSON.stringify(running.map((test) => test.name)) !== + JSON.stringify(owedRunning) + ) + return failed( + `${spec.id} ran ${JSON.stringify(running.map((test) => test.name))} in a path replay that selects ${JSON.stringify(unit ?? null)}, owed ${JSON.stringify(owedRunning)}`, + ) + if (owedRunning.length === 0) continue + const [history] = unitStream(spec, 5, unitOf(unit!)!.name) + const ran = under.log + .filter((entry) => entry.test === `${spec.id} > ${unit}`) + .map((entry) => entry.history) + if (!spec.slow && JSON.stringify(ran) !== JSON.stringify([history])) + return failed( + `${spec.id} "${unit}" ran ${JSON.stringify(ran)} at path 0, owed ${JSON.stringify([history])}`, + ) + const owedKind = + dataOutcome(spec)?.kind ?? + (spec.slow + ? `timeout` + : failsUnit(spec, unit!, history!) + ? (() => { + const verdict = judged(spec, history!) + return verdict.kind === `pass` + ? `constructed-reach` + : verdict.kind + })() + : `pass`) + const observed = + running[0]!.state === `passed` + ? `pass` + : (running[0]!.failure?.kind ?? `other`) + if (observed !== owedKind) + return failed( + `${spec.id} "${unit}" ${running[0]!.state} as ${JSON.stringify(running[0]!.failure ?? null)} at path 0, owed ${owedKind}`, + ) + } + return undefined } // --------------------------------------------------------------------------- @@ -2903,6 +3760,9 @@ const generatedDraft = (overrides: Partial): Draft => ({ statesMode: `exact`, constructed: [], fixed: [], + constructedNames: `indexed`, + fixedNames: `indexed`, + secondSeed: false, arbitraryMap: `none`, mapAt: `history`, enumeratedStates: null, @@ -2945,12 +3805,51 @@ const fixedHistory = ( name: string, enters: Array<(typeof frameworkStates)[number]>, ...drafts: Array -) => ({ name, enters, history: { drafts, seedless: false } }) +) => ({ + name, + enters, + history: { + drafts, + seedless: false, + prefix: `ORACLE` as Prefix, + environment: null, + }, +}) const seedlessHistory = ( name: string, enters: Array<(typeof frameworkStates)[number]>, ...drafts: Array -) => ({ name, enters, history: { drafts, seedless: true } }) +) => ({ + name, + enters, + history: { + drafts, + seedless: true, + prefix: `ORACLE` as Prefix, + environment: null, + }, +}) +// A suite under a custom environment prefix, a drawn replay environment, or both. +const suiteHistory = ( + name: string, + enters: Array<(typeof frameworkStates)[number]>, + { prefix = `ORACLE`, environment = null }: Partial>, + ...drafts: Array +) => ({ + name, + enters, + history: { drafts, seedless: false, prefix, environment }, +}) +const replayOf = ( + environment: Partial, +): ReplayEnvironment => ({ + retired: false, + seed: `valid`, + path: `valid`, + property: `first`, + unit: `named`, + ...environment, +}) const at = (history: SyntheticHistory) => ({ history, enters: null }) const cal = ( kind: CalibrationDraft[`kind`], @@ -3011,7 +3910,7 @@ oracleProperty({ ), fixedHistory( `a replayed campaign failure reproduces its path`, - [`replay-probe`], + [`replay-probe`, `unit-replay-constructed`], generatedDraft({ constructed: [{ prefix: [1, 3], enters: [`saw-1`] }], }), @@ -3771,6 +4670,146 @@ oracleProperty({ [`timeout`], generatedDraft({ timing: `slow`, fixed: [at([0])] }), ), + // Units (maintainer decision, 2026-11-11, option D). At seed 5, the + // generated unit's first failing history holds a 4 first, and the + // constructed unit's history starts with a 3. + fixedHistory( + `each unit decides its own first failure`, + [`unit-split-verdict`, `campaign-violation`, `replay-probe`], + generatedDraft({ + source: { kind: `generated`, runs: 2, seed: 5 }, + constructed: [{ prefix: [3], enters: [] }], + }), + ), + // At seed 6, without constructed histories, the generated unit fails. + fixedHistory( + `a generated unit's replay runs only that unit`, + [`unit-replay-generated`, `replay-probe`], + generatedDraft({ source: { kind: `generated`, runs: 2, seed: 6 } }), + ), + fixedHistory( + `a constructed history named generated fails to load`, + [`registration-error`, `unit-name-load-error`], + generatedDraft({ + constructedNames: `generated`, + constructed: [{ prefix: [0], enters: [`saw-0`] }], + }), + ), + fixedHistory( + `two constructed histories of one name fail to load`, + [`registration-error`, `unit-name-load-error`], + generatedDraft({ + constructedNames: `duplicate`, + constructed: [ + { prefix: [0], enters: [`saw-0`] }, + { prefix: [1], enters: [`saw-1`] }, + ], + }), + ), + fixedHistory( + `two fixed histories of one name fail to load`, + [`registration-error`, `unit-name-load-error`], + generatedDraft({ fixedNames: `duplicate`, fixed: [at([0]), at([1])] }), + ), + // At seed 7, `c` fails and `c.1`, whose name extends it, passes. + fixedHistory( + `a unit's rerun runs it beside a unit whose name extends its name`, + [`unit-rerun`, `unit-rerun-beside-extension`], + generatedDraft({ + constructedNames: `prefixed`, + constructed: [ + { prefix: [3], enters: [] }, + { prefix: [0], enters: [`saw-0`] }, + ], + }), + ), + fixedHistory( + `a second fixed seed, whose text extends the first, runs its own units`, + [`second-fixed-seed`, `unit-rerun`], + generatedDraft({ + source: { kind: `generated`, runs: 2, seed: 1 }, + secondSeed: true, + constructed: [{ prefix: [3], enters: [] }], + }), + ), + seedlessHistory( + `an ordinary run's random units run the one seed they logged`, + [`seedless-units-drawn`, `seedless-route`], + generatedDraft({ + constructed: [ + { prefix: [0], enters: [`saw-0`] }, + { prefix: [1], enters: [`saw-1`] }, + ], + }), + ), + suiteHistory( + `a replay command under a custom prefix names its variables`, + [`unit-replay-custom-prefix`, `replay-probe`], + { prefix: `SYNTH_ORACLE` }, + generatedDraft({ constructed: [{ prefix: [3], enters: [] }] }), + ), + // Law `replay-config` (maintainer decisions, 2026-11-11, Q3 and Q4). + suiteHistory( + `UNIT without PROPERTY fails every load`, + [`replay-environment-error`, `unit-requires-property`], + { environment: replayOf({ path: `absent`, property: `absent` }) }, + generatedDraft({ constructed: [{ prefix: [0], enters: [`saw-0`] }] }), + ), + suiteHistory( + `UNIT alone fails every load under a custom prefix`, + [`replay-environment-error`, `unit-requires-property`], + { + prefix: `SYNTH_ORACLE`, + environment: replayOf({ + seed: `absent`, + path: `absent`, + property: `absent`, + }), + }, + generatedDraft({}), + ), + suiteHistory( + `PATH requires SEED before UNIT requires PROPERTY`, + [`replay-environment-error`], + { + environment: replayOf({ seed: `absent`, property: `absent` }), + }, + generatedDraft({}), + ), + suiteHistory( + `a retired variable's message names UNIT`, + [`replay-environment-error`, `retired-names-unit`], + { environment: replayOf({ retired: true }) }, + generatedDraft({}), + ), + suiteHistory( + `a path replay of a generated source without UNIT fails its load`, + [`replay-without-unit-error`], + { environment: replayOf({ unit: `absent` }) }, + generatedDraft({ constructed: [{ prefix: [0], enters: [`saw-0`] }] }), + ), + suiteHistory( + `a UNIT that names no random unit fails its load`, + [`replay-unit-missing-error`], + { prefix: `SYNTH_ORACLE`, environment: replayOf({ unit: `missing` }) }, + generatedDraft({}), + ), + suiteHistory( + `a UNIT on an enumerated property fails its load`, + [`replay-unit-missing-error`], + { environment: replayOf({}) }, + { + ...generatedDraft({}), + source: { kind: `enumerated`, histories: [[0], [1]] }, + }, + ), + suiteHistory( + `a UNIT that names a random unit runs only that unit`, + [`replay-unit-selected`], + { environment: replayOf({}) }, + generatedDraft({ constructed: [{ prefix: [3], enters: [] }] }), + generatedDraft({ constructed: [{ prefix: [0], enters: [`saw-0`] }] }), + ), ], }, resolve: resolveSuite, From 5a5b8ab0caf585dc02c756738c1d9747d184cfad Mon Sep 17 00:00:00 2001 From: Kyle Mathews Date: Wed, 11 Nov 2026 14:45:01 -0700 Subject: [PATCH 2/4] fix(oracles): an exact units law for passing units, and a random unit's violation built once The self-oracle's units law now requires a unit that the model owes a pass to run exactly its stream, no history more; only a failing unit is compared up to its first failure. Mutant D-M8 (a constructed unit keeps the generated runs) now fails: "fixed seed 7: constructed-0" ran [[0,0,0],[0,0,0],[0,0,0]], owed [[0,0,0]]. The model's comment on unitStream says that its weighting restates production's composition, which the design authorizes, and is no contract promise. A random unit's violation is now built once, after fast-check reports its path, with the real replay command as its rerun line, so its stack holds the message it prints; without a path it prints no rerun line. Before, the message was patched over a placeholder that the stack kept. Vitest reprints a failure's stack header from its message, so the self-oracle cannot observe the raw stack; that is a stated limit. Co-authored-by: Isaac --- packages/oracles/src/oracle-property.ts | 64 ++++++++++++------- .../tests/oracle-property-self-oracle.test.ts | 48 +++++++++----- 2 files changed, 74 insertions(+), 38 deletions(-) diff --git a/packages/oracles/src/oracle-property.ts b/packages/oracles/src/oracle-property.ts index adb5ca0..ca6b59e 100644 --- a/packages/oracles/src/oracle-property.ts +++ b/packages/oracles/src/oracle-property.ts @@ -1696,8 +1696,9 @@ function judge( return { verdict, reached } } -const lawOf = (verdict: Extract) => - verdict.law ?? verdict.checkpoint +type Violation = Extract + +const lawOf = (verdict: Violation) => verdict.law ?? verdict.checkpoint /** * One test per calibration. It tries candidate histories in order until the @@ -1819,18 +1820,29 @@ function calibrationTests( ) } +/** Reports a law violation to the gap report's hook and builds its error. */ function failure( options: { id: string; law: OracleLaw }, verdict: Extract, history: THistory, - rerun: string, + rerun: string | undefined, ): OracleViolation { - const { id, law } = options globalThis.__oracleVerdict?.({ - property: id, + property: options.id, law: lawOf(verdict), checkpoint: verdict.checkpoint, }) + return violationError(options, verdict, history, rerun) +} + +/** A violation's error, with a rerun line when there is a command to print. */ +function violationError( + options: { id: string; law: OracleLaw }, + verdict: Extract, + history: THistory, + rerun: string | undefined, +): OracleViolation { + const { id, law } = options const error = new OracleViolation( [ `${id} violated at checkpoint "${verdict.checkpoint}"${verdict.law ? ` (law: ${verdict.law})` : ``}.`, @@ -1839,7 +1851,7 @@ function failure( `History: ${reportText(history)}`, `Authority: ${law.authority}`, `Known limits: ${law.limits}`, - `Rerun: ${rerun}`, + ...(rerun === undefined ? [] : [`Rerun: ${rerun}`]), ].join(`\n`), verdict.cause === undefined ? undefined : { cause: verdict.cause }, ) @@ -1960,7 +1972,11 @@ function generatedTests( constructionOf: Map>, counts: Map, shrinkUntil: number, - rerun: string, + // The rerun line a violation prints; a random unit's comes only once + // fast-check reports its path. + rerun: string | undefined, + // Each violation thrown, with its verdict and history. + violations: Map, ) => { let firstKind: string | undefined const keeps = (kind: string) => (firstKind ??= kind) === kind @@ -1997,7 +2013,9 @@ function generatedTests( ) } if (!keeps(`law:${lawOf(verdict)}`)) return - throw failure(options, verdict, history, rerun) + const error = failure(options, verdict, history, rerun) + violations.set(error, { verdict, history }) + throw error } } // Constructed history `index`, built from the history its campaign's seed @@ -2080,7 +2098,11 @@ function generatedTests( // random unit of its name with the fixed seed, which draws the same // stream. const replayed = { name: `random seed: ${unit}`, suite: task.suite } - const rerun = random ? replayPlaceholder : rerunOf(task) + const rerun = random ? undefined : rerunOf(task) + const violations = new Map< + unknown, + { verdict: Violation; history: THistory } + >() // A path replay shrinks no further than the counterexample it replays. // Vitest reads a timeout of 0 or less as none, which sets no budget. const timeout = timeoutOf(options) @@ -2093,7 +2115,7 @@ function generatedTests( const details = await fc.check( fc.asyncProperty( arbitrary, - predicateFor(constructionOf, counts, shrinkUntil, rerun), + predicateFor(constructionOf, counts, shrinkUntil, rerun, violations), ), run, ) @@ -2105,18 +2127,18 @@ function generatedTests( path === null ? undefined : `${oracleEnvName(`SEED`)}=${details.seed} ${oracleEnvName(`PATH`)}=${path} ${oracleEnvName(`PROPERTY`)}=${shellQuoted(id)} ${oracleEnvName(`UNIT`)}=${shellQuoted(replayed.name)} vitest run ${rerunOf(replayed)}` - // A random unit's violation names its replay as its rerun. - const cause: unknown = details.errorInstance - if (replay !== undefined && random && cause instanceof OracleViolation) - cause.message = cause.message.replace( - `Rerun: ${replayPlaceholder}`, - // A function, so the command's `$'` is not a replacement pattern. - () => `Rerun: ${replay}`, - ) + // A random unit's violation names its replay as its rerun, so it is + // built again, once, now that the path is known; without a path it + // prints no rerun line. + const thrown = violations.get(details.errorInstance) + const cause: unknown = + random && thrown + ? violationError(options, thrown.verdict, thrown.history, replay) + : details.errorInstance throw new Error( [ report, - ...(random ? [] : [`Rerun: ${rerun}`]), + ...(rerun === undefined ? [] : [`Rerun: ${rerun}`]), ...(replay === undefined ? [] : [`Replay: ${replay}`]), ].join(`\n`), { cause }, @@ -2239,10 +2261,6 @@ function generatedTests( return tests } -// A random unit's violation is thrown before fast-check knows its path, so -// its rerun line is completed once the unit fails. -const replayPlaceholder = `the replay command of this unit's failure` - // A collect-only run (ORACLE_MANIFEST set) records each registration, so the // committed manifest can be generated without running any history. function recordRegistration( diff --git a/packages/oracles/tests/oracle-property-self-oracle.test.ts b/packages/oracles/tests/oracle-property-self-oracle.test.ts index b89f22f..6eb8f26 100644 --- a/packages/oracles/tests/oracle-property-self-oracle.test.ts +++ b/packages/oracles/tests/oracle-property-self-oracle.test.ts @@ -238,7 +238,8 @@ * drawn with path `0` and the first spec's property only, and its unit is the first random unit * of that spec or a missing one. A custom prefix applies to every spec of a suite. Only one fixed * unit's `-t` rerun is probed per property, and only the determinism of a generated source is - * split into units. + * split into units. An error's raw `stack` is not observed: Vitest reprints a failure's stack + * header from its message. * A calibration's required difference is drawn only as four texts and * four patterns, including the empty ones, judged against the difference a wrong answer * reports, `item k is 3`, where k is the first item or a `driver-last` candidate's last item. A @@ -1268,6 +1269,12 @@ const unitOf = (test: string): { seed?: number; name: string } | undefined => { // that fast-check samples from the property's arbitrary with its constructed // weighting (each constructed history weighs 1, and the language weighs their // count) for `runs` draws. Drawn with fast-check itself, never the framework. +// The weighting restates how production composes its arbitrary, which the +// design of option D authorizes the model to state (design-c-d.md, law +// `units`: "the property's arbitrary (with its constructed weighting)"). It +// is that composition, not a contract promise: the header promises only that +// half of a campaign's generated histories are constructed, and a change to +// the composition must change this model with it. function unitStream( spec: SyntheticSpec, seed: number, @@ -3136,15 +3143,23 @@ const failsUnit = ( (construction !== undefined && !reaches(spec, history, construction.enters)) ) } -// A unit's log, compared with its stream: all of it when the unit passes, -// and up to its first failure when it fails, after which it shrinks. -const streamPrefix = ( +// A unit's log and its stream, as law `units` compares them: a unit that the +// model owes a pass ran exactly its stream, no history more; a failing unit +// ran its stream up to its first failure, and then its shrinks, which the +// law does not compare. +const comparedRun = ( spec: SyntheticSpec, unit: string, stream: ReadonlyArray, + logged: ReadonlyArray, ) => { const first = stream.findIndex((history) => failsUnit(spec, unit, history)) - return first < 0 ? stream : stream.slice(0, first + 1) + return first < 0 + ? { ran: logged, owedRun: stream } + : { + ran: logged.slice(0, first + 1), + owedRun: stream.slice(0, first + 1), + } } // Model law `replay-config`: the first error of the drawn replay @@ -3391,16 +3406,19 @@ function checkSuite( ) } } - // Law `units`: each unit ran the stream the model draws, up to its - // first failure. A slow spec's driver runs on after its test timed out, - // so its log names other tests. + // Law `units`: each passing unit ran exactly the stream the model draws, + // and a failing unit that stream up to its first failure. A slow spec's + // driver runs on after its test timed out, so its log names other tests. if (!spec.slow) for (const [unit, stream] of owed.streams) { - const owedRun = streamPrefix(spec, unit, stream) - const ran = run.log - .filter((entry) => entry.test === `${spec.id} > ${unit}`) - .map((entry) => entry.history) - .slice(0, owedRun.length) + const { ran, owedRun } = comparedRun( + spec, + unit, + stream, + run.log + .filter((entry) => entry.test === `${spec.id} > ${unit}`) + .map((entry) => entry.history), + ) if (JSON.stringify(ran) !== JSON.stringify(owedRun)) return violation( `run`, @@ -3490,12 +3508,12 @@ function checkSuite( ) if (!generated || spec.slow) continue for (const unit of unitNames(spec).map(randomUnit)) { - const owedRun = streamPrefix( + const { ran: logged, owedRun } = comparedRun( spec, unit, unitStream(spec, seeds[0]!, unitOf(unit)!.name), + ran[unit] ?? [], ) - const logged = (ran[unit] ?? []).slice(0, owedRun.length) if (JSON.stringify(logged) !== JSON.stringify(owedRun)) return violation( `seedless`, From 54e1723bb696060ed195ab7b35d76d280427250c Mon Sep 17 00:00:00 2001 From: Kyle Mathews Date: Wed, 11 Nov 2026 14:45:01 -0700 Subject: [PATCH 3/4] feat(eslint-plugin-oracles): name _UNIT as a replay variable; state the replay migration oracle/no-disabled reads `${envPrefix}_UNIT` as a shared replay variable and reports a process.env read of any other `*_UNIT` variable as a private replay variable. RED: the two new invalid cases (`ORACLE_UNIT` under another prefix and a destructured `UTILS_ORACLE_UNIT`) were not reported; GREEN: the plugin suite passes. The changeset marks the unit change as breaking for consumers and states how to rebase a recorded path onto its unit. Co-authored-by: Isaac --- .changeset/shardable-units.md | 12 ++++++++++++ .../eslint-plugin-oracles/src/registration.js | 1 + .../src/rules/no-disabled.js | 16 +++++++++++----- .../tests/no-disabled.test.js | 1 + .../tests/package-specifiers.test.js | 18 ++++++++++++++++++ 5 files changed, 43 insertions(+), 5 deletions(-) diff --git a/.changeset/shardable-units.md b/.changeset/shardable-units.md index 1b037ab..f3c8eb5 100644 --- a/.changeset/shardable-units.md +++ b/.changeset/shardable-units.md @@ -1,11 +1,23 @@ --- '@tanstack/oracles': patch +'@tanstack/eslint-plugin-oracles': patch --- +**Breaking for consumers.** Test names of generated sources change, and a path replay of a generated source now needs `${prefix}_UNIT`. A command or script that sets only the seed, the path, and the property now fails when the property registers. + A generated source now registers each part of a campaign as its own test, so a runner can shard a long campaign across jobs. For each fixed seed N, `oracleProperty` registers `fixed seed N: ` for each constructed history and `fixed seed N: generated` for the generated histories. The random campaign registers `random seed: ` and `random seed: generated` in the same way. The determinism test becomes one test per history: `determinism: fixed history: `, `determinism: constructed history: `, and `determinism: generated 0` to `2`. The units of a seed run exactly the histories that the campaign ran. Each unit decides its own first failure, shrinks within its own timeout, and prints its own reach line, ` reach {...}`. A campaign's reach is the sum of its units' lines. A unit that fails or times out prints no reach line. An enumerated source keeps its one `determinism` test. Test names change. A `-t "fixed seed"` filter still selects the fixed-seed units, and `-t "random seed"` the random units. A filter that names the old `determinism` test of a generated source now selects all its determinism units. The random units of a property share one seed, which the first random unit that runs selects and logs in the one `ORACLE_SEED` line. A path replay now names its unit in the new `${prefix}_UNIT` variable, such as `ORACLE_UNIT='random seed: generated'`. `UNIT` requires `PROPERTY`. During a path replay, only the random unit of that name runs. A path replay of a generated source without `UNIT` fails when the property registers, with "`ORACLE_PATH` of a generated source requires `ORACLE_UNIT`". A `UNIT` that names no random unit of the replayed property also fails its registration. A failing unit prints its replay command, with the seed, the path, the property, the unit, and its `-t` pattern, under the configured prefix. A failing fixed-seed unit also prints `Rerun: -t '...'`, which reruns it. The retired-variable message names `${prefix}_UNIT`. +To migrate a recorded path, rebase it onto its unit. In the old campaign, the first index of a path selected the history: an index k below n, the number of constructed histories, was constructed history k, and an index k of n or more was generated history k − n. With `PATH=k:`: + +- for k < n, set `${prefix}_UNIT='random seed: '` and `${prefix}_PATH=0:`; +- for k ≥ n, set `${prefix}_UNIT='random seed: generated'` and `${prefix}_PATH=(k − n):`. + +A path recorded from a fixed-seed campaign replays the same way, with that fixed seed as `${prefix}_SEED`. A new failure prints its replay command, so only paths recorded before this change need rebasing. + A generated source fails to load when two of its tests would share a name: a constructed history named `generated`, two constructed histories of one name, or two fixed histories of one name. + +In `@tanstack/eslint-plugin-oracles`, `oracle/no-disabled` reads `${envPrefix}_UNIT` as a shared replay variable, and reports a `process.env` read of any other variable that ends in `_UNIT` as a private replay variable, as it does for `_SEED`, `_PATH`, `_PROPERTY`, and `_RUNS`. diff --git a/packages/eslint-plugin-oracles/src/registration.js b/packages/eslint-plugin-oracles/src/registration.js index d5ff31b..3add6ad 100644 --- a/packages/eslint-plugin-oracles/src/registration.js +++ b/packages/eslint-plugin-oracles/src/registration.js @@ -455,6 +455,7 @@ export function oracleSettings(context) { seed: `${envPrefix}_SEED`, path: `${envPrefix}_PATH`, property: `${envPrefix}_PROPERTY`, + unit: `${envPrefix}_UNIT`, runsMultiplier: `${envPrefix}_RUNS_MULTIPLIER`, }, implementationModules: moduleList(configured, `implementationModules`), diff --git a/packages/eslint-plugin-oracles/src/rules/no-disabled.js b/packages/eslint-plugin-oracles/src/rules/no-disabled.js index 4f49d19..1873f3a 100644 --- a/packages/eslint-plugin-oracles/src/rules/no-disabled.js +++ b/packages/eslint-plugin-oracles/src/rules/no-disabled.js @@ -41,8 +41,9 @@ * - A literal run count above 1 that has no fixed history. It does not scale with * the runs-multiplier variable (`${envPrefix}_RUNS_MULTIPLIER`), so `oracleRuns` must wrap it. * - A private replay variable: a `process.env` read whose name ends in - * `_SEED`, `_PATH`, `_PROPERTY`, or `_RUNS`, other than the framework's - * shared `${envPrefix}_SEED`, `${envPrefix}_PATH`, and `${envPrefix}_PROPERTY`. The replay manifest, the guarded replay + * `_SEED`, `_PATH`, `_PROPERTY`, `_UNIT`, or `_RUNS`, other than the framework's + * shared `${envPrefix}_SEED`, `${envPrefix}_PATH`, `${envPrefix}_PROPERTY`, and + * `${envPrefix}_UNIT`, the random unit a path replay runs. The replay manifest, the guarded replay * runner, and the retired-variable check see only the shared variables. * * The rule has no inline exception. A known counterexample is kept failing with @@ -76,7 +77,7 @@ const replayConditions = new Set([`oracleReplayRequested`, `oracleReplaySkips`]) // A replay-selection module (`implementationModules`) may read the replay // variables and select a replay from configuration. // Any variable whose name ends in one of these suffixes is a replay variable. -const replayVariableName = /_(PATH|PROPERTY|RUNS|SEED)$/ +const replayVariableName = /_(PATH|PROPERTY|RUNS|SEED|UNIT)$/ const runHelpers = new Set([ `oraclePropertyOptions`, `oracleRandomParameters`, @@ -415,7 +416,12 @@ function environmentKey(node) { } function isPrivateReplayVariable(name, envNames) { - const shared = [envNames.seed, envNames.path, envNames.property] + const shared = [ + envNames.seed, + envNames.path, + envNames.property, + envNames.unit, + ] return replayVariableName.test(name) && !shared.includes(name) } @@ -729,7 +735,7 @@ export default { aliasTest: `\`{{name}}\` is passed around as a value, so the rule cannot see what it registers or switches off. Call it directly, or select a replay with \`oracleReplayTest({{name}}, property)\` from \`@tanstack/oracles\`.`, guarded: `This test registers only under a condition, so it can stop running in ordinary runs. Register it unconditionally. A replay selection uses \`oracleReplayRequested()\` or \`oracleReplaySkips(property)\` from \`@tanstack/oracles\`, or \`oracleReplayTest(test, property)\`.`, singleRun: `A generated property with one run that has no fixed history checks one random history. Pass a base run count to oracleRuns or oraclePropertyOptions, which also selects a replay. A witness passes a recorded \`path\` or a seed that is a number literal or a constant.`, - replayVariable: `\`{{name}}\` selects a replay or a run count outside the shared variables, so the replay manifest, the guarded replay runner, and the retired-variable check cannot see it. Take the options from \`oraclePropertyOptions\` or \`oracleRandomParameters\` in \`@tanstack/oracles\`, which read {{seed}}, {{path}}, and {{property}}, and scale run counts with \`oracleRuns\`.`, + replayVariable: `\`{{name}}\` selects a replay or a run count outside the shared variables, so the replay manifest, the guarded replay runner, and the retired-variable check cannot see it. Take the options from \`oraclePropertyOptions\` or \`oracleRandomParameters\` in \`@tanstack/oracles\`, which read {{seed}}, {{path}}, {{property}}, and {{unit}}, and scale run counts with \`oracleRuns\`.`, literalRuns: `A literal run count does not scale with {{runsMultiplier}}. Wrap it in oracleRuns, or pass it to oraclePropertyOptions.`, }, }, diff --git a/packages/eslint-plugin-oracles/tests/no-disabled.test.js b/packages/eslint-plugin-oracles/tests/no-disabled.test.js index c4b8d05..e50dd8a 100644 --- a/packages/eslint-plugin-oracles/tests/no-disabled.test.js +++ b/packages/eslint-plugin-oracles/tests/no-disabled.test.js @@ -15,6 +15,7 @@ const dbEnvNames = { seed: 'TANSTACK_DB_ORACLE_SEED', path: 'TANSTACK_DB_ORACLE_PATH', property: 'TANSTACK_DB_ORACLE_PROPERTY', + unit: 'TANSTACK_DB_ORACLE_UNIT', runsMultiplier: 'TANSTACK_DB_ORACLE_RUNS_MULTIPLIER', } // The fixtures name the TanStack DB project's files and variables, so the diff --git a/packages/eslint-plugin-oracles/tests/package-specifiers.test.js b/packages/eslint-plugin-oracles/tests/package-specifiers.test.js index cce88b9..07683c0 100644 --- a/packages/eslint-plugin-oracles/tests/package-specifiers.test.js +++ b/packages/eslint-plugin-oracles/tests/package-specifiers.test.js @@ -66,6 +66,7 @@ noDisabledTester.run(`oracle/no-disabled`, noDisabled, { seed: `ORACLE_SEED`, path: `ORACLE_PATH`, property: `ORACLE_PROPERTY`, + unit: `ORACLE_UNIT`, runsMultiplier: `ORACLE_RUNS_MULTIPLIER`, }, }, @@ -100,6 +101,11 @@ projectTester.run(`oracle/no-disabled with a project's settings`, noDisabled, { code: `const seed = process.env.TANSTACK_DB_ORACLE_SEED`, filename: `/repo/tests/checks-oracle.test.ts`, }, + // The unit a path replay runs is a shared replay variable. + { + code: `const unit = process.env.TANSTACK_DB_ORACLE_UNIT`, + filename: `/repo/tests/checks-oracle.test.ts`, + }, // The configured replay module, named by its path, may read a private // replay variable. { @@ -119,5 +125,17 @@ projectTester.run(`oracle/no-disabled with a project's settings`, noDisabled, { filename: `/repo/tests/checks-oracle.test.ts`, errors: [{ messageId: `replayVariable` }], }, + // A unit under another prefix selects a replay the shared variables do + // not see. + { + code: `const unit = process.env.ORACLE_UNIT`, + filename: `/repo/tests/checks-oracle.test.ts`, + errors: [{ messageId: `replayVariable` }], + }, + { + code: `const { UTILS_ORACLE_UNIT } = process.env`, + filename: `/repo/tests/checks-oracle.test.ts`, + errors: [{ messageId: `replayVariable` }], + }, ], }) From 6f095b13153bc3bbaf0170c39cc54269958c1b22 Mon Sep 17 00:00:00 2001 From: Kyle Mathews Date: Wed, 11 Nov 2026 16:44:40 -0700 Subject: [PATCH 4/4] ci(oracles): partition the e2e gap oracle's 96 units into 5 shards The property now registers its campaign parts, calibrations, and determinism histories as units, so the e2e shards name the 96 units. The shards are a longest-first packing of the per-unit costs of one full run of every unit on this branch (2,610 s under load, 2.36 times an idle run), so each shard is about 522 s here, about 221 s idle, and 5.5 to 8.5 minutes in CI by the measured 1.5 to 2.31 factor. The partition check passes against `vitest list`, and each shard's `-t` pattern selects exactly its units. CI keeps its one fixed-seed job: the shards include the random units, whose tail can pass 10 minutes in CI until option M bounds it. Co-authored-by: Isaac --- packages/oracles/scripts/e2e-shards.mjs | 142 ++++++++++++++++++++---- 1 file changed, 120 insertions(+), 22 deletions(-) diff --git a/packages/oracles/scripts/e2e-shards.mjs b/packages/oracles/scripts/e2e-shards.mjs index 197a982..1209d49 100644 --- a/packages/oracles/scripts/e2e-shards.mjs +++ b/packages/oracles/scripts/e2e-shards.mjs @@ -21,35 +21,133 @@ import { fileURLToPath } from 'node:url' const suite = `oracle-gaps.report` -// The shards balance the costs measured in one full local run on main -// (84cd34a, 2026-11-11, an idle 18-core Mac, one Vitest worker), in local -// seconds: determinism about 345 (all 30 histories, twice each), the random -// seed 160 to 600 by its seed, the fixed seed 157, the refused-run -// calibration 102, the two daemon calibrations 56 and 53, and each other -// calibration 38 to 46. CI took 2.31 times as long. The property registers -// each campaign, each calibration, and the determinism test as one test, so -// a shard cannot be smaller than its largest test, and the determinism test -// alone sets the slowest shard. CI keeps its one fixed-seed job until the -// property registers its parts as units that a shard can split. +// The shards balance the costs measured in one full run of every unit on +// feat/unit-replay (2026-11-11, an 18-core Mac under other agents' load, one +// Vitest worker): 2,610 s in all, 370 s for the fixed-seed units, 605 s for +// the random units (their cost varies with the drawn seed), 917 s for the +// calibrations, and 718 s for the determinism units. The fixed-seed units +// took 2.36 times the 157 s of an idle run (84cd34a), and CI took 2.31 times +// an idle run, so a shard of about 522 s here is about 221 s idle and 5.5 to +// 8.5 minutes in CI, before job setup. The property registers each campaign +// part, each calibration, and each determinism history as its own test +// (units), so a shard can hold any of them; the slowest unit, the +// determinism of the edit sequence, is 236 s here. The shards are a +// longest-first packing of those costs, listed by kind. A random unit's +// cost follows its seed, so a shard's time varies from run to run. CI keeps +// its one fixed-seed job until the random units' tail is bounded (option M +// of the e2e speed plan): a random unit that draws a long edit sequence over +// the witness module can pass 10 minutes in CI. export const shards = { - 'e2e-1': [`determinism`], - 'e2e-2': [`random seed`], - 'e2e-3': [ - `fixed seed 20261105`, + // 522 s in the measured run, about 221 s idle. + 'e2e-1': [ + `fixed seed 20261105: a .cjs config that calls require`, + `fixed seed 20261105: a declaration fault: missingSource`, + `fixed seed 20261105: a declaration fault: noTypescript`, + `fixed seed 20261105: a declaration fault: outsideSource`, + `fixed seed 20261105: a declaration fault: projects`, + `random seed: a config that --config names`, + `random seed: a declaration fault: badEntry`, + `random seed: a failing owner under a config that --config names`, + `random seed: a load failure beside a hang`, + `calibration: a key drops its statement text`, + `calibration: a mutant is dropped from the enumeration`, + `calibration: an edit moves a key`, + `determinism: constructed history: a .ts config in a package with no module type that calls require`, + `determinism: constructed history: a config that --config names`, + `determinism: constructed history: a declaration fault: badEntry`, + `determinism: constructed history: a declaration fault: missingSource`, + `determinism: constructed history: a declaration fault: projects`, + `determinism: constructed history: a package with no config`, + `determinism: constructed history: an edit sequence through the daemon`, + ], + // 522 s in the measured run, about 221 s idle. + 'e2e-2': [ + `fixed seed 20261105: a declaration fault: setupThrows`, + `fixed seed 20261105: a package with no config`, + `fixed seed 20261105: an ambiguous authored mutant`, + `fixed seed 20261105: generated`, + `random seed: a config fault in a run that owns nothing`, + `random seed: a declaration fault: apiLessTypescript`, + `calibration: a crash is reported as a kill`, + `calibration: a daemon is left after --stop-daemon`, `calibration: a refused run is reported as complete`, + `determinism: constructed history: a .cjs config that calls require`, + `determinism: constructed history: a declaration fault: configNoDefault`, + `determinism: constructed history: a declaration fault: outsideSource`, + `determinism: constructed history: a declaration fault: setupThrows`, + `determinism: constructed history: a load failure beside a hang`, + `determinism: constructed history: a stale authored mutant and a reformat`, + `determinism: constructed history: an awaiting config in a package with no module type`, + `determinism: constructed history: ordinary tests left out by default`, + `determinism: generated 0`, + `determinism: generated 1`, ], + // 522 s in the measured run, about 221 s idle. + 'e2e-3': [ + `fixed seed 20261105: a config fault in a run that owns nothing`, + `fixed seed 20261105: a declaration fault: brokenOwner`, + `fixed seed 20261105: a declaration fault: configThrows`, + `fixed seed 20261105: a run with eleven contexts`, + `fixed seed 20261105: a stale authored mutant and a reformat`, + `fixed seed 20261105: an awaiting config in a package with no module type`, + `fixed seed 20261105: every outcome class`, + `random seed: a .ts config in a package with no module type that calls require`, + `random seed: a declaration fault: configThrows`, + `random seed: a declaration fault: noTypescript`, + `random seed: a declaration fault: outsideSource`, + `random seed: a stale authored mutant and a reformat`, + `random seed: an edit sequence through the daemon`, + `random seed: every outcome class`, + `random seed: generated`, + `random seed: two authored mutants`, + `determinism: constructed history: a declaration fault: brokenOwner`, + `determinism: constructed history: a declaration fault: configThrows`, + `determinism: constructed history: a declaration fault: nonLiteral`, + ], + // 522 s in the measured run, about 221 s idle. 'e2e-4': [ + `fixed seed 20261105: a .ts config in a package with no module type that calls require`, + `fixed seed 20261105: a config that --config names`, + `fixed seed 20261105: a declaration fault: apiLessTypescript`, + `fixed seed 20261105: a declaration fault: badEntry`, + `fixed seed 20261105: a declaration fault: brokenVitest`, + `fixed seed 20261105: a declaration fault: configNoDefault`, + `fixed seed 20261105: a declaration fault: nonLiteral`, + `fixed seed 20261105: a failing owner under a config that --config names`, + `fixed seed 20261105: a load failure beside a hang`, + `random seed: a .cjs config that calls require`, + `random seed: a declaration fault: configNoDefault`, + `random seed: an awaiting config in a package with no module type`, + `calibration: production code is reported as probe code`, `calibration: the daemon reports another outcome than the cold run`, - `calibration: a daemon is left after --stop-daemon`, - `calibration: a mutant is dropped from the enumeration`, - `calibration: an owned mutant is reported as unowned`, + `calibration: the summary omits a gap`, + `determinism: constructed history: a run with eleven contexts`, + `determinism: constructed history: an ambiguous authored mutant`, + `determinism: constructed history: every outcome class`, + `determinism: constructed history: two authored mutants`, ], + // 522 s in the measured run, about 221 s idle. 'e2e-5': [ - `calibration: a crash is reported as a kill`, - `calibration: a key drops its statement text`, - `calibration: the summary omits a gap`, - `calibration: an edit moves a key`, - `calibration: production code is reported as probe code`, + `fixed seed 20261105: an edit sequence through the daemon`, + `fixed seed 20261105: ordinary tests left out by default`, + `fixed seed 20261105: two authored mutants`, + `random seed: a declaration fault: brokenOwner`, + `random seed: a declaration fault: brokenVitest`, + `random seed: a declaration fault: missingSource`, + `random seed: a declaration fault: nonLiteral`, + `random seed: a declaration fault: projects`, + `random seed: a declaration fault: setupThrows`, + `random seed: a package with no config`, + `random seed: a run with eleven contexts`, + `random seed: an ambiguous authored mutant`, + `random seed: ordinary tests left out by default`, + `calibration: an owned mutant is reported as unowned`, + `determinism: constructed history: a config fault in a run that owns nothing`, + `determinism: constructed history: a declaration fault: apiLessTypescript`, + `determinism: constructed history: a declaration fault: brokenVitest`, + `determinism: constructed history: a declaration fault: noTypescript`, + `determinism: constructed history: a failing owner under a config that --config names`, + `determinism: generated 2`, ], }