From 8ab904b6ea50affb94ac2e7f1370deead513c2f0 Mon Sep 17 00:00:00 2001 From: Test Date: Wed, 28 Oct 2026 12:20:15 -0600 Subject: [PATCH 01/12] test(db): reach every declared source-health state in every run The source-health history property chose its reach prefixes by chance. In about 0.3% of 60-run campaigns it never chose the one prefix that reaches `markReady on a ready run` and `reload's insert of a kept row throws`, so the reach check failed at random in CI (#2287). The history, on-demand, and lazy-demand properties now run each reach prefix, and each driver option a declared state needs, as fast-check examples before the random histories. The examples alone reach every declared state of the three properties. createOracleReach skipped the check for a seed without a path. A seed alone reseeds the full campaign, so the check now runs then too. That is why the CI seed passed locally. Closes #2287. Co-authored-by: Isaac --- docs/contributing/oracle-coverage.md | 15 +++ packages/db/tests/oracle-reach.ts | 9 +- .../db/tests/source-health-oracle.test.ts | 109 +++++++++++++++--- 3 files changed, 113 insertions(+), 20 deletions(-) diff --git a/docs/contributing/oracle-coverage.md b/docs/contributing/oracle-coverage.md index 89c4e5209f..4e33385585 100644 --- a/docs/contributing/oracle-coverage.md +++ b/docs/contributing/oracle-coverage.md @@ -3403,6 +3403,21 @@ does not generate a hook input without `cwd`, a worktree outside the launch checkout, or a worktree branch that has no copy of the script. In that last case the launch checkout's rule lints the worktree. +`packages/db/tests/oracle-reach.ts` (`createOracleReach`, ORC-015) checks +declared reach in an ordinary run and in a run with only +`TANSTACK_DB_ORACLE_SEED`, which reseeds the whole campaign at its full budget. +Only a path replay, which runs one recorded history, skips the check. A declared +state that only random histories reach can still miss by chance at the normal +budget. In `packages/db/tests/source-health-oracle.test.ts`, the +`source-health.history`, `source-health.on-demand`, and +`source-health.lazy-demand` properties run each reach prefix, and each driver +option that a declared state needs, as fast-check `examples` before their random +histories. The examples alone reach every declared state of those three +properties, so their reach check does not depend on the seed (#2287). Other +properties have not been measured for this. Owner: none (oracle machinery). +Needed witness: per property, the declared states that its fixed examples do +not reach, and how often a normal-budget run misses each one. + `packages/db/tests/oracle-replay.test.ts` checks every replay manifest owner: from its cwd, the command's files exist, its target is the owner, and a Vitest config applies. diff --git a/packages/db/tests/oracle-reach.ts b/packages/db/tests/oracle-reach.ts index b6ec08295a..b75ea8dff6 100644 --- a/packages/db/tests/oracle-reach.ts +++ b/packages/db/tests/oracle-reach.ts @@ -14,8 +14,9 @@ import { readOracleRunConfig } from './oracle-config.js' * histories entered. A history counts once per state, however often it * enters it. * - * A replay of one seed or path checks one history, not reach, so the check - * does nothing then. + * A path replay checks one recorded history, not reach, so the check does + * nothing then. A seed alone reseeds the whole campaign, which runs its full + * budget, so its reach is checked like an ordinary run's. */ export function createOracleReach( property: string, @@ -32,8 +33,8 @@ export function createOracleReach( const replaying = replayOverride ?? (() => { - const { replaySeed, replayPath } = readOracleRunConfig() - return replaySeed !== undefined || replayPath !== undefined + const { replayPath } = readOracleRunConfig() + return replayPath !== undefined })() return { /** Starts one generated history. */ diff --git a/packages/db/tests/source-health-oracle.test.ts b/packages/db/tests/source-health-oracle.test.ts index 428da270ef..d333b5426f 100644 --- a/packages/db/tests/source-health-oracle.test.ts +++ b/packages/db/tests/source-health-oracle.test.ts @@ -3372,7 +3372,16 @@ describe(`source failure and health oracle`, () => { ]), fc.boolean(), ], - oraclePropertyOptions(60, `source-health.history`), + { + ...oraclePropertyOptions(60, `source-health.history`), + // Each prefix runs once in every run, before the random histories, so + // the states only a prefix enters cannot miss by chance (#2287). The + // `join` shape queries both sources that the prefixes drive. + examples: reachPrefixes.map((prefix): [[Shape, Array], boolean] => [ + [prefixShapes.get(prefix) ?? `join`, [...prefix]], + true, + ]), + }, )( `generated histories refine the model`, ([shape, steps], directSubscribers) => { @@ -5244,7 +5253,13 @@ describe(`on-demand demand grammar`, () => { ]), fc.boolean(), ], - oraclePropertyOptions(60, `source-health.on-demand`), + { + ...oraclePropertyOptions(60, `source-health.on-demand`), + // Each prefix runs once in every run, before the random histories. + examples: demandReachPrefixes.map( + (prefix): [Array, boolean] => [[...prefix], true], + ), + }, )( `generated demand histories refine the model`, (steps, directSubscriber) => { @@ -6953,6 +6968,16 @@ describe(`lazy join demand grammar`, () => { afterAll(() => { if (lazyHistoriesRan) lazyReach.assertReached() }) + // A reload whose replay fails. A row the provider deletes after it stays. + const failedReload = { + steps: [{ kind: `settle-ok` }, { kind: `reload` }, { kind: `settle-fail` }], + } as const satisfies { steps: ReadonlyArray } + const reloadNotices: ReadonlyArray = [ + `source-health`, + `query-health`, + `loading-subset`, + `subscription-status`, + ] // Prefixes that enter a declared reach state that random steps alone rarely // reach at the base run count, with the driver options the state needs. // Random steps follow each one. @@ -6988,13 +7013,7 @@ describe(`lazy join demand grammar`, () => { { kind: `reload` }, ], }, - { - steps: [ - { kind: `settle-ok` }, - { kind: `reload` }, - { kind: `settle-fail` }, - ], - }, + failedReload, { steps: [{ kind: `truncate` }, { kind: `truncate` }] }, { steps: [{ kind: `settle-ok` }, { kind: `fail` }, { kind: `truncate` }], @@ -7060,6 +7079,43 @@ describe(`lazy join demand grammar`, () => { holdChildReady: false, }, ] + type LazyExample = [ + { + prefix: (typeof lazyReachPrefixes)[number] | null + rest: Array + }, + boolean, + boolean, + boolean, + boolean, + boolean, + `plain` | `reload-in-first-load` | undefined, + { at: ReloadNotice; dependents: boolean } | undefined, + ] + const lazyExample = ( + prefix: (typeof lazyReachPrefixes)[number] | null, + rest: Array, + { + withEffect = false, + windowed = false, + deferredStart, + ending, + }: { + withEffect?: boolean + windowed?: boolean + deferredStart?: `reload-in-first-load` + ending?: { at: ReloadNotice; dependents: boolean } + } = {}, + ): LazyExample => [ + { prefix, rest }, + false, + false, + true, + withEffect, + windowed, + deferredStart, + ending, + ] fcTest.prop( [ fc @@ -7080,18 +7136,39 @@ describe(`lazy join demand grammar`, () => { ), fc.option( fc.record({ - at: fc.constantFrom( - `source-health`, - `query-health`, - `loading-subset`, - `subscription-status`, - ), + at: fc.constantFrom(...reloadNotices), dependents: fc.boolean(), }), { freq: 2, nil: undefined }, ), ], - oraclePropertyOptions(100, `source-health.lazy-demand`), + { + ...oraclePropertyOptions(100, `source-health.lazy-demand`), + // Each prefix runs once in every run, before the random histories, + // and so does each driver option that a declared state needs. Each + // example has a direct subscriber and no other option it does not name. + examples: [ + ...lazyReachPrefixes.map((prefix) => lazyExample(prefix, [])), + // The provider deletes a row after a reload's run ended. + lazyExample(failedReload, [{ kind: `remote-delete`, key: 1 }]), + lazyExample(null, [{ kind: `settle-ok` }], { withEffect: true }), + lazyExample(null, [{ kind: `settle-ok` }], { + deferredStart: `reload-in-first-load`, + }), + // A cleanup at each notice of a reload. The loadingSubset notice + // needs a windowed query whose first load is still open. + ...reloadNotices.map((at) => + at === `loading-subset` + ? lazyExample(null, [], { + windowed: true, + ending: { at, dependents: false }, + }) + : lazyExample(null, [{ kind: `settle-ok` }], { + ending: { at, dependents: false }, + }), + ), + ], + }, )( `generated lazy demand histories refine the model`, ( From 6887fc9fe8dc10c13bf5beff56389c814097393a Mon Sep 17 00:00:00 2001 From: Test Date: Wed, 28 Oct 2026 12:42:15 -0600 Subject: [PATCH 02/12] test(db): make fixed reach examples a shared seam with its own oracle Review of #2287's fix found that the examples displaced random histories (60 became 51), that each property wired them by hand, and that the seed-only reach rule had no test. oraclePropertyOptions now takes `examples` and runs them on top of the base budget, so no random history is lost, and a path replay still runs one history. createOracleReach takes `fixedHistories` and fails for a declared state that the fixed examples did not enter, so the examples-only reach of the three source-health properties is checked in every run, not measured once. The lazy loadingSubset example needs only an open first load, not a window. declared-reach-oracle.property.test.ts (`oracle.declared-reach`) models when the reach check runs and what fixed histories prove, and compares createOracleReach and oracleRandomParameters with it. It fails on the parent's seed-only skip and on the previous commit's missing fixedHistories, and rejects examples that displace random runs and an off-by-one fixed count. Co-authored-by: Isaac --- docs/contributing/oracle-coverage.md | 33 ++- .../declared-reach-oracle.property.test.ts | 265 ++++++++++++++++++ packages/db/tests/oracle-config.ts | 44 ++- packages/db/tests/oracle-reach.ts | 48 +++- packages/db/tests/oracle-replay-manifest.ts | 5 + .../db/tests/source-health-oracle.test.ts | 133 ++++----- 6 files changed, 431 insertions(+), 97 deletions(-) create mode 100644 packages/db/tests/declared-reach-oracle.property.test.ts diff --git a/docs/contributing/oracle-coverage.md b/docs/contributing/oracle-coverage.md index 4e33385585..47f5a0cf09 100644 --- a/docs/contributing/oracle-coverage.md +++ b/docs/contributing/oracle-coverage.md @@ -3403,20 +3403,27 @@ does not generate a hook input without `cwd`, a worktree outside the launch checkout, or a worktree branch that has no copy of the script. In that last case the launch checkout's rule lints the worktree. -`packages/db/tests/oracle-reach.ts` (`createOracleReach`, ORC-015) checks -declared reach in an ordinary run and in a run with only -`TANSTACK_DB_ORACLE_SEED`, which reseeds the whole campaign at its full budget. -Only a path replay, which runs one recorded history, skips the check. A declared -state that only random histories reach can still miss by chance at the normal -budget. In `packages/db/tests/source-health-oracle.test.ts`, the -`source-health.history`, `source-health.on-demand`, and +`packages/db/tests/declared-reach-oracle.property.test.ts` +(`oracle.declared-reach`) owns when `createOracleReach` (ORC-015) checks reach, +and what fixed examples prove. By default the check runs in an ordinary run and +in a run with only `TANSTACK_DB_ORACLE_SEED`, which reseeds the whole campaign +at its full budget. Only a path replay, which runs one recorded history, skips +it. A property can run fixed examples first in every run, through +`oraclePropertyOptions(…, { examples })`. The examples come on top of the base +run budget, so they never displace a random history. With `fixedHistories`, +the check also fails for each declared state that the examples did not enter. +The `source-health.history`, `source-health.on-demand`, and `source-health.lazy-demand` properties run each reach prefix, and each driver -option that a declared state needs, as fast-check `examples` before their random -histories. The examples alone reach every declared state of those three -properties, so their reach check does not depend on the seed (#2287). Other -properties have not been measured for this. Owner: none (oracle machinery). -Needed witness: per property, the declared states that its fixed examples do -not reach, and how often a normal-budget run misses each one. +option that a declared state needs, as examples, so their reach does not depend +on the seed (#2287). The oracle generates ledgers over two to four states, up to +six histories, minimums up to three, and up to four fixed histories, under the +three run kinds. It does not cover `runOracleCampaign` in +`packages/db/tests/oracle-campaign.ts`, which passes its own `replaying` rule: +a seed-only run of its campaign prefix still skips the check. A declared state +of another property that only random histories reach can still miss by chance +at the normal budget. Those properties have not been measured. Needed witness: +per property, the declared states that no fixed example enters, and how often a +normal-budget run misses each one. `packages/db/tests/oracle-replay.test.ts` checks every replay manifest owner: from its cwd, the command's files exist, its target is the owner, and a Vitest diff --git a/packages/db/tests/declared-reach-oracle.property.test.ts b/packages/db/tests/declared-reach-oracle.property.test.ts new file mode 100644 index 0000000000..8e72cb5732 --- /dev/null +++ b/packages/db/tests/declared-reach-oracle.property.test.ts @@ -0,0 +1,265 @@ +/** + * Declared reach (ORC-015) cannot miss by chance where a property fixes it. + * + * A generated property declares the states its laws depend on, and + * `createOracleReach` fails a run in which too few histories entered one. + * Two rules decide when that check runs and what it proves (#2287): + * + * - The check runs in an ordinary run and in a run with only + * `TANSTACK_DB_ORACLE_SEED`: a seed alone reseeds the whole campaign at its + * full budget. Only a path replay, which runs one recorded history, skips + * it. + * - A property can run fixed examples first in every run. With + * `fixedHistories: n`, the check also fails for each declared state that + * the first n histories, the examples, did not enter. Such a state's reach + * would depend on the seed. The examples come on top of the base run + * budget, so they never displace a random history, and a path replay still + * runs one history. + * + * The model below states both rules over a generated ledger: a run kind, a + * minimum, a number of fixed histories, and the states each history enters. + * The driver runs `createOracleReach` and `oracleRandomParameters` under that + * run kind's environment, and the check compares counts, the failure, and + * the states the failure names with the model. + */ +import { fc, test as fcTest } from '@fast-check/vitest' +import { afterAll, expect } from 'vitest' +import { createOracleReach } from './oracle-reach.js' +import { + oraclePropertyOptions, + oracleRandomParameters, +} from './oracle-config.js' +import { declareOracle } from './oracle-declaration.js' + +const property = `oracle.declared-reach` + +type RunKind = `ordinary` | `seed` | `path` +type Ledger = { + run: RunKind + states: ReadonlyArray + minimum: number + fixedHistories: number + // The indices of the states each history enters, with repeats. + histories: ReadonlyArray> +} +type Verdict = { + counts: ReadonlyMap + belowMinimum: ReadonlyMap + unfixed: ReadonlyArray +} + +// The grammar: two to four states, and up to six histories over them. +const ledgerArbitrary: fc.Arbitrary = fc + .integer({ min: 2, max: 4 }) + .chain((stateCount) => + fc.record({ + run: fc.constantFrom(`ordinary`, `seed`, `path`), + states: fc.constant( + Array.from({ length: stateCount }, (_, index) => `state ${index}`), + ), + minimum: fc.integer({ min: 1, max: 3 }), + fixedHistories: fc.integer({ min: 0, max: 4 }), + histories: fc.array( + fc.array(fc.integer({ min: 0, max: stateCount - 1 }), { + maxLength: 4, + }), + { maxLength: 6 }, + ), + }), + ) + +// The model. A history counts once per state it enters. A path replay checks +// nothing. Otherwise a state fails below the minimum, and, when fixed +// histories are declared, a state the first ones did not enter fails too. +function expectedVerdict(ledger: Ledger): Verdict | `skipped` { + if (ledger.run === `path`) return `skipped` + const entered = ledger.histories.map( + (history) => new Set(history.map((index) => ledger.states[index]!)), + ) + const counts = new Map( + ledger.states.map((state) => [ + state, + entered.filter((history) => history.has(state)).length, + ]), + ) + const fixed = entered.slice(0, ledger.fixedHistories) + return { + counts, + belowMinimum: new Map( + [...counts].filter(([, count]) => count < ledger.minimum), + ), + unfixed: + ledger.fixedHistories === 0 + ? [] + : ledger.states.filter((state) => + fixed.every((history) => !history.has(state)), + ), + } +} + +// The environment each run kind sets. +function runEnvironment(run: RunKind): Record { + if (run === `ordinary`) return {} + if (run === `seed`) return { TANSTACK_DB_ORACLE_SEED: `1` } + return { + TANSTACK_DB_ORACLE_SEED: `1`, + TANSTACK_DB_ORACLE_PATH: `0`, + TANSTACK_DB_ORACLE_PROPERTY: property, + } +} + +function withEnvironment(variables: Record, run: () => T) { + const names = [ + `TANSTACK_DB_ORACLE_SEED`, + `TANSTACK_DB_ORACLE_PATH`, + `TANSTACK_DB_ORACLE_PROPERTY`, + ] + const saved = names.map((name) => [name, process.env[name]] as const) + for (const name of names) delete process.env[name] + Object.assign(process.env, variables) + try { + return run() + } finally { + for (const [name, value] of saved) { + if (value === undefined) delete process.env[name] + else process.env[name] = value + } + } +} + +// The driver: one ledger through createOracleReach. +function observeLedger(ledger: Ledger) { + const reach = withEnvironment(runEnvironment(ledger.run), () => + createOracleReach(`ledger`, ledger.states, { + minimum: ledger.minimum, + fixedHistories: ledger.fixedHistories, + }), + ) + for (const history of ledger.histories) { + reach.beginHistory() + for (const index of history) reach.reach(ledger.states[index]!) + } + let failure: string | undefined + try { + reach.assertReached() + } catch (error) { + failure = (error as Error).message + } + return { counts: new Map(reach.counts()), failure } +} + +// The states a failure names: `name (count)` below the minimum, and a list of +// names for the fixed histories. +function namedStates(failure: string) { + const below = /not enforced there: (.*)$/m.exec(failure)?.[1] + const unfixed = /reach depends on the seed: (.*)$/m.exec(failure)?.[1] + return { + belowMinimum: new Map( + (below?.split(`, `) ?? []).map((entry) => { + const match = /^(.*) \((\d+)\)$/.exec(entry)! + return [match[1]!, Number(match[2])] as const + }), + ), + unfixed: unfixed?.split(`, `) ?? [], + } +} + +// The check: the observed ledger refines the model. +function checkLedger(ledger: Ledger) { + const expected = expectedVerdict(ledger) + const observed = observeLedger(ledger) + if (expected === `skipped`) { + expect(observed.failure, `a path replay checks no reach`).toBeUndefined() + return expected + } + expect(observed.counts, `histories per state`).toEqual(expected.counts) + const fails = expected.belowMinimum.size > 0 || expected.unfixed.length > 0 + expect(observed.failure !== undefined, `the reach check fails`).toBe(fails) + if (observed.failure !== undefined) { + const named = namedStates(observed.failure) + expect(named.belowMinimum, `states below the minimum`).toEqual( + expected.belowMinimum, + ) + expect(named.unfixed, `states the fixed histories missed`).toEqual( + expected.unfixed, + ) + } + return expected +} + +// The run budget: the examples come on top of the base runs, except in a +// path replay of this property, which runs one history. +function expectedNumRuns(run: RunKind, baseRuns: number, examples: number) { + return run === `path` ? 1 : baseRuns + examples +} + +function checkRunParameters( + run: RunKind, + baseRuns: number, + examples: ReadonlyArray, +) { + const parameters = oracleRandomParameters( + baseRuns, + run === `ordinary` + ? undefined + : run === `seed` + ? { replaySeed: 1, replayPath: undefined, replayProperty: undefined } + : { replaySeed: 1, replayPath: `0`, replayProperty: property }, + property, + examples, + ) + expect(parameters.numRuns, `runs`).toBe( + expectedNumRuns(run, baseRuns, examples.length), + ) + expect(parameters.examples, `examples`).toEqual(examples) +} + +declareOracle({ + check: [checkLedger, checkRunParameters], + model: [expectedVerdict, expectedNumRuns], + grammar: [ledgerArbitrary], +}) + +const reachStates = [ + `a seed-only run fails below the minimum`, + `a path replay with a state below the minimum`, + `a fixed history miss that a later history enters`, + `a state below a minimum above one`, + `a ledger that passes`, +] as const +const ledgerReach = createOracleReach(`oracle.declared-reach`, reachStates) +let ledgersRan = false +afterAll(() => { + if (ledgersRan) ledgerReach.assertReached() +}) + +fcTest.prop( + [ + ledgerArbitrary, + fc.integer({ min: 1, max: 200 }), + fc.array(fc.integer(), { maxLength: 5 }), + ], + oraclePropertyOptions(200, property), +)( + `reach ledgers refine the declared reach model`, + (ledger, baseRuns, examples) => { + ledgersRan = true + ledgerReach.beginHistory() + const verdict = checkLedger(ledger) + checkRunParameters(ledger.run, baseRuns, examples) + if (verdict === `skipped`) { + const ordinary = expectedVerdict({ ...ledger, run: `ordinary` }) + if (ordinary !== `skipped` && ordinary.belowMinimum.size > 0) + ledgerReach.reach(`a path replay with a state below the minimum`) + return + } + if (ledger.run === `seed` && verdict.belowMinimum.size > 0) + ledgerReach.reach(`a seed-only run fails below the minimum`) + if (verdict.unfixed.some((state) => (verdict.counts.get(state) ?? 0) > 0)) + ledgerReach.reach(`a fixed history miss that a later history enters`) + if (ledger.minimum > 1 && verdict.belowMinimum.size > 0) + ledgerReach.reach(`a state below a minimum above one`) + if (verdict.belowMinimum.size === 0 && verdict.unfixed.length === 0) + ledgerReach.reach(`a ledger that passes`) + }, +) diff --git a/packages/db/tests/oracle-config.ts b/packages/db/tests/oracle-config.ts index 8b77f8feb6..ef17424968 100644 --- a/packages/db/tests/oracle-config.ts +++ b/packages/db/tests/oracle-config.ts @@ -6,6 +6,7 @@ type OracleEnvironment = Record const staticOracleProperties = [ `lint.part-reach`, + `oracle.declared-reach`, `scripts.lint-scope`, `scripts.run-budget`, `react.ssr-ordinary`, @@ -642,14 +643,32 @@ export function readOracleRunConfig( return { multiplier, replaySeed, replayPath, replayProperty } } -export function oracleRandomParameters( +export function oracleRandomParameters( numRuns: number, replay: OracleReplayConfig | number | undefined, property?: string, -): { numRuns: number; seed?: number; path?: string } & ReturnType< - typeof oracleReplayReporter -> { + examples?: ReadonlyArray, +): { + numRuns: number + seed?: number + path?: string + examples?: Array +} & ReturnType { if (property !== undefined) assertRegisteredOracleProperty(property) + // fast-check runs the examples first and counts them in numRuns, so they + // come on top of the random runs: the examples never displace one. A path + // replay runs one recorded history, which can be an example. + if (examples !== undefined) { + const parameters = oracleRandomParameters(numRuns, replay, property) + return { + ...parameters, + examples: [...examples], + numRuns: + parameters.path === undefined + ? parameters.numRuns + examples.length + : parameters.numRuns, + } + } const { replaySeed, replayPath, replayProperty } = typeof replay === `object` ? replay @@ -756,10 +775,19 @@ export function oracleRuns(baseRuns: number): number { return baseRuns * multiplier } -/** Replays broad randomized properties when a campaign seed is supplied. */ -export function oraclePropertyOptions( +/** + * Replays broad randomized properties when a campaign seed is supplied. + * `examples` run first in every run, on top of the base runs. + */ +export function oraclePropertyOptions( baseRuns: number, property?: string, -): ReturnType { - return oracleRandomParameters(oracleRuns(baseRuns), replay, property) + { examples }: { examples?: ReadonlyArray } = {}, +): ReturnType> { + return oracleRandomParameters( + oracleRuns(baseRuns), + replay, + property, + examples, + ) } diff --git a/packages/db/tests/oracle-reach.ts b/packages/db/tests/oracle-reach.ts index b75ea8dff6..2a88430713 100644 --- a/packages/db/tests/oracle-reach.ts +++ b/packages/db/tests/oracle-reach.ts @@ -14,38 +14,46 @@ import { readOracleRunConfig } from './oracle-config.js' * histories entered. A history counts once per state, however often it * enters it. * + * A property that runs fixed examples first, through `oraclePropertyOptions`' + * `examples`, passes their number as `fixedHistories`. The check then also + * fails for every declared state that those first histories did not enter: + * that state's reach would depend on the seed (#2287). + * * A path replay checks one recorded history, not reach, so the check does * nothing then. A seed alone reseeds the whole campaign, which runs its full * budget, so its reach is checked like an ordinary run's. + * `packages/db/tests/declared-reach-oracle.property.test.ts` owns these rules. */ export function createOracleReach( property: string, states: ReadonlyArray, { minimum = 1, + fixedHistories = 0, replaying: replayOverride, - }: { minimum?: number; replaying?: boolean } = {}, + }: { minimum?: number; fixedHistories?: number; replaying?: boolean } = {}, ) { const counts = new Map(states.map((state) => [state, 0])) + const enteredByFixed = new Set() + let histories = 0 let current = new Set() // Other packages use their own replay prefixes. An explicit campaign choice // must not inherit an unrelated DB replay selector from the environment. const replaying = - replayOverride ?? - (() => { - const { replayPath } = readOracleRunConfig() - return replayPath !== undefined - })() + replayOverride ?? readOracleRunConfig().replayPath !== undefined return { /** Starts one generated history. */ beginHistory(): void { current = new Set() + histories += 1 }, /** The current history entered a declared state. */ reach(state: TState): void { if (!counts.has(state)) { throw new Error(`${property}: undeclared reach state ${state}`) } + if (histories > 0 && histories <= fixedHistories) + enteredByFixed.add(state) if (current.has(state)) return current.add(state) counts.set(state, counts.get(state)! + 1) @@ -60,13 +68,27 @@ export function createOracleReach( const missed = [...counts] .filter(([, count]) => count < minimum) .map(([state, count]) => `${state} (${count})`) - if (missed.length > 0) { - throw new Error( - `${property}: generated histories reached these states fewer than ` + - `${minimum} times, so their laws were not enforced there: ` + - missed.join(`, `), - ) - } + const unfixed = + fixedHistories === 0 + ? [] + : states.filter((state) => !enteredByFixed.has(state)) + const failures = [ + ...(missed.length > 0 + ? [ + `${property}: generated histories reached these states fewer ` + + `than ${minimum} times, so their laws were not enforced ` + + `there: ${missed.join(`, `)}`, + ] + : []), + ...(unfixed.length > 0 + ? [ + `${property}: its first ${fixedHistories} histories, the fixed ` + + `examples, did not enter these states, so their reach ` + + `depends on the seed: ${unfixed.join(`, `)}`, + ] + : []), + ] + if (failures.length > 0) throw new Error(failures.join(`\n`)) }, } } diff --git a/packages/db/tests/oracle-replay-manifest.ts b/packages/db/tests/oracle-replay-manifest.ts index 8418d5d773..5a79c7198f 100644 --- a/packages/db/tests/oracle-replay-manifest.ts +++ b/packages/db/tests/oracle-replay-manifest.ts @@ -20,6 +20,11 @@ const ownerGroups: ReadonlyArray< ], [`../scripts/run-budget-oracle.property.test.js`, `scripts`, `run-budget`], [`../scripts/lint-scope-oracle.property.test.js`, `scripts`, `lint-scope`], + [ + `db/tests/declared-reach-oracle.property.test.ts`, + `oracle`, + `declared-reach`, + ], [ `db/tests/ssr-stream-record-wait-oracle.test.ts`, `ssr`, diff --git a/packages/db/tests/source-health-oracle.test.ts b/packages/db/tests/source-health-oracle.test.ts index d333b5426f..8af158b8d6 100644 --- a/packages/db/tests/source-health-oracle.test.ts +++ b/packages/db/tests/source-health-oracle.test.ts @@ -3353,9 +3353,20 @@ describe(`source failure and health oracle`, () => { on(`ready`, `A`), ]), ] + // Each prefix also runs as a fixed example, first in every run and on top + // of the random histories, with a direct subscriber and the `join` shape, + // which queries both sources that the prefixes drive. The reach check fails + // for a declared state that these examples do not enter (#2287). + const historyExamples = reachPrefixes.map( + (prefix): [[Shape, Array], boolean] => [ + [prefixShapes.get(prefix) ?? `join`, [...prefix]], + true, + ], + ) const historyReach = createOracleReach( `source-health.history`, historyReachStates, + { fixedHistories: historyExamples.length }, ) let historiesRan = false fcTest.prop( @@ -3372,16 +3383,9 @@ describe(`source failure and health oracle`, () => { ]), fc.boolean(), ], - { - ...oraclePropertyOptions(60, `source-health.history`), - // Each prefix runs once in every run, before the random histories, so - // the states only a prefix enters cannot miss by chance (#2287). The - // `join` shape queries both sources that the prefixes drive. - examples: reachPrefixes.map((prefix): [[Shape, Array], boolean] => [ - [prefixShapes.get(prefix) ?? `join`, [...prefix]], - true, - ]), - }, + oraclePropertyOptions(60, `source-health.history`, { + examples: historyExamples, + }), )( `generated histories refine the model`, ([shape, steps], directSubscribers) => { @@ -5186,14 +5190,6 @@ describe(`on-demand demand grammar`, () => { `fail`, `crash`, ) - const demandReach = createOracleReach( - `source-health.on-demand`, - demandReachStates, - ) - let demandHistoriesRan = false - afterAll(() => { - if (demandHistoriesRan) demandReach.assertReached() - }) // A prefix that enters a declared reach state that random steps alone // rarely reach at the base run count; random steps follow it. const demandReachPrefixes: ReadonlyArray> = [ @@ -5240,6 +5236,21 @@ describe(`on-demand demand grammar`, () => { `restart`, ], ] + // Each prefix also runs as a fixed example, first in every run and on top + // of the random histories, with a direct subscriber. The reach check fails + // for a declared state that these examples do not enter. + const demandExamples = demandReachPrefixes.map( + (prefix): [Array, boolean] => [[...prefix], true], + ) + const demandReach = createOracleReach( + `source-health.on-demand`, + demandReachStates, + { fixedHistories: demandExamples.length }, + ) + let demandHistoriesRan = false + afterAll(() => { + if (demandHistoriesRan) demandReach.assertReached() + }) fcTest.prop( [ fc @@ -5253,13 +5264,9 @@ describe(`on-demand demand grammar`, () => { ]), fc.boolean(), ], - { - ...oraclePropertyOptions(60, `source-health.on-demand`), - // Each prefix runs once in every run, before the random histories. - examples: demandReachPrefixes.map( - (prefix): [Array, boolean] => [[...prefix], true], - ), - }, + oraclePropertyOptions(60, `source-health.on-demand`, { + examples: demandExamples, + }), )( `generated demand histories refine the model`, (steps, directSubscriber) => { @@ -6960,14 +6967,6 @@ describe(`lazy join demand grammar`, () => { ending: { at: `subscription-status`, dependents }, }), ) - const lazyReach = createOracleReach( - `source-health.lazy-demand`, - lazyReachStates, - ) - let lazyHistoriesRan = false - afterAll(() => { - if (lazyHistoriesRan) lazyReach.assertReached() - }) // A reload whose replay fails. A row the provider deletes after it stays. const failedReload = { steps: [{ kind: `settle-ok` }, { kind: `reload` }, { kind: `settle-fail` }], @@ -7097,12 +7096,10 @@ describe(`lazy join demand grammar`, () => { rest: Array, { withEffect = false, - windowed = false, deferredStart, ending, }: { withEffect?: boolean - windowed?: boolean deferredStart?: `reload-in-first-load` ending?: { at: ReloadNotice; dependents: boolean } } = {}, @@ -7112,10 +7109,44 @@ describe(`lazy join demand grammar`, () => { false, true, withEffect, - windowed, + false, deferredStart, ending, ] + // Each prefix also runs as a fixed example, first in every run and on top + // of the random histories, and so does each driver option that a declared + // state needs. Each example has a direct subscriber and no other option it + // does not name. The reach check fails for a declared state that these + // examples do not enter. + const lazyExamples = [ + ...lazyReachPrefixes.map((prefix) => lazyExample(prefix, [])), + // The provider deletes a row after a reload's run ended. + lazyExample(failedReload, [{ kind: `remote-delete`, key: 1 }]), + lazyExample(null, [{ kind: `settle-ok` }], { withEffect: true }), + lazyExample(null, [{ kind: `settle-ok` }], { + deferredStart: `reload-in-first-load`, + }), + // A cleanup at each notice of a reload. A reload changes loadingSubset + // only while the first load is still open. + ...reloadNotices.map((at) => + lazyExample( + null, + at === `loading-subset` ? [] : [{ kind: `settle-ok` }], + { + ending: { at, dependents: false }, + }, + ), + ), + ] + const lazyReach = createOracleReach( + `source-health.lazy-demand`, + lazyReachStates, + { fixedHistories: lazyExamples.length }, + ) + let lazyHistoriesRan = false + afterAll(() => { + if (lazyHistoriesRan) lazyReach.assertReached() + }) fcTest.prop( [ fc @@ -7142,33 +7173,9 @@ describe(`lazy join demand grammar`, () => { { freq: 2, nil: undefined }, ), ], - { - ...oraclePropertyOptions(100, `source-health.lazy-demand`), - // Each prefix runs once in every run, before the random histories, - // and so does each driver option that a declared state needs. Each - // example has a direct subscriber and no other option it does not name. - examples: [ - ...lazyReachPrefixes.map((prefix) => lazyExample(prefix, [])), - // The provider deletes a row after a reload's run ended. - lazyExample(failedReload, [{ kind: `remote-delete`, key: 1 }]), - lazyExample(null, [{ kind: `settle-ok` }], { withEffect: true }), - lazyExample(null, [{ kind: `settle-ok` }], { - deferredStart: `reload-in-first-load`, - }), - // A cleanup at each notice of a reload. The loadingSubset notice - // needs a windowed query whose first load is still open. - ...reloadNotices.map((at) => - at === `loading-subset` - ? lazyExample(null, [], { - windowed: true, - ending: { at, dependents: false }, - }) - : lazyExample(null, [{ kind: `settle-ok` }], { - ending: { at, dependents: false }, - }), - ), - ], - }, + oraclePropertyOptions(100, `source-health.lazy-demand`, { + examples: lazyExamples, + }), )( `generated lazy demand histories refine the model`, ( From c3a5fa37c1ad7ae28ce92c07e87fcd9d491fef9b Mon Sep 17 00:00:00 2001 From: Test Date: Wed, 28 Oct 2026 12:55:49 -0600 Subject: [PATCH 03/12] test(db): check campaign reach in seed-only runs; name lazy options runOracleCampaign skipped the reach check for a seed-only run of its replay prefix, which runs the full campaign. Only a path replay skips it now, as for createOracleReach (maintainer decision). The declared reach oracle drives the runner too: it failed on the unchanged runner and rejects a mutant whose path replay checks reach. The lazy-demand property takes its seven driver options as one named record, so its fixed examples name each option instead of writing eight positional values. The examples reuse LazyEnding, and the failedReload comment says what the prefix does. The coverage map links #2289 for the properties whose reach has not been measured. Co-authored-by: Isaac --- docs/contributing/oracle-coverage.md | 10 +- .../declared-reach-oracle.property.test.ts | 79 +++++++++++- packages/db/tests/oracle-campaign.ts | 8 +- .../db/tests/source-health-oracle.test.ts | 115 +++++++++--------- 4 files changed, 142 insertions(+), 70 deletions(-) diff --git a/docs/contributing/oracle-coverage.md b/docs/contributing/oracle-coverage.md index 47f5a0cf09..11bef050f4 100644 --- a/docs/contributing/oracle-coverage.md +++ b/docs/contributing/oracle-coverage.md @@ -3417,11 +3417,11 @@ The `source-health.history`, `source-health.on-demand`, and option that a declared state needs, as examples, so their reach does not depend on the seed (#2287). The oracle generates ledgers over two to four states, up to six histories, minimums up to three, and up to four fixed histories, under the -three run kinds. It does not cover `runOracleCampaign` in -`packages/db/tests/oracle-campaign.ts`, which passes its own `replaying` rule: -a seed-only run of its campaign prefix still skips the check. A declared state -of another property that only random histories reach can still miss by chance -at the normal budget. Those properties have not been measured. Needed witness: +three run kinds. It also drives `runOracleCampaign` in +`packages/db/tests/oracle-campaign.ts`, whose seed-only run of its own replay +prefix checks reach in the same way. A declared state of another property that +only random histories reach can still miss by chance at the normal budget. +Those properties have not been measured. Destination: #2289. Needed witness: per property, the declared states that no fixed example enters, and how often a normal-budget run misses each one. diff --git a/packages/db/tests/declared-reach-oracle.property.test.ts b/packages/db/tests/declared-reach-oracle.property.test.ts index 8e72cb5732..9cfaadce0d 100644 --- a/packages/db/tests/declared-reach-oracle.property.test.ts +++ b/packages/db/tests/declared-reach-oracle.property.test.ts @@ -16,15 +16,20 @@ * budget, so they never displace a random history, and a path replay still * runs one history. * + * `runOracleCampaign` follows the first rule for its own replay prefix: a + * seed-only run of its campaign checks reach, and only a path replay skips it. + * * The model below states both rules over a generated ledger: a run kind, a * minimum, a number of fixed histories, and the states each history enters. - * The driver runs `createOracleReach` and `oracleRandomParameters` under that - * run kind's environment, and the check compares counts, the failure, and - * the states the failure names with the model. + * The drivers run `createOracleReach`, `runOracleCampaign`, and + * `oracleRandomParameters` under that run kind's environment, and the checks + * compare counts, the failure, and the states the failure names with the + * model. */ import { fc, test as fcTest } from '@fast-check/vitest' -import { afterAll, expect } from 'vitest' +import { afterAll, expect, vi } from 'vitest' import { createOracleReach } from './oracle-reach.js' +import { runOracleCampaign } from './oracle-campaign.js' import { oraclePropertyOptions, oracleRandomParameters, @@ -187,6 +192,67 @@ function checkLedger(ledger: Ledger) { return expected } +// The campaign runner's replay prefix, and the environment each run kind sets +// for it. +const campaignPrefix = `TANSTACK_DB_REACH_LEDGER` +function campaignEnvironment(run: RunKind): Record { + if (run === `ordinary`) return {} + if (run === `seed`) return { [`${campaignPrefix}_SEED`]: `1` } + return { [`${campaignPrefix}_SEED`]: `1`, [`${campaignPrefix}_PATH`]: `0` } +} + +// The driver: one ledger through each campaign that runOracleCampaign runs. +async function observeCampaign(ledger: Ledger) { + const names = [`${campaignPrefix}_SEED`, `${campaignPrefix}_PATH`] + const saved = names.map((name) => [name, process.env[name]] as const) + for (const name of names) delete process.env[name] + Object.assign(process.env, campaignEnvironment(ledger.run)) + // The runner reports each campaign's counts on the console. + const info = vi.spyOn(console, `info`).mockImplementation(() => {}) + try { + await runOracleCampaign(campaignPrefix, ledger.states, (reach) => { + for (const history of ledger.histories) { + reach.beginHistory() + for (const index of history) reach.reach(ledger.states[index]!) + } + }) + return undefined + } catch (error) { + return (error as Error).message + } finally { + info.mockRestore() + for (const [name, value] of saved) { + if (value === undefined) delete process.env[name] + else process.env[name] = value + } + } +} + +// The check: a campaign's reach refines the model with a minimum of one and +// no fixed histories, the campaign runner's own reach. +async function checkCampaign(ledger: Ledger) { + const expected = expectedVerdict({ + ...ledger, + minimum: 1, + fixedHistories: 0, + }) + const failure = await observeCampaign(ledger) + if (expected === `skipped`) { + expect( + failure, + `a path replay of a campaign checks no reach`, + ).toBeUndefined() + return + } + expect(failure !== undefined, `the campaign's reach check fails`).toBe( + expected.belowMinimum.size > 0, + ) + if (failure !== undefined) + expect(namedStates(failure).belowMinimum, `states below one`).toEqual( + expected.belowMinimum, + ) +} + // The run budget: the examples come on top of the base runs, except in a // path replay of this property, which runs one history. function expectedNumRuns(run: RunKind, baseRuns: number, examples: number) { @@ -215,7 +281,7 @@ function checkRunParameters( } declareOracle({ - check: [checkLedger, checkRunParameters], + check: [checkLedger, checkCampaign, checkRunParameters], model: [expectedVerdict, expectedNumRuns], grammar: [ledgerArbitrary], }) @@ -242,10 +308,11 @@ fcTest.prop( oraclePropertyOptions(200, property), )( `reach ledgers refine the declared reach model`, - (ledger, baseRuns, examples) => { + async (ledger, baseRuns, examples) => { ledgersRan = true ledgerReach.beginHistory() const verdict = checkLedger(ledger) + await checkCampaign(ledger) checkRunParameters(ledger.run, baseRuns, examples) if (verdict === `skipped`) { const ordinary = expectedVerdict({ ...ledger, run: `ordinary` }) diff --git a/packages/db/tests/oracle-campaign.ts b/packages/db/tests/oracle-campaign.ts index 754b33f854..d99f4fb480 100644 --- a/packages/db/tests/oracle-campaign.ts +++ b/packages/db/tests/oracle-campaign.ts @@ -5,7 +5,9 @@ import { createOracleReach } from './oracle-reach' * owns its property, grammar, recorder, comparison, and run budget; only seed * selection changes between the two calls. Counts are histories, not events: * call beginHistory once and reach only after observing the named checkpoint. - * A direct prefix SEED/PATH replay runs immediately without campaign minima. + * A prefix SEED replay runs one campaign at the callback's full budget, and + * checks its reach. A SEED/PATH replay runs one recorded history and checks + * no reach. `declared-reach-oracle.property.test.ts` owns this rule. * This is runner support, not an independent product judgment. */ export async function runOracleCampaign( @@ -50,7 +52,7 @@ export async function runOracleCampaign( ] for (const campaign of campaigns) { const reach = createOracleReach(prefix, states, { - replaying: seed !== undefined, + replaying: path !== undefined, }) await run(reach, campaign.parameters) reach.assertReached() @@ -58,7 +60,7 @@ export async function runOracleCampaign( `ORACLE_REACH ${JSON.stringify({ property: prefix, campaign: campaign.name, - minimum: seed === undefined ? 1 : null, + minimum: path === undefined ? 1 : null, counts: Object.fromEntries(reach.counts()), })}`, ) diff --git a/packages/db/tests/source-health-oracle.test.ts b/packages/db/tests/source-health-oracle.test.ts index 8af158b8d6..49ba433ad2 100644 --- a/packages/db/tests/source-health-oracle.test.ts +++ b/packages/db/tests/source-health-oracle.test.ts @@ -6967,10 +6967,10 @@ describe(`lazy join demand grammar`, () => { ending: { at: `subscription-status`, dependents }, }), ) - // A reload whose replay fails. A row the provider deletes after it stays. - const failedReload = { + // A load, then a reload whose load fails. + const failedReload: { steps: ReadonlyArray } = { steps: [{ kind: `settle-ok` }, { kind: `reload` }, { kind: `settle-fail` }], - } as const satisfies { steps: ReadonlyArray } + } const reloadNotices: ReadonlyArray = [ `source-health`, `query-health`, @@ -7078,40 +7078,57 @@ describe(`lazy join demand grammar`, () => { holdChildReady: false, }, ] - type LazyExample = [ - { - prefix: (typeof lazyReachPrefixes)[number] | null - rest: Array - }, - boolean, - boolean, - boolean, - boolean, - boolean, - `plain` | `reload-in-first-load` | undefined, - { at: ReloadNotice; dependents: boolean } | undefined, - ] + // The driver options a lazy history runs under, by name. + type LazyOptions = { + asyncChildReady: boolean + generatedHoldChildReady: boolean + directSubscriber: boolean + withEffect: boolean + windowed: boolean + deferredStart: `plain` | `reload-in-first-load` | undefined + ending: LazyEnding | undefined + } + const lazyOptions: fc.Arbitrary = fc.record({ + asyncChildReady: fc.boolean(), + generatedHoldChildReady: fc.boolean(), + directSubscriber: fc.boolean(), + withEffect: fc.boolean(), + windowed: fc.boolean(), + deferredStart: fc.constantFrom( + undefined, + `plain` as const, + `reload-in-first-load` as const, + ), + ending: fc.option( + fc.record({ + at: fc.constantFrom(...reloadNotices), + dependents: fc.boolean(), + }), + { freq: 2, nil: undefined }, + ), + }) const lazyExample = ( prefix: (typeof lazyReachPrefixes)[number] | null, rest: Array, + options: Partial = {}, + ): [ { - withEffect = false, - deferredStart, - ending, - }: { - withEffect?: boolean - deferredStart?: `reload-in-first-load` - ending?: { at: ReloadNotice; dependents: boolean } - } = {}, - ): LazyExample => [ + prefix: (typeof lazyReachPrefixes)[number] | null + rest: Array + }, + LazyOptions, + ] => [ { prefix, rest }, - false, - false, - true, - withEffect, - false, - deferredStart, - ending, + { + asyncChildReady: false, + generatedHoldChildReady: false, + directSubscriber: true, + withEffect: false, + windowed: false, + deferredStart: undefined, + ending: undefined, + ...options, + }, ] // Each prefix also runs as a fixed example, first in every run and on top // of the random histories, and so does each driver option that a declared @@ -7155,23 +7172,7 @@ describe(`lazy join demand grammar`, () => { fc.array(step, { maxLength: 10 }), ) .map(([prefix, rest]) => ({ prefix, rest })), - fc.boolean(), - fc.boolean(), - fc.boolean(), - fc.boolean(), - fc.boolean(), - fc.constantFrom( - undefined, - `plain` as const, - `reload-in-first-load` as const, - ), - fc.option( - fc.record({ - at: fc.constantFrom(...reloadNotices), - dependents: fc.boolean(), - }), - { freq: 2, nil: undefined }, - ), + lazyOptions, ], oraclePropertyOptions(100, `source-health.lazy-demand`, { examples: lazyExamples, @@ -7180,13 +7181,15 @@ describe(`lazy join demand grammar`, () => { `generated lazy demand histories refine the model`, ( { prefix, rest }, - asyncChildReady, - generatedHoldChildReady, - directSubscriber, - withEffect, - windowed, - deferredStart, - ending, + { + asyncChildReady, + generatedHoldChildReady, + directSubscriber, + withEffect, + windowed, + deferredStart, + ending, + }, ) => { const steps = [...(prefix?.steps ?? []), ...rest] const holdChildReady = prefix?.holdChildReady ?? generatedHoldChildReady From 1546da8efac99e5a51a2b79f5648956fd854aca4 Mon Sep 17 00:00:00 2001 From: Test Date: Wed, 28 Oct 2026 13:13:36 -0600 Subject: [PATCH 04/12] test(db): keep the oracle parameter type for calls without examples fast-check infers a property's argument types from the `examples` parameter too. The generic return type gave every call an `examples` field, which changed the inferred types in other packages' oracles and failed lint in node-db-sqlite-persistence. Overloads now return `examples` only for a call that passes them. `ReturnType` reads the last overload, the one without examples. Co-authored-by: Isaac --- packages/db/tests/oracle-config.ts | 51 +++++++++++++++++++++--------- 1 file changed, 36 insertions(+), 15 deletions(-) diff --git a/packages/db/tests/oracle-config.ts b/packages/db/tests/oracle-config.ts index ef17424968..3c1eb96bfe 100644 --- a/packages/db/tests/oracle-config.ts +++ b/packages/db/tests/oracle-config.ts @@ -643,17 +643,32 @@ export function readOracleRunConfig( return { multiplier, replaySeed, replayPath, replayProperty } } -export function oracleRandomParameters( +type OracleRunParameters = { + numRuns: number + seed?: number + path?: string +} & ReturnType + +// fast-check infers a property's argument types from `examples` too, so only +// a call with examples returns them. `ReturnType` reads the last overload, +// the one without examples. +export function oracleRandomParameters( + numRuns: number, + replay: OracleReplayConfig | number | undefined, + property: string | undefined, + examples: ReadonlyArray, +): OracleRunParameters & { examples: Array } +export function oracleRandomParameters( + numRuns: number, + replay: OracleReplayConfig | number | undefined, + property?: string, +): OracleRunParameters +export function oracleRandomParameters( numRuns: number, replay: OracleReplayConfig | number | undefined, property?: string, examples?: ReadonlyArray, -): { - numRuns: number - seed?: number - path?: string - examples?: Array -} & ReturnType { +): OracleRunParameters & { examples?: Array } { if (property !== undefined) assertRegisteredOracleProperty(property) // fast-check runs the examples first and counts them in numRuns, so they // come on top of the random runs: the examples never displace one. A path @@ -779,15 +794,21 @@ export function oracleRuns(baseRuns: number): number { * Replays broad randomized properties when a campaign seed is supplied. * `examples` run first in every run, on top of the base runs. */ -export function oraclePropertyOptions( +export function oraclePropertyOptions( + baseRuns: number, + property: string | undefined, + options: { examples: ReadonlyArray }, +): OracleRunParameters & { examples: Array } +export function oraclePropertyOptions( + baseRuns: number, + property?: string, +): OracleRunParameters +export function oraclePropertyOptions( baseRuns: number, property?: string, { examples }: { examples?: ReadonlyArray } = {}, -): ReturnType> { - return oracleRandomParameters( - oracleRuns(baseRuns), - replay, - property, - examples, - ) +): OracleRunParameters & { examples?: Array } { + return examples === undefined + ? oracleRandomParameters(oracleRuns(baseRuns), replay, property) + : oracleRandomParameters(oracleRuns(baseRuns), replay, property, examples) } From 9d0498e03470f75e88359e6246d4d219514ae1fe Mon Sep 17 00:00:00 2001 From: Test Date: Wed, 28 Oct 2026 13:13:36 -0600 Subject: [PATCH 05/12] test(db): fix the declared-reach oracle's own reach The oracle declared five reach states and reached them only through generated ledgers, the defect class of #2287. One fixed ledger per state now runs first in every run, with `fixedHistories: 5`. Dropping any one of them fails every run and names its state. Co-authored-by: Isaac --- .../declared-reach-oracle.property.test.ts | 27 +++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/packages/db/tests/declared-reach-oracle.property.test.ts b/packages/db/tests/declared-reach-oracle.property.test.ts index 9cfaadce0d..6cd431d938 100644 --- a/packages/db/tests/declared-reach-oracle.property.test.ts +++ b/packages/db/tests/declared-reach-oracle.property.test.ts @@ -293,7 +293,30 @@ const reachStates = [ `a state below a minimum above one`, `a ledger that passes`, ] as const -const ledgerReach = createOracleReach(`oracle.declared-reach`, reachStates) +// One fixed ledger enters each reach state, first in every run, so this +// property's own reach cannot miss by chance. +function fixedLedger( + run: RunKind, + minimum: number, + fixedHistories: number, + histories: Ledger[`histories`], +): [Ledger, number, Array] { + return [ + { run, states: [`state 0`, `state 1`], minimum, fixedHistories, histories }, + 60, + [1], + ] +} +const ledgerExamples = [ + fixedLedger(`seed`, 1, 0, []), + fixedLedger(`path`, 1, 0, []), + fixedLedger(`ordinary`, 1, 1, [[0], [1]]), + fixedLedger(`ordinary`, 2, 0, [[0, 1]]), + fixedLedger(`ordinary`, 1, 0, [[0, 1]]), +] +const ledgerReach = createOracleReach(`oracle.declared-reach`, reachStates, { + fixedHistories: ledgerExamples.length, +}) let ledgersRan = false afterAll(() => { if (ledgersRan) ledgerReach.assertReached() @@ -305,7 +328,7 @@ fcTest.prop( fc.integer({ min: 1, max: 200 }), fc.array(fc.integer(), { maxLength: 5 }), ], - oraclePropertyOptions(200, property), + oraclePropertyOptions(200, property, { examples: ledgerExamples }), )( `reach ledgers refine the declared reach model`, async (ledger, baseRuns, examples) => { From 9be45692f8a97364216755b926b9c0e3214ac831 Mon Sep 17 00:00:00 2001 From: Test Date: Thu, 29 Oct 2026 09:01:31 -0600 Subject: [PATCH 06/12] test(db): compare whole reach verdicts in the declared-reach oracle The run-parameter check compared only numRuns and examples, so a mutant that dropped the seed and path from the examples branch passed. The model now states every run parameter: a seed replay keeps its seed, and a path replay keeps its seed and path. The ledger and campaign checks asserted only when a failure occurred. The model now returns the counts and the expected failure, or none, and each driver compares one whole observation. A path replay now also checks its counts. One helper over vi.stubEnv sets each run kind's environment. All eight hostile mutants of the reach machinery now fail at an assertion. Co-authored-by: Isaac --- .../declared-reach-oracle.property.test.ts | 228 +++++++++--------- 1 file changed, 112 insertions(+), 116 deletions(-) diff --git a/packages/db/tests/declared-reach-oracle.property.test.ts b/packages/db/tests/declared-reach-oracle.property.test.ts index 6cd431d938..0cc6a3595e 100644 --- a/packages/db/tests/declared-reach-oracle.property.test.ts +++ b/packages/db/tests/declared-reach-oracle.property.test.ts @@ -13,8 +13,8 @@ * `fixedHistories: n`, the check also fails for each declared state that * the first n histories, the examples, did not enter. Such a state's reach * would depend on the seed. The examples come on top of the base run - * budget, so they never displace a random history, and a path replay still - * runs one history. + * budget, so they never displace a random history. A replay keeps its seed, + * and a path replay keeps its path and still runs one history. * * `runOracleCampaign` follows the first rule for its own replay prefix: a * seed-only run of its campaign checks reach, and only a path replay skips it. @@ -47,11 +47,16 @@ type Ledger = { // The indices of the states each history enters, with repeats. histories: ReadonlyArray> } -type Verdict = { - counts: ReadonlyMap +// The states a failing reach check names, and an absent failure when the check +// passes or does not run. +type Failure = { belowMinimum: ReadonlyMap unfixed: ReadonlyArray } +type Verdict = { + counts: ReadonlyMap + failure: Failure | undefined +} // The grammar: two to four states, and up to six histories over them. const ledgerArbitrary: fc.Arbitrary = fc @@ -73,11 +78,11 @@ const ledgerArbitrary: fc.Arbitrary = fc }), ) -// The model. A history counts once per state it enters. A path replay checks -// nothing. Otherwise a state fails below the minimum, and, when fixed -// histories are declared, a state the first ones did not enter fails too. -function expectedVerdict(ledger: Ledger): Verdict | `skipped` { - if (ledger.run === `path`) return `skipped` +// The model. A history counts once per state it enters, in every run kind. A +// path replay checks nothing. Otherwise a state fails below the minimum, and, +// when fixed histories are declared, a state the first ones did not enter +// fails too. +function expectedVerdict(ledger: Ledger): Verdict { const entered = ledger.histories.map( (history) => new Set(history.map((index) => ledger.states[index]!)), ) @@ -88,17 +93,20 @@ function expectedVerdict(ledger: Ledger): Verdict | `skipped` { ]), ) const fixed = entered.slice(0, ledger.fixedHistories) + const belowMinimum = new Map( + [...counts].filter(([, count]) => count < ledger.minimum), + ) + const unfixed = + ledger.fixedHistories === 0 + ? [] + : ledger.states.filter((state) => + fixed.every((history) => !history.has(state)), + ) + const fails = belowMinimum.size > 0 || unfixed.length > 0 return { counts, - belowMinimum: new Map( - [...counts].filter(([, count]) => count < ledger.minimum), - ), - unfixed: - ledger.fixedHistories === 0 - ? [] - : ledger.states.filter((state) => - fixed.every((history) => !history.has(state)), - ), + failure: + ledger.run !== `path` && fails ? { belowMinimum, unfixed } : undefined, } } @@ -113,32 +121,36 @@ function runEnvironment(run: RunKind): Record { } } -function withEnvironment(variables: Record, run: () => T) { - const names = [ - `TANSTACK_DB_ORACLE_SEED`, - `TANSTACK_DB_ORACLE_PATH`, - `TANSTACK_DB_ORACLE_PROPERTY`, - ] - const saved = names.map((name) => [name, process.env[name]] as const) - for (const name of names) delete process.env[name] - Object.assign(process.env, variables) +// Runs `run` with the given variables set and the other named ones unset, and +// restores the environment afterward. +async function withEnvironment( + names: ReadonlyArray, + variables: Record, + run: () => T | Promise, +): Promise { + for (const name of names) vi.stubEnv(name, variables[name]) try { - return run() + return await run() } finally { - for (const [name, value] of saved) { - if (value === undefined) delete process.env[name] - else process.env[name] = value - } + vi.unstubAllEnvs() } } +const replayNames = [ + `TANSTACK_DB_ORACLE_SEED`, + `TANSTACK_DB_ORACLE_PATH`, + `TANSTACK_DB_ORACLE_PROPERTY`, +] // The driver: one ledger through createOracleReach. -function observeLedger(ledger: Ledger) { - const reach = withEnvironment(runEnvironment(ledger.run), () => - createOracleReach(`ledger`, ledger.states, { - minimum: ledger.minimum, - fixedHistories: ledger.fixedHistories, - }), +async function observeLedger(ledger: Ledger): Promise { + const reach = await withEnvironment( + replayNames, + runEnvironment(ledger.run), + () => + createOracleReach(`ledger`, ledger.states, { + minimum: ledger.minimum, + fixedHistories: ledger.fixedHistories, + }), ) for (const history of ledger.histories) { reach.beginHistory() @@ -150,12 +162,13 @@ function observeLedger(ledger: Ledger) { } catch (error) { failure = (error as Error).message } - return { counts: new Map(reach.counts()), failure } + return { counts: new Map(reach.counts()), failure: namedStates(failure) } } // The states a failure names: `name (count)` below the minimum, and a list of // names for the fixed histories. -function namedStates(failure: string) { +function namedStates(failure: string | undefined): Failure | undefined { + if (failure === undefined) return undefined const below = /not enforced there: (.*)$/m.exec(failure)?.[1] const unfixed = /reach depends on the seed: (.*)$/m.exec(failure)?.[1] return { @@ -170,25 +183,9 @@ function namedStates(failure: string) { } // The check: the observed ledger refines the model. -function checkLedger(ledger: Ledger) { +async function checkLedger(ledger: Ledger) { const expected = expectedVerdict(ledger) - const observed = observeLedger(ledger) - if (expected === `skipped`) { - expect(observed.failure, `a path replay checks no reach`).toBeUndefined() - return expected - } - expect(observed.counts, `histories per state`).toEqual(expected.counts) - const fails = expected.belowMinimum.size > 0 || expected.unfixed.length > 0 - expect(observed.failure !== undefined, `the reach check fails`).toBe(fails) - if (observed.failure !== undefined) { - const named = namedStates(observed.failure) - expect(named.belowMinimum, `states below the minimum`).toEqual( - expected.belowMinimum, - ) - expect(named.unfixed, `states the fixed histories missed`).toEqual( - expected.unfixed, - ) - } + expect(await observeLedger(ledger), `reach verdict`).toEqual(expected) return expected } @@ -202,61 +199,58 @@ function campaignEnvironment(run: RunKind): Record { } // The driver: one ledger through each campaign that runOracleCampaign runs. -async function observeCampaign(ledger: Ledger) { - const names = [`${campaignPrefix}_SEED`, `${campaignPrefix}_PATH`] - const saved = names.map((name) => [name, process.env[name]] as const) - for (const name of names) delete process.env[name] - Object.assign(process.env, campaignEnvironment(ledger.run)) - // The runner reports each campaign's counts on the console. - const info = vi.spyOn(console, `info`).mockImplementation(() => {}) - try { - await runOracleCampaign(campaignPrefix, ledger.states, (reach) => { - for (const history of ledger.histories) { - reach.beginHistory() - for (const index of history) reach.reach(ledger.states[index]!) +function observeCampaign(ledger: Ledger): Promise { + return withEnvironment( + [`${campaignPrefix}_SEED`, `${campaignPrefix}_PATH`], + campaignEnvironment(ledger.run), + async () => { + // The runner reports each campaign's counts on the console. + const info = vi.spyOn(console, `info`).mockImplementation(() => {}) + try { + await runOracleCampaign(campaignPrefix, ledger.states, (reach) => { + for (const history of ledger.histories) { + reach.beginHistory() + for (const index of history) reach.reach(ledger.states[index]!) + } + }) + return undefined + } catch (error) { + return namedStates((error as Error).message) + } finally { + info.mockRestore() } - }) - return undefined - } catch (error) { - return (error as Error).message - } finally { - info.mockRestore() - for (const [name, value] of saved) { - if (value === undefined) delete process.env[name] - else process.env[name] = value - } - } + }, + ) } // The check: a campaign's reach refines the model with a minimum of one and // no fixed histories, the campaign runner's own reach. async function checkCampaign(ledger: Ledger) { - const expected = expectedVerdict({ + const { failure } = expectedVerdict({ ...ledger, minimum: 1, fixedHistories: 0, }) - const failure = await observeCampaign(ledger) - if (expected === `skipped`) { - expect( - failure, - `a path replay of a campaign checks no reach`, - ).toBeUndefined() - return - } - expect(failure !== undefined, `the campaign's reach check fails`).toBe( - expected.belowMinimum.size > 0, + expect(await observeCampaign(ledger), `campaign reach failure`).toEqual( + failure, ) - if (failure !== undefined) - expect(namedStates(failure).belowMinimum, `states below one`).toEqual( - expected.belowMinimum, - ) } -// The run budget: the examples come on top of the base runs, except in a -// path replay of this property, which runs one history. -function expectedNumRuns(run: RunKind, baseRuns: number, examples: number) { - return run === `path` ? 1 : baseRuns + examples +// The run parameters: the examples come on top of the base runs, and the +// replay selection stays. A seed replay keeps its seed. A path replay of this +// property keeps its seed and path, and runs one history. A replay witness +// channel adds reporter keys; no run kind here opens one, so the check leaves +// them out. +function expectedRunParameters( + run: RunKind, + baseRuns: number, + examples: ReadonlyArray, +) { + if (run === `ordinary`) + return { numRuns: baseRuns + examples.length, examples } + if (run === `seed`) + return { numRuns: baseRuns + examples.length, seed: 1, examples } + return { numRuns: 1, seed: 1, path: `0`, examples } } function checkRunParameters( @@ -264,7 +258,12 @@ function checkRunParameters( baseRuns: number, examples: ReadonlyArray, ) { - const parameters = oracleRandomParameters( + const { + numRuns, + seed, + path, + examples: observed, + } = oracleRandomParameters( baseRuns, run === `ordinary` ? undefined @@ -274,15 +273,15 @@ function checkRunParameters( property, examples, ) - expect(parameters.numRuns, `runs`).toBe( - expectedNumRuns(run, baseRuns, examples.length), + // toEqual treats an undefined key as absent. + expect({ numRuns, seed, path, examples: observed }, `run parameters`).toEqual( + expectedRunParameters(run, baseRuns, examples), ) - expect(parameters.examples, `examples`).toEqual(examples) } declareOracle({ check: [checkLedger, checkCampaign, checkRunParameters], - model: [expectedVerdict, expectedNumRuns], + model: [expectedVerdict, expectedRunParameters], grammar: [ledgerArbitrary], }) @@ -334,22 +333,19 @@ fcTest.prop( async (ledger, baseRuns, examples) => { ledgersRan = true ledgerReach.beginHistory() - const verdict = checkLedger(ledger) + const { counts, failure } = await checkLedger(ledger) await checkCampaign(ledger) checkRunParameters(ledger.run, baseRuns, examples) - if (verdict === `skipped`) { - const ordinary = expectedVerdict({ ...ledger, run: `ordinary` }) - if (ordinary !== `skipped` && ordinary.belowMinimum.size > 0) - ledgerReach.reach(`a path replay with a state below the minimum`) - return - } - if (ledger.run === `seed` && verdict.belowMinimum.size > 0) + const ordinary = expectedVerdict({ ...ledger, run: `ordinary` }).failure + if (ledger.run === `path` && (ordinary?.belowMinimum.size ?? 0) > 0) + ledgerReach.reach(`a path replay with a state below the minimum`) + if (ledger.run === `seed` && (failure?.belowMinimum.size ?? 0) > 0) ledgerReach.reach(`a seed-only run fails below the minimum`) - if (verdict.unfixed.some((state) => (verdict.counts.get(state) ?? 0) > 0)) + if (failure?.unfixed.some((state) => (counts.get(state) ?? 0) > 0)) ledgerReach.reach(`a fixed history miss that a later history enters`) - if (ledger.minimum > 1 && verdict.belowMinimum.size > 0) + if (ledger.minimum > 1 && (failure?.belowMinimum.size ?? 0) > 0) ledgerReach.reach(`a state below a minimum above one`) - if (verdict.belowMinimum.size === 0 && verdict.unfixed.length === 0) + if (ledger.run !== `path` && failure === undefined) ledgerReach.reach(`a ledger that passes`) }, ) From 34d1b4f40f2d4474eeea23139e5183943c133ef0 Mon Sep 17 00:00:00 2001 From: Test Date: Thu, 29 Oct 2026 09:01:31 -0600 Subject: [PATCH 07/12] test(db): compute oracle run parameters once The examples branch called oracleRandomParameters again and patched numRuns, and oraclePropertyOptions repeated its call in both branches of a ternary. One private function now computes the parameters, and both overload sets delegate to it. Co-authored-by: Isaac --- packages/db/tests/oracle-config.ts | 71 ++++++++++++++++-------------- 1 file changed, 39 insertions(+), 32 deletions(-) diff --git a/packages/db/tests/oracle-config.ts b/packages/db/tests/oracle-config.ts index 3c1eb96bfe..cb2029eb4f 100644 --- a/packages/db/tests/oracle-config.ts +++ b/packages/db/tests/oracle-config.ts @@ -668,22 +668,17 @@ export function oracleRandomParameters( replay: OracleReplayConfig | number | undefined, property?: string, examples?: ReadonlyArray, +): OracleRunParameters & { examples?: Array } { + return randomParameters(numRuns, replay, property, examples) +} + +function randomParameters( + numRuns: number, + replay: OracleReplayConfig | number | undefined, + property: string | undefined, + examples: ReadonlyArray | undefined, ): OracleRunParameters & { examples?: Array } { if (property !== undefined) assertRegisteredOracleProperty(property) - // fast-check runs the examples first and counts them in numRuns, so they - // come on top of the random runs: the examples never displace one. A path - // replay runs one recorded history, which can be an example. - if (examples !== undefined) { - const parameters = oracleRandomParameters(numRuns, replay, property) - return { - ...parameters, - examples: [...examples], - numRuns: - parameters.path === undefined - ? parameters.numRuns + examples.length - : parameters.numRuns, - } - } const { replaySeed, replayPath, replayProperty } = typeof replay === `object` ? replay @@ -692,22 +687,36 @@ export function oracleRandomParameters( replayPath: undefined, replayProperty: undefined, } - if (replaySeed === undefined) return { numRuns } - return { - numRuns, - seed: replaySeed, - // A path replays one recorded counterexample, so the replay runs once. - // From a path with one segment, fast-check would otherwise run `numRuns` - // histories that start at that index. - ...(property !== undefined && - replayPath !== undefined && - replayProperty === property - ? { - numRuns: 1, - path: replayPath, - ...oracleReplayReporter(property, replaySeed, replayPath), + const parameters: OracleRunParameters = + replaySeed === undefined + ? { numRuns } + : { + numRuns, + seed: replaySeed, + // A path replays one recorded counterexample, so the replay runs + // once. From a path with one segment, fast-check would otherwise + // run `numRuns` histories that start at that index. + ...(property !== undefined && + replayPath !== undefined && + replayProperty === property + ? { + numRuns: 1, + path: replayPath, + ...oracleReplayReporter(property, replaySeed, replayPath), + } + : {}), } - : {}), + if (examples === undefined) return parameters + // fast-check runs the examples first and counts them in numRuns, so they + // come on top of the random runs: the examples never displace one. A path + // replay runs one recorded history, which can be an example. + return { + ...parameters, + examples: [...examples], + numRuns: + parameters.path === undefined + ? parameters.numRuns + examples.length + : parameters.numRuns, } } @@ -808,7 +817,5 @@ export function oraclePropertyOptions( property?: string, { examples }: { examples?: ReadonlyArray } = {}, ): OracleRunParameters & { examples?: Array } { - return examples === undefined - ? oracleRandomParameters(oracleRuns(baseRuns), replay, property) - : oracleRandomParameters(oracleRuns(baseRuns), replay, property, examples) + return randomParameters(oracleRuns(baseRuns), replay, property, examples) } From 74c4f3c02b7fed2cc46b90910aa23fd493e0ba41 Mon Sep 17 00:00:00 2001 From: Test Date: Thu, 29 Oct 2026 09:01:38 -0600 Subject: [PATCH 08/12] test(db): keep reach unit tests ordinary under a replay; name lazy steps A path replay in the environment switched the reach check off, so two createOracleReach examples failed under it. They now choose an ordinary run. The source-health history comment now names the prefix shape that its examples use, and one LazySteps type serves the lazy examples and the arbitrary. Co-authored-by: Isaac --- packages/db/tests/oracle-reach.test.ts | 7 ++++- .../db/tests/source-health-oracle.test.ts | 27 ++++++++++--------- 2 files changed, 20 insertions(+), 14 deletions(-) diff --git a/packages/db/tests/oracle-reach.test.ts b/packages/db/tests/oracle-reach.test.ts index 51f6f08a35..5836dc705e 100644 --- a/packages/db/tests/oracle-reach.test.ts +++ b/packages/db/tests/oracle-reach.test.ts @@ -1,9 +1,13 @@ import { describe, expect, it } from 'vitest' import { createOracleReach } from './oracle-reach.js' +// A replay selection in the environment would switch the reach check off, so +// these examples choose an ordinary run. describe(`createOracleReach`, () => { it(`fails for a declared state that no history entered`, () => { - const reach = createOracleReach(`example`, [`seen`, `unseen`] as const) + const reach = createOracleReach(`example`, [`seen`, `unseen`] as const, { + replaying: false, + }) reach.beginHistory() reach.reach(`seen`) expect(() => reach.assertReached()).toThrow(/unseen \(0\)/) @@ -12,6 +16,7 @@ describe(`createOracleReach`, () => { it(`counts a history once per state`, () => { const reach = createOracleReach(`example`, [`state`] as const, { minimum: 2, + replaying: false, }) reach.beginHistory() reach.reach(`state`) diff --git a/packages/db/tests/source-health-oracle.test.ts b/packages/db/tests/source-health-oracle.test.ts index 49ba433ad2..1416a83024 100644 --- a/packages/db/tests/source-health-oracle.test.ts +++ b/packages/db/tests/source-health-oracle.test.ts @@ -3354,9 +3354,11 @@ describe(`source failure and health oracle`, () => { ]), ] // Each prefix also runs as a fixed example, first in every run and on top - // of the random histories, with a direct subscriber and the `join` shape, - // which queries both sources that the prefixes drive. The reach check fails - // for a declared state that these examples do not enter (#2287). + // of the random histories, with a direct subscriber. A prefix runs the shape + // that prefixShapes gives it, as a generated history with that prefix does, + // and otherwise the `join` shape, which queries both sources that the + // prefixes drive. The reach check fails for a declared state that these + // examples do not enter (#2287). const historyExamples = reachPrefixes.map( (prefix): [[Shape, Array], boolean] => [ [prefixShapes.get(prefix) ?? `join`, [...prefix]], @@ -7107,17 +7109,16 @@ describe(`lazy join demand grammar`, () => { { freq: 2, nil: undefined }, ), }) + // A history's steps: an optional reach prefix, then generated steps. + type LazySteps = { + prefix: (typeof lazyReachPrefixes)[number] | null + rest: Array + } const lazyExample = ( - prefix: (typeof lazyReachPrefixes)[number] | null, - rest: Array, + prefix: LazySteps[`prefix`], + rest: LazySteps[`rest`], options: Partial = {}, - ): [ - { - prefix: (typeof lazyReachPrefixes)[number] | null - rest: Array - }, - LazyOptions, - ] => [ + ): [LazySteps, LazyOptions] => [ { prefix, rest }, { asyncChildReady: false, @@ -7171,7 +7172,7 @@ describe(`lazy join demand grammar`, () => { fc.option(fc.constantFrom(...lazyReachPrefixes), { freq: 4 }), fc.array(step, { maxLength: 10 }), ) - .map(([prefix, rest]) => ({ prefix, rest })), + .map(([prefix, rest]): LazySteps => ({ prefix, rest })), lazyOptions, ], oraclePropertyOptions(100, `source-health.lazy-demand`, { From 64e9c322ae895bc82584903d54a5598c9cd3e3ad Mon Sep 17 00:00:00 2001 From: Test Date: Thu, 29 Oct 2026 09:21:51 -0600 Subject: [PATCH 09/12] test(db): throw for a reach before the first history A reach() call before the first beginHistory() counted toward the totals, and a guard kept it out of the fixed examples. No generated ledger made such a call, so a mutant without the guard passed. The call is a driver error, so it now throws and counts nothing, and the guard goes. The declared-reach grammar now reaches states before the first history in a quarter of the ledgers and in one fixed ledger. The oracle failed on the parent; mutants that keep counting such a call, or that throw but still count it, fail at the reach verdict. The reach and coverage-map docs now state that fixed examples are the first histories only when one property owns the reach and begins every history. Co-authored-by: Isaac --- docs/contributing/oracle-coverage.md | 13 ++-- .../declared-reach-oracle.property.test.ts | 61 ++++++++++++++++--- packages/db/tests/oracle-reach.ts | 15 +++-- 3 files changed, 74 insertions(+), 15 deletions(-) diff --git a/docs/contributing/oracle-coverage.md b/docs/contributing/oracle-coverage.md index 11bef050f4..7468d810f0 100644 --- a/docs/contributing/oracle-coverage.md +++ b/docs/contributing/oracle-coverage.md @@ -3412,18 +3412,23 @@ it. A property can run fixed examples first in every run, through `oraclePropertyOptions(…, { examples })`. The examples come on top of the base run budget, so they never displace a random history. With `fixedHistories`, the check also fails for each declared state that the examples did not enter. -The `source-health.history`, `source-health.on-demand`, and +The examples are the first histories, so such a reach belongs to one property, +and only that property's callback begins its histories. A `reach()` call before +the first history throws and counts nothing. A replay keeps its seed, and a +path replay keeps its path. The `source-health.history`, `source-health.on-demand`, and `source-health.lazy-demand` properties run each reach prefix, and each driver option that a declared state needs, as examples, so their reach does not depend on the seed (#2287). The oracle generates ledgers over two to four states, up to -six histories, minimums up to three, and up to four fixed histories, under the -three run kinds. It also drives `runOracleCampaign` in +six histories, minimums up to three, up to four fixed histories, and reaches +before the first history, under the three run kinds. It also drives `runOracleCampaign` in `packages/db/tests/oracle-campaign.ts`, whose seed-only run of its own replay prefix checks reach in the same way. A declared state of another property that only random histories reach can still miss by chance at the normal budget. Those properties have not been measured. Destination: #2289. Needed witness: per property, the declared states that no fixed example enters, and how often a -normal-budget run misses each one. +normal-budget run misses each one. The oracle does not judge reporter keys, +which only a replay witness channel adds, or a reach shared across properties, +which the precondition above rules out but no check detects. `packages/db/tests/oracle-replay.test.ts` checks every replay manifest owner: from its cwd, the command's files exist, its target is the owner, and a Vitest diff --git a/packages/db/tests/declared-reach-oracle.property.test.ts b/packages/db/tests/declared-reach-oracle.property.test.ts index 0cc6a3595e..07021a9564 100644 --- a/packages/db/tests/declared-reach-oracle.property.test.ts +++ b/packages/db/tests/declared-reach-oracle.property.test.ts @@ -16,11 +16,17 @@ * budget, so they never displace a random history. A replay keeps its seed, * and a path replay keeps its path and still runs one history. * + * The first n histories are the examples only when the reach belongs to one + * property and that property's callback begins every history. A driver calls + * `reach(state)` inside a history: a call before the first `beginHistory()` + * is a driver error, so it throws and counts nothing. + * * `runOracleCampaign` follows the first rule for its own replay prefix: a * seed-only run of its campaign checks reach, and only a path replay skips it. * - * The model below states both rules over a generated ledger: a run kind, a - * minimum, a number of fixed histories, and the states each history enters. + * The model below states these rules over a generated ledger: a run kind, a + * minimum, a number of fixed histories, the states each history enters, and + * the states reached before the first history. * The drivers run `createOracleReach`, `runOracleCampaign`, and * `oracleRandomParameters` under that run kind's environment, and the checks * compare counts, the failure, and the states the failure names with the @@ -44,6 +50,8 @@ type Ledger = { states: ReadonlyArray minimum: number fixedHistories: number + // The indices of the states reached before the first history. + early: ReadonlyArray // The indices of the states each history enters, with repeats. histories: ReadonlyArray> } @@ -54,11 +62,14 @@ type Failure = { unfixed: ReadonlyArray } type Verdict = { + // The states whose reach before the first history threw, in call order. + rejected: ReadonlyArray counts: ReadonlyMap failure: Failure | undefined } -// The grammar: two to four states, and up to six histories over them. +// The grammar: two to four states, and up to six histories over them. A +// quarter of the ledgers first reach a state or two before any history. const ledgerArbitrary: fc.Arbitrary = fc .integer({ min: 2, max: 4 }) .chain((stateCount) => @@ -69,6 +80,16 @@ const ledgerArbitrary: fc.Arbitrary = fc ), minimum: fc.integer({ min: 1, max: 3 }), fixedHistories: fc.integer({ min: 0, max: 4 }), + early: fc.oneof( + { arbitrary: fc.constant([]), weight: 3 }, + { + arbitrary: fc.array(fc.integer({ min: 0, max: stateCount - 1 }), { + minLength: 1, + maxLength: 2, + }), + weight: 1, + }, + ), histories: fc.array( fc.array(fc.integer({ min: 0, max: stateCount - 1 }), { maxLength: 4, @@ -78,8 +99,9 @@ const ledgerArbitrary: fc.Arbitrary = fc }), ) -// The model. A history counts once per state it enters, in every run kind. A -// path replay checks nothing. Otherwise a state fails below the minimum, and, +// The model. Every reach before the first history throws and counts nothing. +// A history counts once per state it enters, in every run kind. A path replay +// checks nothing. Otherwise a state fails below the minimum, and, // when fixed histories are declared, a state the first ones did not enter // fails too. function expectedVerdict(ledger: Ledger): Verdict { @@ -104,6 +126,7 @@ function expectedVerdict(ledger: Ledger): Verdict { ) const fails = belowMinimum.size > 0 || unfixed.length > 0 return { + rejected: ledger.early.map((index) => ledger.states[index]!), counts, failure: ledger.run !== `path` && fails ? { belowMinimum, unfixed } : undefined, @@ -152,6 +175,14 @@ async function observeLedger(ledger: Ledger): Promise { fixedHistories: ledger.fixedHistories, }), ) + const rejected: Array = [] + for (const index of ledger.early) { + try { + reach.reach(ledger.states[index]!) + } catch { + rejected.push(ledger.states[index]!) + } + } for (const history of ledger.histories) { reach.beginHistory() for (const index of history) reach.reach(ledger.states[index]!) @@ -162,7 +193,11 @@ async function observeLedger(ledger: Ledger): Promise { } catch (error) { failure = (error as Error).message } - return { counts: new Map(reach.counts()), failure: namedStates(failure) } + return { + rejected, + counts: new Map(reach.counts()), + failure: namedStates(failure), + } } // The states a failure names: `name (count)` below the minimum, and a list of @@ -291,6 +326,7 @@ const reachStates = [ `a fixed history miss that a later history enters`, `a state below a minimum above one`, `a ledger that passes`, + `a reach before the first history`, ] as const // One fixed ledger enters each reach state, first in every run, so this // property's own reach cannot miss by chance. @@ -299,9 +335,17 @@ function fixedLedger( minimum: number, fixedHistories: number, histories: Ledger[`histories`], + early: Ledger[`early`] = [], ): [Ledger, number, Array] { return [ - { run, states: [`state 0`, `state 1`], minimum, fixedHistories, histories }, + { + run, + states: [`state 0`, `state 1`], + minimum, + fixedHistories, + early, + histories, + }, 60, [1], ] @@ -312,6 +356,7 @@ const ledgerExamples = [ fixedLedger(`ordinary`, 1, 1, [[0], [1]]), fixedLedger(`ordinary`, 2, 0, [[0, 1]]), fixedLedger(`ordinary`, 1, 0, [[0, 1]]), + fixedLedger(`ordinary`, 1, 0, [[0, 1]], [0]), ] const ledgerReach = createOracleReach(`oracle.declared-reach`, reachStates, { fixedHistories: ledgerExamples.length, @@ -347,5 +392,7 @@ fcTest.prop( ledgerReach.reach(`a state below a minimum above one`) if (ledger.run !== `path` && failure === undefined) ledgerReach.reach(`a ledger that passes`) + if (ledger.early.length > 0) + ledgerReach.reach(`a reach before the first history`) }, ) diff --git a/packages/db/tests/oracle-reach.ts b/packages/db/tests/oracle-reach.ts index 2a88430713..b7789dd498 100644 --- a/packages/db/tests/oracle-reach.ts +++ b/packages/db/tests/oracle-reach.ts @@ -9,7 +9,8 @@ import { readOracleRunConfig } from './oracle-config.js' * produces that state. Counting passing runs does not show reach. * * A property declares the states its laws depend on. Its driver calls - * `reach(state)` when a history enters one. After the property ran, + * `reach(state)` when a history enters one. A call before the first + * `beginHistory()` throws: it is a driver error, not a history. After the property ran, * `assertReached()` fails for every declared state that fewer than `minimum` * histories entered. A history counts once per state, however often it * enters it. @@ -17,7 +18,9 @@ import { readOracleRunConfig } from './oracle-config.js' * A property that runs fixed examples first, through `oraclePropertyOptions`' * `examples`, passes their number as `fixedHistories`. The check then also * fails for every declared state that those first histories did not enter: - * that state's reach would depend on the seed (#2287). + * that state's reach would depend on the seed (#2287). The first histories + * are the examples only when the reach belongs to that one property and its + * callback begins every history, so such a reach is not shared. * * A path replay checks one recorded history, not reach, so the check does * nothing then. A seed alone reseeds the whole campaign, which runs its full @@ -52,8 +55,12 @@ export function createOracleReach( if (!counts.has(state)) { throw new Error(`${property}: undeclared reach state ${state}`) } - if (histories > 0 && histories <= fixedHistories) - enteredByFixed.add(state) + if (histories === 0) { + throw new Error( + `${property}: reach(${state}) came before the first beginHistory()`, + ) + } + if (histories <= fixedHistories) enteredByFixed.add(state) if (current.has(state)) return current.add(state) counts.set(state, counts.get(state)! + 1) From 231298b85abe7b6a447820bb438846f6317a9c8a Mon Sep 17 00:00:00 2001 From: Test Date: Thu, 29 Oct 2026 09:45:43 -0600 Subject: [PATCH 10/12] test(db): report a stopped run, and check property options When a failure stopped a run inside its fixed examples, the reach check blamed seed dependence and minimum misses for states that the unrun examples would have entered. It now reports only that k of n fixed histories ran. The declared-reach model states this rule; the oracle failed on the parent's message and now passes. The oracle also drives oraclePropertyOptions under the process's own replay selection and multiplier, which a dropped `examples` option or an ignored multiplier now fails. A new run kind, a path replay of another property, records the existing rule that a path replay turns off every reach check in its process: a reach need not carry its property's name. Docs record that limit and the two conventions for fast-check examples. Co-authored-by: Isaac --- docs/contributing/oracle-coverage.md | 10 +- .../declared-reach-oracle.property.test.ts | 177 +++++++++++++----- packages/db/tests/oracle-config.ts | 4 +- packages/db/tests/oracle-reach.ts | 17 +- 4 files changed, 154 insertions(+), 54 deletions(-) diff --git a/docs/contributing/oracle-coverage.md b/docs/contributing/oracle-coverage.md index 643aaf02a7..c5242bbc8d 100644 --- a/docs/contributing/oracle-coverage.md +++ b/docs/contributing/oracle-coverage.md @@ -3766,7 +3766,15 @@ Those properties have not been measured. Destination: #2289. Needed witness: per property, the declared states that no fixed example enters, and how often a normal-budget run misses each one. The oracle does not judge reporter keys, which only a replay witness channel adds, or a reach shared across properties, -which the precondition above rules out but no check detects. +which the precondition above rules out but no check detects. A path replay +turns off every reach check in its process, also for a property that the replay +does not name and that still runs its seeded budget: a reach need not carry its +property's name, so it cannot tell whose replay runs. When a run stops inside +its fixed examples, the check reports only that. When a property fails after +its examples, the check still reports the states that the stopped run missed. +About twenty other properties set fast-check's `examples` inside their base +runs instead of through `oraclePropertyOptions(…, { examples })`; #2289 owns +moving them when it measures their reach. `packages/db/tests/oracle-replay.test.ts` checks every replay manifest owner: from its cwd, the command's files exist, its target is the owner, and a Vitest diff --git a/packages/db/tests/declared-reach-oracle.property.test.ts b/packages/db/tests/declared-reach-oracle.property.test.ts index 07021a9564..6fad2d6855 100644 --- a/packages/db/tests/declared-reach-oracle.property.test.ts +++ b/packages/db/tests/declared-reach-oracle.property.test.ts @@ -7,14 +7,18 @@ * * - The check runs in an ordinary run and in a run with only * `TANSTACK_DB_ORACLE_SEED`: a seed alone reseeds the whole campaign at its - * full budget. Only a path replay, which runs one recorded history, skips - * it. + * full budget. A path replay, which runs one recorded history, skips it. + * It skips it in every reach of that process, also in a property that the + * replay does not name and that still runs its seeded budget: a reach need + * not carry its property's name, so it cannot tell whose replay runs. * - A property can run fixed examples first in every run. With * `fixedHistories: n`, the check also fails for each declared state that * the first n histories, the examples, did not enter. Such a state's reach - * would depend on the seed. The examples come on top of the base run - * budget, so they never displace a random history. A replay keeps its seed, - * and a path replay keeps its path and still runs one history. + * would depend on the seed. When fewer than n histories ran, a failure + * stopped the run inside the examples, and the check says so instead. The + * examples come on top of the base run budget, so they never displace a + * random history. A replay keeps its seed, and a path replay of the property + * keeps its path and still runs one history. * * The first n histories are the examples only when the reach belongs to one * property and that property's callback begins every history. A driver calls @@ -28,9 +32,9 @@ * minimum, a number of fixed histories, the states each history enters, and * the states reached before the first history. * The drivers run `createOracleReach`, `runOracleCampaign`, and - * `oracleRandomParameters` under that run kind's environment, and the checks - * compare counts, the failure, and the states the failure names with the - * model. + * `oracleRandomParameters` under that run kind's environment, and + * `oraclePropertyOptions` under the process's own. The checks compare counts, + * the failure, and the states the failure names with the model. */ import { fc, test as fcTest } from '@fast-check/vitest' import { afterAll, expect, vi } from 'vitest' @@ -44,7 +48,9 @@ import { declareOracle } from './oracle-declaration.js' const property = `oracle.declared-reach` -type RunKind = `ordinary` | `seed` | `path` +// `other-path` is a path replay of another property, in the same process. +type RunKind = `ordinary` | `seed` | `path` | `other-path` +const otherProperty = `lint.part-reach` type Ledger = { run: RunKind states: ReadonlyArray @@ -60,6 +66,8 @@ type Ledger = { type Failure = { belowMinimum: ReadonlyMap unfixed: ReadonlyArray + // How many histories ran, when fewer than the fixed ones did. + stoppedAt?: number } type Verdict = { // The states whose reach before the first history threw, in call order. @@ -74,7 +82,7 @@ const ledgerArbitrary: fc.Arbitrary = fc .integer({ min: 2, max: 4 }) .chain((stateCount) => fc.record({ - run: fc.constantFrom(`ordinary`, `seed`, `path`), + run: fc.constantFrom(`ordinary`, `seed`, `path`, `other-path`), states: fc.constant( Array.from({ length: stateCount }, (_, index) => `state ${index}`), ), @@ -101,9 +109,10 @@ const ledgerArbitrary: fc.Arbitrary = fc // The model. Every reach before the first history throws and counts nothing. // A history counts once per state it enters, in every run kind. A path replay -// checks nothing. Otherwise a state fails below the minimum, and, -// when fixed histories are declared, a state the first ones did not enter -// fails too. +// of any property checks nothing. Otherwise a state fails below the minimum. +// When fixed histories are declared, a state the first ones did not enter +// fails too, unless fewer histories ran than the fixed ones: then a failure +// stopped the run, and the check names how many histories ran, and no state. function expectedVerdict(ledger: Ledger): Verdict { const entered = ledger.histories.map( (history) => new Set(history.map((index) => ledger.states[index]!)), @@ -118,18 +127,22 @@ function expectedVerdict(ledger: Ledger): Verdict { const belowMinimum = new Map( [...counts].filter(([, count]) => count < ledger.minimum), ) + const stopped = ledger.histories.length < ledger.fixedHistories const unfixed = - ledger.fixedHistories === 0 + ledger.fixedHistories === 0 || stopped ? [] : ledger.states.filter((state) => fixed.every((history) => !history.has(state)), ) - const fails = belowMinimum.size > 0 || unfixed.length > 0 + const failure: Failure = stopped + ? { belowMinimum: new Map(), unfixed, stoppedAt: ledger.histories.length } + : { belowMinimum, unfixed } + const fails = belowMinimum.size > 0 || unfixed.length > 0 || stopped + const checked = ledger.run === `ordinary` || ledger.run === `seed` return { rejected: ledger.early.map((index) => ledger.states[index]!), counts, - failure: - ledger.run !== `path` && fails ? { belowMinimum, unfixed } : undefined, + failure: checked && fails ? failure : undefined, } } @@ -140,7 +153,7 @@ function runEnvironment(run: RunKind): Record { return { TANSTACK_DB_ORACLE_SEED: `1`, TANSTACK_DB_ORACLE_PATH: `0`, - TANSTACK_DB_ORACLE_PROPERTY: property, + TANSTACK_DB_ORACLE_PROPERTY: run === `path` ? property : otherProperty, } } @@ -201,12 +214,16 @@ async function observeLedger(ledger: Ledger): Promise { } // The states a failure names: `name (count)` below the minimum, and a list of -// names for the fixed histories. +// names for the fixed histories, or how many histories ran. function namedStates(failure: string | undefined): Failure | undefined { if (failure === undefined) return undefined const below = /not enforced there: (.*)$/m.exec(failure)?.[1] const unfixed = /reach depends on the seed: (.*)$/m.exec(failure)?.[1] + const stoppedAt = /only (\d+) of its \d+ fixed histories ran/.exec( + failure, + )?.[1] return { + ...(stoppedAt === undefined ? {} : { stoppedAt: Number(stoppedAt) }), belowMinimum: new Map( (below?.split(`, `) ?? []).map((entry) => { const match = /^(.*) \((\d+)\)$/.exec(entry)! @@ -225,8 +242,12 @@ async function checkLedger(ledger: Ledger) { } // The campaign runner's replay prefix, and the environment each run kind sets -// for it. +// for it. The runner reads only its own prefix, so a replay of another +// property is an ordinary run for it. const campaignPrefix = `TANSTACK_DB_REACH_LEDGER` +function campaignRun(run: RunKind): RunKind { + return run === `other-path` ? `ordinary` : run +} function campaignEnvironment(run: RunKind): Record { if (run === `ordinary`) return {} if (run === `seed`) return { [`${campaignPrefix}_SEED`]: `1` } @@ -237,7 +258,7 @@ function campaignEnvironment(run: RunKind): Record { function observeCampaign(ledger: Ledger): Promise { return withEnvironment( [`${campaignPrefix}_SEED`, `${campaignPrefix}_PATH`], - campaignEnvironment(ledger.run), + campaignEnvironment(campaignRun(ledger.run)), async () => { // The runner reports each campaign's counts on the console. const info = vi.spyOn(console, `info`).mockImplementation(() => {}) @@ -263,6 +284,7 @@ function observeCampaign(ledger: Ledger): Promise { async function checkCampaign(ledger: Ledger) { const { failure } = expectedVerdict({ ...ledger, + run: campaignRun(ledger.run), minimum: 1, fixedHistories: 0, }) @@ -272,45 +294,89 @@ async function checkCampaign(ledger: Ledger) { } // The run parameters: the examples come on top of the base runs, and the -// replay selection stays. A seed replay keeps its seed. A path replay of this -// property keeps its seed and path, and runs one history. A replay witness -// channel adds reporter keys; no run kind here opens one, so the check leaves -// them out. +// replay selection stays. A seed replay keeps its seed, as does a path replay +// of another property. A path replay of this property keeps its seed and path, +// and runs one history. A replay witness channel adds reporter keys; no run +// kind here opens one, so the check leaves them out. +type Selection = { run: RunKind; seed: number; path: string } function expectedRunParameters( - run: RunKind, + { run, seed, path }: Selection, baseRuns: number, examples: ReadonlyArray, ) { - if (run === `ordinary`) - return { numRuns: baseRuns + examples.length, examples } - if (run === `seed`) - return { numRuns: baseRuns + examples.length, seed: 1, examples } - return { numRuns: 1, seed: 1, path: `0`, examples } + const numRuns = run === `path` ? 1 : baseRuns + examples.length + if (run === `ordinary`) return { numRuns, examples } + if (run === `path`) return { numRuns, seed, path, examples } + return { numRuns, seed, examples } } +// oraclePropertyOptions reads the process's replay selection and multiplier +// once, at load. The model reads the same variables on its own. +const processEnvironment = process.env +const processSelection: Selection = { + run: + processEnvironment.TANSTACK_DB_ORACLE_PATH !== undefined + ? processEnvironment.TANSTACK_DB_ORACLE_PROPERTY === property + ? `path` + : `other-path` + : processEnvironment.TANSTACK_DB_ORACLE_SEED === undefined + ? `ordinary` + : `seed`, + seed: Number(processEnvironment.TANSTACK_DB_ORACLE_SEED), + path: processEnvironment.TANSTACK_DB_ORACLE_PATH ?? ``, +} +const processMultiplier = Number( + processEnvironment.TANSTACK_DB_ORACLE_RUNS_MULTIPLIER ?? `1`, +) + function checkRunParameters( run: RunKind, baseRuns: number, examples: ReadonlyArray, ) { - const { - numRuns, - seed, - path, - examples: observed, - } = oracleRandomParameters( - baseRuns, - run === `ordinary` - ? undefined - : run === `seed` - ? { replaySeed: 1, replayPath: undefined, replayProperty: undefined } - : { replaySeed: 1, replayPath: `0`, replayProperty: property }, - property, - examples, - ) + const project = (parameters: { + numRuns: number + seed?: number + path?: string + examples?: ReadonlyArray + }) => ({ + numRuns: parameters.numRuns, + seed: parameters.seed, + path: parameters.path, + examples: parameters.examples, + }) + const replayed = run === `path` ? property : otherProperty // toEqual treats an undefined key as absent. - expect({ numRuns, seed, path, examples: observed }, `run parameters`).toEqual( - expectedRunParameters(run, baseRuns, examples), + expect( + project( + oracleRandomParameters( + baseRuns, + run === `ordinary` + ? undefined + : run === `seed` + ? { + replaySeed: 1, + replayPath: undefined, + replayProperty: undefined, + } + : { replaySeed: 1, replayPath: `0`, replayProperty: replayed }, + property, + examples, + ), + ), + `run parameters`, + ).toEqual( + expectedRunParameters({ run, seed: 1, path: `0` }, baseRuns, examples), + ) + expect( + project(oraclePropertyOptions(baseRuns, property, { examples })), + `property options under this process`, + ).toEqual( + expectedRunParameters( + processSelection, + baseRuns * processMultiplier, + examples, + ), ) } @@ -327,6 +393,8 @@ const reachStates = [ `a state below a minimum above one`, `a ledger that passes`, `a reach before the first history`, + `a path replay of another property with a state below the minimum`, + `a run that stopped inside the fixed histories`, ] as const // One fixed ledger enters each reach state, first in every run, so this // property's own reach cannot miss by chance. @@ -357,6 +425,8 @@ const ledgerExamples = [ fixedLedger(`ordinary`, 2, 0, [[0, 1]]), fixedLedger(`ordinary`, 1, 0, [[0, 1]]), fixedLedger(`ordinary`, 1, 0, [[0, 1]], [0]), + fixedLedger(`other-path`, 1, 0, []), + fixedLedger(`ordinary`, 1, 3, [[0, 1]]), ] const ledgerReach = createOracleReach(`oracle.declared-reach`, reachStates, { fixedHistories: ledgerExamples.length, @@ -384,13 +454,22 @@ fcTest.prop( const ordinary = expectedVerdict({ ...ledger, run: `ordinary` }).failure if (ledger.run === `path` && (ordinary?.belowMinimum.size ?? 0) > 0) ledgerReach.reach(`a path replay with a state below the minimum`) + if (ledger.run === `other-path` && (ordinary?.belowMinimum.size ?? 0) > 0) + ledgerReach.reach( + `a path replay of another property with a state below the minimum`, + ) + if (failure?.stoppedAt !== undefined) + ledgerReach.reach(`a run that stopped inside the fixed histories`) if (ledger.run === `seed` && (failure?.belowMinimum.size ?? 0) > 0) ledgerReach.reach(`a seed-only run fails below the minimum`) if (failure?.unfixed.some((state) => (counts.get(state) ?? 0) > 0)) ledgerReach.reach(`a fixed history miss that a later history enters`) if (ledger.minimum > 1 && (failure?.belowMinimum.size ?? 0) > 0) ledgerReach.reach(`a state below a minimum above one`) - if (ledger.run !== `path` && failure === undefined) + if ( + (ledger.run === `ordinary` || ledger.run === `seed`) && + failure === undefined + ) ledgerReach.reach(`a ledger that passes`) if (ledger.early.length > 0) ledgerReach.reach(`a reach before the first history`) diff --git a/packages/db/tests/oracle-config.ts b/packages/db/tests/oracle-config.ts index 00ebc1881a..e4d07ff31f 100644 --- a/packages/db/tests/oracle-config.ts +++ b/packages/db/tests/oracle-config.ts @@ -810,7 +810,9 @@ export function oracleRuns(baseRuns: number): number { /** * Replays broad randomized properties when a campaign seed is supplied. - * `examples` run first in every run, on top of the base runs. + * `examples` run first in every run, on top of the base runs. A site that + * spreads these options and sets fast-check's `examples` itself runs them + * inside the base runs instead, so they displace random histories. */ export function oraclePropertyOptions( baseRuns: number, diff --git a/packages/db/tests/oracle-reach.ts b/packages/db/tests/oracle-reach.ts index b7789dd498..8db1edecb4 100644 --- a/packages/db/tests/oracle-reach.ts +++ b/packages/db/tests/oracle-reach.ts @@ -20,11 +20,15 @@ import { readOracleRunConfig } from './oracle-config.js' * fails for every declared state that those first histories did not enter: * that state's reach would depend on the seed (#2287). The first histories * are the examples only when the reach belongs to that one property and its - * callback begins every history, so such a reach is not shared. + * callback begins every history, so such a reach is not shared. When fewer + * histories ran than the fixed ones, a failure stopped the run inside the + * examples, and the check reports only that, without naming states. * * A path replay checks one recorded history, not reach, so the check does - * nothing then. A seed alone reseeds the whole campaign, which runs its full - * budget, so its reach is checked like an ordinary run's. + * nothing then, in every reach of that process: a reach need not carry its + * property's name, so it cannot tell whose replay runs. A seed alone reseeds + * the whole campaign, which runs its full budget, so its reach is checked like + * an ordinary run's. * `packages/db/tests/declared-reach-oracle.property.test.ts` owns these rules. */ export function createOracleReach( @@ -72,6 +76,13 @@ export function createOracleReach( /** Fails for each declared state that too few histories entered. */ assertReached(): void { if (replaying) return + if (histories < fixedHistories) { + throw new Error( + `${property}: only ${histories} of its ${fixedHistories} fixed ` + + `histories ran, so a failure stopped the run inside the fixed ` + + `examples`, + ) + } const missed = [...counts] .filter(([, count]) => count < minimum) .map(([state, count]) => `${state} (${count})`) From 590588a659e32158793f5065d4d7f68250fc9567 Mon Sep 17 00:00:00 2001 From: Test Date: Thu, 29 Oct 2026 11:04:15 -0600 Subject: [PATCH 11/12] test(db): mark fixed histories, validate reach options, check campaigns Law discovery over the reach machinery found rules that no oracle stated. The declared-reach oracle now generates and checks them, and each failed on the parent before the change: - A property marks each example's history with beginHistory({ fixed: true }), because fast-check passes an example's input by reference. Fixed reach no longer depends on a history's position, so another test may share the reach, as main's source-health.required-history does. Shrinking can run an example again, so an extra fixed history counts as fixed. An earlier draft threw for it, and that error replaced the original failure while fast-check shrank. - Options that cannot describe a reach throw: a minimum below one, a fractional or negative fixed count, a state declared twice. adapter.handler-types declared each state six times on purpose; it now declares each once, with the same counts. The oracle also now generates undeclared reaches, an explicit replaying option, a fixed campaign seed, and invalid campaign environments. It observes the parameters runOracleCampaign passes to each campaign and its ORACLE_REACH lines. All 23 hostile mutants of the machinery fail at an assertion. Co-authored-by: Isaac --- docs/contributing/oracle-coverage.md | 90 +-- .../declared-reach-oracle.property.test.ts | 562 +++++++++++++----- .../mutation-handler-types-oracle.test.ts | 20 +- packages/db/tests/oracle-reach.ts | 49 +- .../db/tests/source-health-oracle.test.ts | 13 +- 5 files changed, 526 insertions(+), 208 deletions(-) diff --git a/docs/contributing/oracle-coverage.md b/docs/contributing/oracle-coverage.md index c5242bbc8d..e87e9cf880 100644 --- a/docs/contributing/oracle-coverage.md +++ b/docs/contributing/oracle-coverage.md @@ -3740,41 +3740,63 @@ checkout, or a worktree branch that has no copy of the script. In that last case the launch checkout's rule lints the worktree. `packages/db/tests/declared-reach-oracle.property.test.ts` -(`oracle.declared-reach`) owns when `createOracleReach` (ORC-015) checks reach, -and what fixed examples prove. By default the check runs in an ordinary run and -in a run with only `TANSTACK_DB_ORACLE_SEED`, which reseeds the whole campaign -at its full budget. Only a path replay, which runs one recorded history, skips -it. A property can run fixed examples first in every run, through -`oraclePropertyOptions(…, { examples })`. The examples come on top of the base -run budget, so they never displace a random history. With `fixedHistories`, -the check also fails for each declared state that the examples did not enter. -The examples are the first histories, so such a reach belongs to one property, -and only that property's callback begins its histories. A `reach()` call before -the first history throws and counts nothing. A replay keeps its seed, and a -path replay keeps its path. The `source-health.on-demand` and -`source-health.lazy-demand` properties run each reach prefix, and each driver -option that a declared state needs, as examples, so their reach does not depend -on the seed (#2287). `source-health.history` gets the same guarantee from +(`oracle.declared-reach`) owns what `createOracleReach` (ORC-015) counts, when +it checks reach, and what fixed examples prove. It also owns the run +parameters that `oracleRandomParameters` and `oraclePropertyOptions` return, +and the campaigns that `runOracleCampaign` in +`packages/db/tests/oracle-campaign.ts` runs. + +- A history counts once per declared state it enters. A `reach()` call for an + undeclared state, or before the first history, throws and counts nothing. + Options that cannot describe a reach (a minimum below one, a fractional or + negative number of fixed histories, a state declared twice) throw. +- The check runs in an ordinary run and in a run with only + `TANSTACK_DB_ORACLE_SEED`, which reseeds the whole campaign at its full + budget. A path replay, which runs one recorded history, skips it in every + reach of its process: a reach need not carry its property's name, so it + cannot tell whose replay runs. An explicit `replaying` option overrides the + environment. +- A property can run fixed examples first in every run, through + `oraclePropertyOptions(…, { examples })`, on top of the base run budget. It + declares their number as `fixedHistories` and begins each example's history + with `beginHistory({ fixed: true })`, which it can do because fast-check + passes an example's input by reference. The check then also fails for each + declared state that no fixed history entered. Fixedness belongs to the + history, so another test may share the reach. Shrinking can run an example + again, so an extra fixed history counts as fixed. When fewer fixed histories + ran than were declared, the check reports only that. +- A replay keeps its seed, and a path replay of the property keeps its path + and runs one history. `runOracleCampaign` runs a fixed-seed and a random + campaign without a prefix seed, one replay campaign with one, passes each + its parameters, and reports each passing campaign on one `ORACLE_REACH` + line. An invalid prefix environment throws. + +The `source-health.on-demand` and `source-health.lazy-demand` properties run +each reach prefix, and each driver option that a declared state needs, as +examples, so their reach does not depend on the seed (#2287). +`source-health.history` gets the same guarantee from `source-health.required-history`, which runs every reach prefix in each -campaign and shares its reach without fixed histories. The oracle generates ledgers over two to four states, up to -six histories, minimums up to three, up to four fixed histories, and reaches -before the first history, under the three run kinds. It also drives `runOracleCampaign` in -`packages/db/tests/oracle-campaign.ts`, whose seed-only run of its own replay -prefix checks reach in the same way. A declared state of another property that -only random histories reach can still miss by chance at the normal budget. -Those properties have not been measured. Destination: #2289. Needed witness: -per property, the declared states that no fixed example enters, and how often a -normal-budget run misses each one. The oracle does not judge reporter keys, -which only a replay witness channel adds, or a reach shared across properties, -which the precondition above rules out but no check detects. A path replay -turns off every reach check in its process, also for a property that the replay -does not name and that still runs its seeded budget: a reach need not carry its -property's name, so it cannot tell whose replay runs. When a run stops inside -its fixed examples, the check reports only that. When a property fails after -its examples, the check still reports the states that the stopped run missed. -About twenty other properties set fast-check's `examples` inside their base -runs instead of through `oraclePropertyOptions(…, { examples })`; #2289 owns -moving them when it measures their reach. +campaign and shares its reach without fixed histories. The oracle generates +ledgers over two to four states, up to six histories with fixed marks, +minimums up to three, up to four declared fixed histories, invalid options, +undeclared and early reaches, an optional `replaying` option, a fixed campaign +seed, and invalid campaign environments, under four run kinds: ordinary, +seed-only, and path replays of the property and of another property. + +Limits. A declared state of another property that only random histories +reach can still miss by chance at the normal budget. Those properties have not +been measured, about twenty set fast-check's `examples` inside their base runs +instead of through the option, and a `runOracleCampaign` reach cannot declare +fixed histories. Destination: #2289. Needed witness: per property, the declared +states that no fixed example enters, and how often a normal-budget run misses +each one. A path replay also skips reach in a property that the replay does not +name and that still runs its seeded budget. When a property fails after its +examples, the check still reports the states that the stopped run missed. The +oracle does not judge reporter keys, which only a replay witness channel adds, +the rejection of an unregistered property, or the compile-time rule that a call +without examples returns parameters without an `examples` key; type-aware +lint in every package that infers from these parameters is that rule's only +witness. `packages/db/tests/oracle-replay.test.ts` checks every replay manifest owner: from its cwd, the command's files exist, its target is the owner, and a Vitest diff --git a/packages/db/tests/declared-reach-oracle.property.test.ts b/packages/db/tests/declared-reach-oracle.property.test.ts index 6fad2d6855..939195b898 100644 --- a/packages/db/tests/declared-reach-oracle.property.test.ts +++ b/packages/db/tests/declared-reach-oracle.property.test.ts @@ -3,38 +3,48 @@ * * A generated property declares the states its laws depend on, and * `createOracleReach` fails a run in which too few histories entered one. - * Two rules decide when that check runs and what it proves (#2287): + * These rules decide what a reach counts, when its check runs, and what the + * check proves (#2287): * - * - The check runs in an ordinary run and in a run with only + * - A history counts once per declared state it enters. A `reach()` call for + * an undeclared state, or before the first `beginHistory()`, is a driver + * error: it throws and counts nothing. Options that cannot describe a reach + * (a minimum below one, a fractional or negative number of fixed + * histories, a state declared twice) throw when the reach is created. + * - The check fails for each state that fewer than `minimum` histories + * entered. It runs in an ordinary run and in a run with only * `TANSTACK_DB_ORACLE_SEED`: a seed alone reseeds the whole campaign at its - * full budget. A path replay, which runs one recorded history, skips it. - * It skips it in every reach of that process, also in a property that the - * replay does not name and that still runs its seeded budget: a reach need - * not carry its property's name, so it cannot tell whose replay runs. - * - A property can run fixed examples first in every run. With - * `fixedHistories: n`, the check also fails for each declared state that - * the first n histories, the examples, did not enter. Such a state's reach - * would depend on the seed. When fewer than n histories ran, a failure - * stopped the run inside the examples, and the check says so instead. The - * examples come on top of the base run budget, so they never displace a - * random history. A replay keeps its seed, and a path replay of the property - * keeps its path and still runs one history. + * full budget. A path replay, which runs one recorded history, skips it in + * every reach of that process, also in a property that the replay does not + * name: a reach need not carry its property's name, so it cannot tell whose + * replay runs. An explicit `replaying` option overrides the environment. + * - A property can run fixed examples first in every run. It declares their + * number as `fixedHistories: n` and begins each example's history with + * `beginHistory({ fixed: true })`. The check then also fails for each state + * that no fixed history entered: such a state's reach would depend on the + * seed. Fixedness belongs to the history, not to its position, so another + * test may share the reach. Shrinking can run an example again, so a fixed + * history beyond the n declared ones counts as a fixed history too. When + * fewer than n fixed histories ran, a failure stopped the run inside the + * examples, and the check reports only that. + * - The examples come on top of the base run budget, so they never displace + * a random history. A replay keeps its seed, and a path replay of the + * property keeps its path and still runs one history. * - * The first n histories are the examples only when the reach belongs to one - * property and that property's callback begins every history. A driver calls - * `reach(state)` inside a history: a call before the first `beginHistory()` - * is a driver error, so it throws and counts nothing. + * `runOracleCampaign` runs a fixed-seed and a random campaign, each with its + * own reach and a minimum of one. A seed-only run of its replay prefix runs one + * campaign with that seed and checks its reach; a seed and path run one + * recorded history and check none. Each campaign that passes reports its + * counts on one `ORACLE_REACH` line. An invalid prefix environment throws. * - * `runOracleCampaign` follows the first rule for its own replay prefix: a - * seed-only run of its campaign checks reach, and only a path replay skips it. - * - * The model below states these rules over a generated ledger: a run kind, a - * minimum, a number of fixed histories, the states each history enters, and - * the states reached before the first history. - * The drivers run `createOracleReach`, `runOracleCampaign`, and + * The model below states these rules over a generated ledger: a run kind, an + * optional `replaying` override, the options, the states reached before the + * first history, each history with its fixed mark and the states it enters, + * the campaign runner's fixed seed, and an optional invalid campaign + * environment. The drivers run `createOracleReach`, `runOracleCampaign`, and * `oracleRandomParameters` under that run kind's environment, and - * `oraclePropertyOptions` under the process's own. The checks compare counts, - * the failure, and the states the failure names with the model. + * `oraclePropertyOptions` under the process's own. Each check compares one + * whole observation with the model. */ import { fc, test as fcTest } from '@fast-check/vitest' import { afterAll, expect, vi } from 'vitest' @@ -51,98 +61,177 @@ const property = `oracle.declared-reach` // `other-path` is a path replay of another property, in the same process. type RunKind = `ordinary` | `seed` | `path` | `other-path` const otherProperty = `lint.part-reach` +type CampaignFault = `bad-seed` | `path-without-seed` | `bad-path` +type LedgerHistory = { + fixed: boolean + // The indices of the states it enters, with repeats. The index equal to + // the number of declared states names an undeclared one. + states: ReadonlyArray +} type Ledger = { run: RunKind + replaying: boolean | undefined states: ReadonlyArray minimum: number fixedHistories: number // The indices of the states reached before the first history. early: ReadonlyArray - // The indices of the states each history enters, with repeats. - histories: ReadonlyArray> + histories: ReadonlyArray + fixedSeed: number + campaignFault: CampaignFault | undefined } // The states a failing reach check names, and an absent failure when the check // passes or does not run. type Failure = { belowMinimum: ReadonlyMap unfixed: ReadonlyArray - // How many histories ran, when fewer than the fixed ones did. + // How many fixed histories ran, when fewer than the declared ones did. stoppedAt?: number } +type Rejection = readonly [string, `undeclared` | `early`] type Verdict = { - // The states whose reach before the first history threw, in call order. - rejected: ReadonlyArray + // Whether creating the reach threw. + invalid: boolean + // The reach calls that threw, in call order. + rejected: ReadonlyArray counts: ReadonlyMap failure: Failure | undefined } -// The grammar: two to four states, and up to six histories over them. A -// quarter of the ledgers first reach a state or two before any history. +const stateName = (index: number) => `state ${index}` + +// The grammar: two to four states, and up to six histories over them. About +// one ledger in twenty has each kind of invalid option, a quarter reach a +// state or two before any history, and about one reach in ten names an +// undeclared state. const ledgerArbitrary: fc.Arbitrary = fc .integer({ min: 2, max: 4 }) - .chain((stateCount) => - fc.record({ + .chain((stateCount) => { + const names = Array.from({ length: stateCount }, (_, index) => + stateName(index), + ) + const reachIndex = fc.oneof( + { arbitrary: fc.integer({ min: 0, max: stateCount - 1 }), weight: 9 }, + { arbitrary: fc.constant(stateCount), weight: 1 }, + ) + const mostly = (valid: fc.Arbitrary, invalid: fc.Arbitrary) => + fc.oneof( + { arbitrary: valid, weight: 19 }, + { arbitrary: invalid, weight: 1 }, + ) + return fc.record({ run: fc.constantFrom(`ordinary`, `seed`, `path`, `other-path`), - states: fc.constant( - Array.from({ length: stateCount }, (_, index) => `state ${index}`), + replaying: fc.oneof( + { arbitrary: fc.constant(undefined), weight: 3 }, + { arbitrary: fc.boolean(), weight: 1 }, + ), + states: mostly(fc.constant(names), fc.constant([...names, names[0]!])), + minimum: mostly( + fc.integer({ min: 1, max: 3 }), + fc.constantFrom(0, -1, 1.5), + ), + fixedHistories: mostly( + fc.integer({ min: 0, max: 4 }), + fc.constantFrom(-1, 0.5), ), - minimum: fc.integer({ min: 1, max: 3 }), - fixedHistories: fc.integer({ min: 0, max: 4 }), early: fc.oneof( { arbitrary: fc.constant([]), weight: 3 }, { - arbitrary: fc.array(fc.integer({ min: 0, max: stateCount - 1 }), { - minLength: 1, - maxLength: 2, - }), + arbitrary: fc.array(reachIndex, { minLength: 1, maxLength: 2 }), weight: 1, }, ), histories: fc.array( - fc.array(fc.integer({ min: 0, max: stateCount - 1 }), { - maxLength: 4, + fc.record({ + fixed: fc.boolean(), + states: fc.array(reachIndex, { maxLength: 4 }), }), { maxLength: 6 }, ), - }), - ) + fixedSeed: fc.integer(), + campaignFault: mostly( + fc.constant(undefined), + fc.constantFrom( + `bad-seed`, + `path-without-seed`, + `bad-path`, + ), + ), + }) + }) -// The model. Every reach before the first history throws and counts nothing. -// A history counts once per state it enters, in every run kind. A path replay -// of any property checks nothing. Otherwise a state fails below the minimum. -// When fixed histories are declared, a state the first ones did not enter -// fails too, unless fewer histories ran than the fixed ones: then a failure -// stopped the run, and the check names how many histories ran, and no state. +// The model. Invalid options throw before any history. A reach call for an +// undeclared state, or before the first history, throws and counts nothing. +// Every fixed history counts as fixed, also one beyond the declared number, +// which shrinking runs again. A history counts once per declared state it +// enters. +// A path replay of any property checks nothing, unless an explicit +// `replaying: false` says otherwise. Otherwise a state fails below the +// minimum, and, when fixed histories are declared, a state that no fixed +// history entered fails too. When fewer fixed histories ran than were +// declared, a failure stopped the run, and the check names how many ran and +// no state. function expectedVerdict(ledger: Ledger): Verdict { - const entered = ledger.histories.map( - (history) => new Set(history.map((index) => ledger.states[index]!)), - ) + const valid = + Number.isInteger(ledger.minimum) && + ledger.minimum >= 1 && + Number.isInteger(ledger.fixedHistories) && + ledger.fixedHistories >= 0 && + new Set(ledger.states).size === ledger.states.length + if (!valid) { + return { + invalid: true, + rejected: [], + counts: new Map(), + failure: undefined, + } + } + const declared = new Set(ledger.states) + const rejected: Array = ledger.early.map((index) => [ + stateName(index), + declared.has(stateName(index)) ? `early` : `undeclared`, + ]) + let fixedBegun = 0 + const begun: Array<{ fixed: boolean; entered: Set }> = [] + for (const history of ledger.histories) { + if (history.fixed) fixedBegun += 1 + const entered = new Set() + for (const index of history.states) { + if (declared.has(stateName(index))) entered.add(stateName(index)) + else rejected.push([stateName(index), `undeclared`]) + } + begun.push({ fixed: history.fixed, entered }) + } const counts = new Map( ledger.states.map((state) => [ state, - entered.filter((history) => history.has(state)).length, + begun.filter(({ entered }) => entered.has(state)).length, ]), ) - const fixed = entered.slice(0, ledger.fixedHistories) + const stopped = fixedBegun < ledger.fixedHistories const belowMinimum = new Map( [...counts].filter(([, count]) => count < ledger.minimum), ) - const stopped = ledger.histories.length < ledger.fixedHistories const unfixed = - ledger.fixedHistories === 0 || stopped + ledger.fixedHistories === 0 ? [] : ledger.states.filter((state) => - fixed.every((history) => !history.has(state)), + begun.every(({ fixed, entered }) => !fixed || !entered.has(state)), ) - const failure: Failure = stopped - ? { belowMinimum: new Map(), unfixed, stoppedAt: ledger.histories.length } - : { belowMinimum, unfixed } - const fails = belowMinimum.size > 0 || unfixed.length > 0 || stopped - const checked = ledger.run === `ordinary` || ledger.run === `seed` + const failure: Failure | undefined = stopped + ? { belowMinimum: new Map(), unfixed: [], stoppedAt: fixedBegun } + : belowMinimum.size > 0 || unfixed.length > 0 + ? { belowMinimum, unfixed } + : undefined + const checked = + ledger.replaying === undefined + ? ledger.run === `ordinary` || ledger.run === `seed` + : !ledger.replaying return { - rejected: ledger.early.map((index) => ledger.states[index]!), + invalid: false, + rejected, counts, - failure: checked && fails ? failure : undefined, + failure: checked ? failure : undefined, } } @@ -179,26 +268,45 @@ const replayNames = [ // The driver: one ledger through createOracleReach. async function observeLedger(ledger: Ledger): Promise { - const reach = await withEnvironment( - replayNames, - runEnvironment(ledger.run), - () => + let reach: ReturnType> + try { + reach = await withEnvironment(replayNames, runEnvironment(ledger.run), () => createOracleReach(`ledger`, ledger.states, { minimum: ledger.minimum, fixedHistories: ledger.fixedHistories, + ...(ledger.replaying === undefined + ? {} + : { replaying: ledger.replaying }), }), - ) - const rejected: Array = [] - for (const index of ledger.early) { + ) + } catch { + return { + invalid: true, + rejected: [], + counts: new Map(), + failure: undefined, + } + } + const rejected: Array = [] + const attempt = (state: string) => { try { - reach.reach(ledger.states[index]!) - } catch { - rejected.push(ledger.states[index]!) + reach.reach(state) + } catch (error) { + const message = (error as Error).message + rejected.push([ + state, + /undeclared reach state/.test(message) + ? `undeclared` + : /before the first beginHistory/.test(message) + ? `early` + : (message as `early`), + ]) } } + for (const index of ledger.early) attempt(stateName(index)) for (const history of ledger.histories) { - reach.beginHistory() - for (const index of history) reach.reach(ledger.states[index]!) + reach.beginHistory({ fixed: history.fixed }) + for (const index of history.states) attempt(stateName(index)) } let failure: string | undefined try { @@ -207,6 +315,7 @@ async function observeLedger(ledger: Ledger): Promise { failure = (error as Error).message } return { + invalid: false, rejected, counts: new Map(reach.counts()), failure: namedStates(failure), @@ -214,7 +323,7 @@ async function observeLedger(ledger: Ledger): Promise { } // The states a failure names: `name (count)` below the minimum, and a list of -// names for the fixed histories, or how many histories ran. +// names for the fixed histories, or how many fixed histories ran. function namedStates(failure: string | undefined): Failure | undefined { if (failure === undefined) return undefined const below = /not enforced there: (.*)$/m.exec(failure)?.[1] @@ -241,37 +350,148 @@ async function checkLedger(ledger: Ledger) { return expected } -// The campaign runner's replay prefix, and the environment each run kind sets -// for it. The runner reads only its own prefix, so a replay of another -// property is an ordinary run for it. +// The campaign runner's replay prefix, and the environment each run kind or +// invalid environment sets for it. The runner reads only its own prefix, so a +// replay of another property is an ordinary run for it. const campaignPrefix = `TANSTACK_DB_REACH_LEDGER` function campaignRun(run: RunKind): RunKind { return run === `other-path` ? `ordinary` : run } -function campaignEnvironment(run: RunKind): Record { +function campaignEnvironment(ledger: Ledger): Record { + const seed = `${campaignPrefix}_SEED` + const path = `${campaignPrefix}_PATH` + if (ledger.campaignFault === `bad-seed`) return { [seed]: `x` } + if (ledger.campaignFault === `path-without-seed`) return { [path]: `0` } + if (ledger.campaignFault === `bad-path`) return { [seed]: `1`, [path]: `a` } + const run = campaignRun(ledger.run) if (run === `ordinary`) return {} - if (run === `seed`) return { [`${campaignPrefix}_SEED`]: `1` } - return { [`${campaignPrefix}_SEED`]: `1`, [`${campaignPrefix}_PATH`]: `0` } + if (run === `seed`) return { [seed]: `1` } + return { [seed]: `1`, [path]: `0` } +} + +type CampaignLine = { + property: string + campaign: string + minimum: number | null + counts: Record +} +type CampaignObservation = { + // The parameters the runner passed to each campaign, in order. + parameters: ReadonlyArray<{ seed?: number; path?: string; numRuns?: number }> + lines: ReadonlyArray + failure: Failure | `invalid environment` | undefined +} + +// The campaign driver replays the ledger's declared reaches, without fixed +// marks or early reaches, and with each state declared once: those rules +// belong to the ledger check above. +function campaignLedger(ledger: Ledger): Ledger { + const states = [...new Set(ledger.states)] + return { + ...ledger, + states, + early: [], + histories: ledger.histories.map((history) => ({ + fixed: false, + states: history.states.filter((index) => index < states.length), + })), + } +} + +// The campaign model: two campaigns without a prefix seed, one replay +// campaign with one. Each campaign has a minimum of one and no fixed +// histories, checks reach unless a path replays it, and reports its counts +// when it passes. The first failing campaign ends the run. +function expectedCampaign(ledger: Ledger): CampaignObservation { + if (ledger.campaignFault !== undefined) { + return { parameters: [], lines: [], failure: `invalid environment` } + } + const run = campaignRun(ledger.run) + const campaigns: ReadonlyArray< + readonly [string, { seed?: number; path?: string; numRuns?: number }] + > = + run === `ordinary` + ? [ + [`fixed`, { seed: ledger.fixedSeed }], + [`random`, {}], + ] + : [ + [ + `replay`, + run === `seed` ? { seed: 1 } : { seed: 1, path: `0`, numRuns: 1 }, + ], + ] + const replayed = campaignLedger(ledger) + const parameters: Array<{ seed?: number; path?: string; numRuns?: number }> = + [] + const lines: Array = [] + for (const [campaign, campaignParameters] of campaigns) { + parameters.push(campaignParameters) + const { counts, failure } = expectedVerdict({ + ...replayed, + minimum: 1, + fixedHistories: 0, + replaying: run === `path`, + }) + if (failure !== undefined) return { parameters, lines, failure } + lines.push({ + property: campaignPrefix, + campaign, + minimum: run === `path` ? null : 1, + counts: Object.fromEntries(counts), + }) + } + return { parameters, lines, failure: undefined } } // The driver: one ledger through each campaign that runOracleCampaign runs. -function observeCampaign(ledger: Ledger): Promise { +function observeCampaign(ledger: Ledger): Promise { + const replayed = campaignLedger(ledger) return withEnvironment( [`${campaignPrefix}_SEED`, `${campaignPrefix}_PATH`], - campaignEnvironment(campaignRun(ledger.run)), + campaignEnvironment(ledger), async () => { + const parameters: Array<{ + seed?: number + path?: string + numRuns?: number + }> = [] // The runner reports each campaign's counts on the console. const info = vi.spyOn(console, `info`).mockImplementation(() => {}) + const lines = () => + info.mock.calls.map( + ([line]) => + JSON.parse( + String(line).replace(/^ORACLE_REACH /, ``), + ) as CampaignLine, + ) try { - await runOracleCampaign(campaignPrefix, ledger.states, (reach) => { - for (const history of ledger.histories) { - reach.beginHistory() - for (const index of history) reach.reach(ledger.states[index]!) - } - }) - return undefined + await runOracleCampaign( + campaignPrefix, + replayed.states, + (reach, campaignParameters) => { + parameters.push(campaignParameters) + for (const history of replayed.histories) { + reach.beginHistory() + for (const index of history.states) { + reach.reach(stateName(index)) + } + } + }, + { fixedSeed: ledger.fixedSeed }, + ) + return { parameters, lines: lines(), failure: undefined } } catch (error) { - return namedStates((error as Error).message) + const message = (error as Error).message + return { + parameters, + lines: lines(), + failure: /_SEED must be an integer|_PATH requires a seed/.test( + message, + ) + ? (`invalid environment` as const) + : namedStates(message), + } } finally { info.mockRestore() } @@ -279,17 +499,10 @@ function observeCampaign(ledger: Ledger): Promise { ) } -// The check: a campaign's reach refines the model with a minimum of one and -// no fixed histories, the campaign runner's own reach. +// The check: the observed campaigns refine the campaign model. async function checkCampaign(ledger: Ledger) { - const { failure } = expectedVerdict({ - ...ledger, - run: campaignRun(ledger.run), - minimum: 1, - fixedHistories: 0, - }) - expect(await observeCampaign(ledger), `campaign reach failure`).toEqual( - failure, + expect(await observeCampaign(ledger), `campaign observation`).toEqual( + expectedCampaign(ledger), ) } @@ -382,7 +595,7 @@ function checkRunParameters( declareOracle({ check: [checkLedger, checkCampaign, checkRunParameters], - model: [expectedVerdict, expectedRunParameters], + model: [expectedVerdict, expectedCampaign, expectedRunParameters], grammar: [ledgerArbitrary], }) @@ -395,39 +608,64 @@ const reachStates = [ `a reach before the first history`, `a path replay of another property with a state below the minimum`, `a run that stopped inside the fixed histories`, + `invalid reach options`, + `a reach of an undeclared state`, + `a replaying option that overrides the environment`, + `a fixed history beyond the declared ones`, + `an unfixed history before the first fixed one`, + `an invalid campaign environment`, ] as const + // One fixed ledger enters each reach state, first in every run, so this // property's own reach cannot miss by chance. -function fixedLedger( - run: RunKind, - minimum: number, - fixedHistories: number, - histories: Ledger[`histories`], - early: Ledger[`early`] = [], -): [Ledger, number, Array] { - return [ - { - run, - states: [`state 0`, `state 1`], - minimum, - fixedHistories, - early, - histories, - }, - 60, - [1], - ] -} +const fixedLedger = ( + overrides: Partial, +): [Ledger, number, Array] => [ + { + run: `ordinary`, + replaying: undefined, + states: [stateName(0), stateName(1)], + minimum: 1, + fixedHistories: 0, + early: [], + histories: [], + fixedSeed: 7, + campaignFault: undefined, + ...overrides, + }, + 60, + [1], +] +const history = (fixed: boolean, ...states: Array) => ({ + fixed, + states, +}) const ledgerExamples = [ - fixedLedger(`seed`, 1, 0, []), - fixedLedger(`path`, 1, 0, []), - fixedLedger(`ordinary`, 1, 1, [[0], [1]]), - fixedLedger(`ordinary`, 2, 0, [[0, 1]]), - fixedLedger(`ordinary`, 1, 0, [[0, 1]]), - fixedLedger(`ordinary`, 1, 0, [[0, 1]], [0]), - fixedLedger(`other-path`, 1, 0, []), - fixedLedger(`ordinary`, 1, 3, [[0, 1]]), + fixedLedger({ run: `seed` }), + fixedLedger({ run: `path` }), + fixedLedger({ + fixedHistories: 1, + histories: [history(true, 0), history(false, 1)], + }), + fixedLedger({ minimum: 2, histories: [history(false, 0, 1)] }), + fixedLedger({ histories: [history(false, 0, 1)] }), + fixedLedger({ early: [0], histories: [history(false, 0, 1)] }), + fixedLedger({ run: `other-path` }), + fixedLedger({ fixedHistories: 3, histories: [history(true, 0, 1)] }), + fixedLedger({ minimum: 0 }), + fixedLedger({ histories: [history(false, 0, 1, 2)] }), + fixedLedger({ replaying: true }), + fixedLedger({ + fixedHistories: 1, + histories: [history(true, 0, 1), history(true, 0)], + }), + fixedLedger({ + fixedHistories: 1, + histories: [history(false, 0), history(true, 0, 1)], + }), + fixedLedger({ campaignFault: `bad-seed`, histories: [history(false, 0, 1)] }), ] +const ledgerExampleInputs = new Set(ledgerExamples.map(([ledger]) => ledger)) const ledgerReach = createOracleReach(`oracle.declared-reach`, reachStates, { fixedHistories: ledgerExamples.length, }) @@ -447,17 +685,40 @@ fcTest.prop( `reach ledgers refine the declared reach model`, async (ledger, baseRuns, examples) => { ledgersRan = true - ledgerReach.beginHistory() - const { counts, failure } = await checkLedger(ledger) + ledgerReach.beginHistory({ fixed: ledgerExampleInputs.has(ledger) }) + const verdict = await checkLedger(ledger) await checkCampaign(ledger) checkRunParameters(ledger.run, baseRuns, examples) - const ordinary = expectedVerdict({ ...ledger, run: `ordinary` }).failure - if (ledger.run === `path` && (ordinary?.belowMinimum.size ?? 0) > 0) + const { counts, failure } = verdict + const ordinary = expectedVerdict({ + ...ledger, + run: `ordinary`, + replaying: undefined, + }).failure + const environmentChecks = ledger.run === `ordinary` || ledger.run === `seed` + if (verdict.invalid) ledgerReach.reach(`invalid reach options`) + if (ledger.campaignFault !== undefined) + ledgerReach.reach(`an invalid campaign environment`) + if (verdict.invalid) return + if ( + ledger.replaying === undefined && + ledger.run === `path` && + (ordinary?.belowMinimum.size ?? 0) > 0 + ) ledgerReach.reach(`a path replay with a state below the minimum`) - if (ledger.run === `other-path` && (ordinary?.belowMinimum.size ?? 0) > 0) + if ( + ledger.replaying === undefined && + ledger.run === `other-path` && + (ordinary?.belowMinimum.size ?? 0) > 0 + ) ledgerReach.reach( `a path replay of another property with a state below the minimum`, ) + if ( + ledger.replaying !== undefined && + ledger.replaying === environmentChecks + ) + ledgerReach.reach(`a replaying option that overrides the environment`) if (failure?.stoppedAt !== undefined) ledgerReach.reach(`a run that stopped inside the fixed histories`) if (ledger.run === `seed` && (failure?.belowMinimum.size ?? 0) > 0) @@ -466,12 +727,19 @@ fcTest.prop( ledgerReach.reach(`a fixed history miss that a later history enters`) if (ledger.minimum > 1 && (failure?.belowMinimum.size ?? 0) > 0) ledgerReach.reach(`a state below a minimum above one`) - if ( - (ledger.run === `ordinary` || ledger.run === `seed`) && - failure === undefined - ) + if (environmentChecks && ledger.replaying === undefined && !failure) ledgerReach.reach(`a ledger that passes`) - if (ledger.early.length > 0) + if (verdict.rejected.some(([, reason]) => reason === `early`)) ledgerReach.reach(`a reach before the first history`) + if (verdict.rejected.some(([, reason]) => reason === `undeclared`)) + ledgerReach.reach(`a reach of an undeclared state`) + if ( + ledger.histories.filter(({ fixed }) => fixed).length > + ledger.fixedHistories + ) + ledgerReach.reach(`a fixed history beyond the declared ones`) + const firstFixed = ledger.histories.findIndex(({ fixed }) => fixed) + if (ledger.fixedHistories > 0 && firstFixed > 0) + ledgerReach.reach(`an unfixed history before the first fixed one`) }, ) diff --git a/packages/db/tests/mutation-handler-types-oracle.test.ts b/packages/db/tests/mutation-handler-types-oracle.test.ts index 6a37d856d1..84b18b6558 100644 --- a/packages/db/tests/mutation-handler-types-oracle.test.ts +++ b/packages/db/tests/mutation-handler-types-oracle.test.ts @@ -306,16 +306,22 @@ function checkHandlerAdmission( ) } -const states = typeShapes.flatMap((shape) => - surfaces.flatMap((surface) => - handlers.flatMap((handler) => - results.map( - (result) => - `${shape.adapter}/${shape.schema ? `schema` : `plain`}/${shape.data}/${surface}/${handler}/${result.name}`, +// A state name leaves out the key and scalar types, so the six shapes that +// differ only there share one state, and `minimum: 6` asks for all of them. +const states = [ + ...new Set( + typeShapes.flatMap((shape) => + surfaces.flatMap((surface) => + handlers.flatMap((handler) => + results.map( + (result) => + `${shape.adapter}/${shape.schema ? `schema` : `plain`}/${shape.data}/${surface}/${handler}/${result.name}`, + ), + ), ), ), ), -) +] const reach = createOracleReach(`adapter.handler-types`, states, { minimum: 6 }) describe(`public handler result admission`, () => { afterAll(() => { diff --git a/packages/db/tests/oracle-reach.ts b/packages/db/tests/oracle-reach.ts index 8db1edecb4..ecf6e43b01 100644 --- a/packages/db/tests/oracle-reach.ts +++ b/packages/db/tests/oracle-reach.ts @@ -9,19 +9,21 @@ import { readOracleRunConfig } from './oracle-config.js' * produces that state. Counting passing runs does not show reach. * * A property declares the states its laws depend on. Its driver calls - * `reach(state)` when a history enters one. A call before the first - * `beginHistory()` throws: it is a driver error, not a history. After the property ran, - * `assertReached()` fails for every declared state that fewer than `minimum` - * histories entered. A history counts once per state, however often it - * enters it. + * `reach(state)` when a history enters one. A call for an undeclared state, or + * before the first `beginHistory()`, throws: it is a driver error, not a + * history. Options that cannot describe a reach throw at creation. After the + * property ran, `assertReached()` fails for every declared state that fewer + * than `minimum` histories entered. A history counts once per state, however + * often it enters it. * * A property that runs fixed examples first, through `oraclePropertyOptions`' - * `examples`, passes their number as `fixedHistories`. The check then also - * fails for every declared state that those first histories did not enter: - * that state's reach would depend on the seed (#2287). The first histories - * are the examples only when the reach belongs to that one property and its - * callback begins every history, so such a reach is not shared. When fewer - * histories ran than the fixed ones, a failure stopped the run inside the + * `examples`, passes their number as `fixedHistories` and begins each + * example's history with `beginHistory({ fixed: true })`. The check then also + * fails for every declared state that no fixed history entered: that state's + * reach would depend on the seed (#2287). Fixedness belongs to the history, so + * other tests may share the reach. Shrinking can run an example again, so a + * fixed history beyond the declared number counts as fixed too. When fewer + * fixed histories ran than were declared, a failure stopped the run inside the * examples, and the check reports only that, without naming states. * * A path replay checks one recorded history, not reach, so the check does @@ -40,17 +42,30 @@ export function createOracleReach( replaying: replayOverride, }: { minimum?: number; fixedHistories?: number; replaying?: boolean } = {}, ) { + if (!Number.isInteger(minimum) || minimum < 1) { + throw new Error(`${property}: minimum must be an integer of at least 1`) + } + if (!Number.isInteger(fixedHistories) || fixedHistories < 0) { + throw new Error(`${property}: fixedHistories must be a nonnegative integer`) + } + if (new Set(states).size !== states.length) { + throw new Error(`${property}: a reach state is declared twice`) + } const counts = new Map(states.map((state) => [state, 0])) const enteredByFixed = new Set() let histories = 0 + let fixedBegun = 0 + let currentFixed = false let current = new Set() // Other packages use their own replay prefixes. An explicit campaign choice // must not inherit an unrelated DB replay selector from the environment. const replaying = replayOverride ?? readOracleRunConfig().replayPath !== undefined return { - /** Starts one generated history. */ - beginHistory(): void { + /** Starts one generated history, a fixed example's when `fixed`. */ + beginHistory({ fixed = false }: { fixed?: boolean } = {}): void { + if (fixed) fixedBegun += 1 + currentFixed = fixed current = new Set() histories += 1 }, @@ -64,7 +79,7 @@ export function createOracleReach( `${property}: reach(${state}) came before the first beginHistory()`, ) } - if (histories <= fixedHistories) enteredByFixed.add(state) + if (currentFixed) enteredByFixed.add(state) if (current.has(state)) return current.add(state) counts.set(state, counts.get(state)! + 1) @@ -76,9 +91,9 @@ export function createOracleReach( /** Fails for each declared state that too few histories entered. */ assertReached(): void { if (replaying) return - if (histories < fixedHistories) { + if (fixedBegun < fixedHistories) { throw new Error( - `${property}: only ${histories} of its ${fixedHistories} fixed ` + + `${property}: only ${fixedBegun} of its ${fixedHistories} fixed ` + `histories ran, so a failure stopped the run inside the fixed ` + `examples`, ) @@ -100,7 +115,7 @@ export function createOracleReach( : []), ...(unfixed.length > 0 ? [ - `${property}: its first ${fixedHistories} histories, the fixed ` + + `${property}: its ${fixedHistories} fixed histories, the ` + `examples, did not enter these states, so their reach ` + `depends on the seed: ${unfixed.join(`, `)}`, ] diff --git a/packages/db/tests/source-health-oracle.test.ts b/packages/db/tests/source-health-oracle.test.ts index 4be82997af..f3db44cca9 100644 --- a/packages/db/tests/source-health-oracle.test.ts +++ b/packages/db/tests/source-health-oracle.test.ts @@ -5326,7 +5326,10 @@ describe(`on-demand demand grammar`, () => { `generated demand histories refine the model`, (steps, directSubscriber) => { demandHistoriesRan = true - demandReach.beginHistory() + // fast-check passes an example's input by reference. + demandReach.beginHistory({ + fixed: demandExamples.some(([example]) => example === steps), + }) return withDeadline( runDemandHistory(steps, directSubscriber, demandReach), ) @@ -7234,7 +7237,7 @@ describe(`lazy join demand grammar`, () => { )( `generated lazy demand histories refine the model`, ( - { prefix, rest }, + lazySteps, { asyncChildReady, generatedHoldChildReady, @@ -7245,10 +7248,14 @@ describe(`lazy join demand grammar`, () => { ending, }, ) => { + const { prefix, rest } = lazySteps const steps = [...(prefix?.steps ?? []), ...rest] const holdChildReady = prefix?.holdChildReady ?? generatedHoldChildReady lazyHistoriesRan = true - lazyReach.beginHistory() + // fast-check passes an example's input by reference. + lazyReach.beginHistory({ + fixed: lazyExamples.some(([example]) => example === lazySteps), + }) return withDeadline( runLazyHistory(steps, { asyncChildReady, From f5e73df21e718c9cd493143cfbd3604f5946ddf2 Mon Sep 17 00:00:00 2001 From: Test Date: Thu, 29 Oct 2026 11:06:24 -0600 Subject: [PATCH 12/12] docs(oracle): record the declared-reach evidence at 590588a65 ORC-012 asks for verdict-critical evidence in a versioned record tied to the reviewed head. The record lists the laws and their authority, the RED results and which of them came after the change, the GREEN command, the 23 mutants, the receiving-path suites, the rubric outcomes, and the open limits. The coverage map links it. Co-authored-by: Isaac --- docs/contributing/oracle-coverage.md | 3 +- .../oracle-reviews/pr-2290-declared-reach.md | 139 ++++++++++++++++++ 2 files changed, 141 insertions(+), 1 deletion(-) create mode 100644 docs/contributing/oracle-reviews/pr-2290-declared-reach.md diff --git a/docs/contributing/oracle-coverage.md b/docs/contributing/oracle-coverage.md index e87e9cf880..e855930fb3 100644 --- a/docs/contributing/oracle-coverage.md +++ b/docs/contributing/oracle-coverage.md @@ -3740,7 +3740,8 @@ checkout, or a worktree branch that has no copy of the script. In that last case the launch checkout's rule lints the worktree. `packages/db/tests/declared-reach-oracle.property.test.ts` -(`oracle.declared-reach`) owns what `createOracleReach` (ORC-015) counts, when +(`oracle.declared-reach`; [review record](oracle-reviews/pr-2290-declared-reach.md)) +owns what `createOracleReach` (ORC-015) counts, when it checks reach, and what fixed examples prove. It also owns the run parameters that `oracleRandomParameters` and `oraclePropertyOptions` return, and the campaigns that `runOracleCampaign` in diff --git a/docs/contributing/oracle-reviews/pr-2290-declared-reach.md b/docs/contributing/oracle-reviews/pr-2290-declared-reach.md new file mode 100644 index 0000000000..d0c568f74d --- /dev/null +++ b/docs/contributing/oracle-reviews/pr-2290-declared-reach.md @@ -0,0 +1,139 @@ +# Declared reach machinery (PR #2290) + +This record applies to the executable oracle at commit `590588a65`. It is +append-only: a later change adds an entry with its own commit and does not +edit an earlier one. It records the evidence behind the +`oracle.declared-reach` owner in the coverage map's "Oracle tooling" section. + +## Entry 1: commit `590588a65` + +### Scope and laws + +The oracle owns these laws of `createOracleReach`, `runOracleCampaign`, +`oracleRandomParameters`, and `oraclePropertyOptions`. Authority is ORC-015, +ORC-007, issue #2287, and maintainer decisions in the PR #2290 session. + +| Law | Authority | Generated witness | +| --- | --- | --- | +| A history counts once per declared state it enters | ORC-015 | repeats within a history | +| A reach call for an undeclared state, or before the first history, throws and counts nothing | maintainer decision | undeclared index, early reaches | +| Invalid options throw at creation | maintainer decision | minimums 0, -1, and 1.5. Fixed counts -1 and 0.5. A state declared twice | +| The check fails below the minimum | ORC-015 | minimums 1 to 3 | +| A fixed history is one begun with `fixed: true`. The check fails for a state that no fixed history entered. An extra fixed history counts as fixed. Too few fixed histories report only the stop | #2287, maintainer decision | fixed marks per history, an unfixed history first, extra and missing fixed histories | +| A seed-only run checks reach, any path replay in the process skips it, an explicit `replaying` overrides the environment | maintainer decisions | four run kinds, optional override | +| Examples come on top of the base runs, a replay keeps its seed, a path replay of the property keeps its path and runs once | #2287, ORC-007 | run kinds, base runs 1 to 200, up to five examples, the process multiplier | +| `runOracleCampaign` runs fixed-seed and random campaigns, or one replay campaign, passes each its parameters, reports each passing campaign, and rejects an invalid environment | ORC-007, ORC-015 | run kinds, a fixed seed, three invalid environments | + +The law discovery behind this table, with the receiving-path inventory and +tension scan, found that the earlier oracle stated only the fixed-example law. +Reviews then found the other laws one round at a time. + +### Experiments + +RED results. Each was run on the parent of its production change with the +extended oracle: + +- Option validation: the oracle failed at fixed ledger 9 (`minimum: 0`), where + the reach did not throw. +- Fixed marks: with validation in place, the parent's reach failed at fixed + ledger 12, where the model of that draft expected a throw. With the final + model, a mutant that restores the parent's positional counting fails at + fixed ledger 13, an unfixed history before the fixed one. +- An extra fixed history: an intermediate draft threw for it. The oracle + failed with that throw, and a mutant hunt showed that the throw replaced the + original assertion failure while fast-check shrank an example. The model + now credits the extra history, and production no longer throws. +- Early reach, the stopped-run report, and seed-only checks in + `createOracleReach` and `runOracleCampaign` failed on their parents in the + same way, in earlier commits of this PR. + +Limit on order: the first commit of this PR changed the seed-only rule and +added `fixedHistories` before this oracle existed. Their RED results were run +afterward against that commit's parent. They are not a pre-change gate. + +GREEN result at `590588a65`, from `packages/db`: + +```sh +pnpm exec vitest run --maxWorkers=2 --coverage.enabled=false \ + tests/declared-reach-oracle.property.test.ts \ + tests/source-health-oracle.test.ts tests/oracle-reach.test.ts \ + tests/oracle-campaign.test.ts tests/mutation-handler-types-oracle.test.ts +``` + +All 556 tests pass with no type errors. The declared-reach property runs 200 +generated ledgers and 14 fixed ledgers. The 14 fixed ledgers enter its 14 +declared reach states in every run. + +Mutants. Each changed one decision in the machinery, ran the declared-reach +oracle, and was restored. All 23 failed at an assertion of the intended +comparison (`reach verdict`, `campaign observation`, `run parameters`, or +`property options under this process`): + +- Fixed counting by position, extra fixed histories not credited. +- Accepting minimum 0, a fractional fixed count, or a duplicate state. +- An ignored campaign fixed seed, a replay campaign without its seed, a path + replay campaign without `numRuns: 1`, a wrong `ORACLE_REACH` minimum, + accepting a non-numeric campaign path. +- An ignored `replaying` override, accepting an undeclared state, counting an + early reach. +- Skipping reach only for the named replay property, skipping reach in a + seed-only run, in `createOracleReach` or in `runOracleCampaign`, checking + reach in a campaign path replay. +- Dropping `examples` in `oraclePropertyOptions`, dropping the replay seed and + path with examples, letting examples displace random runs. +- Naming states after a stopped run, removing the fixed-history check, + counting a state twice in one history. + +A first draft of the extra-fixed mutant capped a counter that is only compared +with the declared count. It survived, and it is equivalent by that invariant. +A separate run with `TANSTACK_DB_ORACLE_RUNS_MULTIPLIER=2` rejected a mutant +that ignores the multiplier. + +Receiving paths. With the new rules, the complete suites of `db` (385 files, +24,216 tests), `db-sqlite-persistence-core`, `offline-transactions`, +`electric-db-collection`, `svelte-db`, `convex-db-collection`, `preact-db`, +and `db-ivm` pass. One `db` file, `mutation-handler-types-oracle.test.ts`, +declared each state six times on purpose and threw. It now declares each +once, and its counts are unchanged. `react-db` passes every test, with type +errors from unbuilt packages in this checkout. Two `query-db-collection` files +and `browser-db-sqlite-persistence` need native SQLite bindings that this +checkout lacks, so only CI runs them. + +### Rubric outcomes + +- ORC-001, ORC-003: the oracle's opening prose states each law, its authority, + and its limits. The model, grammar, drivers, and checks have their own + comments. +- ORC-002: the model recomputes counts and failures from the ledger and reads + the environment on its own. It imports no production helper. +- ORC-004: the grammar reconstructs every known witness above as a fixed + ledger. Its ranges and invalid values are listed in the law table. +- ORC-005, ORC-006: the drivers call the real entry points and compare whole + observations. The mutants above classify as assertion failures. +- ORC-007: the property runs through `oraclePropertyOptions` with fixed + ledgers, and replays through `oracle.declared-reach` in the replay manifest. +- ORC-008: the model keeps a fixed mark per history. The unfixed-first ledger + shows that position alone cannot replace it. +- ORC-009: "ledger" and "run kind" are model-only terms. The oracle maps them + to histories and replay environments. +- ORC-010: the extra-fixed rule exists so that a shrinking rerun cannot + replace the original failure. +- ORC-011: no shared-fault hypothesis needs a second formulation. +- ORC-013: each conditional law has a premise case and a neighbor among the + fixed ledgers (for example, a fixed miss that a later unfixed history enters). +- ORC-014: not applicable. No provider premise. +- ORC-015: 14 declared states, each entered in every run. +- ORC-016: the oracle file has one generated property and no unit tests. + +### Open and limits + +- Other reach properties are not measured for chance misses, about twenty set + examples inside their base runs, and a campaign reach cannot declare fixed + histories. Owner: #2289. +- A path replay also skips reach in a property that the replay does not name. +- After a late property failure, the check still reports missed states. +- Not judged: reporter keys, the rejection of an unregistered property, and + the compile-time rule that a call without examples returns no `examples` + key. Type-aware lint is that rule's only witness. +- Before the merge with main, one local batch failed 1 of 512 tests and its log + was lost. It did not recur in 12 reruns. Its cause is unknown.