From 80530e19bea3c0ce356a25cdf989372ad069149d Mon Sep 17 00:00:00 2001 From: Test Date: Mon, 9 Nov 2026 13:15:18 -0700 Subject: [PATCH 1/6] test(oracles): observe that a replaced load is aborted before its replacement starts Law: a replay that replaces an acquisition aborts the replaced attempt before the replacement's load starts. Authority: lifecycle grammar header ("A replay that replaces an attempt aborts it too"); production comment in subscription.ts ("Abort the old work before it can install rows into the replacement replay"); ARCHITECTURE normative law 9 "Publication" (a truncate replacement stays private until its active replay work settles) and the "Replay participants and failure" section. Gap: the history driver compared each attempt's abort flag with its signal only at checkpoints, after the whole step. A mutant that drops the truncate abort loop (P4) passed all 361 consumer tests because the signal is aborted later in the same step. Observation: the adapter's loadSubset now checks, at the moment a replacement loads, that every earlier attempt the model marks aborted has an aborted signal. Evidence: - Law: as above. - Reach: the check runs at every adapter load in the history oracle's campaigns (96 histories, fixed and random). - RED: P4 (truncate does not abort replaced acquisitions) on this commit's parent grammar with the new check: 13 of 96 histories fail with "replaced attempt N is aborted before replacement M loads". - GREEN: unchanged production, same file: 96 of 96 pass. - Mutant: P4 is killed by the new observation. P1, P2, P3, P5 still killed by the consumer tests (measured separately). - Limits: the check covers replaced attempts that the model marks aborted at load time. It does not check the signal's timing relative to a late result landing. Reach is not counted per history. Co-authored-by: Isaac --- ...iption-lifecycle-history-oracle.property.test.ts | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts b/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts index 62a1225213..0a9d67dc75 100644 --- a/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts +++ b/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts @@ -641,6 +641,19 @@ async function runHistory( ) } watchCoreAbortListeners(observed.id, options.signal) + // A replay that replaces an attempt aborts it before the + // replacement's load starts (header: "A replay that replaces an + // attempt aborts it too"). The model has already reduced this + // command, so every earlier attempt it marks aborted must have an + // aborted signal at this call, not merely by the next checkpoint. + for (const earlier of runtimeAttempts.values()) { + if (earlier.id === observed.id) continue + if (!model.attempts[earlier.id]?.aborted) continue + check( + earlier.options.signal?.aborted, + `replaced attempt ${earlier.id} is aborted before replacement ${observed.id} loads`, + ).toBe(true) + } owner.attemptId = observed.id attemptByOptions.set(options, observed.id) observedLoads.push(observed) From fecdc4e4cfcfceb46686243bc481220b34b8811b Mon Sep 17 00:00:00 2001 From: Test Date: Mon, 9 Nov 2026 13:15:24 -0700 Subject: [PATCH 2/6] docs(oracles): cite ARCHITECTURE normative laws by number and heading The lifecycle grammar header cited "law 9" and "law 10" with section headings ("Replay participants and failure", "Source cancellation and applied settlement"). The normative list in ARCHITECTURE numbers "Publication" as law 9 and "Initial demand" as law 10. The header now names the normative law and its heading, and gives the section as a secondary reference. Law: unchanged. Authority: ARCHITECTURE normative laws 9 and 10. Evidence: comment-only change; no behavior changed. Reach, RED, GREEN, mutant: not applicable (documentation only). Limits: other "law N" references in the grammar's inline comments are not changed here. Co-authored-by: Isaac --- ...llection-subscription-lifecycle-grammar-oracle.ts | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts b/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts index 98d43ce7b6..7abc9e9f4e 100644 --- a/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts +++ b/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts @@ -34,13 +34,15 @@ import { declareOracle } from './oracle-declaration.js' * legal commands with fixed and random seeds. The drivers compare production * loads, unloads, results, status, errors, and publication against this trace. * - * A demand change is one step (ARCHITECTURE law 9, "Replay participants and - * failure"). Its `change` command retires several logical owners at once, as - * a lazy join's demand change retires several segments, and the model judges + * A demand change is one step (ARCHITECTURE normative law 9, "Publication"; + * replay failure is in the "Replay participants and failure" section). Its + * `change` command retires several logical owners at once, as a lazy join's + * demand change retires several segments, and the model judges * an open replay once, after every owner in the change has retired. Its * `replace` command marks one held owner as the replacement for another's - * coverage, as a lazy join's fragmented-churn replacement does (law 10, - * "Source cancellation and applied settlement"): the replacement requests the + * coverage, as a lazy join's fragmented-churn replacement does (ARCHITECTURE + * normative law 10, "Initial demand"; the source rule is in the "Source + * cancellation and applied settlement" section): the replacement requests the * whole current key union, so while it is held and its own acquisition did * not fail, the replay does not fail for the owner it replaces. Retiring the * replacement returns that verdict to the replaced owner. Only the From aa02ed73d951158da4bd5e8b8ea0c4e41c42e435 Mon Sep 17 00:00:00 2001 From: Test Date: Mon, 9 Nov 2026 14:01:55 -0700 Subject: [PATCH 3/6] test(oracles): drive the lifecycle grammar from a transition table Replace the lifecycle reducer's command if-chain with a 23-row table. Each row has an id, a from-phase set, an event, a guard, an effect, the state variables it reads and writes, and an authority. Reach labels are predicates over one step. The table asserts each row's stated end phase. Commands and laws are unchanged; the authority strings now quote the grammar header and ARCHITECTURE laws 9, 10 and 14 instead of undefined labels. LifecycleEffect gains `transition`. Helpers are named defineRow and defineNoopRow. Law: unchanged from the HEAD reducer. Authority: grammar header (unsubscribe, abort, settle, replace, truncate, cleanup, restart paragraphs), ARCHITECTURE normative laws 9, 10, 14, and inference rows marked flagged in the table. Reach: all 23 rows fire in the generated campaigns (68,022 histories, 2.52M steps, four acquisition/cancellation configurations). A breadth-first search over the full command alphabet (58 commands) reaches all 23 rows by depth 3, 59 of 60 reach labels by depth 6, and 128 of 174 var-overlap def-use pairs by depth 6. The remaining 46 pairs are unreachable: a phase-level check over the declared reads and writes shows 38 are absorbed by the unsubscribed phase and 8 are overwritten by an intervening row. One label (change:between-releases-would-publish) is generated 726 times but not reached at depth 6. RED: not applicable: no production code or observable behavior changed, so there is no parent-commit failure to show. The check that stands in for RED is a differential against the HEAD reducer (below). A calibration that drops the replacement owesNothing clause makes the differential fail (21 mismatches). GREEN: differential against the HEAD reducer over 60,088 histories (578,756 steps) and four configurations: zero mismatches in the returned effect (minus transition), trace, reach, and full model state. Consumers (history, publication, oracle) 361 of 361. eslint, lint:changed, and the db typecheck report nothing for these files. Mutant: P1-P5 applied one at a time with production restored after each, on the HEAD grammar and on this grammar: all ten runs kill all five mutants (P1 72, P2 18, P3 3, P4 12 to 13, P5 29 failing tests). P4 (a newer replay does not abort the replaced acquisitions) was missed before 80530e19b and is killed by both now. Limits: the breadth-first search covers depth 6 only (depth 7 ran out of memory). Reads and writes are declared, not measured, so the phase check is only as good as those declarations. Coverage is for the three consumer drivers' campaigns, which are about 400 histories for the demand-change family, so the seven pairs seen under 0.04 percent of generated histories are rare at consumer scale. The table is about 1.75 times the reducer's lines (827 against 474); the proof of equivalence is the differential, not the line count. Co-authored-by: Isaac --- ...n-subscription-lifecycle-grammar-oracle.ts | 945 +++++++++++++----- 1 file changed, 677 insertions(+), 268 deletions(-) diff --git a/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts b/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts index 7abc9e9f4e..bbf0a225fa 100644 --- a/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts +++ b/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts @@ -282,6 +282,8 @@ export type LifecycleEffect = { ownerIds?: Array attemptId?: number requestResult?: boolean + // The lifecycle table row that decided this command. + transition?: string } export function createLifecycleModel( @@ -316,6 +318,60 @@ export function createLifecycleModel( } } +/** + * ## Transition table + * + * The reducer is an extended state machine. Its phase is a function of two + * model flags: `unsubscribed` (this subscription has ended) and `active` (the + * Collection's sync run is live). Each row of `lifecycleTable` fires when its + * event matches the command, the phase is one of its `from` phases, and its + * guard holds. Rows are tried in order: an effective row precedes the noop row + * that catches the same event when its guard fails. The engine asserts that + * each row ends in its `to` phase, so a row whose effect disagrees with the + * table fails at once. + * + * Rows do not write reach. `lifecycleReach` declares each reach label as a + * predicate over one step: the row that fired, the command, state captured + * before the effect, the facts the effect recorded, and the attempts it + * created. Transition coverage is therefore a property of the table: a label + * `effective:` or `noop:` names the kind of row that fired. + * + * `reads` and `writes` list the extended-state variables that a row's guard or + * effect reads or changes. Every row also reads `phase`, because its `from` + * dispatch does. Two rows interact when the second reads a variable the first + * writes. Coverage measures those adjacent pairs. + */ + +export type LifecyclePhase = + | `live` + | `cleaned-up` + | `unsubscribed` + | `unsubscribed-cleaned-up` + +export type LifecycleStateVariable = + | `phase` + | `owners` + | `attempts` + | `generations` + | `publication-barrier` + | `collection-status` + +export type ReplayVerdict = `closed` | `open` | `failed` | `succeeded` + +/** Facts an effect records for the reach predicates. They are data, not reach. */ +export type LifecycleStepFacts = { + // `change`: the replay verdict after each release, in release order. + releaseVerdicts: Array + // This step's replay judgment closed the barrier on a failed owner. + replayFailedOwnerDecided: boolean +} + +export function lifecyclePhase(model: LifecycleModel): LifecyclePhase { + if (model.unsubscribed) + return model.active ? `unsubscribed` : `unsubscribed-cleaned-up` + return model.active ? `live` : `cleaned-up` +} + function setStatus(model: LifecycleModel, queuedReplay = false): void { if (model.unsubscribed) return const status = @@ -362,26 +418,22 @@ function replacementSucceeded(model: LifecycleModel): boolean { ) } -// Judge an open replay: success closes the publication barrier. -function judgeReplay(model: LifecycleModel): void { - if (!model.publicationBarrierOpen || !replacementSucceeded(model)) return +// Judge an open replay: success closes the publication barrier. Returns +// whether the closing judgment decided a failed owner. +function judgeReplay(model: LifecycleModel): boolean { + if (!model.publicationBarrierOpen || !replacementSucceeded(model)) return false model.publicationBarrierOpen = false - if ( - model.owners.some( - ({ attemptId }) => - attemptId !== undefined && - model.attempts[attemptId]!.outcome === `reject` && - !model.attempts[attemptId]!.endedByAbort, - ) + return model.owners.some( + ({ attemptId }) => + attemptId !== undefined && + model.attempts[attemptId]!.outcome === `reject` && + !model.attempts[attemptId]!.endedByAbort, ) - model.reach.add(`replacement-decides-failed-owner`) } // What judging the open replay now would decide. Only `change` asks, to name // the histories in which judging between its releases would differ. -function replayVerdict( - model: LifecycleModel, -): `closed` | `open` | `failed` | `succeeded` { +function replayVerdict(model: LifecycleModel): ReplayVerdict { if (!model.publicationBarrierOpen) return `closed` if ( model.attempts.some(({ gating, inReplacement }) => gating && inReplacement) @@ -432,15 +484,6 @@ function startAttempt( failure: model.failureForAttempt(id), } model.attempts.push(attempt) - model.reach.add( - `attempt-sync-run:${attempt.syncRunGeneration === 0 ? `initial` : `restarted`}`, - ) - model.reach.add( - `attempt-replay:${attempt.replayGeneration === 0 ? `initial` : `replayed`}`, - ) - model.reach.add( - `attempt-location:${attempt.syncRunGeneration === 0 ? `initial` : `restarted`}:${attempt.replayGeneration === 0 ? `initial` : `replayed`}`, - ) model.loads.push({ id, demand: attempt.demand, @@ -517,277 +560,643 @@ function selectAttempt( return command.age === `oldest` ? candidates[0] : candidates.at(-1) } -/** Pure reference transition. It never reads adapter callbacks or SUT state. */ -export function reduceLifecycle( +// A logical owner admitted by `request`. An active Collection starts its +// acquisition; a cleaned-up one holds the owner without claiming one. +function admitRequest( model: LifecycleModel, - command: LifecycleCommand, + demand: DemandName, + acquires: boolean, ): LifecycleEffect { - model.reach.add(`command:${command.type}`) - if (model.unsubscribed) { - if (command.type === `cleanup` && model.active) { - model.reach.add(`effective:cleanup`) - model.active = false - model.collectionStatus = `cleaned-up` - } else if (command.type === `restart` && !model.active) { - model.reach.add(`effective:restart`) - model.active = true - model.syncRunGeneration++ - model.replayGeneration = 0 - model.publicationBarrierOpen = false - model.collectionStatus = `ready` - } else { - model.reach.add(`noop:${command.type}`) - } - return { requestResult: false } + const owner: LifecycleOwner = { + id: model.nextOwnerId++, + demand, + aborted: false, } - - if (command.type === `request`) { - model.reach.add(`effective:request`) - if (model.owners.some(({ demand }) => demand === command.demand)) { - model.reach.add(`duplicate-owner`) - } - if (!model.active) model.reach.add(`request-while-cleaned`) - const owner: LifecycleOwner = { - id: model.nextOwnerId++, - demand: command.demand, - aborted: false, - } - model.owners.push(owner) - if (model.active) { - const attemptId = startAttempt(model, owner).id - const result = { - attemptId, + model.owners.push(owner) + // A waiting owner gets a promise now, without claiming an acquisition. + const result = acquires + ? { + attemptId: startAttempt(model, owner).id, resultKind: model.acquisitionMode === `async-pending` ? (`promise` as const) : (`true` as const), } - model.results.push(result) - model.trace.push({ type: `result`, ...result }) - } else { - // A waiting owner gets a promise now, without claiming an acquisition. - const result = { attemptId: `unacquired`, resultKind: `promise` } as const - model.results.push(result) - model.trace.push({ type: `result`, ...result }) - } - setStatus(model) - if (!model.publicationBarrierOpen) { - model.publications++ - model.trace.push({ type: `publication` }) - } - return { ownerId: owner.id, requestResult: true } + : ({ attemptId: `unacquired`, resultKind: `promise` } as const) + model.results.push(result) + model.trace.push({ type: `result`, ...result }) + setStatus(model) + if (!model.publicationBarrierOpen) { + model.publications++ + model.trace.push({ type: `publication` }) } + return { ownerId: owner.id, requestResult: true } +} - if (command.type === `abort`) { - const owner = model.owners.find( - ({ demand, aborted }) => demand === command.demand && !aborted, - ) - if (!owner) { - model.reach.add(`noop:abort`) - return {} - } - model.reach.add(`effective:abort`) - owner.aborted = true - if (owner.attemptId !== undefined) { - const attempt = model.attempts[owner.attemptId]! - abortAttempt(model, attempt) - attempt.reportable = false - } - // The abort ends the attempt, so the replay is judged as after any - // settlement: a held replacement can still cover it. - judgeReplay(model) - setStatus(model) - return { ownerId: owner.id } +// Replay setup is asynchronous even when every acquisition is synchronous or +// canceled. Logical owners queue setup; live owners start acquisitions. +function startReplay( + model: LifecycleModel, + facts: LifecycleStepFacts, +): void { + model.replayGeneration++ + setStatus(model, model.owners.length > 0) + // A canceled-only truncate starts no new work. It still opens the + // barrier when a prior replay's current attempt was pending; aborting that + // attempt below ends its wait. + model.publicationBarrierOpen = + model.owners.some(({ aborted }) => !aborted) || + model.attempts.some(({ gating, inReplacement }) => gating && inReplacement) + for (const owner of model.owners) { + // Replacing an acquisition is not releasing its logical owner, but it + // ends the replaced load: it holds neither readiness nor publication. + retireAttempt(model, owner, { unload: true }) + if (!owner.aborted) startAttempt(model, owner) } + facts.replayFailedOwnerDecided = judgeReplay(model) + setStatus(model) +} - if (command.type === `release`) { - const owner = retireOwner(model, command.demand) - if (!owner) { - model.reach.add(`noop:release`) - return {} - } - model.reach.add(`effective:release`) - judgeReplay(model) - setStatus(model) - return { ownerId: owner.id } - } +/** The command's type, or the wildcard for every command. */ +type LifecycleEvent = LifecycleCommand[`type`] | `*` +type CommandFor = E extends `*` + ? LifecycleCommand + : Extract + +export type LifecycleRow = { + id: string + kind: `effect` | `noop` + from: ReadonlyArray + event: LifecycleEvent + to: LifecyclePhase | `same` + guard?: (model: LifecycleModel, command: LifecycleCommand) => boolean + reads: ReadonlyArray + writes: ReadonlyArray + effect: ( + model: LifecycleModel, + command: LifecycleCommand, + facts: LifecycleStepFacts, + ) => LifecycleEffect + // The contract clause or dated decision for this row. A noop row cites no + // contract clause: it encodes the grammar's convention that a command with + // no target changes nothing. + authority: string +} - if (command.type === `change`) { - // Law 9: the change is one step. Every named owner retires first, and - // the replay is judged once after the last. The verdicts between its - // releases are recorded only to name the histories they would mislead. - const verdicts: Array> = [] - const retired: Array = [] - for (const demand of command.release) { - const owner = retireOwner(model, demand) - if (!owner) continue - retired.push(owner) - verdicts.push(replayVerdict(model)) - } - if (retired.length === 0) { - model.reach.add(`noop:change`) - return {} - } - model.reach.add(`effective:change`) - const verdict = verdicts.at(-1)! - if (retired.length > 1 && verdict !== `closed`) - model.reach.add(`change:several-owners-during-replay`) - const between = verdicts.slice(0, -1) - if (verdict === `failed` && between.includes(`succeeded`)) - model.reach.add(`change:between-releases-would-publish`) - if (verdict === `succeeded` && between.includes(`failed`)) - model.reach.add(`change:between-releases-would-fail`) - judgeReplay(model) - setStatus(model) - return { ownerIds: retired.map(({ id }) => id) } - } +type RowSpec = { + id: string + from: ReadonlyArray + event: E + to: LifecyclePhase | `same` + guard?: (model: LifecycleModel, command: CommandFor) => boolean + reads?: ReadonlyArray + writes: ReadonlyArray + effect: ( + model: LifecycleModel, + command: CommandFor, + facts: LifecycleStepFacts, + ) => LifecycleEffect + authority: string +} - if (command.type === `replace`) { - const replacement = model.owners.find( - ({ demand }) => demand === command.demand, - ) - if (!replacement) { - model.reach.add(`noop:replace`) - return {} - } - model.reach.add(`effective:replace`) - replacement.replaces = model.owners - .filter(({ demand }) => demand === command.replaced) - .map(({ id }) => id) - return { ownerId: replacement.id } +// The event dispatch selects the command type, so each row's typed command is +// the one the engine passes it. +function defineRow(spec: RowSpec): LifecycleRow { + return { + id: spec.id, + kind: `effect`, + from: spec.from, + event: spec.event, + to: spec.to, + guard: spec.guard as LifecycleRow[`guard`], + reads: spec.reads ?? [], + writes: spec.writes, + effect: spec.effect as LifecycleRow[`effect`], + authority: spec.authority, } +} - if (command.type === `settle`) { - const attempt = selectAttempt(model, command) - if (!attempt) { - model.reach.add(`noop:settle`) - return {} - } - model.reach.add(`effective:settle`) - model.reach.add(`settle-scope:${command.scope}`) - model.reach.add(`settle-age:${command.age}`) - model.reach.add(`settle-outcome:${command.outcome}`) - model.reach.add(`settle:${command.scope}:${command.age}:${command.outcome}`) - attempt.outcome = command.outcome - attempt.gating = false - if ( - command.outcome === `reject` && - attempt.reportable && - !attempt.aborted - ) { - model.lastError = attempt.failure - model.errors.push({ attemptId: attempt.id, error: attempt.failure }) - model.trace.push({ type: `error`, attemptId: attempt.id }) - } - judgeReplay(model) - setStatus(model) - return { attemptId: attempt.id } +function defineNoopRow(spec: { + id: string + from: ReadonlyArray + event: E + reads: ReadonlyArray + result?: LifecycleEffect + authority: string +}): LifecycleRow { + return { + id: spec.id, + kind: `noop`, + from: spec.from, + event: spec.event, + to: `same`, + reads: spec.reads, + writes: [], + effect: () => spec.result ?? {}, + authority: spec.authority, } +} + +const ENDED: ReadonlyArray = [`unsubscribed`, `unsubscribed-cleaned-up`] +const SUBSCRIBED: ReadonlyArray = [`live`, `cleaned-up`] +const LIVE: ReadonlyArray = [`live`] +const CLEANED: ReadonlyArray = [`cleaned-up`] - if (command.type === `truncate`) { - if (!model.active) { - model.reach.add(`noop:truncate`) +/** + * The lifecycle table. Rows are tried in order, so an effective row precedes + * the noop row for its event. Authority cites the header of the grammar file, ARCHITECTURE + * normative laws (law N), the glossary, or a code comment that states the rule. The noop rows and the inferences marked "inference" have + * no contract clause: they follow the grammar's convention. + */ +export const lifecycleTable: ReadonlyArray = [ + // An ended subscription keeps only the Collection's sync-run lifecycle. + defineRow({ + id: `ended-cleanup`, + from: [`unsubscribed`], + event: `cleanup`, + to: `unsubscribed-cleaned-up`, + writes: [`phase`, `collection-status`], + effect: (model) => { + model.active = false + model.collectionStatus = `cleaned-up` + return { requestResult: false } + }, + authority: `Header: \`cleanup\` ends the current sync run. An unsubscribed subscription keeps the Collection's sync run, so this cleanup still applies. Adapter cleanup timing is outside this grammar.`, + }), + defineRow({ + id: `ended-restart`, + from: [`unsubscribed-cleaned-up`], + event: `restart`, + to: `unsubscribed`, + writes: [`phase`, `generations`, `publication-barrier`, `collection-status`], + effect: (model) => { + model.active = true + model.syncRunGeneration++ + model.replayGeneration = 0 + model.publicationBarrierOpen = false + model.collectionStatus = `ready` + return { requestResult: false } + }, + authority: `Header: \`restart\` starts a new sync run; unsubscribe does not end the Collection's sync run, so restart applies only after cleanup.`, + }), + defineNoopRow({ + id: `ended-noop`, + from: ENDED, + event: `*`, + reads: [], + result: { requestResult: false }, + authority: `none: no contract clause. Unsubscribe ends this subscription, so a later command has no target. Grammar convention, flagged.`, + }), + + defineRow({ + id: `request-live`, + from: LIVE, + event: `request`, + to: `same`, + reads: [`publication-barrier`], + writes: [`owners`, `attempts`], + effect: (model, command) => admitRequest(model, command.demand, true), + authority: `Header: "a request combines a new logical owner with any acquisition attempt it starts."`, + }), + defineRow({ + id: `request-cleaned`, + from: CLEANED, + event: `request`, + to: `same`, + reads: [`publication-barrier`], + writes: [`owners`], + effect: (model, command) => admitRequest(model, command.demand, false), + authority: `Header: a request admits a logical owner. A Collection that is cleaned up starts no attempt; the cleanedRestartDemandCases comment says a demand created while cleaned up waits for the next sync run's evidence.`, + }), + + defineRow({ + id: `abort-owner`, + from: SUBSCRIBED, + event: `abort`, + to: `same`, + guard: (model, command) => + model.owners.some( + ({ demand, aborted }) => demand === command.demand && !aborted, + ), + reads: [`owners`, `attempts`, `publication-barrier`], + writes: [`owners`, `attempts`, `publication-barrier`], + effect: (model, command, facts) => { + const owner = model.owners.find( + ({ demand, aborted }) => demand === command.demand && !aborted, + )! + owner.aborted = true + if (owner.attemptId !== undefined) { + const attempt = model.attempts[owner.attemptId]! + abortAttempt(model, attempt) + attempt.reportable = false + } + // The abort ends the attempt, so the replay is judged as after any + // settlement: a held replacement can still cover it. + facts.replayFailedOwnerDecided = judgeReplay(model) + setStatus(model) + return { ownerId: owner.id } + }, + authority: `Header: "abort cancels the owner's current acquisition attempt but does not retire the owner"; "an abort ends the load" (maintainer decision), so the attempt holds no readiness and a later settlement reports nothing.`, + }), + defineNoopRow({ + id: `abort-noop`, + from: SUBSCRIBED, + event: `abort`, + reads: [`owners`], + authority: `none: no live owner for the demand. Grammar convention, flagged.`, + }), + + defineRow({ + id: `release-owner`, + from: SUBSCRIBED, + event: `release`, + to: `same`, + guard: (model, command) => + model.owners.some(({ demand }) => demand === command.demand), + reads: [`owners`, `attempts`, `publication-barrier`], + writes: [`owners`, `attempts`, `publication-barrier`], + effect: (model, command, facts) => { + const owner = retireOwner(model, command.demand)! + facts.replayFailedOwnerDecided = judgeReplay(model) + setStatus(model) + return { ownerId: owner.id } + }, + authority: `Header: "release combines demand retirement with release of that owner's acquisition lease."`, + }), + defineNoopRow({ + id: `release-noop`, + from: SUBSCRIBED, + event: `release`, + reads: [`owners`], + authority: `none: no logical owner for the demand. Grammar convention, flagged.`, + }), + + defineRow({ + id: `change-demands`, + from: SUBSCRIBED, + event: `change`, + to: `same`, + guard: (model, command) => + command.release.some((demand) => + model.owners.some((owner) => owner.demand === demand), + ), + reads: [`owners`, `attempts`, `publication-barrier`], + writes: [`owners`, `attempts`, `publication-barrier`], + effect: (model, command, facts) => { + // Law 9: the change is one step. Every named owner retires first, and + // the replay is judged once after the last. The verdicts between its + // releases are recorded only to name the histories they would mislead. + const retired: Array = [] + for (const demand of command.release) { + const owner = retireOwner(model, demand) + if (!owner) continue + retired.push(owner) + facts.releaseVerdicts.push(replayVerdict(model)) + } + facts.replayFailedOwnerDecided = judgeReplay(model) + setStatus(model) + return { ownerIds: retired.map(({ id }) => id) } + }, + authority: `ARCHITECTURE normative law 9 ("A demand change counts as one step"); header: \`change\` "retires several logical owners at once".`, + }), + defineNoopRow({ + id: `change-noop`, + from: SUBSCRIBED, + event: `change`, + reads: [`owners`], + authority: `none: no named demand has a logical owner. Grammar convention, flagged.`, + }), + + defineRow({ + id: `replace-owner`, + from: SUBSCRIBED, + event: `replace`, + to: `same`, + guard: (model, command) => + model.owners.some(({ demand }) => demand === command.demand), + reads: [`owners`], + writes: [`owners`], + effect: (model, command) => { + const replacement = model.owners.find( + ({ demand }) => demand === command.demand, + )! + replacement.replaces = model.owners + .filter(({ demand }) => demand === command.replaced) + .map(({ id }) => id) + return { ownerId: replacement.id } + }, + authority: `ARCHITECTURE normative law 10 ("A fragmented churn replacement retires prior coverage only after its union applies; failure preserves it"); header: \`replace\` "marks one held owner as the replacement".`, + }), + defineNoopRow({ + id: `replace-noop`, + from: SUBSCRIBED, + event: `replace`, + reads: [`owners`], + authority: `none: no logical owner for the replacement. Grammar convention, flagged.`, + }), + + defineRow({ + id: `settle-attempt`, + from: SUBSCRIBED, + event: `settle`, + to: `same`, + guard: (model, command) => selectAttempt(model, command) !== undefined, + reads: [`attempts`, `publication-barrier`], + writes: [`attempts`, `publication-barrier`], + effect: (model, command, facts) => { + const attempt = selectAttempt(model, command)! + attempt.outcome = command.outcome + attempt.gating = false + // A reject reports only while the attempt is reportable and was not + // ended by an abort: a later outcome decides nothing. + if ( + command.outcome === `reject` && + attempt.reportable && + !attempt.aborted + ) { + model.lastError = attempt.failure + model.errors.push({ attemptId: attempt.id, error: attempt.failure }) + model.trace.push({ type: `error`, attemptId: attempt.id }) + } + facts.replayFailedOwnerDecided = judgeReplay(model) + setStatus(model) + return { attemptId: attempt.id } + }, + authority: `Header: "settle changes an acquisition attempt". A reject reports only while the attempt is reportable and not ended by an abort ("a later settlement reports nothing").`, + }), + defineNoopRow({ + id: `settle-noop`, + from: SUBSCRIBED, + event: `settle`, + reads: [`attempts`], + authority: `none: no open attempt matches the scope and age. Grammar convention, flagged.`, + }), + + defineRow({ + id: `truncate-replay`, + from: LIVE, + event: `truncate`, + to: `same`, + reads: [`generations`, `owners`, `attempts`, `publication-barrier`], + writes: [`generations`, `attempts`, `publication-barrier`], + effect: (model, _command, facts) => { + startReplay(model, facts) return {} - } - model.reach.add(`effective:truncate`) - if ( - model.replayGeneration > 0 && - model.attempts.some( - ({ syncRunGeneration, outcome }) => - syncRunGeneration === model.syncRunGeneration && - outcome === undefined, - ) - ) { - model.reach.add(`overlapping-replay`) - } - model.replayGeneration++ - // Replay setup is asynchronous even when every acquisition is synchronous - // or canceled. Logical owners queue setup; live owners start acquisitions. - setStatus(model, model.owners.length > 0) - // A canceled-only truncate starts no new work. It still opens the - // barrier when a prior replay's current attempt was pending; aborting - // that attempt below ends its wait. - model.publicationBarrierOpen = - model.owners.some(({ aborted }) => !aborted) || - model.attempts.some( - ({ gating, inReplacement }) => gating && inReplacement, - ) - for (const owner of model.owners) { - // Replacing an acquisition is not releasing its logical owner, but it - // ends the replaced load: it holds neither readiness nor publication. - retireAttempt(model, owner, { unload: true }) - if (!owner.aborted) { - startAttempt(model, owner) + }, + authority: `ARCHITECTURE normative law 9 (a truncate replacement stays private until work started by its active replay demands settles); header: "A replay that replaces an attempt aborts it too."`, + }), + defineNoopRow({ + id: `truncate-noop`, + from: CLEANED, + event: `truncate`, + reads: [`phase`], + authority: `inference from the cleanup sentence: no sync run is active, so a truncate has no replay to start. Flagged.`, + }), + + defineRow({ + id: `cleanup-run`, + from: LIVE, + event: `cleanup`, + to: `cleaned-up`, + reads: [`owners`, `attempts`, `generations`], + writes: [`attempts`, `publication-barrier`, `phase`, `collection-status`], + effect: (model) => { + for (const owner of model.owners) + retireAttempt(model, owner, { unload: false }) + for (const attempt of model.attempts) attempt.gating = false + model.active = false + model.publicationBarrierOpen = false + model.collectionStatus = `cleaned-up` + setStatus(model) + return {} + }, + authority: `Header: \`cleanup\` "ends the current sync run"; ARCHITECTURE normative law 14: cleanup start closes restart admission.`, + }), + defineNoopRow({ + id: `cleanup-noop`, + from: CLEANED, + event: `cleanup`, + reads: [`phase`], + authority: `inference from the cleanup sentence: the sync run already ended. Flagged.`, + }), + + defineRow({ + id: `restart-run`, + from: CLEANED, + event: `restart`, + to: `live`, + reads: [`owners`, `phase`], + writes: [ + `phase`, + `generations`, + `attempts`, + `publication-barrier`, + `collection-status`, + ], + effect: (model, _command, facts) => { + model.active = true + model.syncRunGeneration++ + model.replayGeneration = 0 + model.publicationBarrierOpen = model.owners.some(({ aborted }) => !aborted) + model.collectionStatus = `ready` + setStatus(model, model.owners.length > 0) + const replayLoads: Array = [] + for (const owner of model.owners) { + if (!owner.aborted) replayLoads.push(startAttempt(model, owner, false)) } - } - judgeReplay(model) - setStatus(model) - return {} + facts.replayFailedOwnerDecided = judgeReplay(model) + model.publications++ + model.trace.push({ type: `publication` }) + for (const load of replayLoads) { + model.trace.push({ + type: `load`, + id: load.id, + demand: load.demand, + syncRunGeneration: load.syncRunGeneration, + replayGeneration: load.replayGeneration, + }) + } + setStatus(model) + return {} + }, + authority: `Header: \`restart\` "starts a new sync run"; an aborted owner is not restarted ("an abort ends the load").`, + }), + defineNoopRow({ + id: `restart-noop`, + from: LIVE, + event: `restart`, + reads: [`phase`], + authority: `inference from the restart sentence: the sync run is still active. Flagged.`, + }), + + defineRow({ + id: `unsubscribe-live`, + from: LIVE, + event: `unsubscribe`, + to: `unsubscribed`, + reads: [`owners`, `attempts`], + writes: [`owners`, `attempts`, `phase`], + effect: (model) => { + for (const owner of model.owners) + retireAttempt(model, owner, { unload: true }) + model.owners.length = 0 + model.unsubscribed = true + return {} + }, + authority: `Header: "unsubscribe ends this subscription, retires its logical subset owners, and releases their acquisition leases. It does not end the Collection's sync run."`, + }), + defineRow({ + id: `unsubscribe-cleaned`, + from: CLEANED, + event: `unsubscribe`, + to: `unsubscribed-cleaned-up`, + reads: [`owners`, `attempts`], + writes: [`owners`, `attempts`, `phase`], + effect: (model) => { + for (const owner of model.owners) + retireAttempt(model, owner, { unload: true }) + model.owners.length = 0 + model.unsubscribed = true + return {} + }, + authority: `Header: as unsubscribe-live. The cleaned-up Collection keeps its status.`, + }), +] + +/** Reach labels, each a predicate over one step. */ +export type LifecycleStep = { + command: LifecycleCommand + row: LifecycleRow + before: { + attemptCount: number + duplicateOwner: boolean + overlappingReplay: boolean + partialGenerationSupersession: boolean } + facts: LifecycleStepFacts + attempts: ReadonlyArray +} - if (command.type === `cleanup`) { - if (!model.active) { - model.reach.add(`noop:cleanup`) - return {} - } - model.reach.add(`effective:cleanup`) - const current = model.attempts.filter( - ({ syncRunGeneration }) => syncRunGeneration === model.syncRunGeneration, - ) - if ( +function attemptLabels(attempt: LifecycleAttempt): Array { + const sync = attempt.syncRunGeneration === 0 ? `initial` : `restarted` + const replay = attempt.replayGeneration === 0 ? `initial` : `replayed` + return [ + `attempt-sync-run:${sync}`, + `attempt-replay:${replay}`, + `attempt-location:${sync}:${replay}`, + ] +} + +function settleLabels(command: Extract) { + return [ + `settle-scope:${command.scope}`, + `settle-age:${command.age}`, + `settle-outcome:${command.outcome}`, + `settle:${command.scope}:${command.age}:${command.outcome}`, + ] +} + +export const lifecycleReach: ReadonlyArray< + (step: LifecycleStep) => ReadonlyArray +> = [ + ({ command, row }) => [ + `command:${command.type}`, + `${row.kind === `effect` ? `effective` : `noop`}:${command.type}`, + ], + ({ before, row }) => + row.id === `request-live` || row.id === `request-cleaned` + ? before.duplicateOwner + ? [`duplicate-owner`] + : [] + : [], + ({ row }) => (row.id === `request-cleaned` ? [`request-while-cleaned`] : []), + ({ before, row }) => + row.id === `truncate-replay` && before.overlappingReplay + ? [`overlapping-replay`] + : [], + ({ before, row }) => + row.id === `cleanup-run` && before.partialGenerationSupersession + ? [`partial-generation-supersession`] + : [], + ({ command, row }) => + row.kind === `effect` && command.type === `settle` + ? settleLabels(command) + : [], + ({ attempts }) => attempts.flatMap(attemptLabels), + ({ facts }) => + facts.replayFailedOwnerDecided ? [`replacement-decides-failed-owner`] : [], + ({ facts, row }) => { + if (row.id !== `change-demands`) return [] + const verdicts = facts.releaseVerdicts + const verdict = verdicts.at(-1)! + const between = verdicts.slice(0, -1) + const labels: Array = [] + if (verdicts.length > 1 && verdict !== `closed`) + labels.push(`change:several-owners-during-replay`) + if (verdict === `failed` && between.includes(`succeeded`)) + labels.push(`change:between-releases-would-publish`) + if (verdict === `succeeded` && between.includes(`failed`)) + labels.push(`change:between-releases-would-fail`) + return labels + }, +] + +function observeBefore( + model: LifecycleModel, + command: LifecycleCommand, +): LifecycleStep[`before`] { + const current = model.attempts.filter( + ({ syncRunGeneration }) => syncRunGeneration === model.syncRunGeneration, + ) + return { + attemptCount: model.attempts.length, + duplicateOwner: + command.type === `request` && + model.owners.some(({ demand }) => demand === command.demand), + overlappingReplay: + command.type === `truncate` && + model.replayGeneration > 0 && + current.some(({ outcome }) => outcome === undefined), + partialGenerationSupersession: + command.type === `cleanup` && current.some(({ outcome }) => outcome !== undefined) && - current.some(({ outcome }) => outcome === undefined) - ) { - model.reach.add(`partial-generation-supersession`) - } - for (const owner of model.owners) - retireAttempt(model, owner, { unload: false }) - for (const attempt of model.attempts) attempt.gating = false - model.active = false - model.publicationBarrierOpen = false - model.collectionStatus = `cleaned-up` - setStatus(model) - return {} + current.some(({ outcome }) => outcome === undefined), } +} - if (command.type === `restart`) { - if (model.active) { - model.reach.add(`noop:restart`) - return {} - } - model.reach.add(`effective:restart`) - model.active = true - model.syncRunGeneration++ - model.replayGeneration = 0 - model.publicationBarrierOpen = model.owners.some(({ aborted }) => !aborted) - model.collectionStatus = `ready` - setStatus(model, model.owners.length > 0) - const replayLoads: Array = [] - for (const owner of model.owners) { - if (!owner.aborted) replayLoads.push(startAttempt(model, owner, false)) - } - judgeReplay(model) - model.publications++ - model.trace.push({ type: `publication` }) - for (const load of replayLoads) { - model.trace.push({ - type: `load`, - id: load.id, - demand: load.demand, - syncRunGeneration: load.syncRunGeneration, - replayGeneration: load.replayGeneration, - }) - } - setStatus(model) - return {} +/** Pure reference transition. It never reads adapter callbacks or SUT state. */ +export function reduceLifecycle( + model: LifecycleModel, + command: LifecycleCommand, +): LifecycleEffect { + const phase = lifecyclePhase(model) + const row = lifecycleTable.find( + (candidate) => + candidate.from.includes(phase) && + (candidate.event === `*` || candidate.event === command.type) && + (candidate.guard?.(model, command) ?? true), + ) + if (!row) throw new Error(`lifecycle table has no row for ${phase} ${command.type}`) + const before = observeBefore(model, command) + const facts: LifecycleStepFacts = { + releaseVerdicts: [], + replayFailedOwnerDecided: false, } - - model.reach.add(`effective:unsubscribe`) - for (const owner of model.owners) - retireAttempt(model, owner, { unload: true }) - model.owners.length = 0 - model.unsubscribed = true - return {} + const effect = row.effect(model, command, facts) + if (row.to !== `same` && lifecyclePhase(model) !== row.to) + throw new Error( + `lifecycle row ${row.id} ended in ${lifecyclePhase(model)}, not ${row.to}`, + ) + const step: LifecycleStep = { + command, + row, + before, + facts, + attempts: model.attempts.slice(before.attemptCount), + } + for (const label of lifecycleReach.flatMap((rule) => rule(step))) + model.reach.add(label) + return { ...effect, transition: row.id } } export const greenLifecycleHistoryArbitrary = fc.array( From cc6e6c9308553550761ddb902c5dc4140ecbc898 Mon Sep 17 00:00:00 2001 From: "autofix-ci[bot]" <114827586+autofix-ci[bot]@users.noreply.github.com> Date: Mon, 9 Nov 2026 21:05:24 +0000 Subject: [PATCH 4/6] ci: apply automated fixes --- ...n-subscription-lifecycle-grammar-oracle.ts | 32 +++++++++++-------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts b/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts index bbf0a225fa..2516d7b841 100644 --- a/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts +++ b/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts @@ -343,10 +343,7 @@ export function createLifecycleModel( */ export type LifecyclePhase = - | `live` - | `cleaned-up` - | `unsubscribed` - | `unsubscribed-cleaned-up` + `live` | `cleaned-up` | `unsubscribed` | `unsubscribed-cleaned-up` export type LifecycleStateVariable = | `phase` @@ -421,7 +418,8 @@ function replacementSucceeded(model: LifecycleModel): boolean { // Judge an open replay: success closes the publication barrier. Returns // whether the closing judgment decided a failed owner. function judgeReplay(model: LifecycleModel): boolean { - if (!model.publicationBarrierOpen || !replacementSucceeded(model)) return false + if (!model.publicationBarrierOpen || !replacementSucceeded(model)) + return false model.publicationBarrierOpen = false return model.owners.some( ({ attemptId }) => @@ -595,10 +593,7 @@ function admitRequest( // Replay setup is asynchronous even when every acquisition is synchronous or // canceled. Logical owners queue setup; live owners start acquisitions. -function startReplay( - model: LifecycleModel, - facts: LifecycleStepFacts, -): void { +function startReplay(model: LifecycleModel, facts: LifecycleStepFacts): void { model.replayGeneration++ setStatus(model, model.owners.length > 0) // A canceled-only truncate starts no new work. It still opens the @@ -697,7 +692,10 @@ function defineNoopRow(spec: { } } -const ENDED: ReadonlyArray = [`unsubscribed`, `unsubscribed-cleaned-up`] +const ENDED: ReadonlyArray = [ + `unsubscribed`, + `unsubscribed-cleaned-up`, +] const SUBSCRIBED: ReadonlyArray = [`live`, `cleaned-up`] const LIVE: ReadonlyArray = [`live`] const CLEANED: ReadonlyArray = [`cleaned-up`] @@ -728,7 +726,12 @@ export const lifecycleTable: ReadonlyArray = [ from: [`unsubscribed-cleaned-up`], event: `restart`, to: `unsubscribed`, - writes: [`phase`, `generations`, `publication-barrier`, `collection-status`], + writes: [ + `phase`, + `generations`, + `publication-barrier`, + `collection-status`, + ], effect: (model) => { model.active = true model.syncRunGeneration++ @@ -997,7 +1000,9 @@ export const lifecycleTable: ReadonlyArray = [ model.active = true model.syncRunGeneration++ model.replayGeneration = 0 - model.publicationBarrierOpen = model.owners.some(({ aborted }) => !aborted) + model.publicationBarrierOpen = model.owners.some( + ({ aborted }) => !aborted, + ) model.collectionStatus = `ready` setStatus(model, model.owners.length > 0) const replayLoads: Array = [] @@ -1176,7 +1181,8 @@ export function reduceLifecycle( (candidate.event === `*` || candidate.event === command.type) && (candidate.guard?.(model, command) ?? true), ) - if (!row) throw new Error(`lifecycle table has no row for ${phase} ${command.type}`) + if (!row) + throw new Error(`lifecycle table has no row for ${phase} ${command.type}`) const before = observeBefore(model, command) const facts: LifecycleStepFacts = { releaseVerdicts: [], From 0d442c52767f0e71d7e9de794df5ede4f27da18c Mon Sep 17 00:00:00 2001 From: Test Date: Mon, 9 Nov 2026 14:21:11 -0700 Subject: [PATCH 5/6] test(oracles): judge replaced attempts per replay step and record the abort check The replacement-abort check ran inside the adapter's loadSubset and threw there. A throw from loadSubset rejects the acquisition, so the oracle could lose the message and skip bookkeeping. It also judged every attempt the model had aborted so far, not the attempts the replay replaces. This commit records violations in a driver array, asserts them at each checkpoint under the header's law, and judges only the attempts this command aborts. An attempt aborted by an earlier command was judged in that command. Law: header of the lifecycle grammar, "A replay that replaces an attempt aborts it too", and ARCHITECTURE normative law 9 (a truncate replacement stays private until its replay's work settles). Reach: `replacement-load-replaces-pending-attempt` (a replacement load whose replaced attempt has no settled outcome in the model) is declared in `subscription-lifecycle.replacement-abort` and asserted over the green campaigns (98 of 98 history tests pass, the declaration is reached). Per-history count: not measured in this commit; see the lifecycle-table report for the model-level count. RED: the per-owner scope in the previous draft did not kill P4 (a same-owner double truncate passes), so it was rejected. The unrestricted check is the HEAD behavior: it kills P4. The exhaustive probe of all histories up to length three with two requests (1,152 runs with both cancellations) found no legal history that fails the HEAD check. The reported counterexample (a per-owner abort followed by a load) is therefore not reproduced; the scope change follows the law's wording, not a failing history. GREEN: unchanged production passes the history oracle (98 of 98, reach asserted). Two fixed regressions (an aborted peer then truncate; a truncate, abort, then truncate) replay the same driver and model. Mutant: P4 (a newer replay does not abort the replaced acquisitions) is killed by the step-scoped check: 15 failing tests, with the new message on 53 lines. Limits: the check covers only aborts the model records in the step that replaces the attempt; a signal aborted after the load but before the checkpoint is still a violation. Replacement-pending reach is not counted per history. Co-authored-by: Isaac --- ...-lifecycle-history-oracle.property.test.ts | 105 +++++++++++++++--- 1 file changed, 92 insertions(+), 13 deletions(-) diff --git a/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts b/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts index 0a9d67dc75..d127b6c3eb 100644 --- a/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts +++ b/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts @@ -454,6 +454,8 @@ function updateCallerOutcomes( } } +const replacementPendingReachLabel = `replacement-load-replaces-pending-attempt` + async function runHistory( history: ReadonlyArray, runOptions: { @@ -474,6 +476,12 @@ async function runHistory( const check = runOptions.continueAfterMismatch ? expect.soft : expect const failures = new Map() const abortFailures = new Map() + // Judged at each checkpoint, not inside the adapter: a throw from + // loadSubset would reject the acquisition instead of failing the oracle. + const replacementAbortViolations: Array = [] + const driverReach = new Set() + // Attempts the model had already aborted before the current command. + let abortedBeforeStep = new Set() const abortFailureForAttempt = (attemptId: number): Error => { let failure = abortFailures.get(attemptId) if (!failure) { @@ -641,18 +649,25 @@ async function runHistory( ) } watchCoreAbortListeners(observed.id, options.signal) - // A replay that replaces an attempt aborts it before the - // replacement's load starts (header: "A replay that replaces an - // attempt aborts it too"). The model has already reduced this - // command, so every earlier attempt it marks aborted must have an - // aborted signal at this call, not merely by the next checkpoint. + // Law (header: "A replay that replaces an attempt aborts it + // too"): every attempt that this command's replay replaces, one + // the model aborts in this step, is aborted before its + // replacement loads. Attempts aborted in earlier steps were + // judged in those steps. The model has already reduced this + // command, so the check reads the aborts it recorded. for (const earlier of runtimeAttempts.values()) { if (earlier.id === observed.id) continue - if (!model.attempts[earlier.id]?.aborted) continue - check( - earlier.options.signal?.aborted, - `replaced attempt ${earlier.id} is aborted before replacement ${observed.id} loads`, - ).toBe(true) + const replaced = model.attempts[earlier.id] + if (!replaced?.aborted || abortedBeforeStep.has(earlier.id)) + continue + // Reach: the replaced attempt had no settled outcome in the + // model when its replacement loaded. + if (replaced.outcome === undefined) + driverReach.add(replacementPendingReachLabel) + if (!earlier.options.signal?.aborted) + replacementAbortViolations.push( + `replaced attempt ${earlier.id} is not aborted before replacement ${observed.id} loads`, + ) } owner.attemptId = observed.id attemptByOptions.set(options, observed.id) @@ -751,6 +766,10 @@ async function runHistory( Array.from({ length: model.publications }, () => []), ) check(observedTrace, context).toEqual(model.trace) + check( + replacementAbortViolations, + `replaced attempts are aborted before their replacements load (header: "A replay that replaces an attempt aborts it too"): ${context}`, + ).toEqual([]) for (const attempt of model.attempts) if (attempt.outcome !== undefined && !attempt.aborted) check( @@ -814,6 +833,9 @@ async function runHistory( } const runtimeAttempt = command.type === `settle` ? selectRuntimeAttempt(command) : undefined + abortedBeforeStep = new Set( + model.attempts.flatMap(({ id, aborted }) => (aborted ? [id] : [])), + ) const effect = reduceLifecycle(model, command) if (command.type === `request` && effect.ownerId !== undefined) { const result = model.results.at(-1)! @@ -1066,7 +1088,7 @@ async function runHistory( ) } if (primaryFailed) throw primaryFailure - return new Set([...model.reach, ...terminalReach]) + return new Set([...model.reach, ...terminalReach, ...driverReach]) } if ( @@ -1697,6 +1719,37 @@ describe(`CollectionSubscription async lifecycle history oracle`, () => { expect(reached).toContain(`change:between-releases-would-publish`) }) + // Two owners across a truncate: each replacement load judges the attempts + // this command's replay replaces. These replay the shared driver and model. + it.each([ + { + name: `an aborted peer and a pending owner`, + history: [ + { type: `request`, demand: `a` }, + { type: `request`, demand: `b` }, + { type: `abort`, demand: `a` }, + { type: `truncate` }, + ], + }, + { + name: `an abort after the first replay`, + history: [ + { type: `request`, demand: `a` }, + { type: `request`, demand: `b` }, + { type: `truncate` }, + { type: `abort`, demand: `a` }, + { type: `truncate` }, + ], + }, + ] satisfies Array<{ name: string; history: Array }>)( + `replaces each owner's pending attempt before its replacement loads for $name`, + async ({ history }) => { + oracleRoute(`fixed history`) + await runHistory(history) + await runHistory(history, { cancellation: `reject` }) + }, + ) + // Prompt cancellation of the replaced owner's replay load is a settlement: // the held replacement covers it, so the replay publishes. it(`publishes a replay when a covered owner's replay load is canceled`, async () => { @@ -1766,6 +1819,32 @@ describe(`CollectionSubscription async lifecycle history oracle`, () => { `reject` as const, ) + // A replacement load that replaces a pending attempt is the state the + // replacement-abort law judges. The campaigns must reach it. + const replacementReachStates = { + [replacementPendingReachLabel]: `a replacement load while its replaced attempt is pending`, + } as const + const replacementReach = createOracleReach( + `subscription-lifecycle.replacement-abort`, + Object.values(replacementReachStates), + ) + let greenHistoriesRan = false + afterAll(() => { + if (greenHistoriesRan) replacementReach.assertReached() + }) + const runGreenHistory = async ( + history: ReadonlyArray, + cancellation: `manual` | `reject`, + ) => { + greenHistoriesRan = true + replacementReach.beginHistory() + const reached = await runHistory(history, { cancellation }) + if (reached.has(replacementPendingReachLabel)) + replacementReach.reach( + replacementReachStates[replacementPendingReachLabel], + ) + } + const greenLifecycleHistoryFixedSeed = oracleFixedSeed(1_657_003, { numRuns: runs, }) @@ -1776,7 +1855,7 @@ describe(`CollectionSubscription async lifecycle history oracle`, () => { `matches the pure lifecycle model for a fixed seed`, async (history, cancellation) => { oracleRoute(oracleRouteOf(greenLifecycleHistoryFixedSeed)) - await runHistory(history, { cancellation }) + await runGreenHistory(history, cancellation) }, 120_000, ) @@ -1792,7 +1871,7 @@ describe(`CollectionSubscription async lifecycle history oracle`, () => { `matches the pure lifecycle model for a random or replayed seed`, async (history, cancellation) => { oracleRoute(oracleRouteOf(greenLifecycleHistoryCampaign)) - await runHistory(history, { cancellation }) + await runGreenHistory(history, cancellation) }, 120_000, ) From 00b621003b7385be0131541bccaf4ad1392c213e Mon Sep 17 00:00:00 2001 From: Test Date: Mon, 9 Nov 2026 14:42:35 -0700 Subject: [PATCH 6/6] test(oracles): check lifecycle row writes mechanically and declare every row The transition table's writes were hand-declared and under-declared: truncate, cleanup, and restart change owners through the attempts they retire and start, and they were not listed. The engine now checks each effect against the projected state. It throws when a row changes a variable it does not declare, and when a row ends in a phase other than `to`, or changes phase on a `same` row. Each fired row adds row:; the campaigns declare all 23 rows. Also in this commit: - replace-owner without a replaced owner is a noop row (law 10: "marks one held owner as the replacement"). Flagged: a second replace overwrites `replaces`. - cleanup-run and restart-run authorities cite the clauses that support them. The status change at cleanup is a flagged inference, because law 14 keeps the prior status only while adapter cleanup is pending. - Two constructed prefixes reach the two pairs that no generated history produced (replace-owner then change-noop; restart-run then replace-owner), each followed by a random tail. - Shared helpers and effects (settleReplay, beginSyncRun, endSyncRun, unsubscribeOwners, replacementHeld, attemptOf), one reach predicate function switched on the row, selected targets passed to effects, no `transition` field, unexported engine internals, and an alias for the duplicate generator. The parked-reload attempt count is a labeled table with its authority. Law: the lifecycle grammar header and ARCHITECTURE normative laws 9, 10, and 14. Changed: replace-owner with no replaced owner (law 10); flagged inferences as noted. Everything else is the pre-splice reducer's law. Reach: row: for all 23 rows, declared in subscription-lifecycle.rows and reached across the green and demand-change campaigns (99 of 99 history tests). Generated coverage over 68,022 histories: all 23 rows fire; the least-fired row (ended-restart) fires in 13,416 histories. The two constructed pairs had zero generated histories before this commit. RED: the new mechanical check was not run against the old declarations; the declarations were corrected by reading the code. Limits of that claim: the check covers writes only. Reads are declared and not measured. Differential against the pre-splice reducer (fecdc4e4c): 60,088 histories, 575,876 steps, four configurations. Zero mismatches in effect and full state (row labels excluded). 1,484 histories diverge at a replace whose replaced demand has no owner, the intended change: the old reducer set `replaces` to [] there. Each such history stops at its first divergence. GREEN: history oracle 99 of 99 (unchanged production); publication and lifecycle consumers 265 of 265; eslint, prettier, lint:changed, and the package typecheck clean (the vite.config rootDir error is pre-existing). Mutant: guarded runs of P1 to P5 on this code, one at a time, tree restored after each: all killed (75, 19, 3, 15, and 30 failing tests). Limits: writes are checked, reads are not. Breadth-first coverage was measured to depth 6 only. The cleanup status change is an inference. The second replace's overwrite is an inference, not a clause. Co-authored-by: Isaac --- ...n-subscription-lifecycle-grammar-oracle.ts | 651 ++++++++++-------- ...-lifecycle-history-oracle.property.test.ts | 58 ++ 2 files changed, 414 insertions(+), 295 deletions(-) diff --git a/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts b/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts index bbf0a225fa..09a7237541 100644 --- a/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts +++ b/packages/db/tests/collection-subscription-lifecycle-grammar-oracle.ts @@ -282,8 +282,6 @@ export type LifecycleEffect = { ownerIds?: Array attemptId?: number requestResult?: boolean - // The lifecycle table row that decided this command. - transition?: string } export function createLifecycleModel( @@ -323,32 +321,28 @@ export function createLifecycleModel( * * The reducer is an extended state machine. Its phase is a function of two * model flags: `unsubscribed` (this subscription has ended) and `active` (the - * Collection's sync run is live). Each row of `lifecycleTable` fires when its - * event matches the command, the phase is one of its `from` phases, and its - * guard holds. Rows are tried in order: an effective row precedes the noop row - * that catches the same event when its guard fails. The engine asserts that - * each row ends in its `to` phase, so a row whose effect disagrees with the - * table fails at once. + * Collection's sync run is live). `lifecycleTable` has one row per phase and + * event. Rows are tried in order: an effective row precedes the noop row that + * catches the same event when the effective row's `select` finds no target. * - * Rows do not write reach. `lifecycleReach` declares each reach label as a - * predicate over one step: the row that fired, the command, state captured - * before the effect, the facts the effect recorded, and the attempts it - * created. Transition coverage is therefore a property of the table: a label - * `effective:` or `noop:` names the kind of row that fired. + * Each row states the phase it ends in (`to`, or `same` when the phase must not + * change) and the state variables it may write (`writes`). The engine checks + * both after every effect. A phase change the row did not state throws, and so + * does a write to a variable the row did not declare. `writes` is therefore + * checked against the state, not hand-audited. Reads (`reads`) are declared + * only: nothing measures them. * - * `reads` and `writes` list the extended-state variables that a row's guard or - * effect reads or changes. Every row also reads `phase`, because its `from` - * dispatch does. Two rows interact when the second reads a variable the first - * writes. Coverage measures those adjacent pairs. + * Reach comes from the table too. Every fired row adds `row:`, and + * `lifecycleRowIds` names all of them, so a campaign declares that it reaches + * every row. The other reach labels are predicates over one step: the command, + * the row, the state captured before the effect, the facts the effect recorded, + * and the attempts it created. */ export type LifecyclePhase = - | `live` - | `cleaned-up` - | `unsubscribed` - | `unsubscribed-cleaned-up` + `live` | `cleaned-up` | `unsubscribed` | `unsubscribed-cleaned-up` -export type LifecycleStateVariable = +type LifecycleStateVariable = | `phase` | `owners` | `attempts` @@ -356,22 +350,32 @@ export type LifecycleStateVariable = | `publication-barrier` | `collection-status` -export type ReplayVerdict = `closed` | `open` | `failed` | `succeeded` +type ReplayVerdict = `closed` | `open` | `failed` | `succeeded` -/** Facts an effect records for the reach predicates. They are data, not reach. */ -export type LifecycleStepFacts = { +// Facts an effect records for the reach predicates. They are data, not reach. +type LifecycleStepFacts = { // `change`: the replay verdict after each release, in release order. releaseVerdicts: Array // This step's replay judgment closed the barrier on a failed owner. replayFailedOwnerDecided: boolean } -export function lifecyclePhase(model: LifecycleModel): LifecyclePhase { +function lifecyclePhase(model: LifecycleModel): LifecyclePhase { if (model.unsubscribed) return model.active ? `unsubscribed` : `unsubscribed-cleaned-up` return model.active ? `live` : `cleaned-up` } +function attemptOf(model: LifecycleModel, attemptId: number): LifecycleAttempt { + const attempt = model.attempts[attemptId] + if (!attempt) throw new Error(`model lost attempt ${attemptId}`) + return attempt +} + +// A held attempt in the replacement's publication boundary keeps it open. +const replacementHeld = (attempt: LifecycleAttempt) => + attempt.gating && attempt.inReplacement + function setStatus(model: LifecycleModel, queuedReplay = false): void { if (model.unsubscribed) return const status = @@ -398,14 +402,12 @@ function setStatus(model: LifecycleModel, queuedReplay = false): void { function replacementSucceeded(model: LifecycleModel): boolean { const loaded = ({ attemptId }: LifecycleOwner) => attemptId === undefined || - (model.attempts[attemptId]!.outcome === `resolve` && - !model.attempts[attemptId]!.endedByAbort) + (attemptOf(model, attemptId).outcome === `resolve` && + !attemptOf(model, attemptId).endedByAbort) const owesNothing = ({ attemptId }: LifecycleOwner) => - attemptId === undefined || model.attempts[attemptId]!.endedByAbort + attemptId === undefined || attemptOf(model, attemptId).endedByAbort return ( - !model.attempts.some( - ({ gating, inReplacement }) => gating && inReplacement, - ) && + !model.attempts.some(replacementHeld) && model.owners.every( (owner) => loaded(owner) || @@ -421,48 +423,46 @@ function replacementSucceeded(model: LifecycleModel): boolean { // Judge an open replay: success closes the publication barrier. Returns // whether the closing judgment decided a failed owner. function judgeReplay(model: LifecycleModel): boolean { - if (!model.publicationBarrierOpen || !replacementSucceeded(model)) return false + if (!model.publicationBarrierOpen || !replacementSucceeded(model)) + return false model.publicationBarrierOpen = false return model.owners.some( ({ attemptId }) => attemptId !== undefined && - model.attempts[attemptId]!.outcome === `reject` && - !model.attempts[attemptId]!.endedByAbort, + attemptOf(model, attemptId).outcome === `reject` && + !attemptOf(model, attemptId).endedByAbort, ) } +// Every effect that can change the replay judges it, then updates status. +function settleReplay(model: LifecycleModel, facts: LifecycleStepFacts): void { + facts.replayFailedOwnerDecided = judgeReplay(model) + setStatus(model) +} + // What judging the open replay now would decide. Only `change` asks, to name // the histories in which judging between its releases would differ. function replayVerdict(model: LifecycleModel): ReplayVerdict { if (!model.publicationBarrierOpen) return `closed` - if ( - model.attempts.some(({ gating, inReplacement }) => gating && inReplacement) - ) - return `open` + if (model.attempts.some(replacementHeld)) return `open` return replacementSucceeded(model) ? `succeeded` : `failed` } // Retire one logical owner and its acquisition lease without judging the // replay: the caller judges once its whole demand change has retired. -function retireOwner( - model: LifecycleModel, - demand: DemandName, -): LifecycleOwner | undefined { - const index = model.owners.findIndex((owner) => owner.demand === demand) - if (index === -1) return undefined - const [owner] = model.owners.splice(index, 1) - retireAttempt(model, owner!, { unload: true }) +function retireOwner(model: LifecycleModel, owner: LifecycleOwner): void { + model.owners.splice(model.owners.indexOf(owner), 1) + retireAttempt(model, owner, true) // Retirement removes the logical owner, including its older transports. - for (const attempt of model.attempts) { - if (attempt.ownerId === owner!.id) attempt.gating = false - } - return owner + for (const attempt of model.attempts) + if (attempt.ownerId === owner.id) attempt.gating = false } +// Starts the owner's acquisition attempt. The caller traces the load, so +// that the trace order is the caller's. function startAttempt( model: LifecycleModel, owner: LifecycleOwner, - trace = true, ): LifecycleAttempt { const id = model.nextAttemptId++ const attempt: LifecycleAttempt = { @@ -484,49 +484,46 @@ function startAttempt( failure: model.failureForAttempt(id), } model.attempts.push(attempt) - model.loads.push({ - id, + model.loads.push(loadEventOf(attempt)) + owner.attemptId = attempt.id + return attempt +} + +function loadEventOf(attempt: LifecycleAttempt): LifecycleLoadEvent { + return { + id: attempt.id, demand: attempt.demand, syncRunGeneration: attempt.syncRunGeneration, replayGeneration: attempt.replayGeneration, - }) - if (trace) { - model.trace.push({ - type: `load`, - id, - demand: attempt.demand, - syncRunGeneration: attempt.syncRunGeneration, - replayGeneration: attempt.replayGeneration, - }) } - owner.attemptId = id - return attempt } +function traceLoad(model: LifecycleModel, attempt: LifecycleAttempt): void { + model.trace.push({ type: `load`, ...loadEventOf(attempt) }) +} + +// Ends the owner's current attempt. `unload` gives the adapter its unload. function retireAttempt( model: LifecycleModel, owner: LifecycleOwner, - options: { unload: boolean; trace?: boolean }, + unload: boolean, ): void { if (owner.attemptId === undefined) return - const attempt = model.attempts[owner.attemptId] + const attempt = attemptOf(model, owner.attemptId) owner.attemptId = undefined - if (!attempt) throw new Error(`model lost attempt`) attempt.gating = false attempt.reportable = false abortAttempt(model, attempt) - if (options.unload) { + if (unload) { model.unloads.push({ attemptId: attempt.id, handlerSyncRunGeneration: model.syncRunGeneration, }) - if (options.trace !== false) { - model.trace.push({ - type: `unload`, - attemptId: attempt.id, - handlerSyncRunGeneration: model.syncRunGeneration, - }) - } + model.trace.push({ + type: `unload`, + attemptId: attempt.id, + handlerSyncRunGeneration: model.syncRunGeneration, + }) } } @@ -540,6 +537,8 @@ function abortAttempt(model: LifecycleModel, attempt: LifecycleAttempt): void { attempt.outcome = `reject` } +// The attempt a settlement names: an open attempt of the demand that is +// current (or obsolete, for `scope`), oldest or newest by `age`. function selectAttempt( model: LifecycleModel, command: Extract, @@ -574,15 +573,19 @@ function admitRequest( } model.owners.push(owner) // A waiting owner gets a promise now, without claiming an acquisition. - const result = acquires - ? { - attemptId: startAttempt(model, owner).id, - resultKind: - model.acquisitionMode === `async-pending` - ? (`promise` as const) - : (`true` as const), - } - : ({ attemptId: `unacquired`, resultKind: `promise` } as const) + let result: LifecycleResultEvent = { + attemptId: `unacquired`, + resultKind: `promise`, + } + if (acquires) { + const attempt = startAttempt(model, owner) + traceLoad(model, attempt) + result = { + attemptId: attempt.id, + resultKind: + model.acquisitionMode === `async-pending` ? `promise` : `true`, + } + } model.results.push(result) model.trace.push({ type: `result`, ...result }) setStatus(model) @@ -595,10 +598,7 @@ function admitRequest( // Replay setup is asynchronous even when every acquisition is synchronous or // canceled. Logical owners queue setup; live owners start acquisitions. -function startReplay( - model: LifecycleModel, - facts: LifecycleStepFacts, -): void { +function startReplay(model: LifecycleModel, facts: LifecycleStepFacts): void { model.replayGeneration++ setStatus(model, model.owners.length > 0) // A canceled-only truncate starts no new work. It still opens the @@ -606,18 +606,38 @@ function startReplay( // attempt below ends its wait. model.publicationBarrierOpen = model.owners.some(({ aborted }) => !aborted) || - model.attempts.some(({ gating, inReplacement }) => gating && inReplacement) + model.attempts.some(replacementHeld) for (const owner of model.owners) { // Replacing an acquisition is not releasing its logical owner, but it // ends the replaced load: it holds neither readiness nor publication. - retireAttempt(model, owner, { unload: true }) - if (!owner.aborted) startAttempt(model, owner) + retireAttempt(model, owner, true) + if (!owner.aborted) traceLoad(model, startAttempt(model, owner)) } - facts.replayFailedOwnerDecided = judgeReplay(model) + settleReplay(model, facts) +} + +// The sync-run boundary that cleanup ends and restart begins. +function endSyncRun(model: LifecycleModel): void { + model.active = false + model.collectionStatus = `cleaned-up` setStatus(model) } -/** The command's type, or the wildcard for every command. */ +function beginSyncRun(model: LifecycleModel): void { + model.active = true + model.syncRunGeneration++ + model.replayGeneration = 0 + model.collectionStatus = `ready` +} + +// Unsubscribe ends this subscription: its owners retire and release their +// acquisition leases. The Collection's sync run survives. +function unsubscribeOwners(model: LifecycleModel): void { + for (const owner of model.owners) retireAttempt(model, owner, true) + model.owners.length = 0 + model.unsubscribed = true +} + type LifecycleEvent = LifecycleCommand[`type`] | `*` type CommandFor = E extends `*` ? LifecycleCommand @@ -629,51 +649,44 @@ export type LifecycleRow = { from: ReadonlyArray event: LifecycleEvent to: LifecyclePhase | `same` - guard?: (model: LifecycleModel, command: LifecycleCommand) => boolean + // The target a row acts on, found once. A row whose select finds none does + // not fire, and the noop row for its event fires instead. + select?: (model: LifecycleModel, command: LifecycleCommand) => unknown reads: ReadonlyArray writes: ReadonlyArray effect: ( model: LifecycleModel, command: LifecycleCommand, + target: unknown, facts: LifecycleStepFacts, ) => LifecycleEffect - // The contract clause or dated decision for this row. A noop row cites no - // contract clause: it encodes the grammar's convention that a command with - // no target changes nothing. + // The contract clause or dated decision for this row. A flagged inference + // names what the grammar assumes beyond the contract. authority: string } -type RowSpec = { +type RowSpec = { id: string from: ReadonlyArray event: E to: LifecyclePhase | `same` - guard?: (model: LifecycleModel, command: CommandFor) => boolean + select?: (model: LifecycleModel, command: CommandFor) => T | undefined reads?: ReadonlyArray writes: ReadonlyArray effect: ( model: LifecycleModel, command: CommandFor, + target: T, facts: LifecycleStepFacts, ) => LifecycleEffect authority: string } -// The event dispatch selects the command type, so each row's typed command is -// the one the engine passes it. -function defineRow(spec: RowSpec): LifecycleRow { - return { - id: spec.id, - kind: `effect`, - from: spec.from, - event: spec.event, - to: spec.to, - guard: spec.guard as LifecycleRow[`guard`], - reads: spec.reads ?? [], - writes: spec.writes, - effect: spec.effect as LifecycleRow[`effect`], - authority: spec.authority, - } +function defineRow( + spec: RowSpec, +): LifecycleRow { + // Erases the row's command and target types to the table's shared shape. + return { kind: `effect`, reads: [], ...spec } as unknown as LifecycleRow } function defineNoopRow(spec: { @@ -684,31 +697,25 @@ function defineNoopRow(spec: { result?: LifecycleEffect authority: string }): LifecycleRow { + const { result, ...row } = spec return { - id: spec.id, kind: `noop`, - from: spec.from, - event: spec.event, to: `same`, - reads: spec.reads, writes: [], - effect: () => spec.result ?? {}, - authority: spec.authority, - } + effect: () => result ?? {}, + ...row, + } as LifecycleRow } -const ENDED: ReadonlyArray = [`unsubscribed`, `unsubscribed-cleaned-up`] +const ENDED: ReadonlyArray = [ + `unsubscribed`, + `unsubscribed-cleaned-up`, +] const SUBSCRIBED: ReadonlyArray = [`live`, `cleaned-up`] const LIVE: ReadonlyArray = [`live`] const CLEANED: ReadonlyArray = [`cleaned-up`] -/** - * The lifecycle table. Rows are tried in order, so an effective row precedes - * the noop row for its event. Authority cites the header of the grammar file, ARCHITECTURE - * normative laws (law N), the glossary, or a code comment that states the rule. The noop rows and the inferences marked "inference" have - * no contract clause: they follow the grammar's convention. - */ -export const lifecycleTable: ReadonlyArray = [ +const lifecycleTable: ReadonlyArray = [ // An ended subscription keeps only the Collection's sync-run lifecycle. defineRow({ id: `ended-cleanup`, @@ -717,27 +724,28 @@ export const lifecycleTable: ReadonlyArray = [ to: `unsubscribed-cleaned-up`, writes: [`phase`, `collection-status`], effect: (model) => { - model.active = false - model.collectionStatus = `cleaned-up` + endSyncRun(model) return { requestResult: false } }, - authority: `Header: \`cleanup\` ends the current sync run. An unsubscribed subscription keeps the Collection's sync run, so this cleanup still applies. Adapter cleanup timing is outside this grammar.`, + authority: `Header: "cleanup ends the current sync run"; unsubscribe does not end it, so cleanup still applies. Flagged inference: adapter cleanup settles before the next command, so the status is cleaned-up at once. ARCHITECTURE law 14 keeps the prior status only while adapter cleanup is pending, which this grammar does not model.`, }), defineRow({ id: `ended-restart`, from: [`unsubscribed-cleaned-up`], event: `restart`, to: `unsubscribed`, - writes: [`phase`, `generations`, `publication-barrier`, `collection-status`], + writes: [ + `phase`, + `generations`, + `publication-barrier`, + `collection-status`, + ], effect: (model) => { - model.active = true - model.syncRunGeneration++ - model.replayGeneration = 0 + beginSyncRun(model) model.publicationBarrierOpen = false - model.collectionStatus = `ready` return { requestResult: false } }, - authority: `Header: \`restart\` starts a new sync run; unsubscribe does not end the Collection's sync run, so restart applies only after cleanup.`, + authority: `Header: "restart starts a new sync run"; restart applies only after cleanup, since unsubscribe does not end the Collection's sync run. Flagged inference: restart closes the publication barrier, because no replay is open for an ended subscription.`, }), defineNoopRow({ id: `ended-noop`, @@ -756,7 +764,7 @@ export const lifecycleTable: ReadonlyArray = [ reads: [`publication-barrier`], writes: [`owners`, `attempts`], effect: (model, command) => admitRequest(model, command.demand, true), - authority: `Header: "a request combines a new logical owner with any acquisition attempt it starts."`, + authority: `Header: "a request combines a new logical owner with any acquisition attempt it starts"; glossary: logical subset owner, acquisition attempt.`, }), defineRow({ id: `request-cleaned`, @@ -774,29 +782,26 @@ export const lifecycleTable: ReadonlyArray = [ from: SUBSCRIBED, event: `abort`, to: `same`, - guard: (model, command) => - model.owners.some( + select: (model, command) => + model.owners.find( ({ demand, aborted }) => demand === command.demand && !aborted, ), reads: [`owners`, `attempts`, `publication-barrier`], writes: [`owners`, `attempts`, `publication-barrier`], - effect: (model, command, facts) => { - const owner = model.owners.find( - ({ demand, aborted }) => demand === command.demand && !aborted, - )! - owner.aborted = true - if (owner.attemptId !== undefined) { - const attempt = model.attempts[owner.attemptId]! + effect: (model, _command, owner, facts) => { + const abortedOwner = owner + abortedOwner.aborted = true + if (abortedOwner.attemptId !== undefined) { + const attempt = attemptOf(model, abortedOwner.attemptId) abortAttempt(model, attempt) attempt.reportable = false } // The abort ends the attempt, so the replay is judged as after any // settlement: a held replacement can still cover it. - facts.replayFailedOwnerDecided = judgeReplay(model) - setStatus(model) - return { ownerId: owner.id } + settleReplay(model, facts) + return { ownerId: abortedOwner.id } }, - authority: `Header: "abort cancels the owner's current acquisition attempt but does not retire the owner"; "an abort ends the load" (maintainer decision), so the attempt holds no readiness and a later settlement reports nothing.`, + authority: `Header: "abort cancels the owner's current acquisition attempt but does not retire the owner"; "an abort ends the load" (maintainer decision): the attempt holds no readiness and a later settlement reports nothing.`, }), defineNoopRow({ id: `abort-noop`, @@ -811,15 +816,15 @@ export const lifecycleTable: ReadonlyArray = [ from: SUBSCRIBED, event: `release`, to: `same`, - guard: (model, command) => - model.owners.some(({ demand }) => demand === command.demand), + select: (model, command) => + model.owners.find(({ demand }) => demand === command.demand), reads: [`owners`, `attempts`, `publication-barrier`], writes: [`owners`, `attempts`, `publication-barrier`], - effect: (model, command, facts) => { - const owner = retireOwner(model, command.demand)! - facts.replayFailedOwnerDecided = judgeReplay(model) - setStatus(model) - return { ownerId: owner.id } + effect: (model, _command, owner, facts) => { + const released = owner + retireOwner(model, released) + settleReplay(model, facts) + return { ownerId: released.id } }, authority: `Header: "release combines demand retirement with release of that owner's acquisition lease."`, }), @@ -836,28 +841,32 @@ export const lifecycleTable: ReadonlyArray = [ from: SUBSCRIBED, event: `change`, to: `same`, - guard: (model, command) => + select: (model, command) => command.release.some((demand) => model.owners.some((owner) => owner.demand === demand), - ), + ) + ? true + : undefined, reads: [`owners`, `attempts`, `publication-barrier`], writes: [`owners`, `attempts`, `publication-barrier`], - effect: (model, command, facts) => { + effect: (model, command, _target, facts) => { // Law 9: the change is one step. Every named owner retires first, and // the replay is judged once after the last. The verdicts between its // releases are recorded only to name the histories they would mislead. const retired: Array = [] for (const demand of command.release) { - const owner = retireOwner(model, demand) + const owner = model.owners.find( + (candidate) => candidate.demand === demand, + ) if (!owner) continue + retireOwner(model, owner) retired.push(owner) facts.releaseVerdicts.push(replayVerdict(model)) } - facts.replayFailedOwnerDecided = judgeReplay(model) - setStatus(model) + settleReplay(model, facts) return { ownerIds: retired.map(({ id }) => id) } }, - authority: `ARCHITECTURE normative law 9 ("A demand change counts as one step"); header: \`change\` "retires several logical owners at once".`, + authority: `ARCHITECTURE normative law 9 ("A demand change counts as one step"); header: change "retires several logical owners at once".`, }), defineNoopRow({ id: `change-noop`, @@ -872,27 +881,34 @@ export const lifecycleTable: ReadonlyArray = [ from: SUBSCRIBED, event: `replace`, to: `same`, - guard: (model, command) => - model.owners.some(({ demand }) => demand === command.demand), - reads: [`owners`], - writes: [`owners`], - effect: (model, command) => { + select: (model, command) => { const replacement = model.owners.find( ({ demand }) => demand === command.demand, - )! - replacement.replaces = model.owners + ) + const replaced = model.owners .filter(({ demand }) => demand === command.replaced) .map(({ id }) => id) + return replacement && replaced.length > 0 + ? { replacement, replaced } + : undefined + }, + reads: [`owners`], + writes: [`owners`], + effect: (_model, _command, target) => { + const { replacement, replaced } = target + // Flagged inference: a second replace names the replacement anew, so + // its replaced set is its latest union. The grammar does not accumulate. + replacement.replaces = replaced return { ownerId: replacement.id } }, - authority: `ARCHITECTURE normative law 10 ("A fragmented churn replacement retires prior coverage only after its union applies; failure preserves it"); header: \`replace\` "marks one held owner as the replacement".`, + authority: `ARCHITECTURE normative law 10 ("A fragmented churn replacement retires prior coverage only after its union applies"); header: replace "marks one held owner as the replacement". Without a replaced owner nothing is replaced, so the row does not apply.`, }), defineNoopRow({ id: `replace-noop`, from: SUBSCRIBED, event: `replace`, reads: [`owners`], - authority: `none: no logical owner for the replacement. Grammar convention, flagged.`, + authority: `none: no held replacement or no owner for the replaced demand. Grammar convention, flagged.`, }), defineRow({ @@ -900,26 +916,26 @@ export const lifecycleTable: ReadonlyArray = [ from: SUBSCRIBED, event: `settle`, to: `same`, - guard: (model, command) => selectAttempt(model, command) !== undefined, - reads: [`attempts`, `publication-barrier`], + select: (model, command) => selectAttempt(model, command), + reads: [`owners`, `attempts`, `publication-barrier`], writes: [`attempts`, `publication-barrier`], - effect: (model, command, facts) => { - const attempt = selectAttempt(model, command)! + effect: (model, command, target, facts) => { + const attempt = target attempt.outcome = command.outcome attempt.gating = false // A reject reports only while the attempt is reportable and was not - // ended by an abort: a later outcome decides nothing. + // ended by an abort: a later outcome decides nothing. Selected attempts + // have no outcome, so `aborted` and `endedByAbort` agree for them. if ( - command.outcome === `reject` && + attempt.outcome === `reject` && attempt.reportable && - !attempt.aborted + !attempt.endedByAbort ) { model.lastError = attempt.failure model.errors.push({ attemptId: attempt.id, error: attempt.failure }) model.trace.push({ type: `error`, attemptId: attempt.id }) } - facts.replayFailedOwnerDecided = judgeReplay(model) - setStatus(model) + settleReplay(model, facts) return { attemptId: attempt.id } }, authority: `Header: "settle changes an acquisition attempt". A reject reports only while the attempt is reportable and not ended by an abort ("a later settlement reports nothing").`, @@ -938,12 +954,12 @@ export const lifecycleTable: ReadonlyArray = [ event: `truncate`, to: `same`, reads: [`generations`, `owners`, `attempts`, `publication-barrier`], - writes: [`generations`, `attempts`, `publication-barrier`], - effect: (model, _command, facts) => { + writes: [`generations`, `owners`, `attempts`, `publication-barrier`], + effect: (model, _command, _target, facts) => { startReplay(model, facts) return {} }, - authority: `ARCHITECTURE normative law 9 (a truncate replacement stays private until work started by its active replay demands settles); header: "A replay that replaces an attempt aborts it too."`, + authority: `ARCHITECTURE normative law 9 (a truncate replacement stays private until all work started by its active replay demands settles); header: "A replay that replaces an attempt aborts it too".`, }), defineNoopRow({ id: `truncate-noop`, @@ -959,18 +975,22 @@ export const lifecycleTable: ReadonlyArray = [ event: `cleanup`, to: `cleaned-up`, reads: [`owners`, `attempts`, `generations`], - writes: [`attempts`, `publication-barrier`, `phase`, `collection-status`], + writes: [ + `owners`, + `attempts`, + `publication-barrier`, + `phase`, + `collection-status`, + ], effect: (model) => { - for (const owner of model.owners) - retireAttempt(model, owner, { unload: false }) + // Cleanup releases the resources at once and gives no unload. + for (const owner of model.owners) retireAttempt(model, owner, false) for (const attempt of model.attempts) attempt.gating = false - model.active = false model.publicationBarrierOpen = false - model.collectionStatus = `cleaned-up` - setStatus(model) + endSyncRun(model) return {} }, - authority: `Header: \`cleanup\` "ends the current sync run"; ARCHITECTURE normative law 14: cleanup start closes restart admission.`, + authority: `Header: "cleanup ends the current sync run" and releases its resources; ARCHITECTURE law 14: cleanup start synchronously closes restart admission. Flagged inference: the Collection status changes at once, as in ended-cleanup.`, }), defineNoopRow({ id: `cleanup-noop`, @@ -985,41 +1005,32 @@ export const lifecycleTable: ReadonlyArray = [ from: CLEANED, event: `restart`, to: `live`, - reads: [`owners`, `phase`], + reads: [`owners`, `attempts`, `phase`], writes: [ `phase`, `generations`, + `owners`, `attempts`, `publication-barrier`, `collection-status`, ], - effect: (model, _command, facts) => { - model.active = true - model.syncRunGeneration++ - model.replayGeneration = 0 - model.publicationBarrierOpen = model.owners.some(({ aborted }) => !aborted) - model.collectionStatus = `ready` + effect: (model, _command, _target, facts) => { + beginSyncRun(model) + model.publicationBarrierOpen = model.owners.some( + ({ aborted }) => !aborted, + ) setStatus(model, model.owners.length > 0) - const replayLoads: Array = [] - for (const owner of model.owners) { - if (!owner.aborted) replayLoads.push(startAttempt(model, owner, false)) - } + const replayAttempts = model.owners + .filter(({ aborted }) => !aborted) + .map((owner) => startAttempt(model, owner)) facts.replayFailedOwnerDecided = judgeReplay(model) model.publications++ model.trace.push({ type: `publication` }) - for (const load of replayLoads) { - model.trace.push({ - type: `load`, - id: load.id, - demand: load.demand, - syncRunGeneration: load.syncRunGeneration, - replayGeneration: load.replayGeneration, - }) - } + for (const attempt of replayAttempts) traceLoad(model, attempt) setStatus(model) return {} }, - authority: `Header: \`restart\` "starts a new sync run"; an aborted owner is not restarted ("an abort ends the load").`, + authority: `Header: "restart starts a new sync run". ARCHITECTURE law 9: a replay stays private until its work settles, so the barrier opens for the owners that are not aborted. Flagged inferences: the publication is emitted before the replay loads, and an aborted owner starts no new attempt ("an abort ends the load").`, }), defineNoopRow({ id: `restart-noop`, @@ -1037,10 +1048,7 @@ export const lifecycleTable: ReadonlyArray = [ reads: [`owners`, `attempts`], writes: [`owners`, `attempts`, `phase`], effect: (model) => { - for (const owner of model.owners) - retireAttempt(model, owner, { unload: true }) - model.owners.length = 0 - model.unsubscribed = true + unsubscribeOwners(model) return {} }, authority: `Header: "unsubscribe ends this subscription, retires its logical subset owners, and releases their acquisition leases. It does not end the Collection's sync run."`, @@ -1053,18 +1061,20 @@ export const lifecycleTable: ReadonlyArray = [ reads: [`owners`, `attempts`], writes: [`owners`, `attempts`, `phase`], effect: (model) => { - for (const owner of model.owners) - retireAttempt(model, owner, { unload: true }) - model.owners.length = 0 - model.unsubscribed = true + unsubscribeOwners(model) return {} }, authority: `Header: as unsubscribe-live. The cleaned-up Collection keeps its status.`, }), ] -/** Reach labels, each a predicate over one step. */ -export type LifecycleStep = { +/** The reach labels of every row. A campaign that declares them must fire each row. */ +export const lifecycleRowLabels: ReadonlyArray = lifecycleTable.map( + ({ id }) => `row:${id}`, +) + +// The observations a step may name. Each is data about one step, not reach. +type LifecycleStep = { command: LifecycleCommand row: LifecycleRow before: { @@ -1096,50 +1106,50 @@ function settleLabels(command: Extract) { ] } -export const lifecycleReach: ReadonlyArray< - (step: LifecycleStep) => ReadonlyArray -> = [ - ({ command, row }) => [ +function changeLabels(verdicts: ReadonlyArray): Array { + const verdict = verdicts.at(-1)! + const between = verdicts.slice(0, -1) + const labels: Array = [] + if (verdicts.length > 1 && verdict !== `closed`) + labels.push(`change:several-owners-during-replay`) + if (verdict === `failed` && between.includes(`succeeded`)) + labels.push(`change:between-releases-would-publish`) + if (verdict === `succeeded` && between.includes(`failed`)) + labels.push(`change:between-releases-would-fail`) + return labels +} + +function lifecycleReachLabels(step: LifecycleStep): Array { + const { command, row, before, facts, attempts } = step + const labels = [ + `row:${row.id}`, `command:${command.type}`, `${row.kind === `effect` ? `effective` : `noop`}:${command.type}`, - ], - ({ before, row }) => - row.id === `request-live` || row.id === `request-cleaned` - ? before.duplicateOwner - ? [`duplicate-owner`] - : [] - : [], - ({ row }) => (row.id === `request-cleaned` ? [`request-while-cleaned`] : []), - ({ before, row }) => - row.id === `truncate-replay` && before.overlappingReplay - ? [`overlapping-replay`] - : [], - ({ before, row }) => - row.id === `cleanup-run` && before.partialGenerationSupersession - ? [`partial-generation-supersession`] - : [], - ({ command, row }) => - row.kind === `effect` && command.type === `settle` - ? settleLabels(command) - : [], - ({ attempts }) => attempts.flatMap(attemptLabels), - ({ facts }) => - facts.replayFailedOwnerDecided ? [`replacement-decides-failed-owner`] : [], - ({ facts, row }) => { - if (row.id !== `change-demands`) return [] - const verdicts = facts.releaseVerdicts - const verdict = verdicts.at(-1)! - const between = verdicts.slice(0, -1) - const labels: Array = [] - if (verdicts.length > 1 && verdict !== `closed`) - labels.push(`change:several-owners-during-replay`) - if (verdict === `failed` && between.includes(`succeeded`)) - labels.push(`change:between-releases-would-publish`) - if (verdict === `succeeded` && between.includes(`failed`)) - labels.push(`change:between-releases-would-fail`) - return labels - }, -] + ...attempts.flatMap(attemptLabels), + ] + if (facts.replayFailedOwnerDecided) + labels.push(`replacement-decides-failed-owner`) + if (row.kind === `effect` && command.type === `settle`) + labels.push(...settleLabels(command)) + switch (row.id) { + case `request-live`: + case `request-cleaned`: + if (before.duplicateOwner) labels.push(`duplicate-owner`) + if (row.id === `request-cleaned`) labels.push(`request-while-cleaned`) + break + case `truncate-replay`: + if (before.overlappingReplay) labels.push(`overlapping-replay`) + break + case `cleanup-run`: + if (before.partialGenerationSupersession) + labels.push(`partial-generation-supersession`) + break + case `change-demands`: + labels.push(...changeLabels(facts.releaseVerdicts)) + break + } + return labels +} function observeBefore( model: LifecycleModel, @@ -1164,29 +1174,72 @@ function observeBefore( } } +// The first row that the phase, event, and select admit, with its target. +function selectRow( + model: LifecycleModel, + command: LifecycleCommand, +): { row: LifecycleRow; target: unknown } { + const phase = lifecyclePhase(model) + for (const row of lifecycleTable) { + if (!row.from.includes(phase)) continue + if (row.event !== `*` && row.event !== command.type) continue + const target = row.select?.(model, command) + if (row.select && target === undefined) continue + return { row, target } + } + throw new Error(`lifecycle table has no row for ${phase} ${command.type}`) +} + +// The state variables the engine checks for undeclared writes. Outputs such as +// `status`, `trace`, `reach`, and the adapter lists are observations, not state. +function projectVariables( + model: LifecycleModel, +): Record { + return { + phase: lifecyclePhase(model), + owners: JSON.stringify(model.owners), + attempts: JSON.stringify(model.attempts, (key, value) => + key === `failure` ? undefined : value, + ), + generations: `${model.syncRunGeneration}/${model.replayGeneration}`, + 'publication-barrier': String(model.publicationBarrierOpen), + 'collection-status': model.collectionStatus, + } +} + +const stateVariables = Object.keys( + projectVariables(createLifecycleModel()), +) as Array + /** Pure reference transition. It never reads adapter callbacks or SUT state. */ export function reduceLifecycle( model: LifecycleModel, command: LifecycleCommand, ): LifecycleEffect { - const phase = lifecyclePhase(model) - const row = lifecycleTable.find( - (candidate) => - candidate.from.includes(phase) && - (candidate.event === `*` || candidate.event === command.type) && - (candidate.guard?.(model, command) ?? true), - ) - if (!row) throw new Error(`lifecycle table has no row for ${phase} ${command.type}`) + const phaseBefore = lifecyclePhase(model) + const { row, target } = selectRow(model, command) const before = observeBefore(model, command) + const variablesBefore = projectVariables(model) const facts: LifecycleStepFacts = { releaseVerdicts: [], replayFailedOwnerDecided: false, } - const effect = row.effect(model, command, facts) - if (row.to !== `same` && lifecyclePhase(model) !== row.to) + const effect = row.effect(model, command, target, facts) + const phaseAfter = lifecyclePhase(model) + const expectedPhase = row.to === `same` ? phaseBefore : row.to + if (phaseAfter !== expectedPhase) throw new Error( - `lifecycle row ${row.id} ended in ${lifecyclePhase(model)}, not ${row.to}`, + `lifecycle row ${row.id} ended in ${phaseAfter}, not ${expectedPhase}`, + ) + const variablesAfter = projectVariables(model) + for (const variable of stateVariables) + if ( + variablesAfter[variable] !== variablesBefore[variable] && + !row.writes.includes(variable) ) + throw new Error( + `lifecycle row ${row.id} wrote ${variable}, which it does not declare`, + ) const step: LifecycleStep = { command, row, @@ -1194,9 +1247,8 @@ export function reduceLifecycle( facts, attempts: model.attempts.slice(before.attemptCount), } - for (const label of lifecycleReach.flatMap((rule) => rule(step))) - model.reach.add(label) - return { ...effect, transition: row.id } + for (const label of lifecycleReachLabels(step)) model.reach.add(label) + return effect } export const greenLifecycleHistoryArbitrary = fc.array( @@ -1204,10 +1256,7 @@ export const greenLifecycleHistoryArbitrary = fc.array( { minLength: 1, maxLength: 20 }, ) -export const syncLifecycleHistoryArbitrary = fc.array( - lifecycleCommandArbitrary, - { minLength: 1, maxLength: 20 }, -) +export const syncLifecycleHistoryArbitrary = greenLifecycleHistoryArbitrary /** * The demand-change grammar: three demands, with `change` and `replace`. @@ -1698,6 +1747,19 @@ export const parkedReloadDemandCases: ReadonlyArray = ( ] as const ).map((newRun) => ({ newRun })) +// Attempts that start work for each case. The reload's replay starts one +// unless a snapshot supersedes it first; a later snapshot starts another. +const parkedReloadAttempts: Record = { + // The reload's replay starts one attempt and nothing supersedes it. + ready: 1, + // A snapshot inside `sync()` supersedes the replay before it starts any + // request, so readiness and the snapshot name one attempt (parkedReloadDemandCases). + 'ready-then-snapshot': 1, + 'snapshot-then-ready': 1, + // A later snapshot is a newer attempt: it replaces the settled acquisition. + 'ready-then-later-snapshot': 2, +} + export function expectedParkedReloadDemand({ newRun, }: ParkedReloadDemandCase): { @@ -1707,9 +1769,7 @@ export function expectedParkedReloadDemand({ status: `ready` collectionStatus: `ready` } { - // Attempts that start work: the reload's replay, which a snapshot inside - // `sync()` supersedes before it begins, and a later snapshot's replay. - const attempts = newRun === `ready-then-later-snapshot` ? 2 : 1 + const attempts = parkedReloadAttempts[newRun] return { loads: attempts, // Each later attempt replaces the acquisition of the one before it. @@ -1843,15 +1903,16 @@ export type StartHandoffHistory = { cause: `error` | `undefined` } +const STATUS_OF_OUTCOME = { + ready: `ready`, + fail: `error`, + throw: `crashed`, +} as const + export function expectedStartHandoff(history: StartHandoffHistory) { return { throws: history.outcome === `throw` && history.timing === `during-release`, - status: - history.outcome === `ready` - ? `ready` - : history.outcome === `fail` - ? `error` - : `crashed`, + status: STATUS_OF_OUTCOME[history.outcome], starts: 1, } as const } diff --git a/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts b/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts index d127b6c3eb..830ab0d9d2 100644 --- a/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts +++ b/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts @@ -15,6 +15,8 @@ import { expectedParkedReloadDemand, greenLifecycleHistories, greenLifecycleHistoryArbitrary, + lifecycleCommandArbitrary, + lifecycleRowLabels, mixedAbortedRestartHistory, parkedReloadDemandCases, pendingSupersessionHistory, @@ -1708,7 +1710,9 @@ describe(`CollectionSubscription async lifecycle history oracle`, () => { cancellation: `manual` | `reject` = `manual`, ) => { demandChangeReach.beginHistory() + lifecycleRowReach.beginHistory() const reached = await runHistory(history, { cancellation }) + markLifecycleRows(reached) for (const [label, state] of Object.entries(demandChangeReachStates)) if (reached.has(label)) demandChangeReach.reach(state) } @@ -1828,9 +1832,21 @@ describe(`CollectionSubscription async lifecycle history oracle`, () => { `subscription-lifecycle.replacement-abort`, Object.values(replacementReachStates), ) + // Every row of the lifecycle transition table must fire somewhere in the + // green and demand-change campaigns, so the table's rows are declared here. + const lifecycleRowReach = createOracleReach( + `subscription-lifecycle.rows`, + lifecycleRowLabels, + ) + const markLifecycleRows = (reached: ReadonlySet) => { + for (const row of lifecycleRowLabels) + if (reached.has(row)) lifecycleRowReach.reach(row) + } let greenHistoriesRan = false afterAll(() => { if (greenHistoriesRan) replacementReach.assertReached() + if (greenHistoriesRan || demandChangeHistoriesRan) + lifecycleRowReach.assertReached() }) const runGreenHistory = async ( history: ReadonlyArray, @@ -1838,13 +1854,55 @@ describe(`CollectionSubscription async lifecycle history oracle`, () => { ) => { greenHistoriesRan = true replacementReach.beginHistory() + lifecycleRowReach.beginHistory() const reached = await runHistory(history, { cancellation }) if (reached.has(replacementPendingReachLabel)) replacementReach.reach( replacementReachStates[replacementPendingReachLabel], ) + markLifecycleRows(reached) } + // Constructed prefixes reach the two pairs that no generated history + // produced: a replacement followed by a change that names no owned demand, + // and a replacement after a restart. Each prefix is the shortest legal path + // the lifecycle table search found, followed by a random tail. + const constructedPrefixes: ReadonlyArray> = [ + [ + { type: `request`, demand: `a` }, + { type: `request`, demand: `b` }, + { type: `replace`, demand: `a`, replaced: `b` }, + { type: `change`, release: [`c`] }, + ], + [ + { type: `request`, demand: `a` }, + { type: `request`, demand: `b` }, + { type: `cleanup` }, + { type: `restart` }, + { type: `replace`, demand: `a`, replaced: `b` }, + ], + ] + const constructedPrefixArbitrary = fc + .tuple( + fc.constantFrom(...constructedPrefixes), + fc.array(lifecycleCommandArbitrary, { maxLength: 8 }), + ) + .map(([prefix, tail]) => [...prefix, ...tail]) + const constructedPrefixSeed = oracleFixedSeed(1_657_011, { + numRuns: runs, + }) + fixedCampaign.prop( + [constructedPrefixArbitrary, cancellationArbitrary], + constructedPrefixSeed, + )( + `matches the pure lifecycle model after a constructed prefix`, + async (history, cancellation) => { + oracleRoute(oracleRouteOf(constructedPrefixSeed)) + await runGreenHistory(history, cancellation) + }, + 120_000, + ) + const greenLifecycleHistoryFixedSeed = oracleFixedSeed(1_657_003, { numRuns: runs, })